ring_1.miz



    begin

    theorem :: RING_1:1

    

     Th1: for L be add-associative right_zeroed right_complementable non empty addLoopStr, a,b be Element of L holds ((a - b) + b) = a

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr, a,b be Element of L;

      

      thus ((a - b) + b) = (a + (( - b) + b)) by RLVECT_1:def 3

      .= (a + ( 0. L)) by RLVECT_1: 5

      .= a by RLVECT_1:def 4;

    end;

    theorem :: RING_1:2

    

     Th2: for L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, b,c be Element of L holds c = (b - (b - c))

    proof

      let L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, b,c be Element of L;

      set a = (b - c);

      ((a + c) - a) = ((c - a) + a) by RLVECT_1: 28

      .= c by Th1;

      hence thesis by Th1;

    end;

    theorem :: RING_1:3

    

     Th3: for L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, a,b,c be Element of L holds ((a - b) - (c - b)) = (a - c)

    proof

      let L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, a,b,c be Element of L;

      

      thus ((a - b) - (c - b)) = (((a - b) - c) + b) by RLVECT_1: 29

      .= (((a - b) + b) - c) by RLVECT_1: 28

      .= ((a - (b - b)) - c) by RLVECT_1: 29

      .= ((a - ( 0. L)) - c) by RLVECT_1: 15

      .= (a - c) by RLVECT_1: 13;

    end;

    begin

    definition

      let K be non empty multMagma, S be Subset of K;

      :: RING_1:def1

      attr S is quasi-prime means for a,b be Element of K st (a * b) in S holds a in S or b in S;

    end

    definition

      let K be non empty multLoopStr, S be Subset of K;

      :: RING_1:def2

      attr S is prime means S is proper quasi-prime;

    end

    definition

      let R be non empty doubleLoopStr;

      let I be Subset of R;

      :: RING_1:def3

      attr I is quasi-maximal means for J be Ideal of R st I c= J holds J = I or J is non proper;

    end

    definition

      let R be non empty doubleLoopStr;

      let I be Subset of R;

      :: RING_1:def4

      attr I is maximal means I is proper quasi-maximal;

    end

    registration

      let K be non empty multLoopStr;

      cluster prime -> proper quasi-prime for Subset of K;

      coherence ;

      cluster proper quasi-prime -> prime for Subset of K;

      coherence ;

    end

    registration

      let R be non empty doubleLoopStr;

      cluster maximal -> proper quasi-maximal for Subset of R;

      coherence ;

      cluster proper quasi-maximal -> maximal for Subset of R;

      coherence ;

    end

    registration

      let R be non empty addLoopStr;

      cluster ( [#] R) -> add-closed;

      coherence ;

    end

    registration

      let R be non empty multMagma;

      cluster ( [#] R) -> left-ideal right-ideal;

      coherence ;

    end

    theorem :: RING_1:4

    for R be domRing holds {( 0. R)} is prime

    proof

      let R be domRing;

       not ( 1_ R) in {( 0. R)} by TARSKI:def 1;

      hence {( 0. R)} is proper by IDEAL_1: 19;

      let a,b be Element of R;

      assume (a * b) in {( 0. R)};

      then (a * b) = ( 0. R) by TARSKI:def 1;

      then a = ( 0. R) or b = ( 0. R) by VECTSP_2:def 1;

      hence thesis by TARSKI:def 1;

    end;

    begin

    reserve R for Ring,

I for Ideal of R,

a,b for Element of R;

    

     Lm1: for R be Ring, I be Ideal of R holds ex E be Equivalence_Relation of the carrier of R st for x,y be object holds [x, y] in E iff x in the carrier of R & y in the carrier of R & ex P,Q be Element of R st P = x & Q = y & (P - Q) in I

    proof

      let R be Ring, I be Ideal of R;

      defpred P[ object, object] means ex P,Q be Element of R st P = $1 & Q = $2 & (P - Q) in I;

      

       A1: for x,y be object st P[x, y] holds P[y, x]

      proof

        let x,y be object;

        given P,Q be Element of R such that

         A2: P = x & Q = y & (P - Q) in I;

        take Q, P;

        ( - (P - Q)) = (Q - P) by RLVECT_1: 33;

        hence thesis by A2, IDEAL_1: 13;

      end;

      

       A3: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z]

      proof

        let x,y,z be object;

        assume P[x, y];

        then

        consider P,Q be Element of R such that

         A4: P = x & Q = y & (P - Q) in I;

        assume P[y, z];

        then

        consider W,S be Element of R such that

         A5: W = y & S = z & (W - S) in I;

        take P, S;

        ((P - Q) + (Q - S)) = (((P - Q) + Q) - S) by RLVECT_1: 28

        .= (P - S) by Th1;

        hence thesis by A4, A5, IDEAL_1:def 1;

      end;

      

       A6: for x be object st x in the carrier of R holds P[x, x]

      proof

        let x be object;

        assume x in the carrier of R;

        then

        reconsider x as Element of R;

        (x - x) = ( 0. R) by RLVECT_1: 15;

        hence thesis by IDEAL_1: 2;

      end;

      thus ex EqR be Equivalence_Relation of the carrier of R st for x,y be object holds [x, y] in EqR iff x in the carrier of R & y in the carrier of R & P[x, y] from EQREL_1:sch 1( A6, A1, A3);

    end;

    definition

      let R be Ring, I be Ideal of R;

      :: RING_1:def5

      func EqRel (R,I) -> Relation of R means

      : Def5: for a,b be Element of R holds [a, b] in it iff (a - b) in I;

      existence

      proof

        consider E be Equivalence_Relation of the carrier of R such that

         A1: for x,y be object holds [x, y] in E iff x in the carrier of R & y in the carrier of R & ex P,Q be Element of R st P = x & Q = y & (P - Q) in I by Lm1;

        take E;

        let a,b be Element of R;

        thus [a, b] in E implies (a - b) in I

        proof

          assume [a, b] in E;

          then ex P,Q be Element of R st P = a & Q = b & (P - Q) in I by A1;

          hence thesis;

        end;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let A,B be Relation of R such that

         A2: for a,b be Element of R holds [a, b] in A iff (a - b) in I and

         A3: for a,b be Element of R holds [a, b] in B iff (a - b) in I;

        let x,y be object;

        thus [x, y] in A implies [x, y] in B

        proof

          assume

           A4: [x, y] in A;

          then

          reconsider x, y as Element of R by ZFMISC_1: 87;

          (x - y) in I by A2, A4;

          hence thesis by A3;

        end;

        assume

         A5: [x, y] in B;

        then

        reconsider x, y as Element of R by ZFMISC_1: 87;

        (x - y) in I by A3, A5;

        hence thesis by A2;

      end;

    end

    registration

      let R be Ring, I be Ideal of R;

      cluster ( EqRel (R,I)) -> non empty total symmetric transitive;

      coherence

      proof

        set A = ( EqRel (R,I));

        consider B be Equivalence_Relation of the carrier of R such that

         A1: for x,y be object holds [x, y] in B iff x in the carrier of R & y in the carrier of R & ex P,Q be Element of R st P = x & Q = y & (P - Q) in I by Lm1;

        A = B

        proof

          let x,y be object;

          thus [x, y] in A implies [x, y] in B

          proof

            assume

             A2: [x, y] in A;

            then

            reconsider x, y as Element of R by ZFMISC_1: 87;

            (x - y) in I by A2, Def5;

            hence thesis by A1;

          end;

          assume [x, y] in B;

          then ex P,Q be Element of R st P = x & Q = y & (P - Q) in I by A1;

          hence thesis by Def5;

        end;

        hence thesis by EQREL_1: 9, RELAT_1: 40;

      end;

    end

    theorem :: RING_1:5

    

     Th5: a in ( Class (( EqRel (R,I)),b)) iff (a - b) in I

    proof

      set E = ( EqRel (R,I));

      hereby

        assume a in ( Class (E,b));

        then [a, b] in E by EQREL_1: 19;

        hence (a - b) in I by Def5;

      end;

      assume (a - b) in I;

      then [a, b] in E by Def5;

      hence thesis by EQREL_1: 19;

    end;

    theorem :: RING_1:6

    

     Th6: ( Class (( EqRel (R,I)),a)) = ( Class (( EqRel (R,I)),b)) iff (a - b) in I

    proof

      set E = ( EqRel (R,I));

      thus ( Class (E,a)) = ( Class (E,b)) implies (a - b) in I

      proof

        assume ( Class (E,a)) = ( Class (E,b));

        then a in ( Class (E,b)) by EQREL_1: 23;

        hence thesis by Th5;

      end;

      assume (a - b) in I;

      then a in ( Class (E,b)) by Th5;

      hence thesis by EQREL_1: 23;

    end;

    theorem :: RING_1:7

    

     Th7: ( Class (( EqRel (R,( [#] R))),a)) = the carrier of R

    proof

      set E = ( EqRel (R,( [#] R)));

      thus ( Class (E,a)) c= the carrier of R;

      let x be object;

      assume x in the carrier of R;

      then

      reconsider x as Element of R;

      (x - a) in ( [#] R);

      then [x, a] in E by Def5;

      hence thesis by EQREL_1: 19;

    end;

    theorem :: RING_1:8

    ( Class ( EqRel (R,( [#] R)))) = {the carrier of R}

    proof

      set E = ( EqRel (R,( [#] R)));

      thus ( Class E) c= {the carrier of R}

      proof

        let A be object;

        assume A in ( Class E);

        then

        consider x be object such that

         A1: x in the carrier of R and

         A2: A = ( Class (E,x)) by EQREL_1:def 3;

        reconsider x as Element of R by A1;

        ( Class (E,x)) = the carrier of R

        proof

          thus ( Class (E,x)) c= the carrier of R;

          let a be object;

          assume a in the carrier of R;

          then

          reconsider a as Element of R;

          (a - x) in ( [#] R);

          then [a, x] in E by Def5;

          hence thesis by EQREL_1: 19;

        end;

        hence thesis by A2, TARSKI:def 1;

      end;

      let A be object;

      assume A in {the carrier of R};

      

      then A = the carrier of R by TARSKI:def 1

      .= ( Class (E,( 0. R))) by Th7;

      hence thesis by EQREL_1:def 3;

    end;

    theorem :: RING_1:9

    

     Th9: ( Class (( EqRel (R, {( 0. R)})),a)) = {a}

    proof

      set E = ( EqRel (R, {( 0. R)}));

      thus ( Class (E,a)) c= {a}

      proof

        let A be object;

        assume

         A1: A in ( Class (E,a));

        then

        reconsider A as Element of R;

         [A, a] in E by A1, EQREL_1: 19;

        then (A - a) in {( 0. R)} by Def5;

        then (A - a) = ( 0. R) by TARSKI:def 1;

        then A = a by RLVECT_1: 21;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {a};

      then

       A2: x = a by TARSKI:def 1;

      (a - a) = ( 0. R) & ( 0. R) in {( 0. R)} by RLVECT_1: 15, TARSKI:def 1;

      then [x, a] in E by A2, Def5;

      hence thesis by EQREL_1: 19;

    end;

    theorem :: RING_1:10

    ( Class ( EqRel (R, {( 0. R)}))) = ( rng ( singleton the carrier of R))

    proof

      set E = ( EqRel (R, {( 0. R)}));

      set f = ( singleton the carrier of R);

      

       A1: ( dom f) = the carrier of R by FUNCT_2:def 1;

      thus ( Class E) c= ( rng f)

      proof

        let A be object;

        assume A in ( Class E);

        then

        consider x be object such that

         A2: x in the carrier of R and

         A3: A = ( Class (E,x)) by EQREL_1:def 3;

        reconsider x as Element of R by A2;

        

         A4: ( Class (E,x)) = {x}

        proof

          thus ( Class (E,x)) c= {x}

          proof

            let a be object;

            assume

             A5: a in ( Class (E,x));

            then

            reconsider a as Element of R;

             [a, x] in E by A5, EQREL_1: 19;

            then (a - x) in {( 0. R)} by Def5;

            then (a - x) = ( 0. R) by TARSKI:def 1;

            then a = x by RLVECT_1: 21;

            hence thesis by TARSKI:def 1;

          end;

          let a be object;

          (x - x) = ( 0. R) by RLVECT_1: 15;

          then

           A6: (x - x) in {( 0. R)} by TARSKI:def 1;

          assume a in {x};

          then a = x by TARSKI:def 1;

          then [a, x] in E by A6, Def5;

          hence thesis by EQREL_1: 19;

        end;

        (f . x) = {x} by SETWISEO:def 6;

        hence thesis by A1, A3, A4, FUNCT_1:def 3;

      end;

      let A be object;

      assume A in ( rng f);

      then

      consider w be object such that

       A7: w in ( dom f) and

       A8: (f . w) = A by FUNCT_1:def 3;

      (f . w) = {w} by A7, SETWISEO:def 6

      .= ( Class (E,w)) by A7, Th9;

      hence thesis by A7, A8, EQREL_1:def 3;

    end;

    begin

    definition

      let R be Ring, I be Ideal of R;

      ::$Notion-Name

      :: RING_1:def6

      func QuotientRing (R,I) -> strict doubleLoopStr means

      : Def6: the carrier of it = ( Class ( EqRel (R,I))) & ( 1. it ) = ( Class (( EqRel (R,I)),( 1. R))) & ( 0. it ) = ( Class (( EqRel (R,I)),( 0. R))) & (for x,y be Element of it holds ex a,b be Element of R st x = ( Class (( EqRel (R,I)),a)) & y = ( Class (( EqRel (R,I)),b)) & (the addF of it . (x,y)) = ( Class (( EqRel (R,I)),(a + b)))) & for x,y be Element of it holds ex a,b be Element of R st x = ( Class (( EqRel (R,I)),a)) & y = ( Class (( EqRel (R,I)),b)) & (the multF of it . (x,y)) = ( Class (( EqRel (R,I)),(a * b)));

      existence

      proof

        set E = ( EqRel (R,I));

        set A = ( Class E);

        defpred P[ set, set, set] means ex P,Q be Element of R st $1 = ( Class (E,P)) & $2 = ( Class (E,Q)) & $3 = ( Class (E,(P + Q)));

        defpred R[ set, set, set] means ex P,Q be Element of R st $1 = ( Class (E,P)) & $2 = ( Class (E,Q)) & $3 = ( Class (E,(P * Q)));

        reconsider u = ( Class (( EqRel (R,I)),( 1_ R))) as Element of A by EQREL_1:def 3;

        reconsider z = ( Class (( EqRel (R,I)),( 0. R))) as Element of A by EQREL_1:def 3;

        

         A1: for x,y be Element of A holds ex z be Element of A st P[x, y, z]

        proof

          let x,y be Element of A;

          consider P be object such that

           A2: P in the carrier of R and

           A3: x = ( Class (E,P)) by EQREL_1:def 3;

          consider Q be object such that

           A4: Q in the carrier of R and

           A5: y = ( Class (E,Q)) by EQREL_1:def 3;

          reconsider P, Q as Element of R by A2, A4;

          ( Class (E,(P + Q))) is Element of A by EQREL_1:def 3;

          hence thesis by A3, A5;

        end;

        consider g be BinOp of A such that

         A6: for a,b be Element of A holds P[a, b, (g . (a,b))] from BINOP_1:sch 3( A1);

        

         A7: for x,y be Element of A holds ex z be Element of A st R[x, y, z]

        proof

          let x,y be Element of A;

          consider P be object such that

           A8: P in the carrier of R and

           A9: x = ( Class (E,P)) by EQREL_1:def 3;

          consider Q be object such that

           A10: Q in the carrier of R and

           A11: y = ( Class (E,Q)) by EQREL_1:def 3;

          reconsider P, Q as Element of R by A8, A10;

          ( Class (E,(P * Q))) is Element of A by EQREL_1:def 3;

          hence thesis by A9, A11;

        end;

        consider h be BinOp of A such that

         A12: for a,b be Element of A holds R[a, b, (h . (a,b))] from BINOP_1:sch 3( A7);

        take doubleLoopStr (# A, g, h, u, z #);

        thus thesis by A6, A12;

      end;

      uniqueness

      proof

        set E = ( EqRel (R,I));

        let X,Y be strict doubleLoopStr such that

         A13: the carrier of X = ( Class E) and

         A14: ( 1. X) = ( Class (E,( 1. R))) & ( 0. X) = ( Class (E,( 0. R))) and

         A15: for x,y be Element of X holds ex a,b be Element of R st x = ( Class (E,a)) & y = ( Class (E,b)) & (the addF of X . (x,y)) = ( Class (E,(a + b))) and

         A16: for x,y be Element of X holds ex a,b be Element of R st x = ( Class (E,a)) & y = ( Class (E,b)) & (the multF of X . (x,y)) = ( Class (E,(a * b))) and

         A17: the carrier of Y = ( Class E) and

         A18: ( 1. Y) = ( Class (E,( 1. R))) & ( 0. Y) = ( Class (E,( 0. R))) and

         A19: for x,y be Element of Y holds ex a,b be Element of R st x = ( Class (E,a)) & y = ( Class (E,b)) & (the addF of Y . (x,y)) = ( Class (E,(a + b))) and

         A20: for x,y be Element of Y holds ex a,b be Element of R st x = ( Class (E,a)) & y = ( Class (E,b)) & (the multF of Y . (x,y)) = ( Class (E,(a * b)));

        

         A21: for x,y be Element of X holds (the multF of X . (x,y)) = (the multF of Y . (x,y))

        proof

          let x,y be Element of X;

          consider a,b be Element of R such that

           A22: x = ( Class (E,a)) and

           A23: y = ( Class (E,b)) and

           A24: (the multF of X . (x,y)) = ( Class (E,(a * b))) by A16;

          consider a1,b1 be Element of R such that

           A25: x = ( Class (E,a1)) and

           A26: y = ( Class (E,b1)) and

           A27: (the multF of Y . (x,y)) = ( Class (E,(a1 * b1))) by A13, A17, A20;

          (b - b1) in I by A23, A26, Th6;

          then

           A28: (a1 * (b - b1)) in I by IDEAL_1:def 2;

          

           A29: (((a - a1) * b) + (a1 * (b - b1))) = (((a * b) - (a1 * b)) + (a1 * (b - b1))) by VECTSP_1: 13

          .= (((a * b) - (a1 * b)) + ((a1 * b) - (a1 * b1))) by VECTSP_1: 11

          .= ((((a * b) - (a1 * b)) + (a1 * b)) - (a1 * b1)) by RLVECT_1: 28

          .= ((a * b) - (a1 * b1)) by Th1;

          (a - a1) in I by A22, A25, Th6;

          then ((a - a1) * b) in I by IDEAL_1:def 3;

          then (((a - a1) * b) + (a1 * (b - b1))) in I by A28, IDEAL_1:def 1;

          hence thesis by A24, A27, A29, Th6;

        end;

        for x,y be Element of X holds (the addF of X . (x,y)) = (the addF of Y . (x,y))

        proof

          let x,y be Element of X;

          consider a,b be Element of R such that

           A30: x = ( Class (E,a)) & y = ( Class (E,b)) and

           A31: (the addF of X . (x,y)) = ( Class (E,(a + b))) by A15;

          consider a1,b1 be Element of R such that

           A32: x = ( Class (E,a1)) & y = ( Class (E,b1)) and

           A33: (the addF of Y . (x,y)) = ( Class (E,(a1 + b1))) by A13, A17, A19;

          (a - a1) in I & (b - b1) in I by A30, A32, Th6;

          then

           A34: ((a - a1) + (b - b1)) in I by IDEAL_1:def 1;

          ((a + b) - (a1 + b1)) = (((a + b) - a1) - b1) by RLVECT_1: 27

          .= (((a - a1) + b) - b1) by RLVECT_1: 28

          .= ((a - a1) + (b - b1)) by RLVECT_1: 28;

          hence thesis by A31, A33, A34, Th6;

        end;

        then the addF of X = the addF of Y by A13, A17, BINOP_1: 2;

        hence thesis by A13, A14, A17, A18, A21, BINOP_1: 2;

      end;

    end

    notation

      let R be Ring, I be Ideal of R;

      synonym R / I for QuotientRing (R,I);

    end

    registration

      let R be Ring, I be Ideal of R;

      cluster (R / I) -> non empty;

      coherence

      proof

        the carrier of (R / I) = ( Class ( EqRel (R,I))) by Def6;

        hence the carrier of (R / I) is non empty;

      end;

    end

    reserve x,y for Element of (R / I);

    theorem :: RING_1:11

    

     Th11: ex a be Element of R st x = ( Class (( EqRel (R,I)),a))

    proof

      the carrier of (R / I) = ( Class ( EqRel (R,I))) by Def6;

      then x in ( Class ( EqRel (R,I)));

      then ex a be object st a in the carrier of R & x = ( Class (( EqRel (R,I)),a)) by EQREL_1:def 3;

      hence thesis;

    end;

    theorem :: RING_1:12

    

     Th12: ( Class (( EqRel (R,I)),a)) is Element of (R / I)

    proof

      the carrier of (R / I) = ( Class ( EqRel (R,I))) by Def6;

      hence thesis by EQREL_1:def 3;

    end;

    theorem :: RING_1:13

    

     Th13: x = ( Class (( EqRel (R,I)),a)) & y = ( Class (( EqRel (R,I)),b)) implies (x + y) = ( Class (( EqRel (R,I)),(a + b)))

    proof

      consider a1,b1 be Element of R such that

       A1: x = ( Class (( EqRel (R,I)),a1)) & y = ( Class (( EqRel (R,I)),b1)) and

       A2: (the addF of (R / I) . (x,y)) = ( Class (( EqRel (R,I)),(a1 + b1))) by Def6;

      

       A3: ((a1 - a) + (b1 - b)) = (((a1 - a) + b1) - b) by RLVECT_1: 28

      .= (((a1 + b1) - a) - b) by RLVECT_1: 28

      .= ((a1 + b1) - (a + b)) by RLVECT_1: 27;

      assume x = ( Class (( EqRel (R,I)),a)) & y = ( Class (( EqRel (R,I)),b));

      then (a1 - a) in I & (b1 - b) in I by A1, Th6;

      then ((a1 + b1) - (a + b)) in I by A3, IDEAL_1:def 1;

      hence thesis by A2, Th6;

    end;

    theorem :: RING_1:14

    

     Th14: x = ( Class (( EqRel (R,I)),a)) & y = ( Class (( EqRel (R,I)),b)) implies (x * y) = ( Class (( EqRel (R,I)),(a * b)))

    proof

      assume that

       A1: x = ( Class (( EqRel (R,I)),a)) and

       A2: y = ( Class (( EqRel (R,I)),b));

      consider a1,b1 be Element of R such that

       A3: x = ( Class (( EqRel (R,I)),a1)) and

       A4: y = ( Class (( EqRel (R,I)),b1)) and

       A5: (the multF of (R / I) . (x,y)) = ( Class (( EqRel (R,I)),(a1 * b1))) by Def6;

      (b1 - b) in I by A2, A4, Th6;

      then

       A6: (a1 * (b1 - b)) in I by IDEAL_1:def 2;

      ((a1 - a) * b) = ((a1 * b) - (a * b)) & (a1 * (b1 - b)) = ((a1 * b1) - (a1 * b)) by VECTSP_1: 11, VECTSP_1: 13;

      

      then

       A7: ((a1 * (b1 - b)) + ((a1 - a) * b)) = ((((a1 * b1) - (a1 * b)) + (a1 * b)) - (a * b)) by RLVECT_1: 28

      .= ((a1 * b1) - (a * b)) by Th1;

      (a1 - a) in I by A1, A3, Th6;

      then ((a1 - a) * b) in I by IDEAL_1:def 3;

      then (((a1 - a) * b) + (a1 * (b1 - b))) in I by A6, IDEAL_1:def 1;

      hence thesis by A5, A7, Th6;

    end;

     Lm2:

    now

      let R be Ring, I be Ideal of R;

      set E = ( EqRel (R,I));

      let e be Element of (R / I) such that

       A1: e = ( Class (E,( 1_ R)));

      let h be Element of (R / I);

      consider a be Element of R such that

       A2: e = ( Class (E,a)) by Th11;

      consider b be Element of R such that

       A3: h = ( Class (E,b)) by Th11;

      

       A4: (a - ( 1_ R)) in I by A1, A2, Th6;

      then

       A5: ((a - ( 1_ R)) * b) in I by IDEAL_1:def 3;

      

       A6: (b * (a - ( 1_ R))) = ((b * a) - (b * ( 1_ R))) by VECTSP_1: 11

      .= ((b * a) - b);

      

       A7: (b * (a - ( 1_ R))) in I by A4, IDEAL_1:def 2;

      

      thus (h * e) = ( Class (E,(b * a))) by A2, A3, Th14

      .= h by A3, A7, A6, Th6;

      

       A8: ((a - ( 1_ R)) * b) = ((a * b) - (( 1_ R) * b)) by VECTSP_1: 13

      .= ((a * b) - b);

      

      thus (e * h) = ( Class (E,(a * b))) by A2, A3, Th14

      .= h by A3, A5, A8, Th6;

    end;

    theorem :: RING_1:15

    ( Class (( EqRel (R,I)),( 1. R))) = ( 1. (R / I)) by Def6;

    registration

      let R be Ring, I be Ideal of R;

      cluster (R / I) -> Abelian add-associative right_zeroed right_complementable associative well-unital distributive;

      coherence

      proof

        set g = the addF of (R / I);

        set E = ( EqRel (R,I));

        hereby

          let x,y be Element of (R / I);

          consider a be Element of R such that

           A1: x = ( Class (E,a)) by Th11;

          consider b be Element of R such that

           A2: y = ( Class (E,b)) by Th11;

          

          thus (x + y) = ( Class (E,(a + b))) by A1, A2, Th13

          .= (y + x) by A1, A2, Th13;

        end;

        hereby

          let x,y,z be Element of (R / I);

          consider a be Element of R such that

           A3: x = ( Class (E,a)) by Th11;

          consider b be Element of R such that

           A4: y = ( Class (E,b)) by Th11;

          consider bc be Element of R such that

           A5: (y + z) = ( Class (E,bc)) by Th11;

          consider c be Element of R such that

           A6: z = ( Class (E,c)) by Th11;

          (y + z) = ( Class (E,(b + c))) by A4, A6, Th13;

          then

           A7: (bc - (b + c)) in I by A5, Th6;

          consider ab be Element of R such that

           A8: (x + y) = ( Class (E,ab)) by Th11;

          (x + y) = ( Class (E,(a + b))) by A3, A4, Th13;

          then (ab - (a + b)) in I by A8, Th6;

          then

           A9: ((ab - (a + b)) - (bc - (b + c))) in I by A7, IDEAL_1: 15;

          

           A10: ((ab - (a + b)) - (bc - (b + c))) = (((ab - (a + b)) - bc) + (b + c)) by RLVECT_1: 29

          .= (((ab - (a + b)) + (b + c)) - bc) by RLVECT_1: 28

          .= ((((ab - a) - b) + (b + c)) - bc) by RLVECT_1: 27

          .= (((((ab - a) - b) + b) + c) - bc) by RLVECT_1:def 3

          .= (((ab - a) + c) - bc) by Th1

          .= (((ab + c) - a) - bc) by RLVECT_1: 28

          .= ((ab + c) - (a + bc)) by RLVECT_1: 27;

          

          thus ((x + y) + z) = ( Class (E,(ab + c))) by A6, A8, Th13

          .= ( Class (E,(a + bc))) by A9, A10, Th6

          .= (x + (y + z)) by A3, A5, Th13;

        end;

        hereby

          let v be Element of (R / I);

          consider a,b be Element of R such that

           A11: v = ( Class (E,a)) and

           A12: ( 0. (R / I)) = ( Class (E,b)) and

           A13: (g . (v,( 0. (R / I)))) = ( Class (E,(a + b))) by Def6;

          

           A14: (b - ( 0. R)) = b by RLVECT_1: 13;

          

           A15: ((a + b) - a) = ((a - a) + b) by RLVECT_1: 28

          .= (( 0. R) + b) by RLVECT_1: 15

          .= b by RLVECT_1:def 4;

          ( 0. (R / I)) = ( Class (E,( 0. R))) by Def6;

          then (b - ( 0. R)) in I by A12, Th6;

          hence (v + ( 0. (R / I))) = v by A11, A13, A14, A15, Th6;

        end;

        thus (R / I) is right_complementable

        proof

          let v be Element of (R / I);

          consider a,b be Element of R such that

           A16: v = ( Class (E,a)) and ( 0. (R / I)) = ( Class (E,b)) and (g . (v,( 0. (R / I)))) = ( Class (E,(a + b))) by Def6;

          reconsider w = ( Class (E,( - a))) as Element of (R / I) by Th12;

          take w;

          

           A17: ( 0. (R / I)) = ( Class (E,( 0. R))) by Def6;

          

          thus (v + w) = ( Class (E,(a + ( - a)))) by A16, Th13

          .= ( 0. (R / I)) by A17, RLVECT_1:def 10;

        end;

        hereby

          let x,y,z be Element of (R / I);

          consider a be Element of R such that

           A18: x = ( Class (E,a)) by Th11;

          consider ab be Element of R such that

           A19: (x * y) = ( Class (E,ab)) by Th11;

          consider c be Element of R such that

           A20: z = ( Class (E,c)) by Th11;

          consider b be Element of R such that

           A21: y = ( Class (E,b)) by Th11;

          (x * y) = ( Class (E,(a * b))) by A18, A21, Th14;

          then (ab - (a * b)) in I by A19, Th6;

          then

           A22: ((ab - (a * b)) * c) in I by IDEAL_1:def 3;

          consider bc be Element of R such that

           A23: (y * z) = ( Class (E,bc)) by Th11;

          (y * z) = ( Class (E,(b * c))) by A21, A20, Th14;

          then (bc - (b * c)) in I by A23, Th6;

          then

           A24: (a * (bc - (b * c))) in I by IDEAL_1:def 2;

          

           A25: ((ab - (a * b)) * c) = ((ab * c) - ((a * b) * c)) & (a * (bc - (b * c))) = ((a * bc) - (a * (b * c))) by VECTSP_1: 11, VECTSP_1: 13;

          (a * (b * c)) = ((a * b) * c) & (((ab * c) - ((a * b) * c)) - ((a * bc) - ((a * b) * c))) = ((ab * c) - (a * bc)) by Th3, GROUP_1:def 3;

          then

           A26: ((ab * c) - (a * bc)) in I by A22, A24, A25, IDEAL_1: 15;

          

          thus ((x * y) * z) = ( Class (E,(ab * c))) by A20, A19, Th14

          .= ( Class (E,(a * bc))) by A26, Th6

          .= (x * (y * z)) by A18, A23, Th14;

        end;

        ( 1. R) = ( 1_ R) & ( Class (E,( 1. R))) = ( 1. (R / I)) by Def6;

        hence for x be Element of (R / I) holds (x * ( 1. (R / I))) = x & (( 1. (R / I)) * x) = x by Lm2;

        let x,y,z be Element of (R / I);

        consider a be Element of R such that

         A27: x = ( Class (E,a)) by Th11;

        consider ab be Element of R such that

         A28: (x * y) = ( Class (E,ab)) by Th11;

        consider ca be Element of R such that

         A29: (z * x) = ( Class (E,ca)) by Th11;

        consider c be Element of R such that

         A30: z = ( Class (E,c)) by Th11;

        (z * x) = ( Class (E,(c * a))) by A27, A30, Th14;

        then

         A31: ((c * a) - ca) in I by A29, Th6;

        consider b be Element of R such that

         A32: y = ( Class (E,b)) by Th11;

        (x * y) = ( Class (E,(a * b))) by A27, A32, Th14;

        then

         A33: (ab - (a * b)) in I by A28, Th6;

        consider ac be Element of R such that

         A34: (x * z) = ( Class (E,ac)) by Th11;

        (x * z) = ( Class (E,(a * c))) by A27, A30, Th14;

        then

         A35: (ac - (a * c)) in I by A34, Th6;

        consider bc be Element of R such that

         A36: (y + z) = ( Class (E,bc)) by Th11;

        (y + z) = ( Class (E,(b + c))) by A32, A30, Th13;

        then

         A37: (bc - (b + c)) in I by A36, Th6;

        then

         A38: ((bc - (b + c)) * a) in I by IDEAL_1:def 3;

        (a * (bc - (b + c))) in I by A37, IDEAL_1:def 2;

        then ((a * (bc - (b + c))) - (ab - (a * b))) in I by A33, IDEAL_1: 15;

        then

         A39: (((a * (bc - (b + c))) - (ab - (a * b))) - (ac - (a * c))) in I by A35, IDEAL_1: 15;

        

         A40: (((a * (bc - (b + c))) - (ab - (a * b))) - (ac - (a * c))) = ((((a * bc) - (a * (b + c))) - (ab - (a * b))) - (ac - (a * c))) by VECTSP_1: 11

        .= ((((a * bc) - ((a * b) + (a * c))) - (ab - (a * b))) - (ac - (a * c))) by VECTSP_1:def 2

        .= (((((a * bc) - (a * b)) - (a * c)) - (ab - (a * b))) - (ac - (a * c))) by RLVECT_1: 27

        .= ((((((a * bc) - (a * b)) - (a * c)) - ab) + (a * b)) - (ac - (a * c))) by RLVECT_1: 29

        .= (((((((a * bc) - (a * b)) - (a * c)) - ab) + (a * b)) - ac) + (a * c)) by RLVECT_1: 29

        .= (((((((a * bc) - (a * b)) - (a * c)) + (a * b)) - ab) - ac) + (a * c)) by RLVECT_1: 28

        .= (((((((a * bc) - (a * b)) + (a * b)) - (a * c)) - ab) - ac) + (a * c)) by RLVECT_1: 28

        .= (((((a * bc) - (a * c)) - ab) - ac) + (a * c)) by Th1

        .= (((((a * bc) - (a * c)) - ab) + (a * c)) - ac) by RLVECT_1: 28

        .= (((((a * bc) - (a * c)) + (a * c)) - ab) - ac) by RLVECT_1: 28

        .= (((a * bc) - ab) - ac) by Th1

        .= ((a * bc) - (ab + ac)) by RLVECT_1: 27;

        

        thus (x * (y + z)) = ( Class (E,(a * bc))) by A27, A36, Th14

        .= ( Class (E,(ab + ac))) by A39, A40, Th6

        .= ((x * y) + (x * z)) by A28, A34, Th13;

        consider ba be Element of R such that

         A41: (y * x) = ( Class (E,ba)) by Th11;

        (y * x) = ( Class (E,(b * a))) by A27, A32, Th14;

        then ((b * a) - ba) in I by A41, Th6;

        then (((bc - (b + c)) * a) + ((b * a) - ba)) in I by A38, IDEAL_1:def 1;

        then

         A42: ((((bc - (b + c)) * a) + ((b * a) - ba)) + ((c * a) - ca)) in I by A31, IDEAL_1:def 1;

        

         A43: ((((bc - (b + c)) * a) + ((b * a) - ba)) + ((c * a) - ca)) = ((((bc * a) - ((b + c) * a)) + ((b * a) - ba)) + ((c * a) - ca)) by VECTSP_1: 13

        .= ((((bc * a) - ((b * a) + (c * a))) + ((b * a) - ba)) + ((c * a) - ca)) by VECTSP_1:def 3

        .= (((((bc * a) - (b * a)) - (c * a)) + ((b * a) - ba)) + ((c * a) - ca)) by RLVECT_1: 27

        .= ((((((bc * a) - (b * a)) - (c * a)) + (b * a)) - ba) + ((c * a) - ca)) by RLVECT_1: 28

        .= (((((((bc * a) - (b * a)) - (c * a)) + (b * a)) - ba) + (c * a)) - ca) by RLVECT_1: 28

        .= (((((((bc * a) - (b * a)) + (b * a)) - (c * a)) - ba) + (c * a)) - ca) by RLVECT_1: 28

        .= (((((bc * a) - (c * a)) - ba) + (c * a)) - ca) by Th1

        .= (((((bc * a) - (c * a)) + (c * a)) - ba) - ca) by RLVECT_1: 28

        .= (((bc * a) - ba) - ca) by Th1

        .= ((bc * a) - (ba + ca)) by RLVECT_1: 27;

        

        thus ((y + z) * x) = ( Class (E,(bc * a))) by A27, A36, Th14

        .= ( Class (E,(ba + ca))) by A42, A43, Th6

        .= ((y * x) + (z * x)) by A41, A29, Th13;

      end;

    end

    registration

      let R be commutative Ring, I be Ideal of R;

      cluster (R / I) -> commutative;

      coherence

      proof

        set E = ( EqRel (R,I));

        let x,y be Element of (R / I);

        consider a be Element of R such that

         A1: x = ( Class (E,a)) by Th11;

        consider b be Element of R such that

         A2: y = ( Class (E,b)) by Th11;

        

        thus (x * y) = ( Class (E,(a * b))) by A1, A2, Th14

        .= (y * x) by A1, A2, Th14;

      end;

    end

    theorem :: RING_1:16

    

     Th16: I is proper iff (R / I) is non degenerated

    proof

      set E = ( EqRel (R,I));

      

       A1: (( 1. R) - ( 0. R)) = ( 1. R) by RLVECT_1: 13;

      

       A2: ( 0. (R / I)) = ( Class (E,( 0. R))) & ( 1. (R / I)) = ( Class (E,( 1. R))) by Def6;

      thus I is proper implies (R / I) is non degenerated by A2, Th6, A1, IDEAL_1: 19;

      assume

       A3: (R / I) is non degenerated;

      assume not I is proper;

      then ( 1. R) in I by IDEAL_1: 19;

      hence thesis by A2, A1, A3, Th6;

    end;

    theorem :: RING_1:17

    

     Th17: I is quasi-prime iff (R / I) is domRing-like

    proof

      set E = ( EqRel (R,I));

      

       A1: ( Class (E,( 0. R))) = ( 0. (R / I)) by Def6;

      thus I is quasi-prime implies (R / I) is domRing-like

      proof

        assume

         A2: I is quasi-prime;

        let x,y be Element of (R / I) such that

         A3: (x * y) = ( 0. (R / I));

        consider a be Element of R such that

         A4: x = ( Class (E,a)) by Th11;

        consider b be Element of R such that

         A5: y = ( Class (E,b)) by Th11;

        (x * y) = ( Class (E,(a * b))) by A4, A5, Th14;

        then ((a * b) - ( 0. R)) = (a * b) & ((a * b) - ( 0. R)) in I by A1, A3, Th6, RLVECT_1: 13;

        then

         A6: a in I or b in I by A2;

        (a - ( 0. R)) = a & (b - ( 0. R)) = b by RLVECT_1: 13;

        hence thesis by A1, A4, A5, A6, Th6;

      end;

      assume

       A7: (R / I) is domRing-like;

      let a,b be Element of R;

      reconsider x = ( Class (E,a)), y = ( Class (E,b)) as Element of (R / I) by Th12;

      

       A8: ((a * b) - ( 0. R)) = (a * b) by RLVECT_1: 13;

      

       A9: ( Class (E,(a * b))) = (x * y) by Th14;

      assume (a * b) in I;

      then ( Class (E,(a * b))) = ( Class (E,( 0. R))) by A8, Th6;

      then x = ( 0. (R / I)) or y = ( 0. (R / I)) by A1, A7, A9;

      then (a - ( 0. R)) in I or (b - ( 0. R)) in I by A1, Th6;

      hence thesis by RLVECT_1: 13;

    end;

    theorem :: RING_1:18

    for R be commutative Ring, I be Ideal of R holds I is prime iff (R / I) is domRing by Th16, Th17;

    theorem :: RING_1:19

    

     Th19: R is commutative & I is quasi-maximal implies (R / I) is almost_left_invertible

    proof

      set E = ( EqRel (R,I));

      assume that

       A1: R is commutative and

       A2: I is quasi-maximal;

      let x be Element of (R / I) such that

       A3: x <> ( 0. (R / I));

      consider a be Element of R such that

       A4: x = ( Class (E,a)) by Th11;

      set M = { ((a * r) + s) where r,s be Element of R : s in I };

      M c= the carrier of R

      proof

        let k be object;

        assume k in M;

        then ex r,s be Element of R st k = ((a * r) + s) & s in I;

        hence thesis;

      end;

      then

      reconsider M as Subset of R;

      

       A5: ( 0. R) in I by IDEAL_1: 2;

      

       A6: M is left-ideal

      proof

        let p,x be Element of R;

        assume x in M;

        then

        consider r,s be Element of R such that

         A7: x = ((a * r) + s) and

         A8: s in I;

        

         A9: (p * s) in I by A8, IDEAL_1:def 2;

        ((a * (r * p)) + (p * s)) = (((a * r) * p) + (p * s)) by GROUP_1:def 3

        .= (((a * r) * p) + (s * p)) by A1

        .= (x * p) by A7, VECTSP_1:def 3

        .= (p * x) by A1;

        hence thesis by A9;

      end;

      

       A10: I c= M

      proof

        let i be object;

        assume i in I;

        then

        reconsider i as Element of I;

        ((a * ( 0. R)) + i) = (( 0. R) + i)

        .= i by RLVECT_1:def 4;

        hence thesis;

      end;

      

       A11: M is right-ideal

      proof

        let p,x be Element of R;

        assume x in M;

        then

        consider r,s be Element of R such that

         A12: x = ((a * r) + s) and

         A13: s in I;

        

         A14: (p * s) in I by A13, IDEAL_1:def 2;

        ((a * (r * p)) + (p * s)) = (((a * r) * p) + (p * s)) by GROUP_1:def 3

        .= (((a * r) * p) + (s * p)) by A1

        .= (x * p) by A12, VECTSP_1:def 3;

        hence thesis by A14;

      end;

      

       A15: M is add-closed

      proof

        let c,d be Element of R;

        assume c in M;

        then

        consider rc,sc be Element of R such that

         A16: c = ((a * rc) + sc) and

         A17: sc in I;

        assume d in M;

        then

        consider rd,sd be Element of R such that

         A18: d = ((a * rd) + sd) and

         A19: sd in I;

        

         A20: ((a * (rc + rd)) + (sc + sd)) = (((a * rc) + (a * rd)) + (sc + sd)) by VECTSP_1:def 2

        .= ((((a * rc) + (a * rd)) + sc) + sd) by RLVECT_1:def 3

        .= ((((a * rc) + sc) + (a * rd)) + sd) by RLVECT_1:def 3

        .= (c + d) by A16, A18, RLVECT_1:def 3;

        (sc + sd) in I by A17, A19, IDEAL_1:def 1;

        hence (c + d) in M by A20;

      end;

       A21:

      now

        

         A22: (a - ( 0. R)) = a by RLVECT_1: 13;

        assume a in I;

        

        then ( Class (E,a)) = ( Class (E,( 0. R))) by A22, Th6

        .= ( 0. (R / I)) by Def6;

        hence contradiction by A3, A4;

      end;

      ((a * ( 1. R)) + ( 0. R)) = (a + ( 0. R))

      .= a by RLVECT_1:def 4;

      then a in M by A5;

      then M is non proper by A2, A15, A6, A11, A21, A10;

      then M = the carrier of R by SUBSET_1:def 6;

      then ( 1. R) in M;

      then

      consider b,m be Element of R such that

       A23: ( 1. R) = ((a * b) + m) and

       A24: m in I;

      

       A25: m = (( 1. R) - (a * b)) by A23, VECTSP_2: 2;

      reconsider y = ( Class (E,b)) as Element of (R / I) by Th12;

      take y;

      

       A26: ( Class (E,( 1. R))) = ( 1. (R / I)) by Def6;

      

      thus (y * x) = ( Class (E,(b * a))) by A4, Th14

      .= ( Class (E,(a * b))) by A1

      .= ( 1. (R / I)) by A24, A25, A26, Th6;

    end;

    theorem :: RING_1:20

    

     Th20: (R / I) is almost_left_invertible implies I is quasi-maximal

    proof

      set E = ( EqRel (R,I));

      assume

       A1: (R / I) is almost_left_invertible;

      given J be Ideal of R such that

       A2: I c= J and

       A3: J <> I and

       A4: J is proper;

       not J c= I by A2, A3;

      then

      consider a be object such that

       A5: a in J and

       A6: not a in I;

      reconsider a as Element of R by A5;

      reconsider x = ( Class (E,a)) as Element of (R / I) by Th12;

      

       A7: ( Class (E,( 0. R))) = ( 0. (R / I)) by Def6;

      now

        assume x = ( 0. (R / I));

        then (a - ( 0. R)) in I by A7, Th6;

        hence contradiction by A6, RLVECT_1: 13;

      end;

      then

      consider y be Element of (R / I) such that

       A8: (y * x) = ( 1. (R / I)) by A1;

      consider b be Element of R such that

       A9: y = ( Class (E,b)) by Th11;

      

       A10: ( Class (E,( 1. R))) = ( 1. (R / I)) by Def6;

      (y * x) = ( Class (E,(b * a))) by A9, Th14;

      then

       A11: ((b * a) - ( 1. R)) in I by A10, A8, Th6;

      

       A12: ( 1. R) = ((b * a) - ((b * a) - ( 1. R))) by Th2;

      (b * a) in J by A5, IDEAL_1:def 2;

      then ( 1. R) in J by A2, A11, A12, IDEAL_1: 15;

      hence thesis by A4, IDEAL_1: 19;

    end;

    theorem :: RING_1:21

    for R be commutative Ring, I be Ideal of R holds I is maximal iff (R / I) is Skew-Field by Th16, Th19, Th20;

    registration

      let R be non degenerated commutative Ring;

      cluster maximal -> prime for Ideal of R;

      coherence

      proof

        let I be Ideal of R;

        assume

         A1: I is proper quasi-maximal;

        then (R / I) is almost_left_invertible non degenerated by Th16, Th19;

        hence I is proper quasi-prime by A1, Th17;

      end;

    end

    ::$Notion-Name

    registration

      let R be non degenerated Ring;

      cluster maximal for Ideal of R;

      existence

      proof

        set S = { A where A be Ideal of R : A is proper };

        set P = ( RelIncl S);

        

         A1: P is_antisymmetric_in S by WELLORD2: 21;

        

         A2: ( field P) = S by WELLORD2:def 1;

        

         A3: S has_upper_Zorn_property_wrt P

        proof

          let Y be set such that

           A4: Y c= S and

           A5: (P |_2 Y) is being_linear-order;

          per cases ;

            suppose

             A6: Y is empty;

            take x = ( {( 0. R)} -Ideal );

            now

              assume x is non proper;

              then

               A7: x = the carrier of R by SUBSET_1:def 6;

              x = {( 0. R)} by IDEAL_1: 47;

              then ( 1. R) = ( 0. R) by A7, TARSKI:def 1;

              hence contradiction;

            end;

            hence x in S;

            thus thesis by A6;

          end;

            suppose Y is non empty;

            then

            consider e be object such that

             A8: e in Y;

            take x = ( union Y);

            x c= the carrier of R

            proof

              let a be object;

              assume a in x;

              then

              consider Z be set such that

               A9: a in Z and

               A10: Z in Y by TARSKI:def 4;

              Z in S by A4, A10;

              then ex A be Ideal of R st Z = A & A is proper;

              hence thesis by A9;

            end;

            then

            reconsider B = x as Subset of R;

            

             A11: B is right-ideal

            proof

              let p,a be Element of R;

              assume a in B;

              then

              consider Aa be set such that

               A12: a in Aa and

               A13: Aa in Y by TARSKI:def 4;

              Aa in S by A4, A13;

              then

              consider Ia be Ideal of R such that

               A14: Aa = Ia and Ia is proper;

              (a * p) in Ia & Ia c= B by A12, A13, A14, IDEAL_1:def 3, ZFMISC_1: 74;

              hence thesis;

            end;

            

             A15: B is left-ideal

            proof

              let p,a be Element of R;

              assume a in B;

              then

              consider Aa be set such that

               A16: a in Aa and

               A17: Aa in Y by TARSKI:def 4;

              Aa in S by A4, A17;

              then

              consider Ia be Ideal of R such that

               A18: Aa = Ia and Ia is proper;

              (p * a) in Ia & Ia c= B by A16, A17, A18, IDEAL_1:def 2, ZFMISC_1: 74;

              hence thesis;

            end;

             A19:

            now

              assume B is non proper;

              then ( 1. R) in B by A15, IDEAL_1: 19;

              then

              consider Aa be set such that

               A20: ( 1. R) in Aa and

               A21: Aa in Y by TARSKI:def 4;

              Aa in S by A4, A21;

              then ex Ia be Ideal of R st Aa = Ia & Ia is proper;

              hence contradiction by A20, IDEAL_1: 19;

            end;

            

             A22: B is add-closed

            proof

              

               A23: ( field (P |_2 Y)) = Y by A2, A4, ORDERS_1: 71;

              let a,b be Element of R;

               A24:

              now

                let A be Ideal of R;

                assume a in A & b in A;

                then

                 A25: (a + b) in A by IDEAL_1:def 1;

                assume A in Y;

                hence (a + b) in B by A25, TARSKI:def 4;

              end;

              assume a in B;

              then

              consider Aa be set such that

               A26: a in Aa and

               A27: Aa in Y by TARSKI:def 4;

              Aa in S by A4, A27;

              then

               A28: ex Ia be Ideal of R st Aa = Ia & Ia is proper;

              assume b in B;

              then

              consider Ab be set such that

               A29: b in Ab and

               A30: Ab in Y by TARSKI:def 4;

              (P |_2 Y) is connected by A5;

              then (P |_2 Y) is_connected_in ( field (P |_2 Y)) by RELAT_2:def 14;

              then [Aa, Ab] in (P |_2 Y) or [Ab, Aa] in (P |_2 Y) or Aa = Ab by A27, A30, A23, RELAT_2:def 6;

              then [Aa, Ab] in P or [Ab, Aa] in P or Aa = Ab by XBOOLE_0:def 4;

              then

               A31: Aa c= Ab or Ab c= Aa by A4, A27, A30, WELLORD2:def 1;

              Ab in S by A4, A30;

              then ex Ib be Ideal of R st Ab = Ib & Ib is proper;

              hence (a + b) in B by A26, A27, A29, A30, A24, A28, A31;

            end;

            e in S by A4, A8;

            then

            consider A be Ideal of R such that

             A32: e = A and A is proper;

            ex q be object st q in A by XBOOLE_0:def 1;

            then B is non empty by A8, A32, TARSKI:def 4;

            hence

             A33: x in S by A22, A15, A11, A19;

            let y be set;

            assume

             A34: y in Y;

            then y c= x by ZFMISC_1: 74;

            hence thesis by A4, A33, A34, WELLORD2:def 1;

          end;

        end;

        P is_reflexive_in S & P is_transitive_in S by WELLORD2: 19, WELLORD2: 20;

        then P partially_orders S by A1;

        then

        consider x be set such that

         A35: x is_maximal_in P by A2, A3, ORDERS_1: 63;

        

         A36: x in ( field P) by A35;

        then

        consider I be Ideal of R such that

         A37: x = I and

         A38: I is proper by A2;

        take I;

        thus I is proper by A38;

        let J be Ideal of R such that

         A39: I c= J;

        now

          assume J is proper;

          then

           A40: J in S;

          then [I, J] in P by A2, A36, A37, A39, WELLORD2:def 1;

          hence I = J by A2, A35, A37, A40;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non degenerated commutative Ring;

      cluster maximal for Ideal of R;

      existence

      proof

        set I = the maximal Ideal of R;

        take I;

        thus thesis;

      end;

    end

    registration

      let R be non degenerated commutative Ring, I be quasi-prime Ideal of R;

      cluster (R / I) -> domRing-like;

      coherence by Th17;

    end

    registration

      let R be non degenerated commutative Ring, I be quasi-maximal Ideal of R;

      cluster (R / I) -> almost_left_invertible;

      coherence by Th19;

    end