ringfrac.miz



    begin

    reserve R,R1 for commutative Ring;

    reserve A,B for non degenerated commutative Ring;

    reserve o,o1,o2 for object;

    reserve r,r1,r2 for Element of R;

    reserve a,a1,a2,b,b1 for Element of A;

    reserve f for Function of R, R1;

    reserve p for Element of ( Spectrum A);

    definition

      let R be commutative Ring;

      let r be Element of R;

      :: RINGFRAC:def1

      attr r is zero_divisible means

      : Def1: ex r1 be Element of R st r1 <> ( 0. R) & (r * r1) = ( 0. R);

    end

    registration

      let A be non degenerated commutative Ring;

      cluster zero_divisible for Element of A;

      existence

      proof

        consider b be Element of A such that

         A1: b = ( 1. A);

        (( 0. A) * b) = ( 0. A);

        then ( 0. A) is zero_divisible by A1;

        hence thesis;

      end;

    end

    definition

      let A;

      mode Zero_Divisor of A is zero_divisible Element of A;

    end

    theorem :: RINGFRAC:1

    

     Th1: ( 0. A) is Zero_Divisor of A

    proof

      consider b be Element of A such that

       A1: b = ( 1. A);

      (( 0. A) * b) = ( 0. A);

      then ( 0. A) is zero_divisible by A1;

      hence thesis;

    end;

    theorem :: RINGFRAC:2

    

     Th2: not ( 1. A) is Zero_Divisor of A

    proof

      assume ( 1. A) is Zero_Divisor of A;

      then

      consider b be Element of A such that

       A2: b <> ( 0. A) and

       A3: (( 1. A) * b) = ( 0. A) by Def1;

      thus contradiction by A2, A3;

    end;

    definition

      let A;

      :: RINGFRAC:def2

      func ZeroDiv_Set (A) -> Subset of A equals { a where a be Element of A : a is Zero_Divisor of A };

      coherence

      proof

        set C = { a where a be Element of A : a is Zero_Divisor of A };

        for x be object holds x in C implies x in ( [#] A)

        proof

          let x be object;

          assume x in C;

          then ex a be Element of ( [#] A) st x = a & a is Zero_Divisor of A;

          hence thesis;

        end;

        then C c= ( [#] A);

        hence thesis;

      end;

    end

    definition

      let A;

      :: RINGFRAC:def3

      func Non_ZeroDiv_Set (A) -> Subset of A equals (( [#] A) \ ( ZeroDiv_Set A));

      coherence ;

    end

    registration

      let A;

      cluster ( ZeroDiv_Set A) -> non empty;

      coherence

      proof

        set a = ( 0. A);

        a is Zero_Divisor of A by Th1;

        then a in ( ZeroDiv_Set A);

        hence thesis;

      end;

      cluster ( Non_ZeroDiv_Set A) -> non empty;

      coherence

      proof

        set a = ( 1. A);

         not a in ( ZeroDiv_Set A)

        proof

          assume a in ( ZeroDiv_Set A);

          then ex a1 be Element of ( [#] A) st a1 = a & a1 is Zero_Divisor of A;

          hence contradiction by Th2;

        end;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    theorem :: RINGFRAC:3

    

     Th3: not ( 0. A) in ( Non_ZeroDiv_Set A)

    proof

      ( 0. A) is Zero_Divisor of A by Th1;

      then ( 0. A) in ( ZeroDiv_Set A);

      hence thesis by XBOOLE_0:def 5;

    end;

    theorem :: RINGFRAC:4

    

     Th4: A is domRing implies {( 0. A)} = ( ZeroDiv_Set A)

    proof

      assume

       A0: A is domRing;

      ( 0. A) is Zero_Divisor of A by Th1;

      then

       A1: ( 0. A) in ( ZeroDiv_Set A);

      

       A2: {( 0. A)} is Subset of ( ZeroDiv_Set A) by A1, SUBSET_1: 33;

      for o st o in ( ZeroDiv_Set A) holds o in {( 0. A)}

      proof

        let o;

        assume o in ( ZeroDiv_Set A);

        then

        consider a be Element of ( [#] A) such that

         A4: o = a and

         A5: a is Zero_Divisor of A;

        consider b be Element of A such that

         A6: b <> ( 0. A) and

         A7: (a * b) = ( 0. A) by A5, Def1;

        a = ( 0. A) by A6, A0, A7, VECTSP_2:def 1;

        hence thesis by A4, TARSKI:def 1;

      end;

      then ( ZeroDiv_Set A) c= {( 0. A)};

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: RINGFRAC:5

    

     Th5: {( 1. R)} is multiplicatively-closed

    proof

      set M = {( 1. R)};

      for r1,r2 be Element of R st r1 in M & r2 in M holds (r1 * r2) in M

      proof

        let r1,r2 be Element of R;

        assume

         A2: r1 in M & r2 in M;

        

        then (r1 * r2) = (( 1. R) * r1) by TARSKI:def 1

        .= ( 1. R) by A2, TARSKI:def 1;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis by TARSKI:def 1;

    end;

    registration

      let R;

      cluster multiplicatively-closed for non empty Subset of R;

      existence

      proof

        reconsider M = {( 1. R)} as non empty Subset of R;

        take M;

        thus thesis by Th5;

      end;

    end

    definition

      let A;

      let V be Subset of A;

      :: RINGFRAC:def4

      attr V is without_zero means not ( 0. A) in V;

    end

    registration

      let A;

      cluster without_zero for non empty multiplicatively-closed Subset of A;

      existence

      proof

        reconsider M = {( 1. A)} as non empty multiplicatively-closed Subset of A by Th5;

        take M;

        thus thesis by TARSKI:def 1;

      end;

    end

    

     Lm5: o in ( Spectrum A) implies o is prime Ideal of A

    proof

      assume o in ( Spectrum A);

      then o in { I where I be Ideal of A : I is quasi-prime & I <> ( [#] A) } by TOPZARI1:def 5;

      then

      consider o1 be Ideal of A such that

       A1: o1 = o & o1 is quasi-prime & o1 <> ( [#] A);

      o1 is proper Ideal of A by A1, SUBSET_1:def 6;

      hence thesis by A1;

    end;

    theorem :: RINGFRAC:6

    

     Th6: (( [#] A) \ p) is multiplicatively-closed

    proof

      reconsider p as prime Ideal of A by Lm5;

      reconsider M = (( [#] A) \ p) as Subset of A;

      

       A1: not ( 1. A) in p by IDEAL_1: 19;

      then

      reconsider M as non empty Subset of A by XBOOLE_0:def 5;

      for a,b be Element of A st a in M & b in M holds (a * b) in M

      proof

        let a,b be Element of A;

        assume

         A2: a in M & b in M;

        assume not (a * b) in M;

        then (a * b) in p by XBOOLE_0:def 5;

        then a in p or b in p by RING_1:def 1;

        hence contradiction by A2, XBOOLE_0:def 5;

      end;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: RINGFRAC:7

    for J be proper Ideal of A holds ( multClSet (J,a)) is multiplicatively-closed;

    registration

      let A;

      cluster ( Non_ZeroDiv_Set A) -> multiplicatively-closed;

      coherence

      proof

        set M = (( [#] A) \ ( ZeroDiv_Set A));

        

         A1: not ( 1. A) in ( ZeroDiv_Set A)

        proof

          assume ( 1. A) in ( ZeroDiv_Set A);

          then

          consider a be Element of ( [#] A) such that

           A2: a = ( 1. A) and

           A3: a is Zero_Divisor of A;

          thus contradiction by Th2, A2, A3;

        end;

        for v,u be Element of A st v in M & u in M holds (v * u) in M

        proof

          let v,u be Element of A;

          assume

           A5: v in M & u in M;

          assume not (v * u) in M;

          then (v * u) in ( ZeroDiv_Set A) by XBOOLE_0:def 5;

          then

          consider w be Element of ( [#] A) such that

           A7: w = (v * u) and

           A8: w is Zero_Divisor of A;

          w is zero_divisible by A8;

          then

          consider b be Element of A such that

           A9: b <> ( 0. A) and

           A10: (w * b) = ( 0. A);

          

           A11: (v * (u * b)) = ( 0. A) by A10, A7, GROUP_1:def 3;

          per cases ;

            suppose (u * b) <> ( 0. A);

            then v is zero_divisible by A11;

            then v in ( ZeroDiv_Set A);

            hence contradiction by A5, XBOOLE_0:def 5;

          end;

            suppose (u * b) = ( 0. A);

            then u is zero_divisible by A9;

            then u in ( ZeroDiv_Set A);

            hence contradiction by A5, XBOOLE_0:def 5;

          end;

        end;

        hence thesis by A1, XBOOLE_0:def 5;

      end;

    end

    definition

      let R;

      :: RINGFRAC:def5

      func Unit_Set (R) -> Subset of R equals { a where a be Element of R : a is Unit of R };

      coherence

      proof

        set C = { a where a be Element of R : a is Unit of R };

        for x be object holds x in C implies x in ( [#] R)

        proof

          let x be object;

          assume x in C;

          then ex a be Element of ( [#] R) st x = a & a is Unit of R;

          hence thesis;

        end;

        then C c= ( [#] R);

        hence thesis;

      end;

    end

    registration

      let R;

      cluster ( Unit_Set R) -> non empty;

      coherence

      proof

        set r = ( 1. R);

        r in ( Unit_Set R);

        hence thesis;

      end;

    end

    

     Th9: r1 in ( Unit_Set R) implies ex r2 st (r1 * r2) = ( 1. R)

    proof

      assume r1 in ( Unit_Set R);

      then

      consider r be Element of ( [#] R) such that

       A2: r1 = r and

       A3: r is Unit of R;

      reconsider r1 as Element of R;

      ( {r1} -Ideal ) = ( [#] R) by A2, A3, RING_2: 20;

      then

       A4: ( 1. R) in ( {r1} -Ideal );

      ( {r1} -Ideal ) = the set of all (r1 * r) where r be Element of R by IDEAL_1: 64;

      hence thesis by A4;

    end;

    

     Th10: r1 in ( Unit_Set R) implies ex r2 st (r2 * r1) = ( 1. R)

    proof

      assume r1 in ( Unit_Set R);

      then ex r2 st (r1 * r2) = ( 1. R) by Th9;

      hence thesis;

    end;

    theorem :: RINGFRAC:8

    

     Th11: r1 in ( Unit_Set R) implies r1 is right_mult-cancelable

    proof

      assume r1 in ( Unit_Set R);

      then

      consider r2 such that

       A2: (r2 * r1) = ( 1. R) by Th10;

      for u,v be Element of R st (u * r1) = (v * r1) holds u = v

      proof

        let u,v be Element of R;

        assume (u * r1) = (v * r1);

        

        then

         A5: (r1 * (u - v)) = ((r1 * v) - (r1 * v)) by VECTSP_1: 11

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

        (u - v) = ((r2 * r1) * (u - v)) by A2

        .= (r2 * (r1 * (u - v))) by GROUP_1:def 3

        .= ( 0. R) by A5;

        hence thesis by VECTSP_1: 19;

      end;

      hence thesis;

    end;

    definition

      let R;

      let r be Element of R;

      assume

       A1: r in ( Unit_Set R);

      :: RINGFRAC:def6

      func recip (r) -> Element of R means

      : Def2: (it * r) = ( 1. R);

      existence by A1, Th10;

      uniqueness

      proof

        r is right_mult-cancelable by Th11, A1;

        hence thesis;

      end;

    end

    notation

      let R;

      let r be Element of R;

      synonym r ["] for recip (r);

    end

    definition

      let R;

      let u,v be Element of R;

      :: RINGFRAC:def7

      func u [/] v -> Element of R equals (u * ( recip u));

      coherence ;

    end

    theorem :: RINGFRAC:9

    

     Th12: for u be Unit of R, v be Element of R holds f is RingHomomorphism implies (f . u) is Unit of R1 & ((f . u) ["] ) = (f . (u ["] ))

    proof

      let u be Unit of R, v be Element of R;

      assume

       A1: f is RingHomomorphism;

      then

       A3: f is multiplicative;

      

       A2: u in ( Unit_Set R);

      f is unity-preserving by A1;

      

      then

       A5: ( 1. R1) = (f . (u * (u ["] ))) by A2, Def2

      .= ((f . u) * (f . (u ["] ))) by A3;

      then (f . u) divides ( 1. R1);

      then

       A7: (f . u) is unital;

      then

       A8: (f . u) in ( Unit_Set R1);

      ((f . u) ["] ) = (((f . u) ["] ) * ((f . u) * (f . (u ["] )))) by A5

      .= ((((f . u) ["] ) * (f . u)) * (f . (u ["] ))) by GROUP_1:def 3

      .= (( 1. R1) * (f . (u ["] ))) by Def2, A8

      .= (f . (u ["] ));

      hence thesis by A7;

    end;

    theorem :: RINGFRAC:10

    for u be Unit of R, v be Element of R holds f is RingHomomorphism implies (f . (v * (u ["] ))) = ((f . v) * ((f . u) ["] ))

    proof

      let u be Unit of R, v be Element of R;

      assume

       A1: f is RingHomomorphism;

      then f is multiplicative;

      

      then (f . (v * (u ["] ))) = ((f . v) * (f . (u ["] )))

      .= ((f . v) * ((f . u) ["] )) by A1, Th12;

      hence thesis;

    end;

    begin

    reserve S for non empty multiplicatively-closed Subset of R;

    definition

      let R, S;

      :: RINGFRAC:def8

      func Frac (S) -> Subset of [:the carrier of R, the carrier of R:] means

      : Def3: for x be set holds x in it iff ex a,b be Element of R st x = [a, b] & b in S;

      existence

      proof

        set M = { [a, b] where a,b be Element of R : b in S };

        

         A1: M c= [:the carrier of R, the carrier of R:]

        proof

          let o be object;

          assume o in M;

          then ex a,b be Element of R st o = [a, b] & b in S;

          hence thesis;

        end;

        for x be set holds x in M iff ex a,b be Element of R st x = [a, b] & b in S;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let M1,M2 be Subset of [:the carrier of R, the carrier of R:];

        assume

         A2: for x be set holds x in M1 iff ex a,b be Element of R st x = [a, b] & b in S;

        assume

         A3: for x be set holds x in M2 iff ex a,b be Element of R st x = [a, b] & b in S;

        

         A4: for x be object holds x in M2 implies x in M1

        proof

          let o be object;

          assume o in M2;

          then ex a,b be Element of R st o = [a, b] & b in S by A3;

          hence thesis by A2;

        end;

        for o be object holds o in M1 implies o in M2

        proof

          let o be object;

          assume o in M1;

          then ex a,b be Element of R st o = [a, b] & b in S by A2;

          hence thesis by A3;

        end;

        hence thesis by A4, TARSKI: 2;

      end;

    end

    theorem :: RINGFRAC:11

    

     Th15: ( Frac S) = [:( [#] R), S:]

    proof

      o in ( Frac S) implies o in [:( [#] R), S:]

      proof

        assume o in ( Frac S);

        then

        consider a,b be Element of R such that

         A2: o = [a, b] and

         A3: b in S by Def3;

        thus thesis by A2, A3, ZFMISC_1:def 2;

      end;

      then

       A3: ( Frac S) c= [:( [#] R), S:];

      o in [:( [#] R), S:] implies o in ( Frac S)

      proof

        assume o in [:( [#] R), S:];

        then

        consider o1,o2 be object such that

         A5: o1 in ( [#] R) and

         A6: o2 in S and

         A7: o = [o1, o2] by ZFMISC_1:def 2;

        consider a,b be Element of R such that

         A8: a = o1 and

         A9: b = o2 by A5, A6;

        o = [a, b] by A8, A9, A7;

        hence thesis by A6, A9, Def3;

      end;

      then [:( [#] R), S:] c= ( Frac S);

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    registration

      let R, S;

      cluster ( Frac S) -> non empty;

      coherence

      proof

        ( 1. R) in S by C0SP1:def 4;

        then [( 1. R), ( 1. R)] in ( Frac S) by Def3;

        hence thesis;

      end;

    end

    

     Lm16: for x be object st x in the carrier of R holds [x, ( 1. R)] in ( Frac S)

    proof

      let x be object;

      assume x in the carrier of R;

      then

      reconsider x as Element of R;

      ( 1. R) in S by C0SP1:def 4;

      then [x, ( 1. R)] in ( Frac S) by Def3;

      hence thesis;

    end;

    definition

      let R, S;

      :: RINGFRAC:def9

      func frac1 (S) -> Function of R, ( Frac S) means

      : Def4: for o be object st o in the carrier of R holds (it . o) = [o, ( 1. R)];

      existence

      proof

        deffunc F( object) = [$1, ( 1. R)];

        

         A1: for o1 be object st o1 in the carrier of R holds F(o1) in ( Frac S) by Lm16;

        ex f be Function of R, ( Frac S) st for o2 be object st o2 in the carrier of R holds (f . o2) = F(o2) from FUNCT_2:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of R, ( Frac S) such that

         A2: for o be object st o in the carrier of R holds (f1 . o) = [o, ( 1. R)] and

         A3: for o be object st o in the carrier of R holds (f2 . o) = [o, ( 1. R)];

        for o1 be object st o1 in the carrier of R holds (f1 . o1) = (f2 . o1)

        proof

          let o1 be object such that

           A4: o1 in the carrier of R;

          (f1 . o1) = [o1, ( 1. R)] by A2, A4;

          hence thesis by A3, A4;

        end;

        hence thesis;

      end;

    end

    reserve u,v,w,x,y,z for Element of ( Frac S);

    

     Lm17: (x `1 ) in R & (x `2 ) in S

    proof

      x in ( Frac S);

      then x in [:( [#] R), S:] by Th15;

      hence thesis by MCART_1: 10;

    end;

    

     Th18: for u be Element of ( Frac S) holds (u `2 ) in S

    proof

      let u be Element of ( Frac S);

      ex a,b be Element of R st u = [a, b] & b in S by Def3;

      hence thesis;

    end;

    definition

      let R, S;

      let u,v be Element of ( Frac S);

      :: RINGFRAC:def10

      func Fracadd (u,v) -> Element of ( Frac S) equals [(((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 ))), ((u `2 ) * (v `2 ))];

      coherence

      proof

        (u `2 ) in S & (v `2 ) in S by Th18;

        then ((u `2 ) * (v `2 )) in S by C0SP1:def 4;

        hence thesis by Def3;

      end;

      commutativity ;

    end

    definition

      let R, S;

      let u,v be Element of ( Frac S);

      :: RINGFRAC:def11

      func Fracmult (u,v) -> Element of ( Frac S) equals [((u `1 ) * (v `1 )), ((u `2 ) * (v `2 ))];

      coherence

      proof

        (u `2 ) in S & (v `2 ) in S by Th18;

        then ((u `2 ) * (v `2 )) in S by C0SP1:def 4;

        hence thesis by Def3;

      end;

      commutativity ;

    end

    definition

      let R, S, x, y;

      :: RINGFRAC:def12

      func x + y -> Element of ( Frac S) equals ( Fracadd (x,y));

      coherence ;

      :: RINGFRAC:def13

      func x * y -> Element of ( Frac S) equals ( Fracmult (x,y));

      coherence ;

    end

    theorem :: RINGFRAC:12

    

     Th19: ( Fracadd (x,( Fracadd (y,z)))) = ( Fracadd (( Fracadd (x,y)),z))

    proof

      ( Fracadd (( Fracadd (x,y)),z)) = [(((((x `1 ) * (y `2 )) * (z `2 )) + (((y `1 ) * (x `2 )) * (z `2 ))) + ((z `1 ) * ((x `2 ) * (y `2 )))), (((x `2 ) * (y `2 )) * (z `2 ))] by VECTSP_1:def 7

      .= [((((x `1 ) * ((y `2 ) * (z `2 ))) + (((y `1 ) * (x `2 )) * (z `2 ))) + ((z `1 ) * ((x `2 ) * (y `2 )))), (((x `2 ) * (y `2 )) * (z `2 ))] by GROUP_1:def 3

      .= [((((x `1 ) * ((y `2 ) * (z `2 ))) + (((y `1 ) * (z `2 )) * (x `2 ))) + ((z `1 ) * ((y `2 ) * (x `2 )))), (((x `2 ) * (y `2 )) * (z `2 ))] by GROUP_1:def 3

      .= [((((x `1 ) * ((y `2 ) * (z `2 ))) + (((y `1 ) * (z `2 )) * (x `2 ))) + (((z `1 ) * (y `2 )) * (x `2 ))), (((x `2 ) * (y `2 )) * (z `2 ))] by GROUP_1:def 3

      .= [((((x `1 ) * ((y `2 ) * (z `2 ))) + (((y `1 ) * (z `2 )) * (x `2 ))) + (((z `1 ) * (y `2 )) * (x `2 ))), ((x `2 ) * ((y `2 ) * (z `2 )))] by GROUP_1:def 3

      .= [(((x `1 ) * ((y `2 ) * (z `2 ))) + ((((y `1 ) * (z `2 )) * (x `2 )) + (((z `1 ) * (y `2 )) * (x `2 )))), ((x `2 ) * ((y `2 ) * (z `2 )))] by RLVECT_1:def 3

      .= ( Fracadd (x,( Fracadd (y,z)))) by VECTSP_1:def 7;

      hence thesis;

    end;

    theorem :: RINGFRAC:13

    

     Th20: ( Fracmult (x,( Fracmult (y,z)))) = ( Fracmult (( Fracmult (x,y)),z))

    proof

       [((x `1 ) * ((y `1 ) * (z `1 ))), ((x `2 ) * ((y `2 ) * (z `2 )))] = [((x `1 ) * ((y `1 ) * (z `1 ))), (((x `2 ) * (y `2 )) * (z `2 ))] by GROUP_1:def 3

      .= ( Fracmult (( Fracmult (x,y)),z)) by GROUP_1:def 3;

      hence thesis;

    end;

    definition

      let R, S;

      let x,y be Element of ( Frac S);

      :: RINGFRAC:def14

      pred x,y Fr_Eq S means ex s1 be Element of R st s1 in S & ((((x `1 ) * (y `2 )) - ((y `1 ) * (x `2 ))) * s1) = ( 0. R);

    end

    theorem :: RINGFRAC:14

    ( 0. R) in S implies (x,y) Fr_Eq S

    proof

      assume

       A1: ( 0. R) in S;

      reconsider s1 = ( 0. R) as Element of R;

      

       A2: ((((x `1 ) * (y `2 )) - ((y `1 ) * (x `2 ))) * s1) = ( 0. R);

      reconsider s1 as Element of S by A1;

      thus thesis by A1, A2;

    end;

    theorem :: RINGFRAC:15

    

     Th22: (x,x) Fr_Eq S

    proof

      reconsider s1 = ( 1. R) as Element of R;

      

       A1: ((((x `1 ) * (x `2 )) - ((x `1 ) * (x `2 ))) * s1) = ( 0. R) by VECTSP_1: 19;

      s1 in S by C0SP1:def 4;

      hence thesis by A1;

    end;

    theorem :: RINGFRAC:16

    

     Th23: (x,y) Fr_Eq S implies (y,x) Fr_Eq S

    proof

      assume (x,y) Fr_Eq S;

      then

      consider s1 be Element of R such that

       A2: s1 in S and

       A3: ((((x `1 ) * (y `2 )) - ((y `1 ) * (x `2 ))) * s1) = ( 0. R);

      reconsider w = ((y `1 ) * (x `2 )), v = ((x `1 ) * (y `2 )) as Element of R;

      ((w - v) * s1) = (( - (v - w)) * s1) by VECTSP_1: 17

      .= ( - ( 0. R)) by A3, VECTSP_1: 9

      .= ( 0. R);

      hence thesis by A2;

    end;

    theorem :: RINGFRAC:17

    

     Th24: (x,y) Fr_Eq S & (y,z) Fr_Eq S implies (x,z) Fr_Eq S

    proof

      assume (x,y) Fr_Eq S & (y,z) Fr_Eq S;

      then

      consider s1,s2 be Element of R such that

       A2: s1 in S and

       A3: s2 in S and

       A4: ((((x `1 ) * (y `2 )) - ((y `1 ) * (x `2 ))) * s1) = ( 0. R) and

       A5: ((((y `1 ) * (z `2 )) - ((z `1 ) * (y `2 ))) * s2) = ( 0. R);

      ( 0. R) = (((((x `1 ) * (y `2 )) - ((y `1 ) * (x `2 ))) * s1) * (z `2 )) by A4

      .= (((((x `1 ) * (y `2 )) * s1) - (((y `1 ) * (x `2 )) * s1)) * (z `2 )) by VECTSP_1: 13

      .= (((z `2 ) * (((x `1 ) * (y `2 )) * s1)) - ((z `2 ) * (((y `1 ) * (x `2 )) * s1))) by VECTSP_1: 11

      .= (((z `2 ) * ((x `1 ) * ((y `2 ) * s1))) - ((z `2 ) * (((y `1 ) * (x `2 )) * s1))) by GROUP_1:def 3

      .= ((((x `1 ) * (z `2 )) * ((y `2 ) * s1)) - ((z `2 ) * (((y `1 ) * (x `2 )) * s1))) by GROUP_1:def 3;

      

      then

       A7: ( 0. R) = (((((x `1 ) * (z `2 )) * ((y `2 ) * s1)) - ((z `2 ) * (((y `1 ) * (x `2 )) * s1))) * s2)

      .= (((((x `1 ) * (z `2 )) * ((y `2 ) * s1)) * s2) - (((z `2 ) * (((y `1 ) * (x `2 )) * s1)) * s2)) by VECTSP_1: 13

      .= ((((x `1 ) * (z `2 )) * (((y `2 ) * s1) * s2)) - (((z `2 ) * (((y `1 ) * (x `2 )) * s1)) * s2)) by GROUP_1:def 3

      .= ((((x `1 ) * (z `2 )) * (((y `2 ) * s1) * s2)) - ((z `2 ) * ((((y `1 ) * (x `2 )) * s1) * s2))) by GROUP_1:def 3;

      

       A8: ( 0. R) = (((((y `1 ) * (z `2 )) - ((z `1 ) * (y `2 ))) * s2) * (x `2 )) by A5

      .= (((((y `1 ) * (z `2 )) * s2) - (((z `1 ) * (y `2 )) * s2)) * (x `2 )) by VECTSP_1: 13

      .= (((((y `1 ) * (z `2 )) * s2) * (x `2 )) - ((x `2 ) * (((z `1 ) * (y `2 )) * s2))) by VECTSP_1: 13

      .= (((((y `1 ) * (z `2 )) * s2) * (x `2 )) - ((x `2 ) * ((z `1 ) * ((y `2 ) * s2)))) by GROUP_1:def 3

      .= (((((y `1 ) * (z `2 )) * s2) * (x `2 )) - (((x `2 ) * (z `1 )) * ((y `2 ) * s2))) by GROUP_1:def 3

      .= ((((z `2 ) * ((y `1 ) * s2)) * (x `2 )) - (((x `2 ) * (z `1 )) * ((y `2 ) * s2))) by GROUP_1:def 3

      .= (((z `2 ) * (((y `1 ) * s2) * (x `2 ))) - (((x `2 ) * (z `1 )) * ((y `2 ) * s2))) by GROUP_1:def 3

      .= (((z `2 ) * (((y `1 ) * (x `2 )) * s2)) - (((x `2 ) * (z `1 )) * ((y `2 ) * s2))) by GROUP_1:def 3

      .= (((z `2 ) * (((y `1 ) * (x `2 )) * s2)) - ((((z `1 ) * (x `2 )) * (y `2 )) * s2)) by GROUP_1:def 3;

      

       A9: ( 0. R) = (( 0. R) * s1)

      .= ((((z `2 ) * (((y `1 ) * (x `2 )) * s2)) - (((z `1 ) * (x `2 )) * ((y `2 ) * s2))) * s1) by A8, GROUP_1:def 3

      .= ((((z `2 ) * (((y `1 ) * (x `2 )) * s2)) * s1) - ((((z `1 ) * (x `2 )) * ((y `2 ) * s2)) * s1)) by VECTSP_1: 13

      .= (((z `2 ) * ((((y `1 ) * (x `2 )) * s2) * s1)) - ((((z `1 ) * (x `2 )) * ((y `2 ) * s2)) * s1)) by GROUP_1:def 3

      .= (((z `2 ) * ((((y `1 ) * (x `2 )) * s2) * s1)) - (((z `1 ) * (x `2 )) * (((y `2 ) * s2) * s1))) by GROUP_1:def 3

      .= (((z `2 ) * ((((y `1 ) * (x `2 )) * s1) * s2)) - (((z `1 ) * (x `2 )) * (((y `2 ) * s2) * s1))) by GROUP_1:def 3

      .= (((z `2 ) * ((((y `1 ) * (x `2 )) * s1) * s2)) - (((z `1 ) * (x `2 )) * (((y `2 ) * s1) * s2))) by GROUP_1:def 3;

      reconsider u = ((z `2 ) * ((((y `1 ) * (x `2 )) * s1) * s2)) as Element of R;

      (y `2 ) in S by Lm17;

      then

      reconsider v = ((y `2 ) * s1) as Element of S by A2, C0SP1:def 4;

      reconsider w = (v * s2) as Element of S by A3, C0SP1:def 4;

      ( 0. R) = ((((((x `1 ) * (z `2 )) * (((y `2 ) * s1) * s2)) - u) + u) - (((z `1 ) * (x `2 )) * (((y `2 ) * s1) * s2))) by A7, A9

      .= (((((x `1 ) * (z `2 )) * (((y `2 ) * s1) * s2)) + (( - u) + u)) - (((z `1 ) * (x `2 )) * (((y `2 ) * s1) * s2))) by RLVECT_1:def 3

      .= (((((x `1 ) * (z `2 )) * (((y `2 ) * s1) * s2)) + ( 0. R)) - (((z `1 ) * (x `2 )) * (((y `2 ) * s1) * s2))) by RLVECT_1: 5

      .= ((((x `1 ) * (z `2 )) - ((z `1 ) * (x `2 ))) * w) by VECTSP_1: 13;

      hence thesis;

    end;

    definition

      let R, S;

      :: RINGFRAC:def15

      func EqRel (S) -> Equivalence_Relation of ( Frac S) means

      : Def5: [u, v] in it iff (u,v) Fr_Eq S;

      existence

      proof

        defpred P[ object, object] means ex u, v st u = $1 & v = $2 & (u,v) Fr_Eq S;

        

         A1: for o,o1 be object st P[o, o1] holds P[o1, o] by Th23;

        

         A2: for o,o1,o2 be object st P[o, o1] & P[o1, o2] holds P[o, o2] by Th24;

        

         A3: for o be object st o in ( Frac S) holds P[o, o] by Th22;

        consider ER be Equivalence_Relation of ( Frac S) such that

         A4: for o,o1 be object holds [o, o1] in ER iff o in ( Frac S) & o1 in ( Frac S) & P[o, o1] from EQREL_1:sch 1( A3, A1, A2);

        take ER;

         [u, v] in ER iff (u,v) Fr_Eq S

        proof

          thus [u, v] in ER implies (u,v) Fr_Eq S

          proof

            assume [u, v] in ER;

            then ex u1,v1 be Element of ( Frac S) st u1 = u & v1 = v & (u1,v1) Fr_Eq S by A4;

            hence thesis;

          end;

          assume (u,v) Fr_Eq S;

          hence thesis by A4;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let R1,R2 be Equivalence_Relation of ( Frac S);

        assume that

         A5: for u, v holds [u, v] in R1 iff (u,v) Fr_Eq S and

         A6: for u, v holds [u, v] in R2 iff (u,v) Fr_Eq S;

        for o,o1 be object holds [o, o1] in R1 iff [o, o1] in R2

        proof

          let o,o1 be object;

          thus [o, o1] in R1 implies [o, o1] in R2

          proof

            assume

             A7: [o, o1] in R1;

            then o is Element of ( Frac S) & o1 is Element of ( Frac S) by ZFMISC_1: 87;

            hence thesis by A5, A6, A7;

          end;

          assume

           A8: [o, o1] in R2;

          then o is Element of ( Frac S) & o1 is Element of ( Frac S) by ZFMISC_1: 87;

          hence thesis by A5, A6, A8;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    theorem :: RINGFRAC:18

    

     Th25: x in ( Class (( EqRel S),y)) iff (x,y) Fr_Eq S

    proof

      set E = ( EqRel S);

      hereby

        assume x in ( Class (E,y));

        then [x, y] in E by EQREL_1: 19;

        hence (x,y) Fr_Eq S by Def5;

      end;

      assume (x,y) Fr_Eq S;

      then [x, y] in E by Def5;

      hence thesis by EQREL_1: 19;

    end;

    theorem :: RINGFRAC:19

    

     Th26: ( Class (( EqRel S),x)) = ( Class (( EqRel S),y)) iff (x,y) Fr_Eq S

    proof

      set E = ( EqRel S);

      thus ( Class (E,x)) = ( Class (E,y)) implies (x,y) Fr_Eq S

      proof

        assume ( Class (E,x)) = ( Class (E,y));

        then x in ( Class (E,y)) by EQREL_1: 23;

        hence thesis by Th25;

      end;

      assume (x,y) Fr_Eq S;

      then x in ( Class (E,y)) by Th25;

      hence thesis by EQREL_1: 23;

    end;

    theorem :: RINGFRAC:20

    

     Th27: (x,u) Fr_Eq S & (y,v) Fr_Eq S implies (( Fracmult (x,y)),( Fracmult (u,v))) Fr_Eq S

    proof

      assume that

       A1: (x,u) Fr_Eq S and

       A2: (y,v) Fr_Eq S;

      consider s1 be Element of R such that

       A3: s1 in S and

       A4: ((((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) * s1) = ( 0. R) by A1;

      consider s2 be Element of R such that

       A5: s2 in S and

       A6: ((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * s2) = ( 0. R) by A2;

      

       A7: (((( Fracmult (x,y)) `1 ) * (( Fracmult (u,v)) `2 )) - (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 )))) = (((((x `1 ) * (y `1 )) * (u `2 )) * (v `2 )) - (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 )))) by GROUP_1:def 3

      .= (((((x `1 ) * (u `2 )) * (y `1 )) * (v `2 )) - (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 )))) by GROUP_1:def 3

      .= ((((x `1 ) * (u `2 )) * ((y `1 ) * (v `2 ))) - (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 )))) by GROUP_1:def 3

      .= ((((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) * ((y `1 ) * (v `2 ))) by VECTSP_1: 13;

      

       A8: ((((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 ))) - ((( Fracmult (u,v)) `1 ) * (( Fracmult (x,y)) `2 ))) = ((((y `1 ) * (v `2 )) * ((u `1 ) * (x `2 ))) - ((((v `1 ) * (u `1 )) * (y `2 )) * (x `2 ))) by GROUP_1:def 3

      .= ((((y `1 ) * (v `2 )) * ((u `1 ) * (x `2 ))) - ((((v `1 ) * (y `2 )) * (u `1 )) * (x `2 ))) by GROUP_1:def 3

      .= ((((y `1 ) * (v `2 )) * ((u `1 ) * (x `2 ))) - (((v `1 ) * (y `2 )) * ((u `1 ) * (x `2 )))) by GROUP_1:def 3

      .= ((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * ((u `1 ) * (x `2 ))) by VECTSP_1: 13;

      

       A9: (((( Fracmult (x,y)) `1 ) * (( Fracmult (u,v)) `2 )) - ((( Fracmult (u,v)) `1 ) * (( Fracmult (x,y)) `2 ))) = ((((( Fracmult (x,y)) `1 ) * (( Fracmult (u,v)) `2 )) - ((( Fracmult (u,v)) `1 ) * (( Fracmult (x,y)) `2 ))) + ( 0. R))

      .= ((((( Fracmult (x,y)) `1 ) * (( Fracmult (u,v)) `2 )) - ((( Fracmult (u,v)) `1 ) * (( Fracmult (x,y)) `2 ))) + (( - (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 )))) + (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 ))))) by RLVECT_1: 5

      .= ((((( Fracmult (x,y)) `1 ) * (( Fracmult (u,v)) `2 )) + (( - (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 )))) + (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 ))))) + ( - ((( Fracmult (u,v)) `1 ) * (( Fracmult (x,y)) `2 )))) by RLVECT_1:def 3

      .= (((((( Fracmult (x,y)) `1 ) * (( Fracmult (u,v)) `2 )) + ( - (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 ))))) + (((u `1 ) * (x `2 )) * ((y `1 ) * (v `2 )))) + ( - ((( Fracmult (u,v)) `1 ) * (( Fracmult (x,y)) `2 )))) by RLVECT_1:def 3

      .= (((((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) * ((y `1 ) * (v `2 ))) + ((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * ((u `1 ) * (x `2 )))) by A8, A7, RLVECT_1:def 3;

      reconsider s = (s1 * s2) as Element of S by A3, A5, C0SP1:def 4;

      reconsider t = (((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) as Element of R;

      reconsider t2 = ((s2 * (y `1 )) * (v `2 )) as Element of R;

      ((((( Fracmult (x,y)) `1 ) * (( Fracmult (u,v)) `2 )) - ((( Fracmult (u,v)) `1 ) * (( Fracmult (x,y)) `2 ))) * s) = (((t * ((y `1 ) * (v `2 ))) * s) + (((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * ((u `1 ) * (x `2 ))) * s)) by A9, VECTSP_1:def 3

      .= (((t * s) * ((y `1 ) * (v `2 ))) + (((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * ((u `1 ) * (x `2 ))) * s)) by GROUP_1:def 3

      .= (((( 0. R) * s2) * ((y `1 ) * (v `2 ))) + (((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * ((u `1 ) * (x `2 ))) * s)) by A4, GROUP_1:def 3

      .= (((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * s) * ((u `1 ) * (x `2 ))) by GROUP_1:def 3

      .= ((( 0. R) * s1) * ((u `1 ) * (x `2 ))) by A6, GROUP_1:def 3

      .= ( 0. R);

      hence thesis;

    end;

    theorem :: RINGFRAC:21

    

     Th28: (x,u) Fr_Eq S & (y,v) Fr_Eq S implies (( Fracadd (x,y)),( Fracadd (u,v))) Fr_Eq S

    proof

      assume that

       A1: (x,u) Fr_Eq S and

       A2: (y,v) Fr_Eq S;

      consider s1 be Element of R such that

       A3: s1 in S and

       A4: ((((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) * s1) = ( 0. R) by A1;

      consider s2 be Element of R such that

       A5: s2 in S and

       A6: ((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * s2) = ( 0. R) by A2;

      reconsider z = ( Fracadd (x,y)) as Element of ( Frac S);

      reconsider w = ( Fracadd (u,v)) as Element of ( Frac S);

      

       A7: (((x `1 ) * (u `2 )) * ((y `2 ) * (v `2 ))) = ((((x `1 ) * (u `2 )) * ((y `2 ) * (v `2 ))) + ( 0. R))

      .= ((((x `1 ) * (u `2 )) * ((y `2 ) * (v `2 ))) + (( - (((u `1 ) * (x `2 )) * ((y `2 ) * (v `2 )))) + (((u `1 ) * (x `2 )) * ((y `2 ) * (v `2 ))))) by RLVECT_1: 5

      .= (((((x `1 ) * (u `2 )) * ((y `2 ) * (v `2 ))) - (((u `1 ) * (x `2 )) * ((y `2 ) * (v `2 )))) + (((u `1 ) * (x `2 )) * ((y `2 ) * (v `2 )))) by RLVECT_1:def 3

      .= (((((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) * ((y `2 ) * (v `2 ))) + (((u `1 ) * (x `2 )) * ((y `2 ) * (v `2 )))) by VECTSP_1: 13;

      reconsider t = ((((u `1 ) * (x `2 )) * (y `2 )) * (v `2 )) as Element of R;

      

       A8: ((((u `1 ) * (v `2 )) * (x `2 )) * (y `2 )) = ((((u `1 ) * (x `2 )) * (v `2 )) * (y `2 )) by GROUP_1:def 3

      .= t by GROUP_1:def 3;

      

       A9: ((((y `1 ) * (x `2 )) * (u `2 )) * (v `2 )) = (((y `1 ) * ((x `2 ) * (u `2 ))) * (v `2 )) by GROUP_1:def 3

      .= (((y `1 ) * (v `2 )) * ((x `2 ) * (u `2 ))) by GROUP_1:def 3;

      

       A10: (((v `1 ) * (u `2 )) * ((x `2 ) * (y `2 ))) = ((((v `1 ) * (u `2 )) * (x `2 )) * (y `2 )) by GROUP_1:def 3

      .= (((v `1 ) * ((u `2 ) * (x `2 ))) * (y `2 )) by GROUP_1:def 3

      .= (((v `1 ) * (y `2 )) * ((x `2 ) * (u `2 ))) by GROUP_1:def 3;

      

       A11: ((((u `1 ) * (x `2 )) * ((y `2 ) * (v `2 ))) + ((((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 ))) - ((w `1 ) * (z `2 )))) = (((((u `1 ) * (x `2 )) * ((y `2 ) * (v `2 ))) + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) - ((w `1 ) * (z `2 ))) by RLVECT_1:def 3

      .= ((((((u `1 ) * (x `2 )) * (y `2 )) * (v `2 )) + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) - ((w `1 ) * (z `2 ))) by GROUP_1:def 3

      .= ((t + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) - ((((u `1 ) * (v `2 )) * ((x `2 ) * (y `2 ))) + (((v `1 ) * (u `2 )) * ((x `2 ) * (y `2 ))))) by VECTSP_1:def 7

      .= ((t + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) - (t + (((v `1 ) * (u `2 )) * ((x `2 ) * (y `2 ))))) by A8, GROUP_1:def 3

      .= ((t + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) + (( - t) + ( - (((v `1 ) * (u `2 )) * ((x `2 ) * (y `2 )))))) by RLVECT_1: 31

      .= ((((((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 ))) + t) + ( - t)) + ( - (((v `1 ) * (u `2 )) * ((x `2 ) * (y `2 ))))) by RLVECT_1:def 3

      .= (((((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 ))) + (t + ( - t))) + ( - (((v `1 ) * (u `2 )) * ((x `2 ) * (y `2 ))))) by RLVECT_1:def 3

      .= (((((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 ))) + ( 0. R)) + ( - (((v `1 ) * (u `2 )) * ((x `2 ) * (y `2 ))))) by RLVECT_1: 5

      .= ((((y `1 ) * (v `2 )) * ((x `2 ) * (u `2 ))) - (((v `1 ) * (y `2 )) * ((x `2 ) * (u `2 )))) by A10, A9, GROUP_1:def 3

      .= ((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * ((x `2 ) * (u `2 ))) by VECTSP_1: 13;

      

       A12: (((z `1 ) * (w `2 )) - ((w `1 ) * (z `2 ))) = (((((x `1 ) * (y `2 )) * ((u `2 ) * (v `2 ))) + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) - ((w `1 ) * (z `2 ))) by VECTSP_1:def 7

      .= ((((((x `1 ) * (y `2 )) * (u `2 )) * (v `2 )) + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) - ((w `1 ) * (z `2 ))) by GROUP_1:def 3

      .= ((((((x `1 ) * (u `2 )) * (y `2 )) * (v `2 )) + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) - ((w `1 ) * (z `2 ))) by GROUP_1:def 3

      .= (((((x `1 ) * (u `2 )) * ((y `2 ) * (v `2 ))) + (((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 )))) - ((w `1 ) * (z `2 ))) by GROUP_1:def 3

      .= ((((((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) * ((y `2 ) * (v `2 ))) + (((u `1 ) * (x `2 )) * ((y `2 ) * (v `2 )))) + ((((y `1 ) * (x `2 )) * ((u `2 ) * (v `2 ))) - ((w `1 ) * (z `2 )))) by A7, RLVECT_1: 28

      .= (((((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) * ((y `2 ) * (v `2 ))) + ((((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) * ((x `2 ) * (u `2 )))) by A11, RLVECT_1:def 3;

      reconsider t1 = (((x `1 ) * (u `2 )) - ((u `1 ) * (x `2 ))) as Element of R;

      reconsider t2 = (((y `1 ) * (v `2 )) - ((v `1 ) * (y `2 ))) as Element of R;

      reconsider s = (s1 * s2) as Element of S by A3, A5, C0SP1:def 4;

      ((((z `1 ) * (w `2 )) - ((w `1 ) * (z `2 ))) * s) = (((t1 * ((y `2 ) * (v `2 ))) * s) + ((t2 * ((x `2 ) * (u `2 ))) * s)) by A12, VECTSP_1:def 7

      .= (((t1 * s) * ((y `2 ) * (v `2 ))) + ((t2 * ((x `2 ) * (u `2 ))) * s)) by GROUP_1:def 3

      .= (((( 0. R) * s2) * ((y `2 ) * (v `2 ))) + ((t2 * ((x `2 ) * (u `2 ))) * s)) by A4, GROUP_1:def 3

      .= ((t2 * (s1 * s2)) * ((x `2 ) * (u `2 ))) by GROUP_1:def 3

      .= ((( 0. R) * s1) * ((x `2 ) * (u `2 ))) by A6, GROUP_1:def 3

      .= ( 0. R);

      hence thesis;

    end;

    theorem :: RINGFRAC:22

    

     Th29: (((x + y) * z),((x * z) + (y * z))) Fr_Eq S

    proof

      

       A1: (((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) = ((((x `1 ) * (z `1 )) * (y `2 )) * (z `2 )) by GROUP_1:def 3

      .= ((((x `1 ) * (y `2 )) * (z `1 )) * (z `2 )) by GROUP_1:def 3

      .= (((x `1 ) * (y `2 )) * ((z `1 ) * (z `2 ))) by GROUP_1:def 3;

      (((y `1 ) * (z `1 )) * ((x `2 ) * (z `2 ))) = ((((y `1 ) * (z `1 )) * (x `2 )) * (z `2 )) by GROUP_1:def 3

      .= ((((y `1 ) * (x `2 )) * (z `1 )) * (z `2 )) by GROUP_1:def 3

      .= (((y `1 ) * (x `2 )) * ((z `1 ) * (z `2 ))) by GROUP_1:def 3;

      then

       A3: ( Fracadd (( Fracmult (x,z)),( Fracmult (y,z)))) = [((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * ((z `1 ) * (z `2 ))), (((x `2 ) * (z `2 )) * ((y `2 ) * (z `2 )))] by A1, VECTSP_1:def 7;

      ((( Fracmult (( Fracadd (x,y)),z)) `1 ) * (( Fracadd (( Fracmult (x,z)),( Fracmult (y,z)))) `2 )) = (((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * (z `1 )) * ((((z `2 ) * (x `2 )) * (y `2 )) * (z `2 ))) by GROUP_1:def 3

      .= (((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * (z `1 )) * (((z `2 ) * ((x `2 ) * (y `2 ))) * (z `2 ))) by GROUP_1:def 3

      .= ((((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * (z `1 )) * (z `2 )) * (((x `2 ) * (y `2 )) * (z `2 ))) by GROUP_1:def 3

      .= ((( Fracadd (( Fracmult (x,z)),( Fracmult (y,z)))) `1 ) * (( Fracmult (( Fracadd (x,y)),z)) `2 )) by A3, GROUP_1:def 3;

      then

       A5: ((((( Fracmult (( Fracadd (x,y)),z)) `1 ) * (( Fracadd (( Fracmult (x,z)),( Fracmult (y,z)))) `2 )) - ((( Fracadd (( Fracmult (x,z)),( Fracmult (y,z)))) `1 ) * (( Fracmult (( Fracadd (x,y)),z)) `2 ))) * ( 1. R)) = ( 0. R) by RLVECT_1: 5;

      ( 1. R) is Element of S by C0SP1:def 4;

      hence thesis by A5;

    end;

    definition

      let R, S;

      :: RINGFRAC:def16

      func 0. (R,S) -> Element of ( Frac S) equals [( 0. R), ( 1. R)];

      coherence

      proof

        ( 1. R) in S by C0SP1:def 4;

        hence thesis by Def3;

      end;

      :: RINGFRAC:def17

      func 1. (R,S) -> Element of ( Frac S) equals [( 1. R), ( 1. R)];

      coherence

      proof

        ( 1. R) in S by C0SP1:def 4;

        hence thesis by Def3;

      end;

    end

    theorem :: RINGFRAC:23

    

     Th30: for s be Element of S holds x = [s, s] implies (x,( 1. (R,S))) Fr_Eq S

    proof

      let s be Element of S;

      assume

       A1: x = [s, s];

      reconsider s1 = ( 1. R) as Element of R;

      

       A2: ((((x `1 ) * (( 1. (R,S)) `2 )) - ((( 1. (R,S)) `1 ) * (x `2 ))) * s1) = ( 0. R) by A1, RLVECT_1: 5;

      s1 in S by C0SP1:def 4;

      hence thesis by A2;

    end;

    begin

    definition

      let R, S;

      :: RINGFRAC:def18

      func FracRing (S) -> strict doubleLoopStr means

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

      existence

      proof

        set E = ( EqRel S);

        set A = ( Class E);

        set SR = ( Frac S);

        defpred P[ set, set, set] means ex P,Q be Element of SR 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 SR st $1 = ( Class (E,P)) & $2 = ( Class (E,Q)) & $3 = ( Class (E,(P * Q)));

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

        reconsider z = ( Class (( EqRel S),( 0. (R,S)))) 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 SR and

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

          consider Q be object such that

           A4: Q in SR and

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

          reconsider P, Q as Element of SR 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 SR and

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

          consider Q be object such that

           A10: Q in SR and

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

          reconsider P, Q as Element of SR 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 SR = ( Frac S);

        set E = ( EqRel S);

        set A = ( Class E);

        set SR = ( Frac S);

        let X,Y be strict doubleLoopStr such that

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

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

         A15: for x,y be Element of X holds ex a,b be Element of SR 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 SR 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,S)))) & ( 0. Y) = ( Class (E,( 0. (R,S)))) and

         A19: for x,y be Element of Y holds ex a,b be Element of SR 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 SR 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 SR 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 SR 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;

          

           A28: (b,b1) Fr_Eq S by A23, A26, Th26;

          

           A29: (a,a1) Fr_Eq S by A22, A25, Th26;

          reconsider u = (a * b) as Element of SR;

          thus thesis by A24, A27, Th26, Th27, A28, A29;

        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 SR 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 SR 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) Fr_Eq S & (b,b1) Fr_Eq S by A30, A32, Th26;

          hence thesis by A31, A33, Th26, Th28;

        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, S;

      synonym S ~ R for FracRing (S);

    end

    registration

      let R, S;

      cluster (S ~ R) -> non empty;

      coherence

      proof

        ( Class (( EqRel S),( 1. (R,S)))) in ( Class ( EqRel S)) by EQREL_1:def 3;

        hence thesis by Def6;

      end;

    end

    theorem :: RINGFRAC:24

    

     Th31: ( 0. R) in S iff (S ~ R) is degenerated

    proof

      

       A1: (S ~ R) is degenerated implies ( 0. R) in S

      proof

        assume (S ~ R) is degenerated;

        

        then ( Class (( EqRel S),( 1. (R,S)))) = ( 0. (S ~ R)) by Def6

        .= ( Class (( EqRel S),( 0. (R,S)))) by Def6;

        then (( 1. (R,S)),( 0. (R,S))) Fr_Eq S by Th26;

        then

        consider s1 be Element of R such that

         A3: s1 in S and

         A4: ((((( 1. (R,S)) `1 ) * (( 0. (R,S)) `2 )) - ((( 0. (R,S)) `1 ) * (( 1. (R,S)) `2 ))) * s1) = ( 0. R);

        thus thesis by A3, A4;

      end;

      ( 0. R) in S implies (S ~ R) is degenerated

      proof

        assume ( 0. R) in S;

        then

         A6: (( 1. (R,S)),( 0. (R,S))) Fr_Eq S;

        ( 1. (S ~ R)) = ( Class (( EqRel S),( 1. (R,S)))) by Def6

        .= ( Class (( EqRel S),( 0. (R,S)))) by A6, Th26

        .= ( 0. (S ~ R)) by Def6;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    reserve a,b,c for Element of ( Frac S);

    reserve x,y,z for Element of (S ~ R);

    theorem :: RINGFRAC:25

    

     Th32: for x holds ex a be Element of ( Frac S) st x = ( Class (( EqRel S),a))

    proof

      let x;

      the carrier of (S ~ R) = ( Class ( EqRel S)) by Def6;

      then x in ( Class ( EqRel S));

      then ex a be object st a in ( Frac S) & x = ( Class (( EqRel S),a)) by EQREL_1:def 3;

      hence thesis;

    end;

    theorem :: RINGFRAC:26

    

     Th33: x = ( Class (( EqRel S),a)) & y = ( Class (( EqRel S),b)) implies (x * y) = ( Class (( EqRel S),(a * b)))

    proof

      assume that

       A1: x = ( Class (( EqRel S),a)) and

       A2: y = ( Class (( EqRel S),b));

      consider a1,b1 be Element of ( Frac S) such that

       A3: x = ( Class (( EqRel S),a1)) and

       A4: y = ( Class (( EqRel S),b1)) and

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

      

       A6: (a1,a) Fr_Eq S by A1, A3, Th26;

      (b1,b) Fr_Eq S by A2, A4, Th26;

      hence thesis by A5, Th26, A6, Th27;

    end;

    theorem :: RINGFRAC:27

    

     Th34: (x * y) = (y * x)

    proof

      consider a such that

       A1: x = ( Class (( EqRel S),a)) by Th32;

      consider b such that

       A2: y = ( Class (( EqRel S),b)) by Th32;

      (x * y) = ( Class (( EqRel S),(a * b))) by A1, A2, Th33

      .= ( Class (( EqRel S),(b * a)))

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

      hence thesis;

    end;

    theorem :: RINGFRAC:28

    

     Th35: x = ( Class (( EqRel S),a)) & y = ( Class (( EqRel S),b)) implies (x + y) = ( Class (( EqRel S),(a + b)))

    proof

      consider a1,b1 be Element of ( Frac S) such that

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

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

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

      then (a,a1) Fr_Eq S & (b,b1) Fr_Eq S by A1, Th26;

      hence thesis by A2, Th26, Th28;

    end;

    

     Lm36: (( Fracadd ((( frac1 S) . r1),(( frac1 S) . r2))),(( frac1 S) . (r1 + r2))) Fr_Eq S

    proof

      

       A1: (( frac1 S) . r1) = [r1, ( 1. R)] by Def4;

      (( frac1 S) . r2) = [r2, ( 1. R)] by Def4;

      then ( Fracadd ((( frac1 S) . r1),(( frac1 S) . r2))) = (( frac1 S) . (r1 + r2)) by A1, Def4;

      hence thesis by Th22;

    end;

    

     Lm37: x = ( Class (( EqRel S),(( frac1 S) . r1))) & y = ( Class (( EqRel S),(( frac1 S) . r2))) implies (x + y) = ( Class (( EqRel S),(( frac1 S) . (r1 + r2))))

    proof

      reconsider rr1 = (( frac1 S) . r1), rr2 = (( frac1 S) . r2) as Element of ( Frac S);

      assume x = ( Class (( EqRel S),(( frac1 S) . r1))) & y = ( Class (( EqRel S),(( frac1 S) . r2)));

      then (x + y) = ( Class (( EqRel S),(rr1 + rr2))) by Th35;

      hence thesis by Th26, Lm36;

    end;

    

     Lm38: (( Fracmult ((( frac1 S) . r1),(( frac1 S) . r2))),(( frac1 S) . (r1 * r2))) Fr_Eq S

    proof

      

       A1: (( frac1 S) . r1) = [r1, ( 1. R)] by Def4;

      (( frac1 S) . r2) = [r2, ( 1. R)] by Def4;

      then ( Fracmult ((( frac1 S) . r1),(( frac1 S) . r2))) = (( frac1 S) . (r1 * r2)) by A1, Def4;

      hence thesis by Th22;

    end;

    

     Lm39: x = ( Class (( EqRel S),(( frac1 S) . r1))) & y = ( Class (( EqRel S),(( frac1 S) . r2))) implies (x * y) = ( Class (( EqRel S),(( frac1 S) . (r1 * r2))))

    proof

      reconsider rr1 = (( frac1 S) . r1), rr2 = (( frac1 S) . r2) as Element of ( Frac S);

      assume x = ( Class (( EqRel S),(( frac1 S) . r1))) & y = ( Class (( EqRel S),(( frac1 S) . r2)));

      then (x * y) = ( Class (( EqRel S),(rr1 * rr2))) by Th33;

      hence thesis by Th26, Lm38;

    end;

    theorem :: RINGFRAC:29

    

     Th40: (S ~ R) is Ring

    proof

      

       A1: (x + y) = (y + x)

      proof

        consider a such that

         A2: x = ( Class (( EqRel S),a)) by Th32;

        consider b such that

         A3: y = ( Class (( EqRel S),b)) by Th32;

        (x + y) = ( Class (( EqRel S),(a + b))) by A2, A3, Th35

        .= ( Class (( EqRel S),(b + a)))

        .= (y + x) by A2, A3, Th35;

        hence thesis;

      end;

      

       A4: ((x + y) + z) = (x + (y + z))

      proof

        consider a such that

         A5: x = ( Class (( EqRel S),a)) by Th32;

        consider b such that

         A6: y = ( Class (( EqRel S),b)) by Th32;

        consider c such that

         A7: z = ( Class (( EqRel S),c)) by Th32;

        

         A8: (y + z) = ( Class (( EqRel S),(b + c))) by A6, A7, Th35;

        (x + y) = ( Class (( EqRel S),(a + b))) by A5, A6, Th35;

        

        then ((x + y) + z) = ( Class (( EqRel S),((a + b) + c))) by A7, Th35

        .= ( Class (( EqRel S),(a + (b + c)))) by Th19

        .= (x + (y + z)) by A8, A5, Th35;

        hence thesis;

      end;

      

       A9: (x + ( 0. (S ~ R))) = x

      proof

        consider a such that

         A10: x = ( Class (( EqRel S),a)) by Th32;

        ( 0. (S ~ R)) = ( Class (( EqRel S),( 0. (R,S)))) by Def6;

        

        then (x + ( 0. (S ~ R))) = ( Class (( EqRel S),(a + ( 0. (R,S))))) by A10, Th35

        .= x by A10;

        hence thesis;

      end;

      

       A11: x is right_complementable

      proof

        ex y be Element of (S ~ R) st (x + y) = ( 0. (S ~ R))

        proof

          consider a,b be Element of ( Frac S) such that

           A12: x = ( Class (( EqRel S),a)) and ( 0. (S ~ R)) = ( Class (( EqRel S),b)) and (the addF of (S ~ R) . (x,( 0. (S ~ R)))) = ( Class (( EqRel S),(a + b))) by Def6;

          reconsider u1 = (a `1 ) as Element of R;

          reconsider u2 = (a `2 ) as Element of S by Lm17;

          reconsider u = [( - u1), u2] as Element of ( Frac S) by Def3;

          

           A13: (a + u) = [((u1 * u2) + ( - (u1 * u2))), (u2 * u2)] by VECTSP_1: 9

          .= [( 0. R), (u2 * u2)] by RLVECT_1: 5;

          reconsider s = ( 1. R) as Element of S by C0SP1:def 4;

          reconsider u3 = (u2 * u2) as Element of S by C0SP1:def 4;

          (((( 0. R) * ( 1. R)) - (( 0. R) * u3)) * s) = ( 0. R);

          then ((a + u),( 0. (R,S))) Fr_Eq S by A13;

          

          then

           A14: ( Class (( EqRel S),(a + u))) = ( Class (( EqRel S),( 0. (R,S)))) by Th26

          .= ( 0. (S ~ R)) by Def6;

          

           A15: the carrier of (S ~ R) = ( Class ( EqRel S)) by Def6;

          reconsider y = ( Class (( EqRel S),u)) as Element of (S ~ R) by A15, EQREL_1:def 3;

          (x + y) = ( 0. (S ~ R)) by A14, A12, Th35;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A16: ((x + y) * z) = ((x * z) + (y * z))

      proof

        consider a such that

         A17: x = ( Class (( EqRel S),a)) by Th32;

        consider b such that

         A18: y = ( Class (( EqRel S),b)) by Th32;

        consider c such that

         A19: z = ( Class (( EqRel S),c)) by Th32;

        

         A21: (x * z) = ( Class (( EqRel S),(a * c))) by A17, A19, Th33;

        

         A22: (y * z) = ( Class (( EqRel S),(b * c))) by A18, A19, Th33;

        (x + y) = ( Class (( EqRel S),(a + b))) by A17, A18, Th35;

        

        then ((x + y) * z) = ( Class (( EqRel S),((a + b) * c))) by A19, Th33

        .= ( Class (( EqRel S),((a * c) + (b * c)))) by Th29, Th26

        .= ((x * z) + (y * z)) by A21, A22, Th35;

        hence thesis;

      end;

      

       A23: (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x))

      proof

        (x * (y + z)) = ((y + z) * x) by Th34

        .= ((y * x) + (z * x)) by A16

        .= ((x * y) + (z * x)) by Th34

        .= ((x * y) + (x * z)) by Th34;

        hence thesis by A16;

      end;

      

       A25: ((x * y) * z) = (x * (y * z))

      proof

        consider a such that

         A26: x = ( Class (( EqRel S),a)) by Th32;

        consider b such that

         A27: y = ( Class (( EqRel S),b)) by Th32;

        consider c such that

         A28: z = ( Class (( EqRel S),c)) by Th32;

        

         A29: (y * z) = ( Class (( EqRel S),(b * c))) by A27, A28, Th33;

        (x * y) = ( Class (( EqRel S),(a * b))) by A26, A27, Th33;

        

        then ((x * y) * z) = ( Class (( EqRel S),((a * b) * c))) by A28, Th33

        .= ( Class (( EqRel S),(a * (b * c)))) by Th20

        .= (x * (y * z)) by A26, A29, Th33;

        hence thesis;

      end;

      (x * ( 1. (S ~ R))) = x & (( 1. (S ~ R)) * x) = x

      proof

        consider a such that

         A30: x = ( Class (( EqRel S),a)) by Th32;

        ( 1. (S ~ R)) = ( Class (( EqRel S),( 1. (R,S)))) by Def6;

        

        then (x * ( 1. (S ~ R))) = ( Class (( EqRel S),(a * ( 1. (R,S))))) by A30, Th33

        .= x by A30;

        hence thesis by Th34;

      end;

      hence thesis by A1, A4, A9, A11, A23, A25, VECTSP_1:def 6, VECTSP_1:def 7, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, ALGSTR_0:def 16;

    end;

    registration

      let R, S;

      cluster (S ~ R) -> commutative Abelian add-associative right_zeroed right_complementable associative well-unital distributive;

      coherence by Th34, Th40;

    end

    

     Lm41: ( Class (( EqRel S),a)) is Element of (S ~ R)

    proof

      the carrier of (S ~ R) = ( Class ( EqRel S)) by Def6;

      hence thesis by EQREL_1:def 3;

    end;

    

     Lm42: (a `1 ) = (a `2 ) implies ( Class (( EqRel S),a)) = ( 1. (S ~ R))

    proof

      assume

       A1: (a `1 ) = (a `2 );

      reconsider s1 = ( 1. R) as Element of S by C0SP1:def 4;

      ((((a `1 ) * (( 1. (R,S)) `2 )) - ((( 1. (R,S)) `1 ) * (a `2 ))) * s1) = ( 0. R) by A1, RLVECT_1: 5;

      then (a,( 1. (R,S))) Fr_Eq S;

      

      then ( Class (( EqRel S),a)) = ( Class (( EqRel S),( 1. (R,S)))) by Th26

      .= ( 1. (S ~ R)) by Def6;

      hence thesis;

    end;

    

     Lm43: ( Class (( EqRel S),(( frac1 S) . ( 1. R)))) = ( 1. (S ~ R))

    proof

      reconsider a = (( frac1 S) . ( 1. R)) as Element of ( Frac S);

      

       A1: (( frac1 S) . ( 1. R)) = [( 1. R), ( 1. R)] by Def4;

      (a `1 ) = (a `2 ) by A1;

      hence thesis by Lm42;

    end;

    

     Lm44: for o be object st o in the carrier of R holds ( Class (( EqRel S),(( frac1 S) . o))) in the carrier of (S ~ R)

    proof

      let o be object;

      assume o in the carrier of R;

      then

      reconsider a = (( frac1 S) . o) as Element of ( Frac S) by FUNCT_2: 5;

      ( Class (( EqRel S),a)) is Element of (S ~ R) by Lm41;

      hence thesis;

    end;

    

     Lm45: (a `1 ) in S implies ( Class (( EqRel S),a)) is Unit of (S ~ R)

    proof

      assume (a `1 ) in S;

      then

      reconsider b = [(a `2 ), (a `1 )] as Element of ( Frac S) by Def3;

      

       A2: ((a * b) `1 ) = ((a * b) `2 );

      reconsider x = ( Class (( EqRel S),a)), y = ( Class (( EqRel S),b)) as Element of (S ~ R) by Lm41;

      

       A3: (x * y) = ( Class (( EqRel S),(a * b))) by Th33

      .= ( 1. (S ~ R)) by A2, Lm42;

      

       A4: x divides ( 1. (S ~ R)) by A3;

      x is unital by A4;

      hence thesis;

    end;

    

     Lm46: for s be Element of S holds ( Class (( EqRel S), [s, ( 1. R)])) is Unit of (S ~ R)

    proof

      let s be Element of S;

      ( 1. R) in S by C0SP1:def 4;

      then

      reconsider a = [s, ( 1. R)] as Element of ( Frac S) by Def3;

      (a `1 ) in S;

      hence thesis by Lm45;

    end;

    theorem :: RINGFRAC:30

    

     Th46: for z holds ex r1,r2 be Element of R st r2 in S & z = ( Class (( EqRel S), [r1, r2]))

    proof

      let z;

      consider r be Element of ( Frac S) such that

       A1: z = ( Class (( EqRel S),r)) by Th32;

      consider r1,r2 be Element of R such that

       A2: r1 = (r `1 ) and

       A3: r2 = (r `2 );

      z = ( Class (( EqRel S), [r1, r2])) by A1, A2, A3;

      hence thesis by A3, Lm17;

    end;

    reserve S for without_zero non empty multiplicatively-closed Subset of A;

    definition

      let A, S;

      :: RINGFRAC:def19

      func canHom (S) -> Function of A, (S ~ A) means

      : Def7: for o be object st o in the carrier of A holds (it . o) = ( Class (( EqRel S),(( frac1 S) . o)));

      existence

      proof

        deffunc F( object) = ( Class (( EqRel S),(( frac1 S) . $1)));

        

         A1: for o1 be object st o1 in the carrier of A holds F(o1) in the carrier of (S ~ A) by Lm44;

        ex g be Function of A, (S ~ A) st for o2 be object st o2 in the carrier of A holds (g . o2) = F(o2) from FUNCT_2:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of A, (S ~ A) such that

         A2: for o be object st o in the carrier of A holds (f1 . o) = ( Class (( EqRel S),(( frac1 S) . o))) and

         A3: for o be object st o in the carrier of A holds (f2 . o) = ( Class (( EqRel S),(( frac1 S) . o)));

        for o1 be object st o1 in the carrier of A holds (f1 . o1) = (f2 . o1)

        proof

          let o1 be object such that

           A4: o1 in the carrier of A;

          (f1 . o1) = ( Class (( EqRel S),(( frac1 S) . o1))) by A2, A4;

          hence thesis by A3, A4;

        end;

        hence thesis;

      end;

    end

    registration

      let A, S;

      cluster ( canHom S) -> additive multiplicative unity-preserving;

      coherence

      proof

        set ER = ( EqRel S), B = (S ~ A);

        for a,b be Element of A holds (( canHom S) . (a + b)) = ((( canHom S) . a) + (( canHom S) . b)) & (( canHom S) . (a * b)) = ((( canHom S) . a) * (( canHom S) . b)) & (( canHom S) . ( 1_ A)) = ( 1_ (S ~ A))

        proof

          let a,b be Element of A;

          reconsider a1 = (( frac1 S) . a), b1 = (( frac1 S) . b), ab1 = (( frac1 S) . (a + b)), ab2 = (( frac1 S) . (a * b)), E1 = (( frac1 S) . ( 1. A)) as Element of ( Frac S);

          reconsider x = ( Class (( EqRel S),a1)), y = ( Class (( EqRel S),b1)) as Element of (S ~ A) by Lm41;

          

           A1: (( canHom S) . a) = x by Def7;

          

           A2: (( canHom S) . b) = y by Def7;

          

          then

           A3: ((( canHom S) . a) + (( canHom S) . b)) = ( Class (( EqRel S),(( frac1 S) . (a + b)))) by A1, Lm37

          .= (( canHom S) . (a + b)) by Def7;

          

           A4: ((( canHom S) . a) * (( canHom S) . b)) = ( Class (( EqRel S),(( frac1 S) . (a * b)))) by A1, A2, Lm39

          .= (( canHom S) . (a * b)) by Def7;

          (( canHom S) . ( 1. A)) = ( Class (( EqRel S),(( frac1 S) . ( 1. A)))) by Def7

          .= ( 1. (S ~ A)) by Lm43;

          hence thesis by A3, A4;

        end;

        hence thesis;

      end;

    end

    theorem :: RINGFRAC:31

    

     Lm49: for a,b be Element of A holds (( canHom S) . (a - b)) = ((( canHom S) . a) - (( canHom S) . b))

    proof

      let a,b be Element of A;

      

      thus (( canHom S) . (a - b)) = ((( canHom S) . a) + (( canHom S) . ( - b))) by VECTSP_1:def 20

      .= ((( canHom S) . a) - (( canHom S) . b)) by RING_2: 7;

    end;

    theorem :: RINGFRAC:32

    

     Lm50: not ( 0. A) in S implies ( ker ( canHom S)) c= ( ZeroDiv_Set A)

    proof

      assume

       A1: not ( 0. A) in S;

      for o st o in ( ker ( canHom S)) holds o in ( ZeroDiv_Set A)

      proof

        let o;

        assume o in ( ker ( canHom S));

        then

        consider v1 be Element of A such that

         A3: v1 = o and

         A4: (( canHom S) . v1) = ( 0. (S ~ A));

        ( 1. A) in S by C0SP1:def 4;

        then

        reconsider w = [v1, ( 1. A)] as Element of ( Frac S) by Def3;

        ( Class (( EqRel S),( 0. (A,S)))) = (( canHom S) . v1) by A4, Def6

        .= ( Class (( EqRel S),(( frac1 S) . v1))) by Def7

        .= ( Class (( EqRel S),w)) by Def4;

        then (( 0. (A,S)),w) Fr_Eq S by Th26;

        then

        consider t1 be Element of A such that

         A5: t1 in S and

         A6: ((((( 0. (A,S)) `1 ) * (w `2 )) - ((w `1 ) * (( 0. (A,S)) `2 ))) * t1) = ( 0. A);

        

         A7: ( 0. A) = ((( - ( 1. A)) * v1) * t1) by A6, VECTSP_2: 29

        .= (( - ( 1. A)) * (v1 * t1)) by GROUP_1:def 3

        .= ( - (v1 * t1)) by VECTSP_2: 29;

        

         A8: ( 0. A) = ( - ( - (v1 * t1))) by A7

        .= (v1 * t1);

        v1 is zero_divisible by A1, A5, A8;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: RINGFRAC:33

     not ( 0. A) in S & A is domRing implies ( ker ( canHom S)) = {( 0. A)} & ( canHom S) is one-to-one

    proof

      assume

       A1: not ( 0. A) in S & A is domRing;

      then

       A2: ( ker ( canHom S)) c= ( ZeroDiv_Set A) by Lm50;

      

       A3: ( ZeroDiv_Set A) = {( 0. A)} by A1, Th4;

      

       A4: (( canHom S) . ( 0. A)) = ( Class (( EqRel S),(( frac1 S) . ( 0. A)))) by Def7

      .= ( Class (( EqRel S),( 0. (A,S)))) by Def4

      .= ( 0. (S ~ A)) by Def6;

      

       A5: ( 0. A) in ( ker ( canHom S)) by A4;

      

       A6: {( 0. A)} is Subset of ( ker ( canHom S)) by A5, SUBSET_1: 33;

      for x,y be object st x in ( dom ( canHom S)) & y in ( dom ( canHom S)) & (( canHom S) . x) = (( canHom S) . y) holds x = y

      proof

        let x,y be object;

        assume

         A8: x in ( dom ( canHom S)) & y in ( dom ( canHom S)) & (( canHom S) . x) = (( canHom S) . y);

        then

        reconsider a = x, b = y as Element of A;

        

         A9: ( 0. (S ~ A)) = ((( canHom S) . a) - (( canHom S) . b)) by A8, RLVECT_1: 15

        .= (( canHom S) . (a - b)) by Lm49;

        

         A10: (a - b) in ( ker ( canHom S)) by A9;

        

         A11: ( 0. A) = (a + ( - b)) by A2, A3, A10, TARSKI:def 1;

        a = ( - ( - b)) by A11, RLVECT_1: 6

        .= b;

        hence thesis;

      end;

      hence thesis by A2, A3, A6, XBOOLE_0:def 10;

    end;

    begin

    reserve p for Element of ( Spectrum A);

    definition

      let A, p;

      :: RINGFRAC:def20

      func Loc (A,p) -> Subset of A equals (( [#] A) \ p);

      coherence ;

    end

    

     Th52: ( 1. A) in ( Loc (A,p))

    proof

      reconsider p as prime Ideal of A by Lm5;

       not ( 1. A) in p by IDEAL_1: 19;

      hence thesis by XBOOLE_0:def 5;

    end;

    registration

      let A, p;

      cluster ( Loc (A,p)) -> non empty;

      coherence by Th52;

      cluster ( Loc (A,p)) -> multiplicatively-closed;

      coherence by Th6;

      cluster ( Loc (A,p)) -> without_zero;

      coherence

      proof

        reconsider p as prime Ideal of A by Lm5;

        ( 0. A) in p by IDEAL_1: 3;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    definition

      let A, p;

      :: RINGFRAC:def21

      func A ~ p -> Ring equals (( Loc (A,p)) ~ A);

      correctness ;

    end

    registration

      let A, p;

      cluster (A ~ p) -> non degenerated;

      coherence

      proof

        reconsider p as prime Ideal of A by Lm5;

        ( 0. A) in p by IDEAL_1: 3;

        then not ( 0. A) in (( [#] A) \ p) by XBOOLE_0:def 5;

        hence thesis by Th31;

      end;

      cluster (A ~ p) -> commutative;

      coherence ;

    end

    definition

      let A, p;

      :: RINGFRAC:def22

      func Loc-Ideal (p) -> Subset of ( [#] (A ~ p)) equals { y where y be Element of (A ~ p) : ex a be Element of ( Frac ( Loc (A,p))) st a in [:p, ( Loc (A,p)):] & y = ( Class (( EqRel ( Loc (A,p))),a)) };

      coherence

      proof

        set C = { y where y be Element of (A ~ p) : ex a be Element of ( Frac ( Loc (A,p))) st a in [:p, ( Loc (A,p)):] & y = ( Class (( EqRel ( Loc (A,p))),a)) };

        for x be object holds x in C implies x in ( [#] (A ~ p))

        proof

          let x be object;

          assume x in C;

          then

          consider y1 be Element of (A ~ p) such that

           A2: y1 = x and ex a be Element of ( Frac ( Loc (A,p))) st a in [:p, ( Loc (A,p)):] & y1 = ( Class (( EqRel ( Loc (A,p))),a));

          thus thesis by A2;

        end;

        then C c= ( [#] (A ~ p));

        hence thesis;

      end;

    end

    registration

      let A, p;

      cluster ( Loc-Ideal p) -> non empty;

      coherence

      proof

        p is prime Ideal of A by Lm5;

        then

         A1: ( 0. A) in p by IDEAL_1: 2;

        

         A2: ( 1. A) in ( Loc (A,p)) by Th52;

        then

        reconsider a = [( 0. A), ( 1. A)] as Element of ( Frac ( Loc (A,p))) by Def3;

        

         A3: a in [:p, ( Loc (A,p)):] by A1, A2, ZFMISC_1: 87;

        reconsider y = ( Class (( EqRel ( Loc (A,p))),a)) as Element of (A ~ p) by Lm41;

        y in ( Loc-Ideal p) by A3;

        hence thesis;

      end;

    end

    reserve a,m,n for Element of (A ~ p);

    theorem :: RINGFRAC:34

    

     Th53: ( Loc-Ideal p) is proper Ideal of (A ~ p)

    proof

      reconsider M = ( Loc-Ideal p) as Subset of (A ~ p);

      

       A1: for m,n be Element of (A ~ p) st m in M & n in M holds (m + n) in M

      proof

        let m,n be Element of (A ~ p);

        assume that

         A2: m in M and

         A3: n in M;

        consider y1 be Element of (A ~ p) such that

         A4: y1 = m and

         A5: ex a be Element of ( Frac ( Loc (A,p))) st a in [:p, ( Loc (A,p)):] & y1 = ( Class (( EqRel ( Loc (A,p))),a)) by A2;

        consider y2 be Element of (A ~ p) such that

         A6: y2 = n and

         A7: ex a be Element of ( Frac ( Loc (A,p))) st a in [:p, ( Loc (A,p)):] & y2 = ( Class (( EqRel ( Loc (A,p))),a)) by A3;

        consider a1 be Element of ( Frac ( Loc (A,p))) such that

         A8: a1 in [:p, ( Loc (A,p)):] and

         A9: y1 = ( Class (( EqRel ( Loc (A,p))),a1)) by A5;

        consider a2 be Element of ( Frac ( Loc (A,p))) such that

         A10: a2 in [:p, ( Loc (A,p)):] and

         A11: y2 = ( Class (( EqRel ( Loc (A,p))),a2)) by A7;

        

         A12: (a1 `1 ) in p & (a2 `1 ) in p by A8, A10, MCART_1: 10;

        (a1 `2 ) in ( Loc (A,p)) & (a2 `2 ) in ( Loc (A,p)) by A8, A10, MCART_1: 10;

        then

         A17: ((a1 `2 ) * (a2 `2 )) in ( Loc (A,p)) by C0SP1:def 4;

        

         A14: p is prime Ideal of A by Lm5;

        then

         A15: ((a1 `1 ) * (a2 `2 )) in p by A12, IDEAL_1:def 3;

        ((a2 `1 ) * (a1 `2 )) in p by A12, A14, IDEAL_1:def 2;

        then

         A16: (((a1 `1 ) * (a2 `2 )) + ((a2 `1 ) * (a1 `2 ))) in p by A14, A15, IDEAL_1:def 1;

        reconsider a3 = (a1 + a2) as Element of ( Frac ( Loc (A,p)));

        

         A18: a3 in [:p, ( Loc (A,p)):] by A16, A17, ZFMISC_1: 87;

        reconsider y3 = (y1 + y2) as Element of (A ~ p);

        y3 = ( Class (( EqRel ( Loc (A,p))),a3)) by A9, A11, Th35;

        hence thesis by A4, A6, A18;

      end;

      for x,m be Element of (A ~ p) st m in M holds (x * m) in M

      proof

        let x,m be Element of (A ~ p);

        assume m in M;

        then

        consider y1 be Element of (A ~ p) such that

         A20: y1 = m and

         A21: ex a be Element of ( Frac ( Loc (A,p))) st a in [:p, ( Loc (A,p)):] & y1 = ( Class (( EqRel ( Loc (A,p))),a));

        consider a1 be Element of ( Frac ( Loc (A,p))) such that

         A22: a1 in [:p, ( Loc (A,p)):] and

         A23: y1 = ( Class (( EqRel ( Loc (A,p))),a1)) by A21;

        consider b be Element of ( Frac ( Loc (A,p))) such that

         A24: x = ( Class (( EqRel ( Loc (A,p))),b)) by Th32;

        

         A25: (a1 `1 ) in p & (a1 `2 ) in ( Loc (A,p)) by A22, MCART_1: 10;

        b in ( Frac ( Loc (A,p)));

        then b in [:( [#] A), ( Loc (A,p)):] by Th15;

        then (b `1 ) in ( [#] A) & (b `2 ) in ( Loc (A,p)) by MCART_1: 10;

        then

         A28: ((b `2 ) * (a1 `2 )) in ( Loc (A,p)) by A25, C0SP1:def 4;

        reconsider ba1 = (b * a1) as Element of ( Frac ( Loc (A,p)));

        p is prime Ideal of A by Lm5;

        then ((b `1 ) * (a1 `1 )) in p by A22, MCART_1: 10, IDEAL_1:def 2;

        then

         A29: ba1 in [:p, ( Loc (A,p)):] by A28, ZFMISC_1: 87;

        reconsider xy = (x * y1) as Element of (A ~ p);

        xy = ( Class (( EqRel ( Loc (A,p))),ba1)) by A23, A24, Th33;

        hence thesis by A20, A29;

      end;

      then

       A31: M is left-ideal by IDEAL_1:def 2;

      M is proper

      proof

        assume not M is proper;

        then ( 1. (A ~ p)) in M by A31, IDEAL_1: 19;

        then

        consider y1 be Element of (A ~ p) such that

         A34: y1 = ( 1. (A ~ p)) and

         A35: ex a be Element of ( Frac ( Loc (A,p))) st a in [:p, ( Loc (A,p)):] & y1 = ( Class (( EqRel ( Loc (A,p))),a));

        consider a be Element of ( Frac ( Loc (A,p))) such that

         A36: a in [:p, ( Loc (A,p)):] and

         A37: y1 = ( Class (( EqRel ( Loc (A,p))),a)) by A35;

        

         A38: (( frac1 ( Loc (A,p))) . ( 1. A)) = [( 1. A), ( 1. A)] by Def4;

        ( Class (( EqRel ( Loc (A,p))),a)) = ( Class (( EqRel ( Loc (A,p))),(( frac1 ( Loc (A,p))) . ( 1. A)))) by A34, A37, Lm43;

        then

         A39: (a,(( frac1 ( Loc (A,p))) . ( 1. A))) Fr_Eq ( Loc (A,p)) by Th26;

        reconsider y = (( frac1 ( Loc (A,p))) . ( 1. A)) as Element of ( Frac ( Loc (A,p)));

        consider s1 be Element of A such that

         A40: s1 in ( Loc (A,p)) and

         A41: ((((a `1 ) * (y `2 )) - ((y `1 ) * (a `2 ))) * s1) = ( 0. A) by A39;

        ( 0. A) = (((a `1 ) * s1) - ((a `2 ) * s1)) by A38, A41, VECTSP_1: 13;

        then

         A42: ((a `1 ) * s1) = ((a `2 ) * s1) by VECTSP_1: 27;

        

         A43: (a `1 ) in p & (a `2 ) in ( Loc (A,p)) by A36, MCART_1: 10;

        p is prime Ideal of A by Lm5;

        then

         A44: ((a `1 ) * s1) in p by A36, MCART_1: 10, IDEAL_1:def 2;

        ((a `2 ) * s1) in ( Loc (A,p)) by A40, A43, C0SP1:def 4;

        hence contradiction by A42, A44, XBOOLE_0:def 5;

      end;

      hence thesis by A1, A31, IDEAL_1:def 1;

    end;

    theorem :: RINGFRAC:35

    

     Th54: for x be object holds x in (( [#] (A ~ p)) \ ( Loc-Ideal p)) implies x is Unit of (A ~ p)

    proof

      let x be object;

      assume

       A1: x in (( [#] (A ~ p)) \ ( Loc-Ideal p));

      then

      consider a be Element of ( Frac ( Loc (A,p))) such that

       A2: x = ( Class (( EqRel ( Loc (A,p))),a)) by Th32;

      a in ( Frac ( Loc (A,p)));

      then a in [:( [#] A), ( Loc (A,p)):] by Th15;

      then

       A3: (a `1 ) in ( [#] A) & (a `2 ) in ( Loc (A,p)) by MCART_1: 10;

      per cases ;

        suppose

         A4: (a `1 ) in (( [#] A) \ p);

        reconsider b = [(a `1 ), (a `2 )] as Element of ( Frac ( Loc (A,p)));

        thus thesis by A4, A2, Lm45;

      end;

        suppose not (a `1 ) in (( [#] A) \ p);

        then

         A7: (a `1 ) in p by XBOOLE_0:def 5;

        reconsider b = [(a `1 ), (a `2 )] as Element of ( Frac ( Loc (A,p)));

        reconsider y = x as Element of (A ~ p) by A1;

        

         A8: b in [:p, ( Loc (A,p)):] by A3, A7, ZFMISC_1: 87;

        y = ( Class (( EqRel ( Loc (A,p))),b)) by A2;

        then x in ( Loc-Ideal p) by A8;

        hence thesis by A1, XBOOLE_0:def 5;

      end;

    end;

    theorem :: RINGFRAC:36

    (A ~ p) is local & ( Loc-Ideal p) is maximal Ideal of (A ~ p)

    proof

      reconsider J = ( Loc-Ideal p) as proper Ideal of (A ~ p) by Th53;

      

       A1: (A ~ p) is local

      proof

        (for x be object holds x in (( [#] (A ~ p)) \ J) implies x is Unit of (A ~ p)) implies (A ~ p) is local by TOPZARI1: 13;

        hence thesis by Th54;

      end;

      J is maximal Ideal of (A ~ p)

      proof

        consider m be maximal Ideal of (A ~ p) such that

         A3: J c= m by TOPZARI1: 8;

        o in m implies o in J

        proof

          assume

           A4: o in m;

          then

           A5: o is NonUnit of (A ~ p) by TOPZARI1: 11;

          per cases ;

            suppose o in (m \ J);

            then

             A7: o in m & not o in J by XBOOLE_0:def 5;

            o in (( [#] (A ~ p)) \ J) by A7, XBOOLE_0:def 5;

            hence thesis by A5, Th54;

          end;

            suppose not o in (m \ J);

            hence thesis by A4, XBOOLE_0:def 5;

          end;

        end;

        then m c= J;

        hence thesis by A3, XBOOLE_0:def 10;

      end;

      hence thesis by A1;

    end;

    begin

    reserve f for Function of A, B;

    theorem :: RINGFRAC:37

    

     Th56: for s be Element of S holds f is RingHomomorphism & (f .: S) c= ( Unit_Set B) implies (f . s) is Unit of B

    proof

      let s be Element of S;

      assume

       A1: f is RingHomomorphism & (f .: S) c= ( Unit_Set B);

      

       A2: ( dom f) = the carrier of A by FUNCT_2:def 1;

      reconsider t = (f . s) as object;

      t in (f .: S) by A2, FUNCT_1:def 6;

      then ( 1. B) = ((f . s) * ((f . s) ["] )) by A1, Def2;

      then (f . s) divides ( 1. B);

      then (f . s) is unital;

      hence thesis;

    end;

    definition

      let A, B, S, f;

      assume

       A1: f is RingHomomorphism & (f .: S) c= ( Unit_Set B);

      :: RINGFRAC:def23

      func Univ_Map (S,f) -> Function of (S ~ A), B means

      : Def8: for x be object st x in the carrier of (S ~ A) holds ex a,s be Element of A st s in S & x = ( Class (( EqRel S), [a, s])) & (it . x) = ((f . a) * ((f . s) ["] ));

      existence

      proof

        defpred P[ object, object] means ex a,s be Element of A st s in S & $1 = ( Class (( EqRel S), [a, s])) & $2 = ((f . a) * ((f . s) ["] ));

        

         A2: for x be object st x in the carrier of (S ~ A) holds ex y be object st y in the carrier of B & P[x, y]

        proof

          let x be object;

          assume x in the carrier of (S ~ A);

          then

          reconsider z = x as Element of (S ~ A);

          consider a,s be Element of A such that

           A4: s in S and

           A5: z = ( Class (( EqRel S), [a, s])) by Th46;

          reconsider y = ((f . a) * ((f . s) ["] )) as Element of B;

           P[x, y] by A4, A5;

          hence thesis;

        end;

        ex g be Function of (S ~ A), B st for x be object st x in the carrier of (S ~ A) holds P[x, (g . x)] from FUNCT_2:sch 1( A2);

        then

        consider g be Function of (S ~ A), B such that

         A6: for x be object st x in the carrier of (S ~ A) holds ex a,s be Element of A st s in S & x = ( Class (( EqRel S), [a, s])) & (g . x) = ((f . a) * ((f . s) ["] ));

        take g;

        thus thesis by A6;

      end;

      uniqueness

      proof

        let g1,g2 be Function of (S ~ A), B such that

         A7: for x be object st x in the carrier of (S ~ A) holds ex a1,s1 be Element of A st s1 in S & x = ( Class (( EqRel S), [a1, s1])) & (g1 . x) = ((f . a1) * ((f . s1) ["] )) and

         A8: for x be object st x in the carrier of (S ~ A) holds ex a2,s2 be Element of A st s2 in S & x = ( Class (( EqRel S), [a2, s2])) & (g2 . x) = ((f . a2) * ((f . s2) ["] ));

        

         A9: ( dom g1) = the carrier of (S ~ A) by FUNCT_2:def 1

        .= ( dom g2) by FUNCT_2:def 1;

        now

          let x be object;

          assume

           A10: x in ( dom g1);

          then

          consider a1,s1 be Element of A such that

           A11: s1 in S and

           A12: x = ( Class (( EqRel S), [a1, s1])) and

           A13: (g1 . x) = ((f . a1) * ((f . s1) ["] )) by A7;

          consider a2,s2 be Element of A such that

           A14: s2 in S and

           A15: x = ( Class (( EqRel S), [a2, s2])) and

           A16: (g2 . x) = ((f . a2) * ((f . s2) ["] )) by A8, A10;

          reconsider as1 = [a1, s1] as Element of ( Frac S) by A11, Def3;

          reconsider as2 = [a2, s2] as Element of ( Frac S) by A14, Def3;

          (as1,as2) Fr_Eq S by A15, A12, Th26;

          then

          consider s3 be Element of A such that

           A18: s3 in S and

           A19: ((((as1 `1 ) * (as2 `2 )) - ((as2 `1 ) * (as1 `2 ))) * s3) = ( 0. A);

          

           A20: f is multiplicative by A1;

          

           A21: ( 0. B) = (f . ( 0. A)) by A1, QUOFIELD: 50

          .= ((f . ((a1 * s2) - (a2 * s1))) * (f . s3)) by A19, A20;

          (f . s3) is Unit of B by A1, Th56, A18;

          then

           A22: (f . s3) in ( Unit_Set B);

          

           A23: ( 0. B) = (((f . ((a1 * s2) - (a2 * s1))) * (f . s3)) * ((f . s3) ["] )) by A21

          .= ((f . ((a1 * s2) - (a2 * s1))) * ((f . s3) * ((f . s3) ["] ))) by GROUP_1:def 3

          .= ((f . ((a1 * s2) - (a2 * s1))) * ( 1. B)) by A22, Def2

          .= ((f . (a1 * s2)) - (f . (a2 * s1))) by A1, RING_2: 8;

          (f . s1) is Unit of B by A1, A11, Th56;

          then

           A24: (f . s1) in ( Unit_Set B);

          (f . s2) is Unit of B by A1, A14, Th56;

          then

           A26: (f . s2) in ( Unit_Set B);

          reconsider fa1 = (f . a1), fa2 = (f . a2) as Element of B;

          reconsider fs1 = (f . s1), fs2 = (f . s2) as Element of B;

          

           A27: ((f . a1) * (f . s2)) = (f . (a1 * s2)) by A20

          .= (f . (a2 * s1)) by A23, VECTSP_1: 27

          .= ((f . a2) * (f . s1)) by A20;

          ((fa1 * fs2) * (fs2 ["] )) = (fa1 * (fs2 * (fs2 ["] ))) by GROUP_1:def 3

          .= (fa1 * ( 1. B)) by Def2, A26

          .= fa1;

          

          then (g1 . x) = (((fa2 * (fs2 ["] )) * fs1) * (fs1 ["] )) by A27, A13, GROUP_1:def 3

          .= ((fa2 * (fs2 ["] )) * (fs1 * (fs1 ["] ))) by GROUP_1:def 3

          .= ((fa2 * (fs2 ["] )) * ( 1. B)) by A24, Def2

          .= (g2 . x) by A16;

          hence (g1 . x) = (g2 . x);

        end;

        hence thesis by A9;

      end;

    end

    theorem :: RINGFRAC:38

    

     Th57: f is RingHomomorphism & (f .: S) c= ( Unit_Set B) implies ( Univ_Map (S,f)) is additive

    proof

      set F = ( Univ_Map (S,f));

      assume

       A1: f is RingHomomorphism & (f .: S) c= ( Unit_Set B);

      for x,y be Element of (S ~ A) holds (( Univ_Map (S,f)) . (x + y)) = ((( Univ_Map (S,f)) . x) + (( Univ_Map (S,f)) . y))

      proof

        let x,y be Element of (S ~ A);

        consider a1,s1 be Element of A such that

         A3: s1 in S and

         A4: x = ( Class (( EqRel S), [a1, s1])) and

         A5: (F . x) = ((f . a1) * ((f . s1) ["] )) by A1, Def8;

        consider a2,s2 be Element of A such that

         A6: s2 in S and

         A7: y = ( Class (( EqRel S), [a2, s2])) and

         A8: (F . y) = ((f . a2) * ((f . s2) ["] )) by A1, Def8;

        reconsider as1 = [a1, s1] as Element of ( Frac S) by A3, Def3;

        reconsider as2 = [a2, s2] as Element of ( Frac S) by A6, Def3;

        reconsider z = (x + y) as Element of (S ~ A);

        consider a3,s3 be Element of A such that

         A9: s3 in S and

         A10: z = ( Class (( EqRel S), [a3, s3])) and

         A11: (F . z) = ((f . a3) * ((f . s3) ["] )) by A1, Def8;

        reconsider as3 = [a3, s3] as Element of ( Frac S) by A9, Def3;

        ( Class (( EqRel S),as3)) = ( Class (( EqRel S),(as1 + as2))) by Th35, A4, A7, A10;

        then (as3,(as1 + as2)) Fr_Eq S by Th26;

        then

        consider s0 be Element of A such that

         A14: s0 in S and

         A15: ((((as3 `1 ) * ((as1 + as2) `2 )) - (((as1 + as2) `1 ) * (as3 `2 ))) * s0) = ( 0. A);

        

         A16: ( 0. B) = (f . ( 0. A)) by A1, QUOFIELD: 50

        .= ((f . ((a3 * (s1 * s2)) - (((a1 * s2) + (a2 * s1)) * s3))) * (f . s0)) by A1, A15, GROUP_6:def 6;

        (f . s0) is Unit of B by A1, A14, Th56;

        then

         A17: (f . s0) in ( Unit_Set B);

        (f . s1) is Unit of B by A1, A3, Th56;

        then

         A18: (f . s1) in ( Unit_Set B);

        (f . s2) is Unit of B by A1, A6, Th56;

        then

         A19: (f . s2) in ( Unit_Set B);

        (f . s3) is Unit of B by A1, A9, Th56;

        then

         A20: (f . s3) in ( Unit_Set B);

        

         A21: ( 0. B) = (((f . ((a3 * (s1 * s2)) - (((a1 * s2) + (a2 * s1)) * s3))) * (f . s0)) * ((f . s0) ["] )) by A16

        .= ((f . ((a3 * (s1 * s2)) - (((a1 * s2) + (a2 * s1)) * s3))) * ((f . s0) * ((f . s0) ["] ))) by GROUP_1:def 3

        .= ((f . ((a3 * (s1 * s2)) - (((a1 * s2) + (a2 * s1)) * s3))) * ( 1. B)) by A17, Def2

        .= ((f . (a3 * (s1 * s2))) - (f . (((a1 * s2) + (a2 * s1)) * s3))) by A1, RING_2: 8;

        ((f . a3) * ((f . s1) * (f . s2))) = ((f . a3) * (f . (s1 * s2))) by A1, GROUP_6:def 6

        .= (f . (a3 * (s1 * s2))) by A1, GROUP_6:def 6

        .= (f . (((a1 * s2) + (a2 * s1)) * s3)) by A21, VECTSP_1: 27

        .= ((f . ((a1 * s2) + (a2 * s1))) * (f . s3)) by A1, GROUP_6:def 6;

        

        then

         A23: (((f . a3) * ((f . s3) ["] )) * ((f . s1) * (f . s2))) = (((f . ((a1 * s2) + (a2 * s1))) * (f . s3)) * ((f . s3) ["] )) by GROUP_1:def 3

        .= ((f . ((a1 * s2) + (a2 * s1))) * ((f . s3) * ((f . s3) ["] ))) by GROUP_1:def 3

        .= ((f . ((a1 * s2) + (a2 * s1))) * ( 1. B)) by A20, Def2

        .= ((f . (a1 * s2)) + (f . (a2 * s1))) by A1, VECTSP_1:def 20;

        reconsider fa1 = (f . a1), fa2 = (f . a2), fa3 = (f . a3) as Element of B;

        reconsider fs1 = (f . s1), fs2 = (f . s2), fs3 = (f . s3) as Element of B;

        

         A24: ((fa3 * (fs3 ["] )) * fs1) = (((fa3 * (fs3 ["] )) * fs1) * ( 1. B))

        .= (((fa3 * (fs3 ["] )) * fs1) * (fs2 * (fs2 ["] ))) by A19, Def2

        .= ((((fa3 * (fs3 ["] )) * fs1) * fs2) * (fs2 ["] )) by GROUP_1:def 3

        .= (((f . (a1 * s2)) + (f . (a2 * s1))) * ((f . s2) ["] )) by A23, GROUP_1:def 3

        .= ((((f . a1) * (f . s2)) + (f . (a2 * s1))) * ((f . s2) ["] )) by A1, GROUP_6:def 6

        .= (((fa1 * fs2) + (fa2 * fs1)) * (fs2 ["] )) by A1, GROUP_6:def 6

        .= (((fa1 * fs2) * (fs2 ["] )) + ((fa2 * fs1) * (fs2 ["] ))) by VECTSP_1:def 3

        .= ((fa1 * (fs2 * (fs2 ["] ))) + ((fa2 * fs1) * (fs2 ["] ))) by GROUP_1:def 3

        .= ((fa1 * ( 1. B)) + ((fa2 * fs1) * (fs2 ["] ))) by A19, Def2

        .= (fa1 + ((fa2 * (fs2 ["] )) * fs1)) by GROUP_1:def 3;

        (( Univ_Map (S,f)) . (x + y)) = ((fa3 * (fs3 ["] )) * ( 1. B)) by A11

        .= ((fa3 * (fs3 ["] )) * (fs1 * (fs1 ["] ))) by A18, Def2

        .= ((fa1 + ((fa2 * (fs2 ["] )) * fs1)) * (fs1 ["] )) by A24, GROUP_1:def 3

        .= ((fa1 * (fs1 ["] )) + (((fa2 * (fs2 ["] )) * fs1) * (fs1 ["] ))) by VECTSP_1:def 3

        .= ((fa1 * (fs1 ["] )) + ((fa2 * (fs2 ["] )) * (fs1 * (fs1 ["] )))) by GROUP_1:def 3

        .= ((fa1 * (fs1 ["] )) + ((fa2 * (fs2 ["] )) * ( 1. B))) by A18, Def2

        .= ((( Univ_Map (S,f)) . x) + (( Univ_Map (S,f)) . y)) by A5, A8;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: RINGFRAC:39

    

     Th58: f is RingHomomorphism & (f .: S) c= ( Unit_Set B) implies ( Univ_Map (S,f)) is multiplicative

    proof

      set F = ( Univ_Map (S,f));

      assume

       A1: f is RingHomomorphism & (f .: S) c= ( Unit_Set B);

      for x,y be Element of (S ~ A) holds (( Univ_Map (S,f)) . (x * y)) = ((( Univ_Map (S,f)) . x) * (( Univ_Map (S,f)) . y))

      proof

        let x,y be Element of (S ~ A);

        consider a1,s1 be Element of A such that

         A3: s1 in S and

         A4: x = ( Class (( EqRel S), [a1, s1])) and

         A5: (F . x) = ((f . a1) * ((f . s1) ["] )) by A1, Def8;

        consider a2,s2 be Element of A such that

         A6: s2 in S and

         A7: y = ( Class (( EqRel S), [a2, s2])) and

         A8: (F . y) = ((f . a2) * ((f . s2) ["] )) by A1, Def8;

        reconsider as1 = [a1, s1] as Element of ( Frac S) by A3, Def3;

        reconsider as2 = [a2, s2] as Element of ( Frac S) by A6, Def3;

        reconsider z = (x * y) as Element of (S ~ A);

        consider a3,s3 be Element of A such that

         A9: s3 in S and

         A10: z = ( Class (( EqRel S), [a3, s3])) and

         A11: (F . z) = ((f . a3) * ((f . s3) ["] )) by A1, Def8;

        reconsider as3 = [a3, s3] as Element of ( Frac S) by A9, Def3;

        ( Class (( EqRel S),as3)) = ( Class (( EqRel S),(as1 * as2))) by Th33, A4, A7, A10;

        then (as3,(as1 * as2)) Fr_Eq S by Th26;

        then

        consider s0 be Element of A such that

         A14: s0 in S and

         A15: ((((as3 `1 ) * ((as1 * as2) `2 )) - (((as1 * as2) `1 ) * (as3 `2 ))) * s0) = ( 0. A);

        

         A16: ( 0. B) = (f . ( 0. A)) by A1, QUOFIELD: 50

        .= ((f . ((a3 * (s1 * s2)) - ((a1 * a2) * s3))) * (f . s0)) by A15, A1, GROUP_6:def 6;

        (f . s0) is Unit of B by A1, A14, Th56;

        then

         A17: (f . s0) in ( Unit_Set B);

        (f . s1) is Unit of B by A1, A3, Th56;

        then

         A18: (f . s1) in ( Unit_Set B) & (f . s1) is unital Element of B;

        (f . s2) is Unit of B by A1, A6, Th56;

        then

         A19: (f . s2) in ( Unit_Set B) & (f . s2) is unital Element of B;

        (f . s3) is Unit of B by A1, A9, Th56;

        then

         A20: (f . s3) in ( Unit_Set B);

        (s1 * s2) is Element of S by A3, A6, C0SP1:def 4;

        then (f . (s1 * s2)) is Unit of B by A1, Th56;

        then

         A21: (f . (s1 * s2)) in ( Unit_Set B);

        

         A22: ((f . (s1 * s2)) * (((f . s2) ["] ) * ((f . s1) ["] ))) = (((f . s1) * (f . s2)) * (((f . s2) ["] ) * ((f . s1) ["] ))) by A1, GROUP_6:def 6

        .= ((((f . s1) * (f . s2)) * ((f . s2) ["] )) * ((f . s1) ["] )) by GROUP_1:def 3

        .= (((f . s1) * ((f . s2) * ((f . s2) ["] ))) * ((f . s1) ["] )) by GROUP_1:def 3

        .= (((f . s1) * ( 1. B)) * ((f . s1) ["] )) by A19, Def2

        .= ( 1. B) by A18, Def2;

        

         A23: ( 0. B) = (((f . ((a3 * (s1 * s2)) - ((a1 * a2) * s3))) * (f . s0)) * ((f . s0) ["] )) by A16

        .= ((f . ((a3 * (s1 * s2)) - ((a1 * a2) * s3))) * ((f . s0) * ((f . s0) ["] ))) by GROUP_1:def 3

        .= ((f . ((a3 * (s1 * s2)) - ((a1 * a2) * s3))) * ( 1. B)) by A17, Def2

        .= ((f . (a3 * (s1 * s2))) - (f . ((a1 * a2) * s3))) by A1, RING_2: 8;

        

         A24: ((f . a3) * (f . (s1 * s2))) = (f . (a3 * (s1 * s2))) by A1, GROUP_6:def 6

        .= (f . ((a1 * a2) * s3)) by A23, VECTSP_1: 27

        .= ((f . (a1 * a2)) * (f . s3)) by A1, GROUP_6:def 6;

        

         A25: (((f . a3) * ((f . s3) ["] )) * (f . (s1 * s2))) = (((f . a3) * (f . (s1 * s2))) * ((f . s3) ["] )) by GROUP_1:def 3

        .= ((f . (a1 * a2)) * ((f . s3) * ((f . s3) ["] ))) by A24, GROUP_1:def 3

        .= ((f . (a1 * a2)) * ( 1. B)) by A20, Def2

        .= ((f . a1) * (f . a2)) by A1, GROUP_6:def 6;

        

         A26: ((f . (s1 * s2)) ["] ) = (((f . (s1 * s2)) ["] ) * ((f . (s1 * s2)) * (((f . s2) ["] ) * ((f . s1) ["] )))) by A22

        .= ((((f . (s1 * s2)) ["] ) * (f . (s1 * s2))) * (((f . s2) ["] ) * ((f . s1) ["] ))) by GROUP_1:def 3

        .= (( 1. B) * (((f . s2) ["] ) * ((f . s1) ["] ))) by A21, Def2

        .= (((f . s2) ["] ) * ((f . s1) ["] ));

        reconsider fa1 = (f . a1), fa2 = (f . a2), fa3 = (f . a3) as Element of B;

        reconsider fs1 = (f . s1), fs2 = (f . s2), fs3 = (f . s3) as Element of B;

        reconsider fs1s2 = (f . (s1 * s2)) as Element of B;

        (( Univ_Map (S,f)) . (x * y)) = ((fa3 * (fs3 ["] )) * ( 1. B)) by A11

        .= ((fa3 * (fs3 ["] )) * (fs1s2 * (fs1s2 ["] ))) by A21, Def2

        .= ((fa1 * fa2) * ((fs2 ["] ) * (fs1 ["] ))) by A26, A25, GROUP_1:def 3

        .= (((fa1 * fa2) * (fs1 ["] )) * (fs2 ["] )) by GROUP_1:def 3

        .= (((fa1 * (fs1 ["] )) * fa2) * (fs2 ["] )) by GROUP_1:def 3

        .= ((( Univ_Map (S,f)) . x) * (( Univ_Map (S,f)) . y)) by A5, A8, GROUP_1:def 3;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: RINGFRAC:40

    

     Th59: f is RingHomomorphism & (f .: S) c= ( Unit_Set B) implies ( Univ_Map (S,f)) is unity-preserving

    proof

      set F = ( Univ_Map (S,f));

      assume

       A1: f is RingHomomorphism & (f .: S) c= ( Unit_Set B);

      (( Univ_Map (S,f)) . ( 1. (S ~ A))) = ( 1. B)

      proof

        consider a1,s1 be Element of A such that

         A3: s1 in S and

         A4: ( 1. (S ~ A)) = ( Class (( EqRel S), [a1, s1])) and

         A5: (F . ( 1. (S ~ A))) = ((f . a1) * ((f . s1) ["] )) by A1, Def8;

        reconsider as1 = [a1, s1] as Element of ( Frac S) by A3, Def3;

        ( Class (( EqRel S),( 1. (A,S)))) = ( Class (( EqRel S),as1)) by A4, Def6;

        then

         A6: (as1,( 1. (A,S))) Fr_Eq S by Th26;

        consider s0 be Element of A such that

         A7: s0 in S and

         A8: ((((as1 `1 ) * (( 1. (A,S)) `2 )) - ((( 1. (A,S)) `1 ) * (as1 `2 ))) * s0) = ( 0. A) by A6;

        

         A9: ( 0. B) = (f . ( 0. A)) by A1, QUOFIELD: 50

        .= ((f . (a1 - s1)) * (f . s0)) by A1, A8, GROUP_6:def 6;

        (f . s0) is Unit of B by A1, A7, Th56;

        then

         A10: (f . s0) in ( Unit_Set B);

        

         A11: ( 0. B) = (((f . (a1 - s1)) * (f . s0)) * ((f . s0) ["] )) by A9

        .= ((f . (a1 - s1)) * ((f . s0) * ((f . s0) ["] ))) by GROUP_1:def 3

        .= ((f . (a1 - s1)) * ( 1. B)) by A10, Def2

        .= ((f . a1) - (f . s1)) by A1, RING_2: 8;

        (f . s1) is Unit of B by A1, A3, Th56;

        then

         A12: (f . s1) in ( Unit_Set B);

        (( Univ_Map (S,f)) . ( 1. (S ~ A))) = ((f . s1) * ((f . s1) ["] )) by A5, A11, VECTSP_1: 27

        .= ( 1. B) by A12, Def2;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: RINGFRAC:41

    f is RingHomomorphism & (f .: S) c= ( Unit_Set B) implies ( Univ_Map (S,f)) is RingHomomorphism by Th57, Th58, Th59;

    theorem :: RINGFRAC:42

    

     Th61: f is RingHomomorphism & (f .: S) c= ( Unit_Set B) implies f = (( Univ_Map (S,f)) * ( canHom S))

    proof

      set h = ( canHom S);

      set g = ( Univ_Map (S,f));

      set g1 = (( Univ_Map (S,f)) * ( canHom S));

      assume

       A1: f is RingHomomorphism & (f .: S) c= ( Unit_Set B);

      

       A2: ( dom h) = ( [#] A) by FUNCT_2:def 1;

      

       A3: ( dom g1) = the carrier of A by FUNCT_2:def 1

      .= ( dom f) by FUNCT_2:def 1;

      for x be object st x in ( dom f) holds (f . x) = (g1 . x)

      proof

        set g1 = (( Univ_Map (S,f)) * ( canHom S));

        let x be object;

        assume x in ( dom f);

        then

        reconsider x as Element of A;

        

         A7: (h . x) = ( Class (( EqRel S),(( frac1 S) . x))) by Def7

        .= ( Class (( EqRel S), [x, ( 1. A)])) by Def4;

        (( frac1 S) . x) = [x, ( 1. A)] by Def4;

        then

        reconsider x1 = [x, ( 1. A)] as Element of ( Frac S);

        reconsider hx = (h . x) as Element of (S ~ A);

        consider a1,s1 be Element of A such that

         A9: s1 in S and

         A10: hx = ( Class (( EqRel S), [a1, s1])) and

         A11: (g . hx) = ((f . a1) * ((f . s1) ["] )) by A1, Def8;

        reconsider as1 = [a1, s1] as Element of ( Frac S) by A9, Def3;

        (as1,x1) Fr_Eq S by A7, A10, Th26;

        then

        consider s0 be Element of A such that

         A13: s0 in S and

         A14: ((((as1 `1 ) * (x1 `2 )) - ((x1 `1 ) * (as1 `2 ))) * s0) = ( 0. A);

        (f . s0) is Unit of B by A1, A13, Th56;

        then

         A15: (f . s0) in ( Unit_Set B);

        (f . s1) is Unit of B by A1, A9, Th56;

        then

         A16: (f . s1) in ( Unit_Set B);

        ( 0. B) = (f . ( 0. A)) by A1, QUOFIELD: 50

        .= ((f . (a1 - (x * s1))) * (f . s0)) by A1, A14, GROUP_6:def 6;

        

        then ( 0. B) = (((f . (a1 - (x * s1))) * (f . s0)) * ((f . s0) ["] ))

        .= ((f . (a1 - (x * s1))) * ((f . s0) * ((f . s0) ["] ))) by GROUP_1:def 3

        .= ((f . (a1 - (x * s1))) * ( 1. B)) by A15, Def2

        .= ((f . a1) - (f . (x * s1))) by A1, RING_2: 8;

        

        then

         A19: (f . a1) = (f . (x * s1)) by VECTSP_1: 27

        .= ((f . x) * (f . s1)) by A1, GROUP_6:def 6;

        ((f . a1) * ((f . s1) ["] )) = ((f . x) * ((f . s1) * ((f . s1) ["] ))) by A19, GROUP_1:def 3

        .= ((f . x) * ( 1. B)) by A16, Def2

        .= (f . x);

        hence thesis by A2, A11, FUNCT_1: 13;

      end;

      hence thesis by A3;

    end;

    begin

    definition

      let A;

      :: RINGFRAC:def24

      func Total-Quotient-Ring (A) -> Ring equals (( Non_ZeroDiv_Set A) ~ A);

      correctness ;

    end

    registration

      let A;

      cluster ( Total-Quotient-Ring A) -> non degenerated;

      coherence

      proof

        ( 0. A) is Zero_Divisor of A by Th1;

        then ( 0. A) in ( ZeroDiv_Set A);

        then not ( 0. A) in ( Non_ZeroDiv_Set A) by XBOOLE_0:def 5;

        hence thesis by Th31;

      end;

    end

    reserve x for object;

    theorem :: RINGFRAC:43

    A is Field implies ( Ideals A) = { {( 0. A)}, the carrier of A}

    proof

      assume

       A1: A is Field;

      

       A2: x in ( Ideals A) implies x in { {( 0. A)}, the carrier of A}

      proof

        assume x in ( Ideals A);

        then x in the set of all I where I be Ideal of A by RING_2:def 3;

        then

        consider x1 be Ideal of A such that

         A4: x1 = x;

        x = {( 0. A)} or x = the carrier of A by A1, A4, IDEAL_1: 22;

        hence thesis by TARSKI:def 2;

      end;

      x in { {( 0. A)}, the carrier of A} implies x in ( Ideals A)

      proof

        assume x in { {( 0. A)}, the carrier of A};

        per cases by TARSKI:def 2;

          suppose x = {( 0. A)};

          then x in the set of all I where I be Ideal of A;

          hence thesis by RING_2:def 3;

        end;

          suppose x = the carrier of A;

          then x is Ideal of A by IDEAL_1: 10;

          then x in the set of all I where I be Ideal of A;

          hence thesis by RING_2:def 3;

        end;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    reserve A for domRing;

    theorem :: RINGFRAC:44

    

     Lm63: ( Non_ZeroDiv_Set A) = (( [#] A) \ {( 0. A)}) & ( Non_ZeroDiv_Set A) is without_zero non empty multiplicatively-closed Subset of A

    proof

      

       A1: ( Non_ZeroDiv_Set A) = (( [#] A) \ {( 0. A)}) by Th4;

      ( 0. A) in ( [#] A) & ( 0. A) in {( 0. A)} by TARSKI:def 1;

      then ( Non_ZeroDiv_Set A) is without_zero by A1, XBOOLE_0:def 5;

      hence thesis by Th4;

    end;

    theorem :: RINGFRAC:45

    

     Th64: for a be Element of A holds a in ( Non_ZeroDiv_Set A) iff a <> ( 0. A)

    proof

      let a be Element of A;

      thus a in ( Non_ZeroDiv_Set A) implies a <> ( 0. A)

      proof

        assume a in ( Non_ZeroDiv_Set A);

        then a in (( [#] A) \ {( 0. A)}) by Lm63;

        then a in ( [#] A) & not a in {( 0. A)} by XBOOLE_0:def 5;

        hence thesis by TARSKI:def 1;

      end;

      assume a <> ( 0. A);

      then not a in {( 0. A)} by TARSKI:def 1;

      then a in (( [#] A) \ {( 0. A)}) by XBOOLE_0:def 5;

      hence thesis by Lm63;

    end;

    theorem :: RINGFRAC:46

    

     Th65: ( Total-Quotient-Ring A) is Field

    proof

      set S = ( Non_ZeroDiv_Set A);

      

       A0: S = (( [#] A) \ {( 0. A)}) by Th4;

      for x be Element of (S ~ A) st x <> ( 0. (S ~ A)) holds x is left_invertible

      proof

        let x be Element of (S ~ A);

        assume

         A1: x <> ( 0. (S ~ A));

        consider a1,s1 be Element of A such that

         A2: s1 in S and

         A3: x = ( Class (( EqRel S), [a1, s1])) by Th46;

        reconsider as1 = [a1, s1] as Element of ( Frac S) by A2, Def3;

        a1 <> ( 0. A)

        proof

          assume

           A5: a1 = ( 0. A);

          reconsider t = ( 1. A) as Element of A;

          t in S by C0SP1:def 4;

          then (as1,( 0. (A,S))) Fr_Eq S by A5;

          

          then x = ( Class (( EqRel S),( 0. (A,S)))) by A3, Th26

          .= ( 0. (S ~ A)) by Def6;

          hence contradiction by A1;

        end;

        then not a1 in {( 0. A)} by TARSKI:def 1;

        then (as1 `1 ) in S by A0, XBOOLE_0:def 5;

        then ( Class (( EqRel S),as1)) is Unit of (S ~ A) by Lm45;

        then x in ( Unit_Set (S ~ A)) by A3;

        then ((x ["] ) * x) = ( 1. (S ~ A)) by Def2;

        hence thesis;

      end;

      then (S ~ A) is almost_left_invertible;

      hence thesis;

    end;

    reserve x for Element of ( Q. A),

y for object;

    theorem :: RINGFRAC:47

    for A be domRing holds ( the_Field_of_Quotients A) is_ringisomorph_to ( Total-Quotient-Ring A)

    proof

      let A be domRing;

      set S = ( Non_ZeroDiv_Set A);

      set B = ( the_Field_of_Quotients A);

      set f = ( canHom A);

      

       A1: f is RingHomomorphism by QUOFIELD: 56;

      

       A2: f is RingMonomorphism by QUOFIELD: 57;

      

       A3: (f .: S) c= ( Unit_Set B)

      proof

        y in (f .: S) implies y in ( Unit_Set B)

        proof

          assume y in (f .: S);

          then

          consider x be object such that

           A5: x in ( dom f) and

           A6: x in S and

           A7: y = (f . x) by FUNCT_1:def 6;

          

           A8: x <> ( 0. A) by A6, Th3;

          reconsider x as Element of A by A5;

          

           A9: (f . x) <> ( 0. B) by A2, A8, QUOFIELD: 51;

          (f . x) is Element of B;

          then

          reconsider y as Element of B by A7;

           not y is zero by A7, A9;

          hence thesis;

        end;

        hence thesis;

      end;

      reconsider S = ( Non_ZeroDiv_Set A) as without_zero non empty multiplicatively-closed Subset of A by Lm63;

      

       A11: ( Univ_Map (S,f)) is RingHomomorphism by A3, QUOFIELD: 56, Th57, Th58, Th59;

      

       A12: ( Total-Quotient-Ring A) is Field by Th65;

      set g = ( Univ_Map (S,f));

      set h = ( canHom S);

      

       A13: ( dom g) = ( [#] (S ~ A)) by FUNCT_2:def 1;

      

       A14: y in ( [#] B) implies y in ( rng g)

      proof

        assume y in ( [#] B);

        then

        reconsider y as Element of ( Quot. A) by QUOFIELD: 30;

        consider y12 be Element of ( Q. A) such that

         A16: y = ( QClass. y12) by QUOFIELD:def 5;

        consider y1,y2 be Element of A such that

         A17: y12 = [y1, y2] and

         A18: y2 <> ( 0. A) by QUOFIELD:def 1;

        

         A19: y2 in ( Non_ZeroDiv_Set A) by A18, Th64;

        then

         A20: [y1, y2] in ( Frac S) by Def3;

        reconsider yy12 = y12 as Element of ( Frac S) by A17, A19, Def3;

        reconsider x = ( Class (( EqRel S),yy12)) as Element of (S ~ A) by Lm41;

        

         A21: ( 1. A) <> ( 0. A);

        then

        reconsider p1 = [y1, ( 1. A)] as Element of ( Q. A) by QUOFIELD:def 1;

        reconsider p2 = [y2, ( 1. A)] as Element of ( Q. A) by A21, QUOFIELD:def 1;

        reconsider q = [( 1. A), y2] as Element of ( Q. A) by A18, QUOFIELD:def 1;

        reconsider r12 = [y1, y2] as Element of ( Q. A) by A18, QUOFIELD:def 1;

        ( quotient (y1,( 1. A))) = p1 by A21, QUOFIELD:def 24;

        then

         A24: (f . y1) = ( QClass. p1) by QUOFIELD:def 25;

        ( quotient (y2,( 1. A))) = p2 by A21, QUOFIELD:def 24;

        then

         A25: (f . y2) = ( QClass. p2) by QUOFIELD:def 25;

        then

         A26: ( QClass. p2) <> ( 0. B) by A2, A18, QUOFIELD: 51;

        then

         A27: ((f . y2) " ) = ( QClass. q) by A18, A25, QUOFIELD: 47;

        

         A28: ( pmult (p1,q)) = [((p1 `1 ) * (q `1 )), ((p1 `2 ) * (q `2 ))] by QUOFIELD:def 3

        .= [y1, y2];

        

         A29: r12 in ( QClass. r12) by QUOFIELD: 5;

        ((r12 `1 ) * (y12 `2 )) = ((r12 `2 ) * (y12 `1 )) by A17;

        then r12 in ( QClass. y12) by QUOFIELD:def 4;

        then

         A30: r12 in (( QClass. r12) /\ ( QClass. y12)) by A29, XBOOLE_0:def 4;

        

         A31: ((f . y1) * ((f . y2) " )) = (( quotmult A) . ((f . y1),((f . y2) " ))) by QUOFIELD: 37

        .= ( qmult (( QClass. p1),( QClass. q))) by A24, A27, QUOFIELD:def 13

        .= ( QClass. r12) by A28, QUOFIELD: 10

        .= y by QUOFIELD: 8, XBOOLE_0: 4, A30, A16;

        reconsider x = ( Class (( EqRel S), [y1, y2])) as Element of (S ~ A) by A20, Lm41;

        consider x1,x2 be Element of A such that

         A32: x2 in S and x = ( Class (( EqRel S), [x1, x2])) and (g . x) = ((f . x1) * ((f . x2) ["] )) by A1, A3, Def8;

        reconsider x12 = [x1, x2] as Element of ( Frac S) by Def3, A32;

        

         A33: ( dom h) = ( [#] A) by FUNCT_2:def 1;

        

         A34: (h . y2) = ( Class (( EqRel S),(( frac1 S) . y2))) by Def7

        .= ( Class (( EqRel S), [y2, ( 1. A)])) by Def4;

        then (h . y2) is Unit of (S ~ A) by A19, Lm46;

        then

         A35: (h . y2) in ( Unit_Set (S ~ A));

        

         A36: (f . y2) = ((g * h) . y2) by Th61, QUOFIELD: 56, A3

        .= (g . (h . y2)) by A33, FUNCT_1: 13;

        

         A37: g is unity-preserving by QUOFIELD: 56, A3, Th59;

        ((f . y2) * (g . ((h . y2) ["] ))) = (g . ((h . y2) * ((h . y2) ["] ))) by A11, A36, GROUP_6:def 6

        .= ( 1. B) by A37, A35, Def2;

        

        then

         A39: ((f . y2) " ) = (((f . y2) " ) * ((f . y2) * (g . ((h . y2) ["] ))))

        .= ((((f . y2) " ) * (f . y2)) * (g . ((h . y2) ["] ))) by GROUP_1:def 3

        .= (( 1. B) * (g . ((h . y2) ["] ))) by A25, A26, VECTSP_1:def 10

        .= (g . ((h . y2) ["] ));

        

         A40: (h . y1) = ( Class (( EqRel S),(( frac1 S) . y1))) by Def7

        .= ( Class (( EqRel S), [y1, ( 1. A)])) by Def4;

        

         A41: ( 1. A) in S by C0SP1:def 4;

        then

        reconsider zz1 = [y1, ( 1. A)] as Element of ( Frac S) by Def3;

        reconsider zz2 = [y2, ( 1. A)] as Element of ( Frac S) by A41, Def3;

        reconsider zz2inv = [( 1. A), y2] as Element of ( Frac S) by A19, Def3;

        reconsider z1 = ( Class (( EqRel S),zz1)) as Element of (S ~ A) by Lm41;

        reconsider z2 = ( Class (( EqRel S),zz2)) as Element of (S ~ A) by Lm41;

        reconsider z2inv = ( Class (( EqRel S),zz2inv)) as Element of (S ~ A) by Lm41;

        ( Class (( EqRel S), [y2, ( 1. A)])) is Unit of (S ~ A) by A19, Lm46;

        then

         A43: z2 in ( Unit_Set (S ~ A));

        

         A44: (z2inv * z2) = ( Class (( EqRel S),(zz2inv * zz2))) by Th33

        .= ( Class (( EqRel S),( 1. (A,S)))) by A19, Th30, Th26

        .= ( 1. (S ~ A)) by Def6;

        (z2 ["] ) = ((z2inv * z2) * (z2 ["] )) by A44

        .= (z2inv * (z2 * (z2 ["] ))) by GROUP_1:def 3

        .= (z2inv * ( 1. (S ~ A))) by A43, Def2

        .= z2inv;

        

        then

         A46: (z1 * (z2 ["] )) = ( Class (( EqRel S),(zz1 * zz2inv))) by Th33

        .= ( Class (( EqRel S), [y1, y2]));

        (f . y1) = ((g * h) . y1) by Th61, QUOFIELD: 56, A3

        .= (g . (h . y1)) by A33, FUNCT_1: 13;

        then

         A49: y = (g . ( Class (( EqRel S), [y1, y2]))) by A40, A34, A46, A11, A39, A31, GROUP_6:def 6;

        ( Class (( EqRel S), [y1, y2])) is Element of (S ~ A) by A20, Lm41;

        hence thesis by A13, A49, FUNCT_1:def 3;

      end;

      ( [#] B) c= ( rng g) by A14;

      then g is onto by XBOOLE_0:def 10;

      hence thesis by A11, A12, QUOFIELD:def 23;

    end;