ring_3.miz



    begin

    theorem :: RING_3:1

    

     Th1: for f be Function, A be set, a,b be object st a in A & b in A holds ((f || A) . (a,b)) = (f . (a,b))

    proof

      let f be Function;

      let A be set;

      let a,b be object;

      assume a in A & b in A;

      then [a, b] in [:A, A:] by ZFMISC_1:def 2;

      hence thesis by FUNCT_1: 49;

    end;

    theorem :: RING_3:2

    

     Th2: ( addcomplex || REAL ) = addreal

    proof

      set ad = ( addcomplex || REAL );

       [: REAL , REAL :] c= [: COMPLEX , COMPLEX :] by NUMBERS: 11, ZFMISC_1: 96;

      then

       A1: [: REAL , REAL :] c= ( dom addcomplex ) by FUNCT_2:def 1;

      then

       A2: ( dom ad) = [: REAL , REAL :] by RELAT_1: 62;

      

       A3: ( dom addreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

      for z be object st z in ( dom ad) holds (ad . z) = ( addreal . z)

      proof

        let z be object;

        assume

         A4: z in ( dom ad);

        then

        consider x,y be object such that

         A5: x in REAL & y in REAL & z = [x, y] by A2, ZFMISC_1:def 2;

        reconsider x1 = x, y1 = y as Real by A5;

        

        thus (ad . z) = ( addcomplex . (x1,y1)) by A4, A5, A2, FUNCT_1: 49

        .= (x1 + y1) by BINOP_2:def 3

        .= ( addreal . (x1,y1)) by BINOP_2:def 9

        .= ( addreal . z) by A5;

      end;

      hence thesis by A1, A3, RELAT_1: 62;

    end;

    theorem :: RING_3:3

    

     Th3: ( multcomplex || REAL ) = multreal

    proof

      set mu = ( multcomplex || REAL );

       [: REAL , REAL :] c= [: COMPLEX , COMPLEX :] by NUMBERS: 11, ZFMISC_1: 96;

      then

       A1: [: REAL , REAL :] c= ( dom multcomplex ) by FUNCT_2:def 1;

      then

       A2: ( dom mu) = [: REAL , REAL :] by RELAT_1: 62;

      

       A3: ( dom multreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

      for z be object st z in ( dom mu) holds (mu . z) = ( multreal . z)

      proof

        let z be object;

        assume

         A4: z in ( dom mu);

        then

        consider x,y be object such that

         A5: x in REAL & y in REAL & z = [x, y] by A2, ZFMISC_1:def 2;

        reconsider x1 = x, y1 = y as Real by A5;

        

        thus (mu . z) = ( multcomplex . (x1,y1)) by A4, A5, A2, FUNCT_1: 49

        .= (x1 * y1) by BINOP_2:def 5

        .= ( multreal . (x1,y1)) by BINOP_2:def 11

        .= ( multreal . z) by A5;

      end;

      hence thesis by A1, A3, RELAT_1: 62;

    end;

    theorem :: RING_3:4

    

     Th4: ( addrat || INT ) = addint

    proof

      set ad = ( addrat || INT );

       [: INT , INT :] c= [: RAT , RAT :] by NUMBERS: 14, ZFMISC_1: 96;

      then

       A1: [: INT , INT :] c= ( dom addrat ) by FUNCT_2:def 1;

      then

       A2: ( dom ad) = [: INT , INT :] by RELAT_1: 62;

      

       A3: ( dom addint ) = [: INT , INT :] by FUNCT_2:def 1;

      for z be object st z in ( dom ad) holds (ad . z) = ( addint . z)

      proof

        let z be object;

        assume

         A4: z in ( dom ad);

        then

        consider x,y be object such that

         A5: x in INT & y in INT & z = [x, y] by A2, ZFMISC_1:def 2;

        reconsider x1 = x, y1 = y as Integer by A5;

        

        thus (ad . z) = ( addrat . (x1,y1)) by A4, A5, A2, FUNCT_1: 49

        .= (x1 + y1) by BINOP_2:def 15

        .= ( addint . (x1,y1)) by BINOP_2:def 20

        .= ( addint . z) by A5;

      end;

      hence thesis by A1, A3, RELAT_1: 62;

    end;

    theorem :: RING_3:5

    

     Th5: ( multrat || INT ) = multint

    proof

      set mu = ( multrat || INT );

       [: INT , INT :] c= [: RAT , RAT :] by NUMBERS: 14, ZFMISC_1: 96;

      then

       A1: [: INT , INT :] c= ( dom multrat ) by FUNCT_2:def 1;

      then

       A2: ( dom mu) = [: INT , INT :] by RELAT_1: 62;

      

       A3: ( dom multint ) = [: INT , INT :] by FUNCT_2:def 1;

      for z be object st z in ( dom mu) holds (mu . z) = ( multint . z)

      proof

        let z be object;

        assume

         A4: z in ( dom mu);

        then

        consider x,y be object such that

         A5: x in INT & y in INT & z = [x, y] by A2, ZFMISC_1:def 2;

        reconsider x1 = x, y1 = y as Integer by A5;

        

        thus (mu . z) = ( multrat . (x1,y1)) by A4, A5, A2, FUNCT_1: 49

        .= (x1 * y1) by BINOP_2:def 17

        .= ( multint . (x1,y1)) by BINOP_2:def 22

        .= ( multint . z) by A5;

      end;

      hence thesis by A1, A3, RELAT_1: 62;

    end;

    begin

    reserve p,q for Rational;

    reserve g,m,m1,m2,n,n1,n2 for Nat;

    reserve i,i1,i2,j,j1,j2 for Integer;

    theorem :: RING_3:6

    

     Th6: n divides i implies (i div n) = (i / n)

    proof

      per cases ;

        suppose n = 0 ;

        hence thesis by INT_1: 48;

      end;

        suppose

         A1: n <> 0 ;

        assume

         A2: n divides i;

        (i mod n) = 0 by A1, A2, INT_1: 62;

        hence thesis by A1, PEPIN: 63;

      end;

    end;

    theorem :: RING_3:7

    

     Th7: (i div (i gcd n)) = (i / (i gcd n))

    proof

      (i gcd n) divides i & (i gcd n) divides n by INT_2:def 2;

      hence thesis by Th6;

    end;

    theorem :: RING_3:8

    

     Th8: (n div (n gcd i)) = (n / (n gcd i))

    proof

      (i gcd n) divides i & (i gcd n) divides n by INT_2:def 2;

      hence thesis by Th6;

    end;

    theorem :: RING_3:9

    

     Th9: g divides i & g divides m implies (i / m) = ((i div g) / (m div g))

    proof

      assume that

       A1: g divides i and

       A2: g divides m;

      per cases ;

        suppose

         A3: g = 0 ;

        ( 0 gcd 0 ) = 0 by INT_2: 5;

        then ( 0 div ( 0 gcd 0 )) = 0 by INT_1: 48;

        hence thesis by A1, A3;

      end;

        suppose

         A4: m = 0 ;

        ( 0 div g) = 0 by NAT_2: 2;

        then (i / 0 ) = 0 & ((i div g) / ( 0 div g)) = 0 by XCMPLX_1: 49;

        hence thesis by A4;

      end;

        suppose that

         A5: g <> 0 and

         A6: m <> 0 ;

        g <= m by A2, A6, INT_2: 27;

        then

         A7: (m div g) <> 0 by A5, NAT_2: 13;

        (i mod g) = 0 & (m mod g) = 0 by A1, A2, A5, INT_1: 62;

        then (m div g) = (m / g) & (i div g) = (i / g) by A5, PEPIN: 63;

        then (i * (m div g)) = (m * (i div g));

        hence thesis by A6, A7, XCMPLX_1: 94;

      end;

    end;

    theorem :: RING_3:10

    

     Th10: (i / m) = ((i div (i gcd m)) / (m div (i gcd m)))

    proof

      (i gcd m) divides i & (i gcd m) divides m by INT_2:def 2;

      hence thesis by Th9;

    end;

    theorem :: RING_3:11

    

     Th11: 0 < m & (m * i) divides m implies i = 1 or i = ( - 1)

    proof

      assume that

       A1: 0 < m and

       A2: (m * i) divides m;

      m divides (m * i);

      then m = (m * i) or m = ( - ( - ( - (m * i)))) by A2, INT_2: 11;

      hence i = 1 or i = ( - 1) by A1, XCMPLX_1: 7, XCMPLX_1: 181;

    end;

    theorem :: RING_3:12

     0 < m & (m * n) divides m implies n = 1

    proof

      assume that

       A1: 0 < m and

       A2: (m * n) divides m;

      m divides (m * n);

      then m = (m * n) or m = ( - (m * n)) by A2, INT_2: 11;

      hence n = 1 by A1, XCMPLX_1: 7;

    end;

    theorem :: RING_3:13

    m divides i implies (i div m) divides i

    proof

      assume

       A1: m divides i;

      per cases ;

        suppose

         A2: m <> 0 ;

        take m;

        (i div m) = (i / m) by A1, Th6;

        hence thesis by A2, XCMPLX_1: 87;

      end;

        suppose m = 0 ;

        hence thesis by A1, INT_1: 48;

      end;

    end;

    theorem :: RING_3:14

    

     Th14: m <> 0 implies ((i div (i gcd m)) gcd (m div (i gcd m))) = 1

    proof

      set g = (i gcd m);

      set a = (i div g), b = (m div g);

      assume

       A1: m <> 0 ;

      then

       A2: g <> 0 by INT_2: 5;

      

       A3: 1 divides a & 1 divides b by INT_2: 12;

      now

        let w be Integer such that

         A4: w divides a and

         A5: w divides b;

        consider i1 such that

         A6: a = (i1 * w) by A4;

        consider i2 such that

         A7: b = (i2 * w) by A5;

        

         A8: g divides i by INT_2:def 2;

        

         A9: g divides m by INT_2:def 2;

         A10:

        now

          assume

           A11: w = 0 ;

          g <= m by A1, A9, INT_2: 27;

          hence contradiction by A2, A5, A11, NAT_2: 13;

        end;

        

         A12: (((i / g) / w) * w) = (i / g) by A10, XCMPLX_1: 87;

        

         A13: (((m / g) / w) * w) = (m / g) by A10, XCMPLX_1: 87;

        ((i / g) / w) = ((i1 * w) / w) by A6, A8, Th6

        .= i1 by A10, XCMPLX_1: 89;

        then ((((i / g) / w) * w) * g) = ((i1 * w) * g);

        then i = (i1 * (g * w)) by A12, A2, XCMPLX_1: 87;

        then

         A14: (g * w) divides i;

        ((m / g) / w) = ((i2 * w) / w) by A7, A9, Th6

        .= i2 by A10, XCMPLX_1: 89;

        then ((((m / g) / w) * w) * g) = ((i2 * w) * g);

        then m = (i2 * (g * w)) by A13, A2, XCMPLX_1: 87;

        then (g * w) divides m;

        then (g * w) divides g by A14, INT_2:def 2;

        then w = 1 or w = ( - 1) by A2, Th11;

        hence w divides 1 by INT_2: 14;

      end;

      hence (a gcd b) = 1 by A3, INT_2:def 2;

    end;

    theorem :: RING_3:15

    

     Th15: m <> 0 implies ( denominator (i / m)) = (m div (i gcd m)) & ( numerator (i / m)) = (i div (i gcd m))

    proof

      set p = (i / m);

      set g = (i gcd m);

      set d = (m div g);

      assume

       A1: 0 <> m;

      then

       A2: g <> 0 by INT_2: 5;

      g divides m by INT_2:def 2;

      then g <= m by A1, INT_2: 27;

      then

       A3: d <> 0 by A2, PRE_FF: 3;

      

       A4: p = ((i div g) / d) by Th10;

      now

        given w be Nat such that

         A5: 1 < w and

         A6: ex i1, m1 st (i div g) = (i1 * w) & (m div g) = (m1 * w);

        consider i1, m1 such that

         A7: (i div g) = (i1 * w) and

         A8: d = (m1 * w) by A6;

        w divides (i div g) & w divides (m div g) by A7, A8;

        then

         A9: w divides ((i div g) gcd (m div g)) by INT_2:def 2;

        ((i div g) gcd (m div g)) = 1 by A1, Th14;

        hence contradiction by A5, A9, WSIERP_1: 15;

      end;

      hence thesis by A3, A4, RAT_1: 30;

    end;

    theorem :: RING_3:16

    m <> 0 implies ( denominator (i / m)) = (m / (i gcd m)) & ( numerator (i / m)) = (i / (i gcd m))

    proof

      assume

       A1: m <> 0 ;

      

      hence ( denominator (i / m)) = (m div (i gcd m)) by Th15

      .= (m / (i gcd m)) by Th8;

      

      thus ( numerator (i / m)) = (i div (i gcd m)) by A1, Th15

      .= (i / (i gcd m)) by Th7;

    end;

    theorem :: RING_3:17

    

     Th17: m <> 0 implies ( denominator ( - (i / m))) = (m div (( - i) gcd m)) & ( numerator ( - (i / m))) = (( - i) div (( - i) gcd m))

    proof

      ( - (i / m)) = (( - i) / m);

      hence thesis by Th15;

    end;

    theorem :: RING_3:18

    m <> 0 implies ( denominator ( - (i / m))) = (m / (( - i) gcd m)) & ( numerator ( - (i / m))) = (( - i) / (( - i) gcd m))

    proof

      assume

       A1: m <> 0 ;

      

      hence ( denominator ( - (i / m))) = (m div (( - i) gcd m)) by Th17

      .= (m / (( - i) gcd m)) by Th8;

      

      thus ( numerator ( - (i / m))) = (( - i) div (( - i) gcd m)) by A1, Th17

      .= (( - i) / (( - i) gcd m)) by Th7;

    end;

    theorem :: RING_3:19

    

     Th19: m <> 0 implies ( denominator ((m / i) " )) = (m div (m gcd i)) & ( numerator ((m / i) " )) = (i div (m gcd i))

    proof

      ((m / i) " ) = (i / m) by XCMPLX_1: 213;

      hence thesis by Th15;

    end;

    theorem :: RING_3:20

    m <> 0 implies ( denominator ((m / i) " )) = (m / (m gcd i)) & ( numerator ((m / i) " )) = (i / (m gcd i))

    proof

      assume

       A1: m <> 0 ;

      

      hence ( denominator ((m / i) " )) = (m div (m gcd i)) by Th19

      .= (m / (m gcd i)) by Th8;

      

      thus ( numerator ((m / i) " )) = (i div (m gcd i)) by A1, Th19

      .= (i / (m gcd i)) by Th7;

    end;

    theorem :: RING_3:21

    

     Th21: m <> 0 & n <> 0 implies ( denominator ((i / m) + (j / n))) = ((m * n) div (((i * n) + (j * m)) gcd (m * n))) & ( numerator ((i / m) + (j / n))) = (((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)))

    proof

      assume that

       A1: m <> 0 and

       A2: n <> 0 ;

      ((i / m) + (j / n)) = (((i * n) / (m * n)) + (j / n)) by A2, XCMPLX_1: 91

      .= (((i * n) / (m * n)) + ((j * m) / (m * n))) by A1, XCMPLX_1: 91

      .= (((i * n) + (j * m)) / (m * n));

      hence thesis by A1, A2, Th15;

    end;

    theorem :: RING_3:22

    m <> 0 & n <> 0 implies ( denominator ((i / m) + (j / n))) = ((m * n) / (((i * n) + (j * m)) gcd (m * n))) & ( numerator ((i / m) + (j / n))) = (((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)))

    proof

      assume

       A1: m <> 0 & n <> 0 ;

      

      hence ( denominator ((i / m) + (j / n))) = ((m * n) div (((i * n) + (j * m)) gcd (m * n))) by Th21

      .= ((m * n) / (((i * n) + (j * m)) gcd (m * n))) by Th8;

      

      thus ( numerator ((i / m) + (j / n))) = (((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n))) by A1, Th21

      .= (((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n))) by Th7;

    end;

    theorem :: RING_3:23

    

     Th23: m <> 0 & n <> 0 implies ( denominator ((i / m) - (j / n))) = ((m * n) div (((i * n) - (j * m)) gcd (m * n))) & ( numerator ((i / m) - (j / n))) = (((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)))

    proof

      assume that

       A1: m <> 0 and

       A2: n <> 0 ;

      ((i / m) - (j / n)) = (((i * n) / (m * n)) - (j / n)) by A2, XCMPLX_1: 91

      .= (((i * n) / (m * n)) - ((j * m) / (m * n))) by A1, XCMPLX_1: 91

      .= (((i * n) - (j * m)) / (m * n));

      hence thesis by A1, A2, Th15;

    end;

    theorem :: RING_3:24

    m <> 0 & n <> 0 implies ( denominator ((i / m) - (j / n))) = ((m * n) / (((i * n) - (j * m)) gcd (m * n))) & ( numerator ((i / m) - (j / n))) = (((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n)))

    proof

      assume

       A1: m <> 0 & n <> 0 ;

      

      hence ( denominator ((i / m) - (j / n))) = ((m * n) div (((i * n) - (j * m)) gcd (m * n))) by Th23

      .= ((m * n) / (((i * n) - (j * m)) gcd (m * n))) by Th8;

      

      thus ( numerator ((i / m) - (j / n))) = (((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n))) by A1, Th23

      .= (((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n))) by Th7;

    end;

    theorem :: RING_3:25

    

     Th25: m <> 0 & n <> 0 implies ( denominator ((i / m) * (j / n))) = ((m * n) div ((i * j) gcd (m * n))) & ( numerator ((i / m) * (j / n))) = ((i * j) div ((i * j) gcd (m * n)))

    proof

      ((i / m) * (j / n)) = ((i * j) / (m * n)) by XCMPLX_1: 76;

      hence thesis by Th15;

    end;

    theorem :: RING_3:26

    m <> 0 & n <> 0 implies ( denominator ((i / m) * (j / n))) = ((m * n) / ((i * j) gcd (m * n))) & ( numerator ((i / m) * (j / n))) = ((i * j) / ((i * j) gcd (m * n)))

    proof

      assume

       A1: m <> 0 & n <> 0 ;

      

      hence ( denominator ((i / m) * (j / n))) = ((m * n) div ((i * j) gcd (m * n))) by Th25

      .= ((m * n) / ((i * j) gcd (m * n))) by Th8;

      

      thus ( numerator ((i / m) * (j / n))) = ((i * j) div ((i * j) gcd (m * n))) by A1, Th25

      .= ((i * j) / ((i * j) gcd (m * n))) by Th7;

    end;

    theorem :: RING_3:27

    

     Th27: m <> 0 & n <> 0 implies ( denominator ((i / m) / (n / j))) = ((m * n) div ((i * j) gcd (m * n))) & ( numerator ((i / m) / (n / j))) = ((i * j) div ((i * j) gcd (m * n)))

    proof

      ((i / m) / (n / j)) = ((i * j) / (m * n)) by XCMPLX_1: 84;

      hence thesis by Th15;

    end;

    theorem :: RING_3:28

    m <> 0 & n <> 0 implies ( denominator ((i / m) / (n / j))) = ((m * n) / ((i * j) gcd (m * n))) & ( numerator ((i / m) / (n / j))) = ((i * j) / ((i * j) gcd (m * n)))

    proof

      assume

       A1: m <> 0 & n <> 0 ;

      

      hence ( denominator ((i / m) / (n / j))) = ((m * n) div ((i * j) gcd (m * n))) by Th27

      .= ((m * n) / ((i * j) gcd (m * n))) by Th8;

      

      thus ( numerator ((i / m) / (n / j))) = ((i * j) div ((i * j) gcd (m * n))) by A1, Th27

      .= ((i * j) / ((i * j) gcd (m * n))) by Th7;

    end;

    theorem :: RING_3:29

    ( denominator p) = (( denominator p) div (( numerator p) gcd ( denominator p)))

    proof

      p = (( numerator p) / ( denominator p)) by RAT_1: 15;

      hence thesis by Th15;

    end;

    theorem :: RING_3:30

    ( numerator p) = (( numerator p) div (( numerator p) gcd ( denominator p)))

    proof

      p = (( numerator p) / ( denominator p)) by RAT_1: 15;

      hence thesis by Th15;

    end;

    theorem :: RING_3:31

    

     Th31: m = ( denominator p) & i = ( numerator p) implies ( denominator ( - p)) = (m div (( - i) gcd m)) & ( numerator ( - p)) = (( - i) div (( - i) gcd m))

    proof

      p = (( numerator p) / ( denominator p)) by RAT_1: 15;

      hence thesis by Th17;

    end;

    theorem :: RING_3:32

    m = ( denominator p) & i = ( numerator p) implies ( denominator ( - p)) = (m / (( - i) gcd m)) & ( numerator ( - p)) = (( - i) / (( - i) gcd m))

    proof

      assume

       A1: m = ( denominator p) & i = ( numerator p);

      

      hence ( denominator ( - p)) = (m div (( - i) gcd m)) by Th31

      .= (m / (( - i) gcd m)) by Th8;

      

      thus ( numerator ( - p)) = (( - i) div (( - i) gcd m)) by A1, Th31

      .= (( - i) / (( - i) gcd m)) by Th7;

    end;

    theorem :: RING_3:33

    

     Th33: m = ( denominator p) & n = ( numerator p) & n <> 0 implies ( denominator (p " )) = (n div (n gcd m)) & ( numerator (p " )) = (m div (n gcd m))

    proof

      assume m = ( denominator p) & n = ( numerator p);

      then p = (n / m) by RAT_1: 15;

      hence thesis by Th19;

    end;

    theorem :: RING_3:34

    m = ( denominator p) & n = ( numerator p) & n <> 0 implies ( denominator (p " )) = (n / (n gcd m)) & ( numerator (p " )) = (m / (n gcd m))

    proof

      assume

       A1: m = ( denominator p) & n = ( numerator p) & n <> 0 ;

      

      hence ( denominator (p " )) = (n div (n gcd m)) by Th33

      .= (n / (n gcd m)) by Th8;

      

      thus ( numerator (p " )) = (m div (n gcd m)) by A1, Th33

      .= (m / (n gcd m)) by Th7;

    end;

    theorem :: RING_3:35

    

     Th35: m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q) implies ( denominator (p + q)) = ((m * n) div (((i * n) + (j * m)) gcd (m * n))) & ( numerator (p + q)) = (((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)))

    proof

      p = (( numerator p) / ( denominator p)) & q = (( numerator q) / ( denominator q)) by RAT_1: 15;

      hence thesis by Th21;

    end;

    theorem :: RING_3:36

    m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q) implies ( denominator (p + q)) = ((m * n) / (((i * n) + (j * m)) gcd (m * n))) & ( numerator (p + q)) = (((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)))

    proof

      assume

       A1: m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q);

      

      hence ( denominator (p + q)) = ((m * n) div (((i * n) + (j * m)) gcd (m * n))) by Th35

      .= ((m * n) / (((i * n) + (j * m)) gcd (m * n))) by Th8;

      

      thus ( numerator (p + q)) = (((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n))) by A1, Th35

      .= (((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n))) by Th7;

    end;

    theorem :: RING_3:37

    

     Th37: m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q) implies ( denominator (p - q)) = ((m * n) div (((i * n) - (j * m)) gcd (m * n))) & ( numerator (p - q)) = (((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)))

    proof

      p = (( numerator p) / ( denominator p)) & q = (( numerator q) / ( denominator q)) by RAT_1: 15;

      hence thesis by Th23;

    end;

    theorem :: RING_3:38

    m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q) implies ( denominator (p - q)) = ((m * n) / (((i * n) - (j * m)) gcd (m * n))) & ( numerator (p - q)) = (((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n)))

    proof

      assume

       A1: m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q);

      

      hence ( denominator (p - q)) = ((m * n) div (((i * n) - (j * m)) gcd (m * n))) by Th37

      .= ((m * n) / (((i * n) - (j * m)) gcd (m * n))) by Th8;

      

      thus ( numerator (p - q)) = (((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n))) by A1, Th37

      .= (((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n))) by Th7;

    end;

    theorem :: RING_3:39

    

     Th39: m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q) implies ( denominator (p * q)) = ((m * n) div ((i * j) gcd (m * n))) & ( numerator (p * q)) = ((i * j) div ((i * j) gcd (m * n)))

    proof

      p = (( numerator p) / ( denominator p)) & q = (( numerator q) / ( denominator q)) by RAT_1: 15;

      hence thesis by Th25;

    end;

    theorem :: RING_3:40

    m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q) implies ( denominator (p * q)) = ((m * n) / ((i * j) gcd (m * n))) & ( numerator (p * q)) = ((i * j) / ((i * j) gcd (m * n)))

    proof

      assume

       A1: m = ( denominator p) & n = ( denominator q) & i = ( numerator p) & j = ( numerator q);

      

      hence ( denominator (p * q)) = ((m * n) div ((i * j) gcd (m * n))) by Th39

      .= ((m * n) / ((i * j) gcd (m * n))) by Th8;

      

      thus ( numerator (p * q)) = ((i * j) div ((i * j) gcd (m * n))) by A1, Th39

      .= ((i * j) / ((i * j) gcd (m * n))) by Th7;

    end;

    theorem :: RING_3:41

    

     Th41: m1 = ( denominator p) & m2 = ( denominator q) & n1 = ( numerator p) & n2 = ( numerator q) & n2 <> 0 implies ( denominator (p / q)) = ((m1 * n2) div ((n1 * m2) gcd (m1 * n2))) & ( numerator (p / q)) = ((n1 * m2) div ((n1 * m2) gcd (m1 * n2)))

    proof

      assume

       A1: m1 = ( denominator p) & m2 = ( denominator q) & n1 = ( numerator p) & n2 = ( numerator q) & n2 <> 0 ;

      then p = (n1 / m1) & q = (n2 / m2) by RAT_1: 15;

      hence thesis by A1, Th27;

    end;

    theorem :: RING_3:42

    m1 = ( denominator p) & m2 = ( denominator q) & n1 = ( numerator p) & n2 = ( numerator q) & n2 <> 0 implies ( denominator (p / q)) = ((m1 * n2) / ((n1 * m2) gcd (m1 * n2))) & ( numerator (p / q)) = ((n1 * m2) / ((n1 * m2) gcd (m1 * n2)))

    proof

      assume

       A1: m1 = ( denominator p) & m2 = ( denominator q) & n1 = ( numerator p) & n2 = ( numerator q) & n2 <> 0 ;

      

      hence ( denominator (p / q)) = ((m1 * n2) div ((n1 * m2) gcd (m1 * n2))) by Th41

      .= ((m1 * n2) / ((n1 * m2) gcd (m1 * n2))) by Th8;

      

      thus ( numerator (p / q)) = ((n1 * m2) div ((n1 * m2) gcd (m1 * n2))) by A1, Th41

      .= ((n1 * m2) / ((n1 * m2) gcd (m1 * n2))) by Th7;

    end;

    begin

    reserve R for Ring,

F for Field;

    set I = INT.Ring ;

    registration

      cluster positive for Element of INT.Ring ;

      existence ;

      cluster negative for Element of INT.Ring ;

      existence

      proof

        take ( - ( 1. INT.Ring ));

        thus thesis;

      end;

    end

    registration

      let a be non zero Element of F_Rat , x be Rational;

      identify x " with a " when a = x;

      compatibility

      proof

        reconsider b = (x " ) as Element of F_Rat by RAT_1:def 2;

        assume

         A1: x = a;

        

         A2: a <> ( 0. F_Rat );

        then (b * a) = ( 1. F_Rat ) by A1, XCMPLX_0:def 7;

        hence thesis by A2, VECTSP_1:def 10;

      end;

    end

    registration

      let a be Element of F_Rat , b be non zero Element of F_Rat ;

      let x,y be Rational;

      identify x / y with a / b when a = x, b = y;

      compatibility ;

    end

    registration

      let F be Field;

      reduce (( 1. F) " ) to ( 1. F);

      reducibility by EC_PF_2: 2;

    end

    definition

      let R,S be Ring;

      :: RING_3:def1

      pred R includes_an_isomorphic_copy_of S means ex T be strict Subring of R st (T,S) are_isomorphic ;

    end

    notation

      let R,S be Ring;

      synonym R includes S for R includes_an_isomorphic_copy_of S;

    end

    definition

      let R,S be Ring;

      :: original: are_isomorphic

      redefine

      pred R,S are_isomorphic ;

      reflexivity

      proof

        let R be Ring;

        ( id R) is isomorphism;

        hence (R,R) are_isomorphic ;

      end;

    end

    theorem :: RING_3:43

    

     Lm1: for E be Field, F be Subfield of E holds F is Subring of E

    proof

      let E be Field, F be Subfield of E;

      the carrier of F c= the carrier of E & the addF of F = (the addF of E || the carrier of F) & the multF of F = (the multF of E || the carrier of F) & ( 1. E) = ( 1. F) & ( 0. E) = ( 0. F) by EC_PF_1:def 1;

      hence F is Subring of E by C0SP1:def 3;

    end;

    theorem :: RING_3:44

    

     Th43: for R,S,T be Ring st (R,S) are_isomorphic & (S,T) are_isomorphic holds (R,T) are_isomorphic

    proof

      let R,S,T be Ring;

      assume

       A1: (R,S) are_isomorphic & (S,T) are_isomorphic ;

      then

      consider f be Function of R, S such that

       A2: f is isomorphism;

      consider g be Function of S, T such that

       A3: g is isomorphism by A1;

      (g * f) is one-to-one onto by A2, A3, FUNCT_2: 27;

      hence thesis by A2, A3;

    end;

    theorem :: RING_3:45

    for F be Field, R be Subring of F holds R is Subfield of F iff R is Field

    proof

      let F be Field, R be Subring of F;

      the carrier of R c= the carrier of F & the addF of R = (the addF of F || the carrier of R) & the multF of R = (the multF of F || the carrier of R) & ( 1. R) = ( 1. F) & ( 0. R) = ( 0. F) by C0SP1:def 3;

      hence thesis by EC_PF_1:def 1;

    end;

    theorem :: RING_3:46

    for E be Field, F be strict Subfield of E holds E includes F

    proof

      let E be Field, F be strict Subfield of E;

      the carrier of F c= the carrier of E & the addF of F = (the addF of E || the carrier of F) & the multF of F = (the multF of E || the carrier of F) & ( 1. E) = ( 1. F) & ( 0. E) = ( 0. F) by EC_PF_1:def 1;

      then F is strict Subring of E by C0SP1:def 3;

      then ex T be strict Subring of E st (T,F) are_isomorphic ;

      hence thesis;

    end;

    

     Lm2: the carrier of F_Real is Subset of the carrier of F_Complex & the addF of F_Real = (the addF of F_Complex || the carrier of F_Real ) & the multF of F_Real = (the multF of F_Complex || the carrier of F_Real ) & ( 1. F_Complex ) = ( 1. F_Real ) & ( 0. F_Complex ) = ( 0. F_Real ) by NUMBERS: 11, COMPLFLD:def 1, Th2, Th3;

    

     Lm3: for u,v be Integer holds for p,q be Element of INT.Ring st u = p & v = q holds u divides v iff p divides q

    proof

      let u,v be Integer, p,q be Element of INT.Ring ;

      assume

       A1: u = p & v = q;

      hereby

        assume u divides v;

        then

        consider w be Integer such that

         A2: v = (u * w);

        reconsider r = w as Element of INT.Ring by INT_1:def 2;

        q = (p * r) by A1, A2;

        hence p divides q by GCD_1:def 1;

      end;

      assume p divides q;

      then ex r be Element of INT.Ring st q = (p * r) by GCD_1:def 1;

      hence u divides v by A1;

    end;

    

     Lm4: the carrier of INT.Ring c= the carrier of F_Rat & the addF of INT.Ring = (the addF of F_Rat || the carrier of INT.Ring ) & the multF of INT.Ring = (the multF of F_Rat || the carrier of INT.Ring ) & ( 1. INT.Ring ) = ( 1. F_Rat ) & ( 0. INT.Ring ) = ( 0. F_Rat ) by NUMBERS: 14, Th4, Th5;

    theorem :: RING_3:47

     INT.Ring is Subring of F_Rat by Lm4, C0SP1:def 3;

    theorem :: RING_3:48

    

     Th47: F_Real is Subfield of F_Complex by Lm2, EC_PF_1: 2;

    registration

      let R be domRing;

      cluster R -homomorphic for domRing;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

      cluster R -homomorphic for comRing;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

      cluster R -homomorphic for Ring;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

    end

    registration

      let R be Field;

      cluster R -homomorphic for domRing;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

    end

    registration

      let F be Field, R be F -homomorphic Ring, f be Homomorphism of F, R;

      cluster ( Image f) -> almost_left_invertible;

      coherence

      proof

        set K = ( Image f);

        now

          let x be Element of K;

          assume

           A1: x <> ( 0. K);

          

           A2: the carrier of K = ( rng f) by RING_2:def 6;

          consider y be object such that

           A3: y in ( dom f) & x = (f . y) by A2, FUNCT_1:def 3;

          reconsider y as Element of F by A3;

          now

            assume y = ( 0. F);

            

            then (f . y) = ( 0. R) by RING_2: 6

            .= ( 0. K) by RING_2:def 6;

            hence contradiction by A3, A1;

          end;

          then

          consider a be Element of F such that

           A4: (a * y) = ( 1. F) by VECTSP_1:def 9;

          reconsider b = (f . a) as Element of K by A2, FUNCT_2: 4;

          ( 1. K) = ( 1_ R) by RING_2:def 6

          .= (f . ( 1_ F)) by GROUP_1:def 13

          .= ((f . a) * (f . y)) by A4, GROUP_6:def 6

          .= ((the multF of R || ( rng f)) . (b,x)) by Th1, A2, A3

          .= (b * x) by RING_2:def 6;

          hence ex z be Element of K st (z * x) = ( 1. K);

        end;

        hence thesis;

      end;

    end

    registration

      let F be domRing, E be F -homomorphic domRing, f be Homomorphism of F, E;

      cluster ( Image f) -> non degenerated;

      coherence

      proof

        ( 0. ( Image f)) = ( 0. E) & ( 1. ( Image f)) = ( 1. E) by RING_2:def 6;

        hence ( 0. ( Image f)) <> ( 1. ( Image f));

      end;

    end

    theorem :: RING_3:49

    

     Th48: for R be Ring, E be R -homomorphic Ring, K be Subring of R holds for f be Function of R, E, g be Function of K, E st g = (f | the carrier of K) & f is additive holds g is additive

    proof

      let R be Ring, E be R -homomorphic Ring, K be Subring of R, f be Function of R, E, g be Function of K, E such that

       A1: g = (f | the carrier of K) and

       A2: f is additive;

      let x,y be Element of K;

      the carrier of K c= the carrier of R by C0SP1:def 3;

      then

      reconsider x1 = x, y1 = y as Element of R;

      

       A3: (x + y) = ((the addF of R || the carrier of K) . (x,y)) by C0SP1:def 3

      .= (x1 + y1) by Th1;

      

      thus (g . (x + y)) = (f . (x + y)) by A1, FUNCT_1: 49

      .= ((f . x1) + (f . y1)) by A2, A3

      .= ((g . x) + (f . y1)) by A1, FUNCT_1: 49

      .= ((g . x) + (g . y)) by A1, FUNCT_1: 49;

    end;

    theorem :: RING_3:50

    

     Th49: for R be Ring, E be R -homomorphic Ring, K be Subring of R holds for f be Function of R, E, g be Function of K, E st g = (f | the carrier of K) & f is multiplicative holds g is multiplicative

    proof

      let R be Ring, E be R -homomorphic Ring, K be Subring of R, f be Function of R, E, g be Function of K, E such that

       A1: g = (f | the carrier of K) and

       A2: f is multiplicative;

      let x,y be Element of K;

      the carrier of K c= the carrier of R by C0SP1:def 3;

      then

      reconsider x1 = x, y1 = y as Element of R;

      

       A3: (x * y) = ((the multF of R || the carrier of K) . (x,y)) by C0SP1:def 3

      .= (x1 * y1) by Th1;

      

      thus (g . (x * y)) = (f . (x * y)) by A1, FUNCT_1: 49

      .= ((f . x1) * (f . y1)) by A2, A3

      .= ((g . x) * (f . y1)) by A1, FUNCT_1: 49

      .= ((g . x) * (g . y)) by A1, FUNCT_1: 49;

    end;

    theorem :: RING_3:51

    

     Th50: for R be Ring, E be R -homomorphic Ring, K be Subring of R holds for f be Function of R, E, g be Function of K, E st g = (f | the carrier of K) & f is unity-preserving holds g is unity-preserving

    proof

      let R be Ring, E be R -homomorphic Ring, K be Subring of R, f be Function of R, E, g be Function of K, E such that

       A1: g = (f | the carrier of K) and

       A2: f is unity-preserving;

      

      thus (g . ( 1_ K)) = (f . ( 1_ K)) by A1, FUNCT_1: 49

      .= ( 1_ E) by A2, C0SP1:def 3;

    end;

    theorem :: RING_3:52

    for R be Ring, E be R -homomorphic Ring, K be Subring of R holds E is K -homomorphic

    proof

      let R be Ring, E be R -homomorphic Ring, K be Subring of R;

      consider f be Function of R, E such that

       A1: f is RingHomomorphism by RING_2:def 4;

      the carrier of K c= the carrier of R by C0SP1:def 3;

      then

      reconsider g = (f | the carrier of K) as Function of K, E by FUNCT_2: 32;

      take g;

      thus thesis by A1, Th48, Th49, Th50;

    end;

    theorem :: RING_3:53

    for R be Ring, E be R -homomorphic Ring, K be Subring of R, EK be K -homomorphic Ring holds for f be Homomorphism of R, E st E = EK holds (f | K) is Homomorphism of K, EK

    proof

      let R be Ring, E be R -homomorphic Ring, K be Subring of R;

      let EK be K -homomorphic Ring;

      let f be Homomorphism of R, E;

      the carrier of K c= the carrier of R by C0SP1:def 3;

      then

      reconsider g = (f | the carrier of K) as Function of K, E by FUNCT_2: 32;

      g = (f | K);

      hence thesis by Th48, Th49, Th50;

    end;

    theorem :: RING_3:54

    

     Th53: for F be Field, E be F -homomorphic Field, K be Subfield of F holds for f be Function of F, E, g be Function of K, E st g = (f | the carrier of K) & f is additive holds g is additive

    proof

      let F be Field, E be F -homomorphic Field, K be Subfield of F, f be Function of F, E, g be Function of K, E such that

       A1: g = (f | the carrier of K) and

       A2: f is additive;

      let x,y be Element of K;

      the carrier of K c= the carrier of F by EC_PF_1:def 1;

      then

      reconsider x1 = x, y1 = y as Element of F;

      

       A3: (x + y) = ((the addF of F || the carrier of K) . (x,y)) by EC_PF_1:def 1

      .= (x1 + y1) by Th1;

      

      thus (g . (x + y)) = (f . (x + y)) by A1, FUNCT_1: 49

      .= ((f . x1) + (f . y1)) by A2, A3

      .= ((g . x) + (f . y1)) by A1, FUNCT_1: 49

      .= ((g . x) + (g . y)) by A1, FUNCT_1: 49;

    end;

    theorem :: RING_3:55

    

     Th54: for F be Field, E be F -homomorphic Field, K be Subfield of F holds for f be Function of F, E, g be Function of K, E st g = (f | the carrier of K) & f is multiplicative holds g is multiplicative

    proof

      let F be Field, E be F -homomorphic Field, K be Subfield of F, f be Function of F, E, g be Function of K, E such that

       A1: g = (f | the carrier of K) and

       A2: f is multiplicative;

      let x,y be Element of K;

      the carrier of K c= the carrier of F by EC_PF_1:def 1;

      then

      reconsider x1 = x, y1 = y as Element of F;

      

       A3: (x * y) = ((the multF of F || the carrier of K) . (x,y)) by EC_PF_1:def 1

      .= (x1 * y1) by Th1;

      

      thus (g . (x * y)) = (f . (x * y)) by A1, FUNCT_1: 49

      .= ((f . x1) * (f . y1)) by A2, A3

      .= ((g . x) * (f . y1)) by A1, FUNCT_1: 49

      .= ((g . x) * (g . y)) by A1, FUNCT_1: 49;

    end;

    theorem :: RING_3:56

    

     Th55: for F be Field, E be F -homomorphic Field, K be Subfield of F holds for f be Function of F, E, g be Function of K, E st g = (f | the carrier of K) & f is unity-preserving holds g is unity-preserving

    proof

      let F be Field, E be F -homomorphic Field, K be Subfield of F, f be Function of F, E, g be Function of K, E such that

       A1: g = (f | the carrier of K) and

       A2: f is unity-preserving;

      

      thus (g . ( 1_ K)) = (f . ( 1_ K)) by A1, FUNCT_1: 49

      .= ( 1_ E) by A2, EC_PF_1:def 1;

    end;

    theorem :: RING_3:57

    

     Th56: for F be Field, E be F -homomorphic Field, K be Subfield of F holds E is K -homomorphic

    proof

      let F be Field, E be F -homomorphic Field, K be Subfield of F;

      consider f be Function of F, E such that

       A1: f is RingHomomorphism by RING_2:def 4;

      the carrier of K c= the carrier of F by EC_PF_1:def 1;

      then

      reconsider g = (f | the carrier of K) as Function of K, E by FUNCT_2: 32;

      take g;

      thus thesis by A1, Th53, Th54, Th55;

    end;

    theorem :: RING_3:58

    

     Th57: for F be Field, E be F -homomorphic Field, K be Subfield of F, EK be K -homomorphic Field holds for f be Homomorphism of F, E st E = EK holds (f | K) is Homomorphism of K, EK

    proof

      let F be Field, E be F -homomorphic Field, K be Subfield of F;

      let EK be K -homomorphic Field;

      let f be Homomorphism of F, E;

      the carrier of K c= the carrier of F by EC_PF_1:def 1;

      then

      reconsider g = (f | the carrier of K) as Function of K, E by FUNCT_2: 32;

      g = (f | K);

      hence thesis by Th53, Th54, Th55;

    end;

    notation

      let n be Nat;

      synonym Z/ n for INT.Ring n;

    end

    registration

      let n be Nat;

      cluster ( Z/ n) -> finite;

      coherence ;

    end

    registration

      let n be non trivial Nat;

      cluster ( Z/ n) -> non degenerated;

      coherence

      proof

        n >= (1 + 1) by NAT_2: 29;

        then n > 1 by NAT_1: 13;

        hence thesis by INT_3: 11;

      end;

    end

    registration

      let n be positive Nat;

      cluster ( Z/ n) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        (n + 1) > ( 0 + 1) by XREAL_1: 6;

        then

         A1: n >= 1 by NAT_1: 13;

        per cases by A1, XXREAL_0: 1;

          suppose n = 1;

          hence thesis by INT_3: 10;

        end;

          suppose n > 1;

          hence thesis by INT_3: 11;

        end;

      end;

    end

    registration

      let n be positive Nat;

      cluster ( Z/ n) -> associative well-unital distributive commutative;

      coherence

      proof

        (n + 1) > ( 0 + 1) by XREAL_1: 6;

        then

         A1: n >= 1 by NAT_1: 13;

        per cases by A1, XXREAL_0: 1;

          suppose n = 1;

          hence thesis by INT_3: 10;

        end;

          suppose n > 1;

          hence thesis by INT_3: 11;

        end;

      end;

    end

    registration

      let p be Prime;

      cluster ( Z/ p) -> almost_left_invertible;

      coherence ;

    end

    begin

    definition

      let R be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of R, i be Integer;

      :: RING_3:def2

      func i '*' a -> Element of R means

      : Def2: ex n be Nat st (i = n & it = (n * a)) or (i = ( - n) & it = ( - (n * a)));

      existence

      proof

        i in INT by INT_1:def 2;

        then

        consider n be Nat such that

         A1: i = n or i = ( - n) by INT_1:def 1;

        per cases by A1;

          suppose

           A2: i = n;

          take (n * a);

          thus thesis by A2;

        end;

          suppose

           A3: i = ( - n);

          take ( - (n * a));

          thus thesis by A3;

        end;

      end;

      uniqueness

      proof

        let x1,x2 be Element of R such that

         A4: ex n be Nat st (i = n & x1 = (n * a)) or (i = ( - n) & x1 = ( - (n * a))) and

         A5: ex n be Nat st (i = n & x2 = (n * a)) or (i = ( - n) & x2 = ( - (n * a)));

        i in INT by INT_1:def 2;

        then

        consider n be Nat such that

         A6: i = n or i = ( - n) by INT_1:def 1;

        per cases ;

          suppose

           A7: n = 0 ;

          then

           A8: x1 = ( 0. R) or x1 = ( - ( 0. R)) by A6, A4, BINOM: 12;

          x2 = ( 0. R) or x2 = ( - ( 0. R)) by A6, A5, A7, BINOM: 12;

          hence x1 = x2 by A8;

        end;

          suppose

           A9: n <> 0 ;

          per cases by A6;

            suppose i = n;

            hence x1 = x2 by A9, A5, A4;

          end;

            suppose i = ( - n);

            hence x1 = x2 by A5, A9, A4;

          end;

        end;

      end;

    end

    theorem :: RING_3:59

    

     Th58: for R be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of R holds ( 0 '*' a) = ( 0. R)

    proof

      let R be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of R;

      

      thus ( 0 '*' a) = ( 0 * a) by Def2

      .= ( 0. R) by BINOM: 12;

    end;

    theorem :: RING_3:60

    

     Th59: for R be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of R holds (1 '*' a) = a

    proof

      let R be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of R;

      

      thus (1 '*' a) = (1 * a) by Def2

      .= a by BINOM: 13;

    end;

    theorem :: RING_3:61

    

     Th60: for R be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of R holds (( - 1) '*' a) = ( - a)

    proof

      let R be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of R;

      (( - 1) '*' a) = ( - (1 * a)) by Def2

      .= ( - a) by BINOM: 13;

      hence thesis;

    end;

    

     Lm5: for R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i be Integer holds ((i + 1) '*' a) = ((i '*' a) + a)

    proof

      let R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i be Integer;

      i in INT by INT_1:def 2;

      then

      consider n be Nat such that

       A1: i = n or i = ( - n) by INT_1:def 1;

      per cases ;

        suppose

         A2: n = 0 ;

        

        hence ((i + 1) '*' a) = (( 0. R) + a) by A1, Th59

        .= ((i '*' a) + a) by A1, A2, Th58;

      end;

        suppose

         A3: n <> 0 ;

        per cases by A1;

          suppose

           A4: i = n;

          then

           A5: (i '*' a) = (n * a) by Def2;

          ((n + 1) * a) = ((n * a) + (1 * a)) by BINOM: 15

          .= ((n * a) + a) by BINOM: 13;

          hence ((i + 1) '*' a) = ((i '*' a) + a) by A4, A5, Def2;

        end;

          suppose

           A6: i = ( - n);

          reconsider n1 = (n - 1) as Element of NAT by INT_1: 3, A3;

          ((n1 + 1) * a) = ((n1 * a) + (1 * a)) by BINOM: 15

          .= ((n1 * a) + a) by BINOM: 13;

          

          then (i '*' a) = ( - ((n1 * a) + a)) by A6, Def2

          .= (( - (n1 * a)) + ( - a)) by RLVECT_1: 31;

          

          then

           A7: ((i '*' a) + a) = (( - (n1 * a)) + (( - a) + a)) by RLVECT_1:def 3

          .= (( - (n1 * a)) + ( 0. R)) by RLVECT_1: 5;

          (i + 1) = ( - (n - 1)) by A6;

          hence ((i + 1) '*' a) = ((i '*' a) + a) by Def2, A7;

        end;

      end;

    end;

    

     Lm6: for R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i be Integer holds ((i - 1) '*' a) = ((i '*' a) - a)

    proof

      let R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i be Integer;

      i in INT by INT_1:def 2;

      then

      consider n be Nat such that

       A1: i = n or i = ( - n) by INT_1:def 1;

      per cases ;

        suppose

         A2: n = 0 ;

        

        hence ((i - 1) '*' a) = (( 0. R) + ( - a)) by Th60, A1

        .= ((i '*' a) - a) by A1, A2, Th58;

      end;

        suppose

         A3: n <> 0 ;

        per cases by A1;

          suppose

           A4: i = ( - n);

          then (i - 1) = ( - (n + 1));

          

          hence ((i - 1) '*' a) = ( - ((n + 1) * a)) by Def2

          .= ( - ((n * a) + (1 * a))) by BINOM: 15

          .= ( - ((n * a) + a)) by BINOM: 13

          .= (( - (n * a)) + ( - a)) by RLVECT_1: 31

          .= ((i '*' a) - a) by A4, Def2;

        end;

          suppose

           A5: i = n;

          reconsider n1 = (n - 1) as Element of NAT by A3, INT_1: 3;

          ((n1 + 1) * a) = ((n1 * a) + (1 * a)) by BINOM: 15

          .= ((n1 * a) + a) by BINOM: 13;

          

          then ((i '*' a) - a) = (((n1 * a) + a) - a) by A5, Def2

          .= ((n1 * a) + (a + ( - a))) by RLVECT_1:def 3

          .= ((n1 * a) + ( 0. R)) by RLVECT_1: 5;

          hence ((i - 1) '*' a) = ((i '*' a) - a) by A5, Def2;

        end;

      end;

    end;

    theorem :: RING_3:62

    

     Th61: for R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i,j be Integer holds ((i + j) '*' a) = ((i '*' a) + (j '*' a))

    proof

      let R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i,j be Integer;

      defpred P[ Integer] means for k be Integer st k = $1 holds ((i + k) '*' a) = ((i '*' a) + (k '*' a));

      now

        let k be Integer;

        assume

         A1: k = 0 ;

        

        hence ((i + k) '*' a) = ((i '*' a) + ( 0. R))

        .= ((i '*' a) + (k '*' a)) by A1, Th58;

      end;

      then

       A2: P[ 0 ];

      

       A3: for u be Integer holds P[u] implies P[(u - 1)] & P[(u + 1)]

      proof

        let u be Integer;

        assume

         A4: P[u];

        now

          let k be Integer;

          assume k = (u - 1);

          

          then

           A5: ((i + (k + 1)) '*' a) = ((i '*' a) + ((k + 1) '*' a)) by A4

          .= ((i '*' a) + ((k '*' a) + a)) by Lm5

          .= (((i '*' a) + (k '*' a)) + a) by RLVECT_1:def 3;

          ((i + (k + 1)) '*' a) = (((i + k) + 1) '*' a)

          .= (((i + k) '*' a) + a) by Lm5;

          hence ((i + k) '*' a) = ((i '*' a) + (k '*' a)) by A5, RLVECT_1: 8;

        end;

        hence P[(u - 1)];

        now

          let k be Integer;

          assume k = (u + 1);

          

          then

           A6: ((i + (k - 1)) '*' a) = ((i '*' a) + ((k - 1) '*' a)) by A4

          .= ((i '*' a) + ((k '*' a) - a)) by Lm6

          .= (((i '*' a) + (k '*' a)) - a) by RLVECT_1:def 3;

          ((i + (k - 1)) '*' a) = (((i + k) - 1) '*' a)

          .= (((i + k) '*' a) - a) by Lm6;

          hence ((i + k) '*' a) = ((i '*' a) + (k '*' a)) by A6, RLVECT_1: 8;

        end;

        hence P[(u + 1)];

      end;

      for i be Integer holds P[i] from INT_1:sch 4( A2, A3);

      hence thesis;

    end;

    theorem :: RING_3:63

    

     Th62: for R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i be Integer holds (( - i) '*' a) = ( - (i '*' a))

    proof

      let R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i be Integer;

      defpred P[ Integer] means for k be Integer st k = $1 holds (( - k) '*' a) = ( - (k '*' a));

      now

        let k be Integer;

        assume

         A1: k = 0 ;

        

        hence (( - k) '*' a) = ( - ( 0. R)) by Th58

        .= ( - (k '*' a)) by A1, Th58;

      end;

      then

       A2: P[ 0 ];

      

       A3: for u be Integer holds P[u] implies P[(u - 1)] & P[(u + 1)]

      proof

        let u be Integer;

        assume

         A4: P[u];

        now

          let k be Integer;

          assume

           A5: k = (u - 1);

          

          hence (( - k) '*' a) = ((( 0 - u) + 1) '*' a)

          .= ((( 0 - u) '*' a) + a) by Lm5

          .= (( - (u '*' a)) + a) by A4

          .= ( - ((u '*' a) - a)) by RLVECT_1: 33

          .= ( - (k '*' a)) by Lm6, A5;

        end;

        hence P[(u - 1)];

        now

          let k be Integer;

          assume

           A6: k = (u + 1);

          

          hence (( - k) '*' a) = ((( 0 - u) - 1) '*' a)

          .= ((( 0 - u) '*' a) - a) by Lm6

          .= (( - (u '*' a)) - a) by A4

          .= ( - ((u '*' a) + a)) by RLVECT_1: 30

          .= ( - (k '*' a)) by Lm5, A6;

        end;

        hence P[(u + 1)];

      end;

      for i be Integer holds P[i] from INT_1:sch 4( A2, A3);

      hence thesis;

    end;

    theorem :: RING_3:64

    

     Th63: for R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i,j be Integer holds ((i - j) '*' a) = ((i '*' a) - (j '*' a))

    proof

      let R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i,j be Integer;

      

      thus ((i - j) '*' a) = ((i '*' a) + (( 0 - j) '*' a)) by Th61

      .= ((i '*' a) - (j '*' a)) by Th62;

    end;

    theorem :: RING_3:65

    

     Th64: for R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i,j be Integer holds ((i * j) '*' a) = (i '*' (j '*' a))

    proof

      let R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i,j be Integer;

      defpred P[ Integer] means for k be Integer st k = $1 holds ((k * j) '*' a) = (k '*' (j '*' a));

      now

        let k be Integer;

        assume

         A1: k = 0 ;

        

        hence ((k * j) '*' a) = ( 0. R) by Th58

        .= (k '*' (j '*' a)) by A1, Th58;

      end;

      then

       A2: P[ 0 ];

      

       A3: for u be Integer holds P[u] implies P[(u - 1)] & P[(u + 1)]

      proof

        let u be Integer;

        assume

         A4: P[u];

        now

          let k be Integer;

          assume

           A5: k = (u - 1);

          

          hence ((k * j) '*' a) = (((u * j) - j) '*' a)

          .= (((u * j) '*' a) - (j '*' a)) by Th63

          .= ((u '*' (j '*' a)) - (j '*' a)) by A4

          .= (k '*' (j '*' a)) by A5, Lm6;

        end;

        hence P[(u - 1)];

        now

          let k be Integer;

          assume

           A6: k = (u + 1);

          

          hence ((k * j) '*' a) = (((u * j) + j) '*' a)

          .= (((u * j) '*' a) + (j '*' a)) by Th61

          .= ((u '*' (j '*' a)) + (j '*' a)) by A4

          .= (k '*' (j '*' a)) by A6, Lm5;

        end;

        hence P[(u + 1)];

      end;

      for i be Integer holds P[i] from INT_1:sch 4( A2, A3);

      hence thesis;

    end;

    theorem :: RING_3:66

    for R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i,j be Integer holds (i '*' (j '*' a)) = (j '*' (i '*' a))

    proof

      let R be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, a be Element of R, i,j be Integer;

      

      thus (i '*' (j '*' a)) = ((i * j) '*' a) by Th64

      .= (j '*' (i '*' a)) by Th64;

    end;

    theorem :: RING_3:67

    

     Th66: for R be add-associative right_zeroed right_complementable Abelian left_unital distributive non empty doubleLoopStr, i,j be Integer holds ((i * j) '*' ( 1. R)) = ((i '*' ( 1. R)) * (j '*' ( 1. R)))

    proof

      let R be add-associative right_zeroed right_complementable Abelian left_unital distributive non empty doubleLoopStr, i,j be Integer;

      defpred P[ Integer] means for k be Integer st k = $1 holds ((k * j) '*' ( 1. R)) = ((k '*' ( 1. R)) * (j '*' ( 1. R)));

      now

        let k be Integer;

        assume

         A1: k = 0 ;

        

        hence ((k * j) '*' ( 1. R)) = (( 0. R) * (j '*' ( 1. R))) by Th58

        .= ((k '*' ( 1. R)) * (j '*' ( 1. R))) by A1, Th58;

      end;

      then

       A2: P[ 0 ];

      

       A3: for u be Integer holds P[u] implies P[(u - 1)] & P[(u + 1)]

      proof

        let u be Integer;

        assume

         A4: P[u];

        now

          let k be Integer;

          assume

           A5: k = (u - 1);

          

          hence ((k * j) '*' ( 1. R)) = (((u * j) - j) '*' ( 1. R))

          .= (((u * j) '*' ( 1. R)) - (j '*' ( 1. R))) by Th63

          .= (((u '*' ( 1. R)) * (j '*' ( 1. R))) - (j '*' ( 1. R))) by A4

          .= (((u '*' ( 1. R)) * (j '*' ( 1. R))) + ( - (( 1. R) * (j '*' ( 1. R)))))

          .= (((u '*' ( 1. R)) * (j '*' ( 1. R))) + (( - ( 1. R)) * (j '*' ( 1. R)))) by VECTSP_1: 9

          .= (((u '*' ( 1. R)) + ( - ( 1. R))) * (j '*' ( 1. R))) by VECTSP_1:def 3

          .= (((u '*' ( 1. R)) - (1 '*' ( 1. R))) * (j '*' ( 1. R))) by Th59

          .= ((k '*' ( 1. R)) * (j '*' ( 1. R))) by Th63, A5;

        end;

        hence P[(u - 1)];

        now

          let k be Integer;

          assume

           A6: k = (u + 1);

          

          hence ((k * j) '*' ( 1. R)) = (((u * j) + j) '*' ( 1. R))

          .= (((u * j) '*' ( 1. R)) + (j '*' ( 1. R))) by Th61

          .= (((u '*' ( 1. R)) * (j '*' ( 1. R))) + (j '*' ( 1. R))) by A4

          .= (((u '*' ( 1. R)) * (j '*' ( 1. R))) + (( 1. R) * (j '*' ( 1. R))))

          .= (((u '*' ( 1. R)) + ( 1. R)) * (j '*' ( 1. R))) by VECTSP_1:def 3

          .= (((u '*' ( 1. R)) + (1 '*' ( 1. R))) * (j '*' ( 1. R))) by Th59

          .= ((k '*' ( 1. R)) * (j '*' ( 1. R))) by Th61, A6;

        end;

        hence P[(u + 1)];

      end;

      for i be Integer holds P[i] from INT_1:sch 4( A2, A3);

      hence thesis;

    end;

    theorem :: RING_3:68

    for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds for a be Element of R, i be Integer holds (f . (i '*' a)) = (i '*' (f . a))

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      let a be Element of R, i be Integer;

      defpred P[ Integer] means for j be Integer st j = $1 holds (f . (j '*' a)) = (j '*' (f . a));

      now

        let j be Integer;

        assume

         A1: j = 0 ;

        

        hence (f . (j '*' a)) = (f . ( 0. R)) by Th58

        .= ( 0. S) by RING_2: 6

        .= (j '*' (f . a)) by A1, Th58;

      end;

      then

       A2: P[ 0 ];

      

       A3: for i be Integer holds P[i] implies P[(i - 1)] & P[(i + 1)]

      proof

        let i be Integer;

        assume

         A4: P[i];

        now

          let k be Integer;

          assume k = (i - 1);

          

          then

           A5: (f . ((k + 1) '*' a)) = ((k + 1) '*' (f . a)) by A4

          .= ((k '*' (f . a)) + (1 '*' (f . a))) by Th61

          .= ((k '*' (f . a)) + (f . a)) by Th59;

          (f . ((k + 1) '*' a)) = (f . ((k '*' a) + (1 '*' a))) by Th61

          .= (f . ((k '*' a) + a)) by Th59

          .= ((f . (k '*' a)) + (f . a)) by VECTSP_1:def 20;

          hence (f . (k '*' a)) = (k '*' (f . a)) by A5, RLVECT_1: 8;

        end;

        hence P[(i - 1)];

        now

          let k be Integer;

          assume k = (i + 1);

          

          then

           A6: (f . ((k - 1) '*' a)) = ((k - 1) '*' (f . a)) by A4

          .= ((k '*' (f . a)) + (( - ( 1. INT.Ring )) '*' (f . a))) by Th61

          .= ((k '*' (f . a)) - (f . a)) by Th60;

          (f . ((k - 1) '*' a)) = (f . ((k '*' a) + (( - ( 1. INT.Ring )) '*' a))) by Th61

          .= (f . ((k '*' a) - a)) by Th60

          .= ((f . (k '*' a)) - (f . a)) by RING_2: 8;

          hence (f . (k '*' a)) = (k '*' (f . a)) by A6, RLVECT_1: 8;

        end;

        hence P[(i + 1)];

      end;

      for i be Integer holds P[i] from INT_1:sch 4( A2, A3);

      hence thesis;

    end;

    begin

    definition

      let R,S be Ring;

      :: RING_3:def3

      attr S is R -monomorphic means

      : Def3: ex f be Function of R, S st f is RingHomomorphism monomorphism;

    end

    registration

      let R be Ring;

      cluster R -monomorphic for Ring;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

    end

    registration

      let R be comRing;

      cluster R -monomorphic for comRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -monomorphic for Ring;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

    end

    registration

      let R be domRing;

      cluster R -monomorphic for domRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -monomorphic for comRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -monomorphic for Ring;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

    end

    registration

      let R be Field;

      cluster R -monomorphic for Field;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -monomorphic for domRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -monomorphic for comRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -monomorphic for Ring;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

    end

    registration

      let R be Ring, S be R -monomorphic Ring;

      cluster additive multiplicative unity-preserving monomorphism for Function of R, S;

      existence

      proof

        consider f be Function of R, S such that

         A1: f is RingHomomorphism monomorphism by Def3;

        take f;

        thus f is additive by A1;

        thus f is multiplicative by A1;

        thus f is unity-preserving by A1;

        thus f is monomorphism by A1;

      end;

    end

    definition

      let R be Ring, S be R -monomorphic Ring;

      mode Monomorphism of R,S is additive multiplicative unity-preserving monomorphism Function of R, S;

    end

    registration

      let R be Ring, S be R -monomorphic Ring;

      cluster -> R -monomorphic for S -monomorphic Ring;

      coherence

      proof

        let T be S -monomorphic Ring;

        ( the Monomorphism of S, T * the Monomorphism of R, S) is monomorphism;

        hence thesis;

      end;

    end

    registration

      let R be Ring;

      cluster -> R -homomorphic for R -monomorphic Ring;

      coherence

      proof

        let S be R -monomorphic Ring;

        ex f be Function of R, S st f is RingHomomorphism monomorphism by Def3;

        hence thesis;

      end;

    end

    registration

      let R be Ring;

      let S be R -monomorphic Ring;

      let f be Monomorphism of R, S;

      reduce ((f " ) " ) to f;

      reducibility by FUNCT_1: 43;

    end

    theorem :: RING_3:69

    

     Th68: for R be Ring, S be R -homomorphic Ring, T be S -homomorphic Ring holds for f be Homomorphism of R, S holds for g be Homomorphism of S, T holds ( ker f) c= ( ker (g * f))

    proof

      let R be Ring, S be R -homomorphic Ring, T be S -homomorphic Ring;

      let f be Homomorphism of R, S;

      let g be Homomorphism of S, T;

      now

        let x be object;

        assume x in ( ker f);

        then

        consider r be Element of R such that

         A1: x = r & (f . r) = ( 0. S);

        ((g * f) . r) = (g . (f . r)) by FUNCT_2: 15

        .= ( 0. T) by A1, RING_2: 6;

        hence x in ( ker (g * f)) by A1;

      end;

      hence thesis;

    end;

    theorem :: RING_3:70

    

     Th69: for R be Ring, S be R -homomorphic Ring, T be S -monomorphic Ring holds for f be Homomorphism of R, S holds for g be Monomorphism of S, T holds ( ker f) = ( ker (g * f))

    proof

      let R be Ring, S be R -homomorphic Ring, T be S -monomorphic Ring;

      let f be Homomorphism of R, S;

      let g be Monomorphism of S, T;

      

       A1: ( ker g) = {( 0. S)} by RING_2: 12;

      now

        let x be object;

        assume x in ( ker (g * f));

        then

        consider r be Element of R such that

         A2: x = r & ((g * f) . r) = ( 0. T);

        (g . (f . r)) = ( 0. T) by A2, FUNCT_2: 15;

        then (f . r) in {( 0. S)} by A1;

        then (f . r) = ( 0. S) by TARSKI:def 1;

        hence x in ( ker f) by A2;

      end;

      then ( ker (g * f)) c= ( ker f);

      hence thesis by Th68;

    end;

    theorem :: RING_3:71

    

     Th70: for R be Ring, S be Subring of R holds R is S -monomorphic

    proof

      let R be Ring, S be Subring of R;

      the carrier of S c= the carrier of R by C0SP1:def 3;

      then

      reconsider f = ( id S) as Function of S, R by FUNCT_2: 7;

       A1:

      now

        let x,y be Element of S;

        

         A2: [x, y] in [:the carrier of S, the carrier of S:];

        

        thus (f . (x + y)) = ((the addF of R || the carrier of S) . (x,y)) by C0SP1:def 3

        .= ((f . x) + (f . y)) by A2, FUNCT_1: 49;

      end;

       A3:

      now

        let x,y be Element of S;

        

         A4: [x, y] in [:the carrier of S, the carrier of S:];

        

        thus (f . (x * y)) = ((the multF of R || the carrier of S) . (x,y)) by C0SP1:def 3

        .= ((f . x) * (f . y)) by A4, FUNCT_1: 49;

      end;

      (f . ( 1_ S)) = ( 1_ R) by C0SP1:def 3;

      then f is RingHomomorphism by A1, A3, VECTSP_1:def 20, GROUP_1:def 13, GROUP_6:def 6;

      hence thesis;

    end;

    theorem :: RING_3:72

    

     Th71: for R,S be Ring holds S is R -monomorphic Ring iff S includes R

    proof

      let R,S be Ring;

       A1:

      now

        assume S is R -monomorphic;

        then

        reconsider T = S as R -monomorphic Ring;

        set f = the Monomorphism of R, T;

        ( ker f) = {( 0. R)} by RING_2: 12;

        then

         A2: ((R / ( ker f)),R) are_isomorphic by RING_2: 17;

        ((R / ( ker f)),( Image f)) are_isomorphic by RING_2: 15;

        hence S includes R by Th43, A2;

      end;

      now

        assume S includes R;

        then

        consider T be Subring of S such that

         A3: (T,R) are_isomorphic ;

        consider f be Function of R, T such that

         A4: f is isomorphism by A3, QUOFIELD:def 23;

        

         A5: f is additive multiplicative unity-preserving one-to-one by A4;

        the carrier of T c= the carrier of S by C0SP1:def 3;

        then

        reconsider g = f as Function of R, S by FUNCT_2: 7;

        now

          let x,y be Element of R;

          

           A6: [(f . x), (f . y)] in [:the carrier of T, the carrier of T:];

          

          thus (g . (x + y)) = ((f . x) + (f . y)) by A5

          .= ((the addF of S || the carrier of T) . ((f . x),(f . y))) by C0SP1:def 3

          .= ((g . x) + (g . y)) by A6, FUNCT_1: 49;

        end;

        then

         A7: g is additive;

        now

          let x,y be Element of R;

          

           A8: [(f . x), (f . y)] in [:the carrier of T, the carrier of T:];

          

          thus (g . (x * y)) = ((f . x) * (f . y)) by A5

          .= ((the multF of S || the carrier of T) . ((f . x),(f . y))) by C0SP1:def 3

          .= ((g . x) * (g . y)) by A8, FUNCT_1: 49;

        end;

        then

         A9: g is multiplicative;

        g is unity-preserving by A5, C0SP1:def 3;

        hence S is R -monomorphic by A7, A9, A4;

      end;

      hence thesis by A1;

    end;

    definition

      let R,S be Ring;

      :: RING_3:def4

      attr S is R -isomorphic means

      : Def4: ex f be Function of R, S st f is RingHomomorphism isomorphism;

    end

    registration

      let R be Ring;

      cluster R -isomorphic for Ring;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

    end

    registration

      let R be comRing;

      cluster R -isomorphic for comRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -isomorphic for Ring;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

    end

    registration

      let R be domRing;

      cluster R -isomorphic for domRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -isomorphic for comRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -isomorphic for Ring;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

    end

    registration

      let R be Field;

      cluster R -isomorphic for Field;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -isomorphic for domRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -isomorphic for comRing;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

      cluster R -isomorphic for Ring;

      existence

      proof

        take R;

        take ( id R);

        thus thesis;

      end;

    end

    registration

      let R be Ring, S be R -isomorphic Ring;

      cluster additive multiplicative unity-preserving isomorphism for Function of R, S;

      existence

      proof

        consider f be Function of R, S such that

         A1: f is RingHomomorphism isomorphism by Def4;

        take f;

        thus f is additive by A1;

        thus f is multiplicative by A1;

        thus f is unity-preserving by A1;

        thus f is isomorphism by A1;

      end;

    end

    definition

      let R be Ring, S be R -isomorphic Ring;

      mode Isomorphism of R,S is additive multiplicative unity-preserving isomorphism Function of R, S;

    end

    definition

      let R be Ring;

      let S be R -isomorphic Ring;

      let f be Isomorphism of R, S;

      :: original: "

      redefine

      func f " -> Function of S, R ;

      coherence

      proof

        ( rng f) = the carrier of S by FUNCT_2:def 3;

        then

        reconsider g = (f " ) as Function of the carrier of S, the carrier of R by FUNCT_2: 25;

        g is Function of S, R;

        hence thesis;

      end;

    end

    

     Lm7: for R be Ring, S be R -isomorphic Ring, f be Isomorphism of R, S holds (f " ) is additive multiplicative unity-preserving isomorphism

    proof

      let R be Ring, S be R -isomorphic Ring, f be Isomorphism of R, S;

      set g = (f " );

      

       A1: ( rng f) = the carrier of S by FUNCT_2:def 3;

      now

        let a,b be Element of S;

        consider x be object such that

         A2: x in the carrier of R & a = (f . x) by A1, FUNCT_2: 11;

        reconsider x as Element of R by A2;

        consider y be object such that

         A3: y in the carrier of R & b = (f . y) by A1, FUNCT_2: 11;

        reconsider y as Element of R by A3;

        

        thus ((g . a) + (g . b)) = (x + (g . (f . y))) by A2, A3, FUNCT_2: 26

        .= (x + y) by FUNCT_2: 26

        .= (g . (f . (x + y))) by FUNCT_2: 26

        .= (g . (a + b)) by A2, A3, VECTSP_1:def 20;

      end;

      hence

       A4: g is additive;

      now

        let a,b be Element of S;

        consider x be object such that

         A5: x in the carrier of R & a = (f . x) by A1, FUNCT_2: 11;

        reconsider x as Element of R by A5;

        consider y be object such that

         A6: y in the carrier of R & b = (f . y) by A1, FUNCT_2: 11;

        reconsider y as Element of R by A6;

        

        thus ((g . a) * (g . b)) = (x * (g . (f . y))) by A5, A6, FUNCT_2: 26

        .= (x * y) by FUNCT_2: 26

        .= (g . (f . (x * y))) by FUNCT_2: 26

        .= (g . (a * b)) by A5, A6, GROUP_6:def 6;

      end;

      hence

       A7: g is multiplicative;

      ( 1. R) = (g . (f . ( 1_ R))) by FUNCT_2: 26

      .= (g . ( 1_ S)) by GROUP_1:def 13

      .= (g . ( 1. S));

      hence

       A8: g is unity-preserving;

      now

        let x be object;

        now

          assume x in the carrier of R;

          then

          reconsider x1 = x as Element of R;

          (f . x1) in the carrier of S;

          then

           A9: (f . x1) in ( dom g) by FUNCT_2:def 1;

          (g . (f . x1)) = x1 by FUNCT_2: 26;

          hence x in ( rng g) by A9, FUNCT_1:def 3;

        end;

        hence x in ( rng g) iff x in the carrier of R;

      end;

      then g is onto by FUNCT_2:def 3, TARSKI: 2;

      hence thesis by A8, A4, A7;

    end;

    registration

      let R be Ring, S be R -isomorphic Ring;

      cluster additive multiplicative unity-preserving isomorphism for Function of S, R;

      existence

      proof

        take ( the Isomorphism of R, S " );

        thus thesis by Lm7;

      end;

    end

    definition

      let R be Ring, S be R -isomorphic Ring;

      mode Isomorphism of S,R is additive multiplicative unity-preserving isomorphism Function of S, R;

    end

    registration

      let R be Ring, S be R -isomorphic Ring;

      cluster -> R -isomorphic for S -isomorphic Ring;

      coherence

      proof

        let T be S -isomorphic Ring;

        ( the Isomorphism of S, T * the Isomorphism of R, S) is onto by FUNCT_2: 27;

        hence thesis;

      end;

    end

    registration

      let R be Ring;

      cluster -> R -monomorphic for R -isomorphic Ring;

      coherence

      proof

        let S be R -isomorphic Ring;

         the Isomorphism of R, S is additive multiplicative unity-preserving monomorphism;

        hence thesis;

      end;

    end

    theorem :: RING_3:73

    

     Th72: for R be Ring, S be R -isomorphic Ring, f be Isomorphism of R, S holds (f " ) is Isomorphism of S, R by Lm7;

    theorem :: RING_3:74

    for R be Ring, S be R -isomorphic Ring holds R is S -isomorphic

    proof

      let R be Ring, S be R -isomorphic Ring;

      ( the Isomorphism of R, S " ) is additive multiplicative unity-preserving monomorphism epimorphism by Th72;

      hence thesis;

    end;

    registration

      let R be comRing;

      cluster -> commutative for R -isomorphic Ring;

      coherence

      proof

        let S be R -isomorphic Ring;

        set f = the Isomorphism of R, S;

        reconsider g = (f " ) as Isomorphism of S, R by Lm7;

        

         A1: (g " ) = f;

        now

          let a,b be Element of the carrier of S;

          

          thus (a * b) = (f . (g . (a * b))) by A1, FUNCT_2: 26

          .= (f . ((g . a) * (g . b))) by GROUP_6:def 6

          .= (f . (g . (b * a))) by GROUP_6:def 6

          .= (b * a) by A1, FUNCT_2: 26;

        end;

        hence S is commutative;

      end;

    end

    registration

      let R be domRing;

      cluster -> non degenerated domRing-like for R -isomorphic Ring;

      coherence

      proof

        let S be R -isomorphic Ring;

        set f = the Isomorphism of R, S;

        reconsider g = (f " ) as Isomorphism of S, R by Lm7;

        

         A1: (g " ) = f;

        now

          assume

           A2: S is degenerated;

          ( 1. R) = ((f " ) . (f . ( 1_ R))) by FUNCT_2: 26

          .= ((f " ) . ( 1_ S)) by GROUP_1:def 13

          .= ((f " ) . (f . ( 0. R))) by A2, RING_2: 6

          .= ( 0. R) by FUNCT_2: 26;

          hence contradiction;

        end;

        hence S is non degenerated;

        now

          let x,y be Element of S;

          assume

           A3: (x * y) = ( 0. S);

          

           A4: ( 0. R) = (g . ( 0. S)) by RING_2: 6

          .= ((g . x) * (g . y)) by A3, GROUP_6:def 6;

          per cases by A4, VECTSP_2:def 1;

            suppose (g . x) = ( 0. R);

            

            then ( 0. S) = (f . (g . x)) by RING_2: 6

            .= x by A1, FUNCT_2: 26;

            hence x = ( 0. S) or y = ( 0. S);

          end;

            suppose (g . y) = ( 0. R);

            

            then ( 0. S) = (f . (g . y)) by RING_2: 6

            .= y by A1, FUNCT_2: 26;

            hence x = ( 0. S) or y = ( 0. S);

          end;

        end;

        hence thesis by VECTSP_2:def 1;

      end;

    end

    registration

      let F be Field;

      cluster -> almost_left_invertible for F -isomorphic Ring;

      coherence

      proof

        let K be F -isomorphic Ring;

        set f = the Isomorphism of F, K;

        reconsider g = (f " ) as Isomorphism of K, F by Lm7;

        

         A1: (g " ) = f;

        now

          let x be Element of K;

          assume

           A2: x <> ( 0. K);

          now

            assume (g . x) = ( 0. F);

            then (g . x) = (g . ( 0. K)) by RING_2: 6;

            hence contradiction by A2, FUNCT_2: 19;

          end;

          then

          consider a be Element of F such that

           A3: (a * (g . x)) = ( 1. F) by VECTSP_1:def 9;

          ( 1. K) = ( 1_ K)

          .= (f . ( 1_ F)) by GROUP_1:def 13

          .= ((f . a) * (f . (g . x))) by A3, GROUP_6:def 6

          .= ((f . a) * x) by A1, FUNCT_2: 26;

          hence ex y be Element of K st (y * x) = ( 1. K);

        end;

        hence thesis;

      end;

    end

    theorem :: RING_3:75

    for E,F be Field holds E includes F iff ex K be strict Subfield of E st (K,F) are_isomorphic

    proof

      let E,F be Field;

      hereby

        assume

         A1: E includes F;

        reconsider EE = E as Ring;

        consider K be strict Subring of EE such that

         A2: (K,F) are_isomorphic by A1;

        ex f be Function of F, K st f is RingIsomorphism by A2, QUOFIELD:def 23;

        then

        reconsider KK = K as F -isomorphic Ring by Def4;

        the carrier of KK c= the carrier of E & the addF of KK = (the addF of E || the carrier of KK) & the multF of KK = (the multF of E || the carrier of KK) & ( 1. E) = ( 1. KK) & ( 0. E) = ( 0. KK) by C0SP1:def 3;

        then KK is strict Subfield of E by EC_PF_1:def 1;

        hence ex K be strict Subfield of E st (K,F) are_isomorphic by A2;

      end;

      given K be strict Subfield of E such that

       A3: (K,F) are_isomorphic ;

      the carrier of K c= the carrier of E & the addF of K = (the addF of E || the carrier of K) & the multF of K = (the multF of E || the carrier of K) & ( 1. E) = ( 1. K) & ( 0. E) = ( 0. K) by EC_PF_1:def 1;

      then K is strict Subring of E by C0SP1:def 3;

      hence E includes F by A3;

    end;

    begin

    definition

      let R be Ring;

      :: RING_3:def5

      func Char R -> Nat means

      : Def5: ((it '*' ( 1. R)) = ( 0. R) & it <> 0 & for m be positive Nat st m < it holds (m '*' ( 1. R)) <> ( 0. R)) or (it = 0 & for m be positive Nat holds (m '*' ( 1. R)) <> ( 0. R));

      existence

      proof

        per cases ;

          suppose

           A1: for m be positive Nat holds (m '*' ( 1. R)) <> ( 0. R);

          take 0 ;

          thus thesis by A1;

        end;

          suppose

           A2: ex m be positive Nat st (m '*' ( 1. R)) = ( 0. R);

          defpred P[ Nat] means $1 <> 0 & ($1 '*' ( 1. R)) = ( 0. R);

          

           A3: ex k be Nat st P[k] by A2;

          ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A3);

          then

          consider k be Nat such that

           A4: P[k] & for n be Nat st P[n] holds k <= n;

          take k;

          thus thesis by A4;

        end;

      end;

      uniqueness

      proof

        let n1,n2 be Nat such that

         A5: ((n1 '*' ( 1. R)) = ( 0. R) & n1 <> 0 & for m be positive Nat st m < n1 holds (m '*' ( 1. R)) <> ( 0. R)) or (n1 = 0 & for m be positive Nat holds (m '*' ( 1. R)) <> ( 0. R)) and

         A6: ((n2 '*' ( 1. R)) = ( 0. R) & n2 <> 0 & for m be positive Nat st m < n2 holds (m '*' ( 1. R)) <> ( 0. R)) or (n2 = 0 & for m be positive Nat holds (m '*' ( 1. R)) <> ( 0. R));

        per cases ;

          suppose n1 = 0 ;

          hence thesis by A5, A6;

        end;

          suppose n1 <> 0 ;

           not (n1 < n2) & not (n2 < n1) by A6, A5;

          hence n1 = n2 by XXREAL_0: 1;

        end;

      end;

    end

    definition

      let n be Nat;

      let R be Ring;

      :: RING_3:def6

      attr R is n -characteristic means

      : Def6: ( Char R) = n;

    end

    

     Lm8: for i be Integer holds (i '*' ( 1. INT.Ring )) = i

    proof

      let i be Integer;

      set R = INT.Ring ;

      defpred P[ Integer] means for k be Integer st k = $1 holds k = (k '*' ( 1. R));

      ( 0 '*' ( 1. R)) = ( 0. R) by Th58;

      then

       A1: P[ 0 ];

       A2:

      now

        let u be Integer;

        assume

         A3: P[u];

        ((u - 1) '*' ( 1. R)) = ((u '*' ( 1. R)) - ( 1. R)) by Lm6

        .= (u - 1) by A3;

        hence P[(u - 1)];

        ((u + 1) '*' ( 1. R)) = ((u '*' ( 1. R)) + ( 1. R)) by Lm5

        .= (u + 1) by A3;

        hence P[(u + 1)];

      end;

      for k be Integer holds P[k] from INT_1:sch 4( A1, A2);

      hence (i '*' ( 1. INT.Ring )) = i;

    end;

    theorem :: RING_3:76

    

     Th75: ( Char INT.Ring ) = 0

    proof

      for n be positive Nat holds (n '*' ( 1. INT.Ring )) <> ( 0. INT.Ring ) by Lm8;

      hence thesis by Def5;

    end;

    theorem :: RING_3:77

    

     Th76: for n be positive Nat holds ( Char ( Z/ n)) = n

    proof

      let n be positive Nat;

      set R = ( Z/ n);

      per cases by NAT_1: 25;

        suppose

         A1: n = 1;

        then

         A2: (1 '*' ( 1. R)) = ( 0. R) by Th59, INT_3: 10;

        for n be positive Nat st n < 1 holds (n '*' ( 1. R)) <> ( 0. R) by NAT_1: 14;

        hence thesis by A2, A1, Def5;

      end;

        suppose

         A3: n > 1;

        reconsider m = (n - 1) as Nat;

        (n - 1) < (n - 0 ) by XREAL_1: 15;

        then

        reconsider mm = m as Element of ( Segm n) by NAT_1: 44;

        reconsider e = 1 as Element of ( Segm n) by A3, NAT_1: 44;

        

         A4: (1 '*' ( 1. R)) = ( 1. R) by Th59

        .= 1 by INT_3: 14, A3;

        

         A5: for k be Nat st k <= m holds (k '*' ( 1. R)) = k

        proof

          let k be Nat;

          assume

           A6: k <= m;

          defpred P[ Nat] means ($1 '*' ( 1. R)) = $1;

          reconsider u = m as Element of NAT by INT_1: 3;

          ( 0 '*' ( 1. R)) = ( 0. R) by Th58

          .= 0 by NAT_1: 44, SUBSET_1:def 8;

          then

           A7: P[ 0 ];

          

           A8: for k be Element of NAT st 0 <= k & k < u holds P[k] implies P[(k + 1)]

          proof

            let k be Element of NAT ;

            assume

             A9: 0 <= k & k < u;

            assume

             A10: P[k];

            reconsider z = (k '*' ( 1. R)) as Element of ( Segm n);

            

             A11: (k + 1) < (m + 1) by A9, XREAL_1: 6;

            ((k + 1) '*' ( 1. R)) = ((k '*' ( 1. R)) + ( 1. R)) by Lm5

            .= ((k '*' ( 1. R)) + (1 '*' ( 1. R))) by Th59

            .= (k + 1) by INT_3: 7, A11, A10, A4;

            hence P[(k + 1)];

          end;

          

           A12: for i be Element of NAT st 0 <= i & i <= u holds P[i] from INT_1:sch 7( A7, A8);

          k is Element of NAT by INT_1: 3;

          hence thesis by A12, A6;

        end;

        

         A13: (n '*' ( 1. R)) = ((m + 1) '*' ( 1. R))

        .= ((m '*' ( 1. R)) + ( 1. R)) by Lm5

        .= ((m '*' ( 1. R)) + (1 '*' ( 1. R))) by Th59

        .= (( addint n) . (mm,e)) by A4, A5

        .= ((m + 1) mod n) by GR_CY_1:def 4

        .= 0 by INT_1: 50

        .= ( 0. R) by NAT_1: 44, SUBSET_1:def 8;

        now

          let k be positive Nat;

          assume k < n;

          then k < (m + 1);

          then

           A14: k <= m by NAT_1: 13;

          now

            assume (k '*' ( 1. R)) = ( 0. R);

            

            then k = ( 0. R) by A5, A14

            .= 0 by NAT_1: 44, SUBSET_1:def 8;

            hence contradiction;

          end;

          hence (k '*' ( 1. R)) <> ( 0. R);

        end;

        hence thesis by A13, Def5;

      end;

    end;

    registration

      cluster INT.Ring -> 0 -characteristic;

      coherence by Th75;

    end

    registration

      let n be positive Nat;

      cluster ( Z/ n) -> n -characteristic;

      coherence by Th76;

    end

    registration

      let n be Nat;

      cluster n -characteristic for comRing;

      existence

      proof

        per cases ;

          suppose n = 0 ;

          hence thesis by Th75;

        end;

          suppose n <> 0 ;

          then

          reconsider k = n as positive Nat;

          ( Char ( Z/ k)) = k by Th76;

          hence thesis;

        end;

      end;

    end

    registration

      let n be positive Nat;

      let R be n -characteristic Ring;

      cluster ( Char R) -> positive;

      coherence by Def6;

    end

    definition

      let R be Ring;

      :: RING_3:def7

      func CharSet R -> Subset of NAT equals { n where n be positive Nat : (n '*' ( 1. R)) = ( 0. R) };

      coherence

      proof

        set M = { n where n be positive Nat : (n '*' ( 1. R)) = ( 0. R) };

        now

          let x be object;

          assume x in M;

          then

          consider k be positive Nat such that

           A1: x = k & (k '*' ( 1. R)) = ( 0. R);

          thus x in NAT by A1, ORDINAL1:def 12;

        end;

        then M c= NAT ;

        hence thesis;

      end;

    end

    registration

      let n be positive Nat, R be n -characteristic Ring;

      cluster ( CharSet R) -> non empty;

      coherence

      proof

        ( Char R) = n by Def6;

        then (n '*' ( 1. R)) = ( 0. R) & n <> 0 & for m be positive Nat st m < n holds (m '*' ( 1. R)) <> ( 0. R) by Def5;

        then n in { k where k be positive Nat : (k '*' ( 1. R)) = ( 0. R) };

        hence thesis;

      end;

    end

    theorem :: RING_3:78

    

     Th77: for R be Ring holds ( Char R) = 0 iff ( CharSet R) = {}

    proof

      let R be Ring;

       A1:

      now

        assume

         A2: ( Char R) = 0 ;

        now

          let x be object;

          assume x in ( CharSet R);

          then ex n be positive Nat st x = n & (n '*' ( 1. R)) = ( 0. R);

          hence contradiction by A2, Def5;

        end;

        hence ( CharSet R) = {} by XBOOLE_0:def 1;

      end;

      now

        assume

         A3: ( CharSet R) = {} ;

        now

          assume ex m be positive Nat st (m '*' ( 1. R)) = ( 0. R);

          then

          consider m be positive Nat such that

           A4: (m '*' ( 1. R)) = ( 0. R);

          m in { k where k be positive Nat : (k '*' ( 1. R)) = ( 0. R) } by A4;

          hence contradiction by A3;

        end;

        hence ( Char R) = 0 by Def5;

      end;

      hence thesis by A1;

    end;

    theorem :: RING_3:79

    

     Th78: for n be positive Nat, R be n -characteristic Ring holds ( Char R) = ( min ( CharSet R))

    proof

      let n be positive Nat, R be n -characteristic Ring;

      set M = ( CharSet R);

      

       A1: n = ( Char R) by Def6;

      (n '*' ( 1. R)) = ( 0. R) & n <> 0 & for m be positive Nat st m < n holds (m '*' ( 1. R)) <> ( 0. R) by A1, Def5;

      then

       A2: n in M;

      now

        let x be ExtReal;

        assume x in M;

        then

        consider m be positive Nat such that

         A3: x = m & (m '*' ( 1. R)) = ( 0. R);

        thus n <= x by A3, A1, Def5;

      end;

      hence thesis by A2, A1, XXREAL_2:def 7;

    end;

    theorem :: RING_3:80

    

     Th79: for R be Ring holds ( Char R) = ( min* ( CharSet R))

    proof

      let R be Ring;

      set n = ( Char R);

      per cases ;

        suppose

         A1: ( Char R) = 0 ;

        then ( CharSet R) = {} by Th77;

        hence thesis by A1, NAT_1:def 1;

      end;

        suppose ( Char R) > 0 ;

        then

        reconsider n1 = n as positive Nat;

        reconsider R1 = R as n1 -characteristic Ring by Def6;

        

         A2: ( Char R) = ( Char R1) = ( min ( CharSet R1)) by Th78;

        then

         A3: n in ( CharSet R) by XXREAL_2:def 7;

        for k be Nat st k in ( CharSet R) holds n <= k by A2, XXREAL_2:def 7;

        hence thesis by A3, NAT_1:def 1;

      end;

    end;

    theorem :: RING_3:81

    for p be Prime, R be p -characteristic Ring, n be positive Nat holds n is Element of ( CharSet R) iff p divides n

    proof

      let p be Prime, R be p -characteristic Ring, j be positive Nat;

      

       A1: ( Char R) = p by Def6;

      then

       A2: (p '*' ( 1. R)) = ( 0. R) by Def5;

       A3:

      now

        assume

         A4: j is Element of ( CharSet R);

        

         A5: (((j div p) * p) '*' ( 1. R)) = (((j div p) '*' ( 1. R)) * (p '*' ( 1. R))) by Th66

        .= ( 0. R) by A2;

        

         A6: (j '*' ( 1. R)) = ((((j div p) * p) + (j mod p)) '*' ( 1. R)) by INT_1: 59

        .= (( 0. R) + ((j mod p) '*' ( 1. R))) by A5, Th61

        .= ((j mod p) '*' ( 1. R));

        j in { k where k be positive Nat : (k '*' ( 1. R)) = ( 0. R) } by A4;

        then

        consider l be positive Nat such that

         A7: l = j & (l '*' ( 1. R)) = ( 0. R);

        now

          assume (j mod p) > 0 ;

          then

          reconsider l = (j mod p) as positive Nat;

          

           A8: l in { k where k be positive Nat : (k '*' ( 1. R)) = ( 0. R) } by A7, A6;

          p = ( min ( CharSet R)) by A1, Th78;

          then p <= (j mod p) by A8, XXREAL_2:def 7;

          hence contradiction by INT_1: 58;

        end;

        then

         A9: (j mod p) = 0 ;

        j = (((j div p) * p) + (j mod p)) by INT_1: 59;

        hence p divides j by A9;

      end;

      now

        assume p divides j;

        then

        consider i be Integer such that

         A10: j = (p * i);

        (j '*' ( 1. R)) = ((p '*' ( 1. R)) * (i '*' ( 1. R))) by A10, Th66

        .= (( 0. R) * (i '*' ( 1. R))) by A1, Def5

        .= ( 0. R);

        then j in { k where k be positive Nat : (k '*' ( 1. R)) = ( 0. R) };

        hence j is Element of ( CharSet R);

      end;

      hence thesis by A3;

    end;

    definition

      let R be Ring;

      :: RING_3:def8

      func canHom_Int R -> Function of INT.Ring , R means

      : Def8: for x be Element of INT.Ring holds (it . x) = (x '*' ( 1. R));

      existence

      proof

        defpred P[ object, object] means ex a be Element of I st $1 = a & $2 = (a '*' ( 1. R));

        

         A1: for x be object st x in the carrier of I holds ex y be object st y in the carrier of R & P[x, y]

        proof

          let x be object;

          assume x in the carrier of I;

          then

          reconsider a = x as Element of I;

          take (a '*' ( 1. R));

          thus thesis;

        end;

        consider g be Function of the carrier of I, the carrier of R such that

         A2: for x be object st x in the carrier of I holds P[x, (g . x)] from FUNCT_2:sch 1( A1);

        now

          let x be Element of I;

          consider a be Element of I such that

           A3: x = a & (g . x) = (a '*' ( 1. R)) by A2;

          thus (g . x) = (x '*' ( 1. R)) by A3;

        end;

        then

        consider f be Function of I, R such that

         A4: for x be Element of I holds (f . x) = (x '*' ( 1. R));

        take f;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let g1,g2 be Function of I, R such that

         A5: for a be Element of I holds (g1 . a) = (a '*' ( 1. R)) and

         A6: for a be Element of I holds (g2 . a) = (a '*' ( 1. R));

        let a be Element of I;

        

        thus (g1 . a) = (a '*' ( 1. R)) by A5

        .= (g2 . a) by A6;

      end;

    end

    registration

      let R be Ring;

      cluster ( canHom_Int R) -> additive multiplicative unity-preserving;

      coherence

      proof

        set g = ( canHom_Int R);

        now

          let x,y be Element of I;

          

          thus (g . (x + y)) = ((x + y) '*' ( 1. R)) by Def8

          .= ((x '*' ( 1. R)) + (y '*' ( 1. R))) by Th61

          .= ((g . x) + (y '*' ( 1. R))) by Def8

          .= ((g . x) + (g . y)) by Def8;

        end;

        hence g is additive;

        now

          let x,y be Element of I;

          reconsider x1 = x, y1 = y as Integer;

          

          thus (g . (x * y)) = ((x * y) '*' ( 1. R)) by Def8

          .= ((x1 '*' ( 1. R)) * (y1 '*' ( 1. R))) by Th66

          .= ((g . x) * (y '*' ( 1. R))) by Def8

          .= ((g . x) * (g . y)) by Def8;

        end;

        hence g is multiplicative;

        (g . ( 1_ I)) = (1 '*' ( 1. R)) by Def8

        .= ( 1_ R) by Th59;

        hence thesis;

      end;

    end

    registration

      cluster -> INT.Ring -homomorphic for Ring;

      coherence

      proof

        let R be Ring;

        ( canHom_Int R) is additive multiplicative unity-preserving;

        hence thesis;

      end;

    end

    theorem :: RING_3:82

    

     Th81: for R be Ring, n be non negative Element of INT.Ring holds ( Char R) = n iff ( ker ( canHom_Int R)) = ( {n} -Ideal )

    proof

      let R be Ring, n be non negative Element of INT.Ring ;

      set f = ( canHom_Int R);

      reconsider k = n as Integer;

       A1:

      now

        assume

         A2: ( Char R) = n;

        reconsider k as Nat;

        per cases ;

          suppose

           A3: k = 0 ;

          then

           A4: ( {n} -Ideal ) = {( 0. I)} by IDEAL_1: 47;

          now

            let x1,x2 be object;

            assume

             A5: x1 in the carrier of I & x2 in the carrier of I & (f . x1) = (f . x2);

            then

            reconsider y1 = x1, y2 = x2 as Integer;

            (y1 '*' ( 1. R)) = (f . y1) by A5, Def8

            .= (y2 '*' ( 1. R)) by A5, Def8;

            

            then

             A6: ( 0. R) = ((y1 '*' ( 1. R)) - (y2 '*' ( 1. R))) by RLVECT_1: 15

            .= ((y1 - y2) '*' ( 1. R)) by Th63;

            now

              assume (y1 - y2) <> 0 ;

              then

               A7: y1 <> y2;

              ex n be positive Nat st (n '*' ( 1. R)) = ( 0. R)

              proof

                per cases by A7, XREAL_1: 55;

                  suppose (y1 - y2) > 0 ;

                  hence thesis by A6;

                end;

                  suppose

                   A8: 0 < (y2 - y1);

                  ((y2 - y1) '*' ( 1. R)) = (( 0 - (y1 - y2)) '*' ( 1. R))

                  .= ( - ((y1 - y2) '*' ( 1. R))) by Th62

                  .= ( 0. R) by A6;

                  hence thesis by A8;

                end;

              end;

              hence contradiction by Def5, A2, A3;

            end;

            hence x1 = x2;

          end;

          then f is one-to-one by FUNCT_2: 19;

          hence ( ker ( canHom_Int R)) = ( {n} -Ideal ) by A4, RING_2: 12;

        end;

          suppose

           A9: k > 0 ;

           A10:

          now

            let x be object;

            assume x in ( {n} -Ideal );

            then x in the set of all (n * r) where r be Element of I by IDEAL_1: 64;

            then

            consider r be Element of I such that

             A11: x = (n * r);

            (f . x) = ((f . n) * (f . r)) by A11, GROUP_6:def 6

            .= ((n '*' ( 1. R)) * (f . r)) by Def8

            .= (( 0. R) * (f . r)) by A2, Def5, A9

            .= ( 0. R);

            hence x in ( ker ( canHom_Int R)) by A11;

          end;

          now

            let x be object;

            assume x in ( ker ( canHom_Int R));

            then

            consider y be Element of I such that

             A12: y = x & (f . y) = ( 0. R);

            reconsider d = (y div n), r = (y mod n) as Element of I;

            

             A13: (y mod n) < n by A9, INT_1: 58;

            

             A14: y = ((d * n) + r) by A9, INT_1: 59;

            (y mod n) in NAT by INT_1: 3, INT_1: 57;

            then

            reconsider rr = (y mod n) as Nat;

            ( 0. R) = ((f . (d * n)) + (f . r)) by A12, A14, VECTSP_1:def 20

            .= (((f . d) * (f . n)) + (f . r)) by GROUP_6:def 6

            .= (((f . d) * (n '*' ( 1. R))) + (f . r)) by Def8

            .= (((f . d) * ( 0. R)) + (f . r)) by Def5, A9, A2

            .= ((y mod n) '*' ( 1. R)) by Def8;

            then rr = 0 by A13, Def5, A2;

            then y in the set of all (n * a) where a be Element of I by A14;

            hence x in ( {n} -Ideal ) by A12, IDEAL_1: 64;

          end;

          hence ( ker ( canHom_Int R)) = ( {n} -Ideal ) by A10, TARSKI: 2;

        end;

      end;

      now

        assume

         A15: ( ker ( canHom_Int R)) = ( {n} -Ideal );

        per cases ;

          suppose

           A16: n = 0 ;

          then ( ker ( canHom_Int R)) = {( 0. I)} by A15, IDEAL_1: 47;

          then

           A17: ( canHom_Int R) is monomorphism by RING_2: 12;

          now

            assume ex n be positive Nat st (n '*' ( 1. R)) = ( 0. R);

            then

            consider k be positive Nat such that

             A18: (k '*' ( 1. R)) = ( 0. R);

            reconsider kk = k as Element of I by INT_1:def 2;

            (f . kk) = ( 0. R) by A18, Def8

            .= (f . ( 0. I)) by RING_2: 6;

            hence contradiction by A17, FUNCT_2: 19;

          end;

          hence ( Char R) = n by A16, Def5;

        end;

          suppose

           A19: n <> 0 ;

          reconsider l = n as positive Nat by A19;

          n in ( ker ( canHom_Int R)) by A15, IDEAL_1: 66;

          then

          consider y be Element of I such that

           A20: y = n & (f . y) = ( 0. R);

          (f . n) = (n '*' ( 1. R)) by Def8;

          then

           A21: n in ( CharSet R) by A19, A20;

          now

            let x be Nat;

            assume x in ( CharSet R);

            then

            consider m be positive Nat such that

             A22: x = m & (m '*' ( 1. R)) = ( 0. R);

            reconsider a = m as Element of I by INT_1:def 2;

            (f . a) = ( 0. R) by A22, Def8;

            then a in ( {n} -Ideal ) by A15;

            then a in the set of all (n * r) where r be Element of I by IDEAL_1: 64;

            then

            consider q be Element of I such that

             A23: a = (n * q);

            reconsider qq = q as Integer;

            now

              assume n > a;

              then (l / l) > ((l * qq) / l) by A23, XREAL_1: 74;

              then 1 > (qq * (l / l)) by XCMPLX_1: 60;

              then 1 > (qq * 1) by XCMPLX_1: 60;

              then (qq + 1) <= 1 by INT_1: 7;

              then ((qq + 1) - 1) <= (1 - 1) by XREAL_1: 13;

              hence contradiction by A23;

            end;

            hence n <= x by A22;

          end;

          then n = ( min* ( CharSet R)) by A21, NAT_1:def 1;

          hence ( Char R) = n by Th79;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: RING_3:83

    

     Th82: for R be Ring holds ( Char R) = 0 iff ( canHom_Int R) is monomorphism

    proof

      let R be Ring;

      set f = ( canHom_Int R);

      ( canHom_Int R) is monomorphism iff ( ker f) = {( 0. INT.Ring )} by RING_2: 12;

      then ( canHom_Int R) is monomorphism iff ( ker f) = ( {( 0. INT.Ring )} -Ideal ) by IDEAL_1: 47;

      hence thesis by Th81;

    end;

    registration

      let R be 0 -characteristic Ring;

      cluster ( canHom_Int R) -> monomorphism;

      coherence

      proof

        ( Char R) = 0 by Def6;

        hence thesis by Th82;

      end;

    end

    registration

      let R be 0 -characteristic Ring;

      cluster additive multiplicative unity-preserving monomorphism for Function of INT.Ring , R;

      existence

      proof

        take ( canHom_Int R);

        thus thesis;

      end;

    end

    theorem :: RING_3:84

    

     Th83: for R be Ring, f be Homomorphism of INT.Ring , R holds f = ( canHom_Int R)

    proof

      let R be Ring, f be Homomorphism of INT.Ring , R;

      set g = ( canHom_Int R);

      

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

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

      defpred P[ Integer] means for j be Integer st j = $1 holds (f . j) = (j '*' ( 1. R));

      now

        let j be Integer;

        assume

         A2: j = 0 ;

        

        hence (f . j) = (f . ( 0. INT.Ring ))

        .= ( 0. R) by RING_2: 6

        .= (j '*' ( 1. R)) by A2, Th58;

      end;

      then

       A3: P[ 0 ];

      

       A4: for u be Integer holds P[u] implies P[(u - 1)] & P[(u + 1)]

      proof

        let u be Integer;

        assume

         A5: P[u];

        reconsider uu = u as Element of INT.Ring by INT_1:def 2;

        now

          let k be Integer;

          assume

           A6: k = (u - 1);

          then k = (uu - ( 1. I));

          

          hence (f . k) = ((f . uu) - (f . ( 1. I))) by RING_2: 8

          .= ((uu '*' ( 1. R)) - (f . ( 1_ I))) by A5

          .= ((uu '*' ( 1. R)) - ( 1_ R)) by GROUP_1:def 13

          .= ((uu '*' ( 1. R)) - (1 '*' ( 1. R))) by Th59

          .= (k '*' ( 1. R)) by Th63, A6;

        end;

        hence P[(u - 1)];

        now

          let k be Integer;

          assume

           A7: k = (u + 1);

          then k = (uu + ( 1. I));

          

          hence (f . k) = ((f . uu) + (f . ( 1. I))) by VECTSP_1:def 20

          .= ((uu '*' ( 1. R)) + (f . ( 1_ I))) by A5

          .= ((uu '*' ( 1. R)) + ( 1_ R)) by GROUP_1:def 13

          .= ((uu '*' ( 1. R)) + (1 '*' ( 1. R))) by Th59

          .= (k '*' ( 1. R)) by Th61, A7;

        end;

        hence P[(u + 1)];

      end;

      

       A8: for i be Integer holds P[i] from INT_1:sch 4( A3, A4);

      now

        let x be object;

        assume x in ( dom f);

        then

        reconsider a = x as Element of INT.Ring ;

        reconsider aa = a as Integer;

        (f . a) = (aa '*' ( 1. R)) by A8;

        hence (f . x) = (g . x) by Def8;

      end;

      hence thesis by A1;

    end;

    theorem :: RING_3:85

    for f be Homomorphism of INT.Ring , INT.Ring holds f = ( id INT.Ring )

    proof

      ( canHom_Int INT.Ring ) = ( id INT.Ring ) by Th83;

      hence thesis by Th83;

    end;

    theorem :: RING_3:86

    

     Th85: for R be domRing holds ( Char R) = 0 or ( Char R) is prime

    proof

      let R be domRing;

      set n = ( Char R);

      now

        assume

         A1: ( Char R) <> 0 ;

        then

         A2: (n '*' ( 1. R)) = ( 0. R) & n <> 0 & for m be positive Nat st m < n holds (m '*' ( 1. R)) <> ( 0. R) by Def5;

        per cases by A1, NAT_1: 25;

          suppose n = 1;

          hence ( Char R) is prime by A2, Th59;

        end;

          suppose

           A3: n > 1;

          now

            assume not (n is prime);

            then

            consider m be Nat such that

             A4: m divides n & not (m = 1 or m = n) by A3, INT_2:def 4;

            consider u be Integer such that

             A5: (m * u) = n by A4;

            u > 0 by A5, A3;

            then u in NAT by INT_1: 3;

            then

            reconsider u as positive Nat by A5, A3;

            m <> 0 by A5, A3;

            then

            reconsider m as positive Nat;

            ( 0. R) = ((m * u) '*' ( 1. R)) by A5, Def5

            .= ((m '*' ( 1. R)) * (u '*' ( 1. R))) by Th66;

            then

             A6: (m '*' ( 1. R)) = ( 0. R) or (u '*' ( 1. R)) = ( 0. R) by VECTSP_2:def 1;

            m <= n by A3, A4, INT_2: 27;

            then

             A7: m < n by A4, XXREAL_0: 1;

            

             A8: u <= n by A3, INT_2: 27, A5, INT_1:def 3;

            now

              assume u = n;

              

              then (n / n) = ((m * n) / n) by A5

              .= (m * (n / n))

              .= (m * 1) by A1, XCMPLX_1: 60;

              hence contradiction by A4, A3, XCMPLX_1: 60;

            end;

            then u < n by A8, XXREAL_0: 1;

            hence contradiction by A7, A6, Def5;

          end;

          hence ( Char R) is prime;

        end;

      end;

      hence thesis;

    end;

    theorem :: RING_3:87

    for R be Ring, S be R -homomorphic Ring holds ( Char S) divides ( Char R)

    proof

      let R be Ring, S be R -homomorphic Ring;

      set n = ( Char S), m = ( Char R);

      reconsider n1 = n, m1 = m as Element of INT.Ring by INT_1:def 2;

      ( the Homomorphism of R, S * ( canHom_Int R)) = ( canHom_Int S) by Th83;

      then ( ker ( canHom_Int R)) c= ( ker ( canHom_Int S)) by Th68;

      then ( {m1} -Ideal ) c= ( ker ( canHom_Int S)) by Th81;

      then ( {m1} -Ideal ) c= ( {n1} -Ideal ) by Th81;

      then n1 divides m1 by RING_2: 19;

      hence thesis by Lm3;

    end;

    theorem :: RING_3:88

    

     Th87: for R be Ring, S be R -monomorphic Ring holds ( Char S) = ( Char R)

    proof

      let R be Ring, S be R -monomorphic Ring;

      set n = ( Char S), m = ( Char R);

      reconsider n1 = n, m1 = m as Element of INT.Ring by INT_1:def 2;

      ( the Monomorphism of R, S * ( canHom_Int R)) = ( canHom_Int S) by Th83;

      then ( ker ( canHom_Int R)) = ( ker ( canHom_Int S)) by Th69;

      then

       A1: ( {m1} -Ideal ) = ( ker ( canHom_Int S)) by Th81;

      then

       A2: n divides m & m divides n by Th81;

      per cases ;

        suppose

         A3: m = 0 ;

        

        then

         A4: {( 0. INT.Ring )} = ( {m1} -Ideal ) by IDEAL_1: 47

        .= ( {n1} -Ideal ) by A1, Th81;

        now

          assume

           A5: n <> ( 0. INT.Ring );

          n1 in ( {n1} -Ideal ) by IDEAL_1: 66;

          hence contradiction by A5, A4, TARSKI:def 1;

        end;

        hence n = m by A3;

      end;

        suppose

         A6: m > 0 ;

        consider u be Integer such that

         A7: m = (n * u) by A2;

        consider v be Integer such that

         A8: n = (m * v) by A2;

        m = ((m * v) * u) by A7, A8

        .= (m * (v * u));

        then (m / m) = ((v * u) * (m / m)) by XCMPLX_1: 74;

        then (m / m) = ((u * v) * 1) by A6, XCMPLX_1: 60;

        then

         A9: (u * v) = 1 by A6, XCMPLX_1: 60;

        u <> ( - 1) by A7, A6;

        then u = 1 & v = 1 by A9, INT_1: 9;

        hence thesis by A7;

      end;

    end;

    theorem :: RING_3:89

    

     Th88: for R be Ring, S be Subring of R holds ( Char S) = ( Char R)

    proof

      let R be Ring, S be Subring of R;

      R is S -monomorphic by Th70;

      hence thesis by Th87;

    end;

    registration

      let n be Nat;

      let R be n -characteristic Ring;

      cluster R -monomorphic -> n -characteristic for Ring;

      coherence

      proof

        let S be Ring;

        assume

         A1: S is R -monomorphic;

        ( Char R) = n by Def6;

        hence thesis by A1, Th87;

      end;

      cluster -> n -characteristic for Subring of R;

      coherence

      proof

        let S be Subring of R;

        ( Char R) = n by Def6;

        hence thesis by Th88;

      end;

    end

    

     Lm9: for n be Nat holds (n '*' ( 1. F_Complex )) = n

    proof

      let n be Nat;

      defpred P[ Nat] means ($1 '*' ( 1. F_Complex )) = $1;

      ( 0 '*' ( 1. F_Complex )) = ( 0. F_Complex ) by Th58;

      then

       A1: P[ 0 ] by COMPLFLD:def 1;

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

        reconsider kk = k as Nat;

        ((kk + 1) '*' ( 1. F_Complex )) = ((kk '*' ( 1. F_Complex )) + ( 1. F_Complex )) by Lm5

        .= (kk + 1) by A3, COMPLFLD:def 1;

        hence P[(k + 1)];

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    registration

      cluster F_Complex -> 0 -characteristic;

      coherence

      proof

        now

          let n be positive Nat;

          (n '*' ( 1. F_Complex )) = n by Lm9;

          hence (n '*' ( 1. F_Complex )) <> ( 0. F_Complex ) by COMPLFLD:def 1;

        end;

        hence thesis by Def5;

      end;

    end

    registration

      cluster F_Real -> 0 -characteristic;

      coherence

      proof

         F_Real is Subring of F_Complex by Th47, Lm1;

        hence thesis;

      end;

    end

    registration

      cluster F_Rat -> 0 -characteristic;

      coherence

      proof

         F_Rat is Subring of F_Real by Lm1, GAUSSINT: 14;

        hence thesis;

      end;

    end

    registration

      cluster 0 -characteristic for Field;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    registration

      let p be Prime;

      cluster p -characteristic for Field;

      existence

      proof

        take ( Z/ p);

        thus thesis;

      end;

    end

    registration

      let p be Prime;

      let R be p -characteristic domRing;

      cluster ( Char R) -> prime;

      coherence by Th85;

    end

    registration

      let F be 0 -characteristic Field;

      cluster -> 0 -characteristic for Subfield of F;

      coherence

      proof

        let S be Subfield of F;

        S is Subring of F by Lm1;

        hence thesis;

      end;

    end

    registration

      let p be Prime;

      let F be p -characteristic Field;

      cluster -> p -characteristic for Subfield of F;

      coherence

      proof

        let S be Subfield of F;

        S is Subring of F by Lm1;

        hence thesis;

      end;

    end

    begin

    definition

      let F be Field;

      :: RING_3:def9

      func carrier/\ F -> Subset of F equals { x where x be Element of F : for K be Subfield of F holds x in K };

      coherence

      proof

        now

          let x be object;

          assume x in { x where x be Element of F : for K be Subfield of F holds x in K };

          then

          consider x1 be Element of F such that

           A1: x1 = x & for K be Subfield of F holds x1 in K;

          thus x in the carrier of F by A1;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let F be Field;

      :: RING_3:def10

      func PrimeField F -> strict doubleLoopStr means

      : Def10: the carrier of it = ( carrier/\ F) & the addF of it = (the addF of F || ( carrier/\ F)) & the multF of it = (the multF of F || ( carrier/\ F)) & the OneF of it = ( 1. F) & the ZeroF of it = ( 0. F);

      existence

      proof

        set C = ( carrier/\ F);

        set f = the addF of F;

        C is f -binopclosed

        proof

          let x be set;

          assume x in [:C, C:];

          then

          consider x1,x2 be object such that

           A1: x1 in C and

           A2: x2 in C and

           A3: x = [x1, x2] by ZFMISC_1:def 2;

          consider y1 be Element of F such that

           A4: x1 = y1 and

           A5: for K be Subfield of F holds y1 in K by A1;

          consider y2 be Element of F such that

           A6: x2 = y2 and

           A7: for K be Subfield of F holds y2 in K by A2;

          now

            let K be Subfield of F;

            y1 in K & y2 in K by A5, A7;

            then

            reconsider a1 = y1, a2 = y2 as Element of K;

            the addF of K = (f || the carrier of K) by EC_PF_1:def 1;

            then (the addF of K . (a1,a2)) = (f . (a1,a2)) by Th1;

            hence (f . (y1,y2)) in K;

          end;

          hence (f . x) in C by A3, A4, A6;

        end;

        then

        reconsider C as Preserv of the addF of F;

        set f = the multF of F;

        C is f -binopclosed

        proof

          let x be set;

          assume x in [:C, C:];

          then

          consider x1,x2 be object such that

           A8: x1 in C and

           A9: x2 in C and

           A10: x = [x1, x2] by ZFMISC_1:def 2;

          consider y1 be Element of F such that

           A11: x1 = y1 and

           A12: for K be Subfield of F holds y1 in K by A8;

          consider y2 be Element of F such that

           A13: x2 = y2 and

           A14: for K be Subfield of F holds y2 in K by A9;

          now

            let K be Subfield of F;

            y1 in K & y2 in K by A12, A14;

            then

            reconsider a1 = y1, a2 = y2 as Element of K;

            the multF of K = (f || the carrier of K) by EC_PF_1:def 1;

            then (the multF of K . (a1,a2)) = (f . (a1,a2)) by Th1;

            hence (f . (y1,y2)) in K;

          end;

          hence (f . x) in C by A10, A11, A13;

        end;

        then

        reconsider D = C as Preserv of the multF of F;

        reconsider m = (the multF of F || D) as BinOp of C;

        set o = ( 1. F), z = ( 0. F);

        now

          let K be Subfield of F;

          o = ( 1. K) & z = ( 0. K) by EC_PF_1:def 1;

          hence o in K & z in K;

        end;

        then o in C & z in C;

        then

        reconsider o, z as Element of C;

        take doubleLoopStr (# C, (the addF of F || C), m, o, z #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let F be Field;

      cluster ( PrimeField F) -> non degenerated;

      coherence

      proof

        ( 0. ( PrimeField F)) = ( 0. F) & ( 1. ( PrimeField F)) = ( 1. F) by Def10;

        hence ( 0. ( PrimeField F)) <> ( 1. ( PrimeField F));

      end;

    end

    

     Lm10: for x be Element of ( PrimeField F) holds x is Element of F

    proof

      let x be Element of ( PrimeField F);

      

       A1: the carrier of ( PrimeField F) = ( carrier/\ F) by Def10;

      x in the carrier of ( PrimeField F);

      hence thesis by A1;

    end;

    

     Lm11: for a,b be Element of F holds for x,y be Element of ( PrimeField F) st a = x & b = y holds (a + b) = (x + y)

    proof

      let a,b be Element of F;

      let x,y be Element of ( PrimeField F) such that

       A1: a = x & b = y;

      the carrier of ( PrimeField F) = ( carrier/\ F) by Def10;

      

      hence (a + b) = ((the addF of F || ( carrier/\ F)) . (x,y)) by A1, Th1

      .= (x + y) by Def10;

    end;

    

     Lm12: for a,b be Element of F holds for x,y be Element of ( PrimeField F) st a = x & b = y holds (a * b) = (x * y)

    proof

      let a,b be Element of F;

      let x,y be Element of ( PrimeField F) such that

       A1: a = x & b = y;

      the carrier of ( PrimeField F) = ( carrier/\ F) by Def10;

      

      hence (a * b) = ((the multF of F || ( carrier/\ F)) . (x,y)) by A1, Th1

      .= (x * y) by Def10;

    end;

    registration

      let F be Field;

      cluster ( PrimeField F) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set P = ( PrimeField F);

        

         A1: ( 0. P) = ( 0. F) by Def10;

        

         A2: the carrier of ( PrimeField F) = ( carrier/\ F) by Def10;

        hereby

          let x,y be Element of P;

          reconsider a = x, b = y as Element of F by Lm10;

          

          thus (x + y) = (a + b) by Lm11

          .= (y + x) by Lm11;

        end;

        hereby

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of F by Lm10;

          

           A3: (y + z) = (b + c) by Lm11;

          (x + y) = (a + b) by Lm11;

          

          hence ((x + y) + z) = ((a + b) + c) by Lm11

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

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

        end;

        hereby

          let x be Element of P;

          reconsider a = x as Element of F by Lm10;

          

          thus (x + ( 0. P)) = (a + ( 0. F)) by A1, Lm11

          .= x;

        end;

        let x be Element of P;

        reconsider a = x as Element of F by Lm10;

        x in ( carrier/\ F) by A2;

        then

        consider x1 be Element of F such that

         A4: x = x1 and

         A5: for K be Subfield of F holds x1 in K;

        now

          let K be Subfield of F;

          x1 in K by A5;

          then

          reconsider t = x1 as Element of K;

          ( - t) = ( - x1) by GAUSSINT: 19;

          hence ( - x1) in K;

        end;

        then ( - x1) in ( carrier/\ F);

        then

        reconsider y = ( - x1) as Element of P by Def10;

        take y;

        

        thus (x + y) = (a + ( - x1)) by Lm11

        .= ( 0. P) by A1, A4, RLVECT_1: 5;

      end;

    end

    registration

      let F be Field;

      cluster ( PrimeField F) -> commutative;

      coherence

      proof

        let x,y be Element of ( PrimeField F);

        reconsider a = x, b = y as Element of F by Lm10;

        

        thus (x * y) = (a * b) by Lm12

        .= (y * x) by Lm12;

      end;

    end

    registration

      let F be Field;

      cluster ( PrimeField F) -> associative well-unital distributive almost_left_invertible;

      coherence

      proof

        set P = ( PrimeField F);

        

         A1: ( 1. P) = ( 1. F) by Def10;

        

         A2: ( 0. P) = ( 0. F) by Def10;

        hereby

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of F by Lm10;

          

           A3: (y * z) = (b * c) by Lm12;

          (x * y) = (a * b) by Lm12;

          

          hence ((x * y) * z) = ((a * b) * c) by Lm12

          .= (a * (b * c)) by GROUP_1:def 3

          .= (x * (y * z)) by A3, Lm12;

        end;

        hereby

          let x be Element of P;

          reconsider a = x as Element of F by Lm10;

          

          thus (x * ( 1. P)) = (a * ( 1. F)) by A1, Lm12

          .= x;

          

          thus (( 1. P) * x) = (( 1. F) * a) by A1, Lm12

          .= x;

        end;

        hereby

          let x,y,z be Element of P;

          reconsider a = x, b = y, c = z as Element of F by Lm10;

          

           A4: (a * b) = (x * y) & (a * c) = (x * z) by Lm12;

          (y + z) = (b + c) by Lm11;

          

          hence (x * (y + z)) = (a * (b + c)) by Lm12

          .= ((a * b) + (a * c)) by VECTSP_1:def 7

          .= ((x * y) + (x * z)) by A4, Lm11;

          hence ((y + z) * x) = ((y * x) + (z * x));

        end;

        let x be Element of P such that

         A5: x <> ( 0. P);

        reconsider a = x as Element of F by Lm10;

        the carrier of ( PrimeField F) = ( carrier/\ F) by Def10;

        then x in ( carrier/\ F);

        then

        consider x1 be Element of F such that

         A6: x = x1 and

         A7: for K be Subfield of F holds x1 in K;

        now

          let K be Subfield of F;

          x1 in K by A7;

          then

          reconsider t = x1 as Element of K;

          (t " ) = (x1 " ) by A5, A6, A2, GAUSSINT: 21;

          hence (x1 " ) in K;

        end;

        then (x1 " ) in ( carrier/\ F);

        then

        reconsider y = (x1 " ) as Element of P by Def10;

        take y;

        

        thus (y * x) = ((x1 " ) * a) by Lm12

        .= ( 1. P) by A1, A2, A5, A6, VECTSP_1:def 10;

      end;

    end

    definition

      let F be Field;

      :: original: PrimeField

      redefine

      func PrimeField F -> strict Subfield of F ;

      coherence

      proof

        set P = ( PrimeField F);

        the carrier of P = ( carrier/\ F) by Def10;

        then the carrier of P is Subset of the carrier of F & the addF of P = (the addF of F || the carrier of P) & the multF of P = (the multF of F || the carrier of P) & ( 1. P) = ( 1. F) & ( 0. P) = ( 0. F) by Def10;

        hence thesis by EC_PF_1: 2;

      end;

    end

    

     Lm13: for F be Field, K be Subfield of F holds ( carrier/\ F) c= the carrier of K

    proof

      let F be Field, K be Subfield of F;

      now

        let x be object;

        assume x in ( carrier/\ F);

        then

        consider y be Element of F such that

         A1: x = y & for E be Subfield of F holds y in E;

        y in K by A1;

        hence x in the carrier of K by A1;

      end;

      hence thesis;

    end;

    theorem :: RING_3:90

    

     Th89: for F be Field, E be strict Subfield of ( PrimeField F) holds E = ( PrimeField F)

    proof

      let F be Field, E be strict Subfield of ( PrimeField F);

      set K = ( PrimeField F);

      

       A1: the carrier of E c= the carrier of K & the addF of E = (the addF of K || the carrier of E) & the multF of E = (the multF of K || the carrier of E) & ( 1. E) = ( 1. K) & ( 0. E) = ( 0. K) by EC_PF_1:def 1;

      E is Subfield of F by EC_PF_1: 5;

      then ( carrier/\ F) c= the carrier of E by Lm13;

      then the carrier of E = the carrier of ( PrimeField F) by EC_PF_1:def 1, Def10;

      hence thesis by A1;

    end;

    theorem :: RING_3:91

    

     Th90: for F be Field, E be Subfield of F holds ( PrimeField F) is Subfield of E

    proof

      let F be Field, E be Subfield of F;

      the carrier of ( PrimeField F) c= the carrier of E

      proof

        let x be object;

        assume x in the carrier of ( PrimeField F);

        then x in ( carrier/\ F) by Def10;

        then ex y be Element of F st x = y & for K be Subfield of F holds y in K;

        then x in E;

        hence thesis;

      end;

      hence thesis by EC_PF_1: 6;

    end;

    theorem :: RING_3:92

    

     Th91: for F,K be Field holds K = ( PrimeField F) iff (K is strict Subfield of F & for E be strict Subfield of K holds E = K)

    proof

      let F,K be Field;

      now

        assume

         A1: K is strict Subfield of F & for E be strict Subfield of K holds E = K;

        then ( PrimeField F) is Subfield of K by Th90;

        hence K = ( PrimeField F) by A1;

      end;

      hence thesis by Th89;

    end;

    theorem :: RING_3:93

    

     Th92: for F,K be Field holds K = ( PrimeField F) iff (K is strict Subfield of F & for E be Subfield of F holds K is Subfield of E)

    proof

      let F,K be Field;

      now

        assume

         A1: K is strict Subfield of F & for E be Subfield of F holds K is Subfield of E;

        then

         A2: the carrier of K c= the carrier of F & the addF of K = (the addF of F || the carrier of K) & the multF of K = (the multF of F || the carrier of K) & ( 1. F) = ( 1. K) & ( 0. F) = ( 0. K) by EC_PF_1:def 1;

         A3:

        now

          let x be object;

          assume x in ( carrier/\ F);

          then

          consider y be Element of F such that

           A4: x = y & for E be Subfield of F holds y in E;

          x in K by A4, A1;

          hence x in the carrier of K;

        end;

        now

          let x be object;

          assume

           A5: x in the carrier of K;

          for E be Subfield of F holds x in E

          proof

            let E be Subfield of F;

            K is Subfield of E by A1;

            then the carrier of K c= the carrier of E by EC_PF_1:def 1;

            hence x in E by A5;

          end;

          hence x in ( carrier/\ F) by A2, A5;

        end;

        then the carrier of K = ( carrier/\ F) by A3, TARSKI: 2;

        hence K = ( PrimeField F) by A1, A2, Def10;

      end;

      hence thesis by Th90;

    end;

    theorem :: RING_3:94

    for E be Field, F be Subfield of E holds ( PrimeField F) = ( PrimeField E)

    proof

      let E be Field, F be Subfield of E;

      ( PrimeField F) is Subfield of E by EC_PF_1: 5;

      then ( PrimeField E) is Subfield of ( PrimeField F) by Th92;

      hence thesis by Th91;

    end;

    theorem :: RING_3:95

    for F be Field holds ( PrimeField ( PrimeField F)) = ( PrimeField F) by Th91;

    registration

      let F be Field;

      cluster ( PrimeField F) -> prime;

      coherence

      proof

        for K be Field holds K is strict Subfield of ( PrimeField F) implies K = ( PrimeField F) by Th91;

        hence thesis by EC_PF_1:def 2;

      end;

    end

    theorem :: RING_3:96

    for F be Field holds F is prime iff F = ( PrimeField F) by EC_PF_1:def 2;

    theorem :: RING_3:97

    

     Th96: for F be 0 -characteristic Field, i,j be non zero Integer st j divides i holds ((i div j) '*' ( 1. F)) = ((i '*' ( 1. F)) * ((j '*' ( 1. F)) " ))

    proof

      let F be 0 -characteristic Field, i,j be non zero Integer;

      

       A1: ( Char F) = 0 by Def6;

      assume j divides i;

      then

      consider k be Integer such that

       A2: i = (j * k);

      

       A3: ((i div j) * j) = ( [\(k * (j / j))/] * j) by A2

      .= ( [\(k * 1)/] * j) by XCMPLX_1: 60

      .= i by A2, INT_1: 25;

      

       A4: (j '*' ( 1. F)) <> ( 0. F)

      proof

        per cases ;

          suppose j > 0 ;

          then j is Element of NAT by INT_1: 3;

          hence thesis by A1, Def5;

        end;

          suppose j < 0 ;

          then

           A5: ( - j) is Element of NAT by INT_1: 3;

          

           A6: (j '*' ( 1. F)) = (( - ( - j)) '*' ( 1. F))

          .= ( - (( - j) '*' ( 1. F))) by Th62;

          now

            assume (j '*' ( 1. F)) = ( 0. F);

            then ( - ( - (( - j) '*' ( 1. F)))) = ( 0. F) by A6;

            hence (( - j) '*' ( 1. F)) = ( 0. F);

          end;

          hence thesis by A5, A1, Def5;

        end;

      end;

      

       A7: (i '*' ( 1. F)) <> ( 0. F)

      proof

        per cases ;

          suppose i > 0 ;

          then i is Element of NAT by INT_1: 3;

          hence thesis by A1, Def5;

        end;

          suppose i < 0 ;

          then

           A8: ( - i) is Element of NAT by INT_1: 3;

          

           A9: (i '*' ( 1. F)) = (( - ( - i)) '*' ( 1. F))

          .= ( - (( - i) '*' ( 1. F))) by Th62;

          now

            assume (i '*' ( 1. F)) = ( 0. F);

            then ( - ( - (( - i) '*' ( 1. F)))) = ( 0. F) by A9;

            hence (( - i) '*' ( 1. F)) = ( 0. F);

          end;

          hence thesis by A8, A1, Def5;

        end;

      end;

      ((((i div j) '*' ( 1. F)) * ((i '*' ( 1. F)) " )) * (j '*' ( 1. F))) = (((i '*' ( 1. F)) " ) * (((i div j) '*' ( 1. F)) * (j '*' ( 1. F)))) by GROUP_1:def 3

      .= (((i '*' ( 1. F)) " ) * (((i div j) * j) '*' ( 1. F))) by Th66

      .= ( 1. F) by A3, A7, VECTSP_1:def 10;

      then ((j '*' ( 1. F)) " ) = (((i div j) '*' ( 1. F)) * ((i '*' ( 1. F)) " )) by A4, VECTSP_1:def 10;

      

      hence ((i '*' ( 1. F)) * ((j '*' ( 1. F)) " )) = (((i '*' ( 1. F)) * ((i '*' ( 1. F)) " )) * ((i div j) '*' ( 1. F))) by GROUP_1:def 3

      .= (( 1. F) * ((i div j) '*' ( 1. F))) by A7, VECTSP_1:def 10

      .= ((i div j) '*' ( 1. F));

    end;

    definition

      let x be Element of F_Rat ;

      :: original: denominator

      redefine

      func denominator (x) -> positive Element of INT.Ring ;

      coherence by INT_1:def 2;

      :: original: numerator

      redefine

      func numerator (x) -> Element of INT.Ring ;

      coherence by INT_1:def 2;

    end

    definition

      let F be Field;

      :: RING_3:def11

      func canHom_Rat F -> Function of F_Rat , F means

      : Def11: for x be Element of F_Rat holds (it . x) = ((( canHom_Int F) . ( numerator x)) / (( canHom_Int F) . ( denominator x)));

      existence

      proof

        deffunc F( Element of F_Rat ) = ((( canHom_Int F) . ( numerator $1)) / (( canHom_Int F) . ( denominator $1)));

        ex f be Function of F_Rat , F st for x be Element of F_Rat holds (f . x) = F(x) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of F_Rat , F such that

         A1: for x be Element of F_Rat holds (f . x) = ((( canHom_Int F) . ( numerator x)) / (( canHom_Int F) . ( denominator x))) and

         A2: for x be Element of F_Rat holds (g . x) = ((( canHom_Int F) . ( numerator x)) / (( canHom_Int F) . ( denominator x)));

        let x be Element of F_Rat ;

        

        thus (f . x) = ((( canHom_Int F) . ( numerator x)) / (( canHom_Int F) . ( denominator x))) by A1

        .= (g . x) by A2;

      end;

    end

    registration

      let F be Field;

      cluster ( canHom_Rat F) -> unity-preserving;

      coherence

      proof

        set f = ( canHom_Rat F);

        set c = ( canHom_Int F);

        

         A1: ( numerator 1) = 1 & ( denominator 1) = 1 by RAT_1: 17;

        (c . ( 1_ INT.Ring )) = ( 1_ F) by GROUP_1:def 13;

        

        hence (f . ( 1_ F_Rat )) = (( 1. F) / ( 1. F)) by A1, Def11

        .= ( 1_ F);

      end;

    end

    registration

      let F be 0 -characteristic Field;

      cluster ( canHom_Rat F) -> additive multiplicative;

      coherence

      proof

        set f = ( canHom_Rat F);

        set c = ( canHom_Int F);

        hereby

          let x,y be Element of F_Rat ;

          reconsider x1 = x, y1 = y as Rational;

          set m = ( denominator x1), n = ( denominator y1);

          set i = ( numerator x1), j = ( numerator y1);

          

           A1: (c . ( numerator x)) = (( numerator x) '*' ( 1. F)) by Def8;

          

           A2: (c . ( numerator y)) = (( numerator y) '*' ( 1. F)) by Def8;

          

           A3: (c . ( numerator (x + y))) = (( numerator (x + y)) '*' ( 1. F)) by Def8;

          

           A4: ( Char F) = 0 by Def6;

          

           A5: (((i * n) + (j * m)) gcd (m * n)) <> 0 by INT_2: 5;

          

           A6: (((i * n) + (j * m)) gcd (m * n)) divides ((i * n) + (j * m)) by INT_2:def 2;

          

           A7: (((i * n) + (j * m)) gcd (m * n)) divides (m * n) by INT_2:def 2;

          

           A8: ((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) <> ( 0. F) by A4, A5, Def5;

          then

           A9: (((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " ) <> ( 0. F) by VECTSP_2: 13;

          

           A10: ((m * n) '*' ( 1. F)) <> ( 0. F) by A4, Def5;

          

           A11: (m '*' ( 1. F)) <> ( 0. F) by A4, Def5;

          

           A12: (n '*' ( 1. F)) <> ( 0. F) by A4, Def5;

          

           A13: ((f . x) + (f . y)) = ((f . x) + ((c . ( numerator y)) / (c . ( denominator y)))) by Def11

          .= (((c . ( numerator x)) / (c . ( denominator x))) + ((c . ( numerator y)) / (c . ( denominator y)))) by Def11

          .= (((i '*' ( 1. F)) * ((m '*' ( 1. F)) " )) + ((c . ( numerator y)) / (c . ( denominator y)))) by A1, Def8

          .= (((i '*' ( 1. F)) * ((m '*' ( 1. F)) " )) + ((j '*' ( 1. F)) / (n '*' ( 1. F)))) by A2, Def8

          .= ((((i '*' ( 1. F)) * ((m '*' ( 1. F)) " )) * ( 1. F)) + ((j '*' ( 1. F)) * ((n '*' ( 1. F)) " )))

          .= ((((i '*' ( 1. F)) * ((m '*' ( 1. F)) " )) * (1 '*' ( 1. F))) + ((j '*' ( 1. F)) * ((n '*' ( 1. F)) " ))) by Th59

          .= ((((i '*' ( 1. F)) * ((m '*' ( 1. F)) " )) * ((n div n) '*' ( 1. F))) + ((j '*' ( 1. F)) * ((n '*' ( 1. F)) " ))) by INT_1: 49

          .= ((((i '*' ( 1. F)) * ((m '*' ( 1. F)) " )) * ((n '*' ( 1. F)) * ((n '*' ( 1. F)) " ))) + ((j '*' ( 1. F)) * ((n '*' ( 1. F)) " ))) by Th96

          .= (((i '*' ( 1. F)) * (((m '*' ( 1. F)) " ) * ((n '*' ( 1. F)) * ((n '*' ( 1. F)) " )))) + ((j '*' ( 1. F)) * ((n '*' ( 1. F)) " ))) by GROUP_1:def 3

          .= (((i '*' ( 1. F)) * ((n '*' ( 1. F)) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " )))) + ((j '*' ( 1. F)) * ((n '*' ( 1. F)) " ))) by GROUP_1:def 3

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) + ((j '*' ( 1. F)) * ((n '*' ( 1. F)) " ))) by GROUP_1:def 3

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) + (((j '*' ( 1. F)) * ((n '*' ( 1. F)) " )) * ( 1. F)))

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) + (((j '*' ( 1. F)) * ((n '*' ( 1. F)) " )) * (1 '*' ( 1. F)))) by Th59

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) + (((j '*' ( 1. F)) * ((n '*' ( 1. F)) " )) * ((m div m) '*' ( 1. F)))) by INT_1: 49

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) + (((j '*' ( 1. F)) * ((n '*' ( 1. F)) " )) * ((m '*' ( 1. F)) * ((m '*' ( 1. F)) " )))) by Th96

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) + ((j '*' ( 1. F)) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) * ((m '*' ( 1. F)) " ))))) by GROUP_1:def 3

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) + ((j '*' ( 1. F)) * ((m '*' ( 1. F)) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))))) by GROUP_1:def 3

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) + (((j '*' ( 1. F)) * (m '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " )))) by GROUP_1:def 3

          .= ((((i '*' ( 1. F)) * (n '*' ( 1. F))) + ((j '*' ( 1. F)) * (m '*' ( 1. F)))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) by VECTSP_1:def 7

          .= ((((i * n) '*' ( 1. F)) + ((j '*' ( 1. F)) * (m '*' ( 1. F)))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) by Th66

          .= ((((i * n) '*' ( 1. F)) + ((j * m) '*' ( 1. F))) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) by Th66

          .= ((((i * n) + (j * m)) '*' ( 1. F)) * (((n '*' ( 1. F)) " ) * ((m '*' ( 1. F)) " ))) by Th61

          .= ((((i * n) + (j * m)) '*' ( 1. F)) * (((n '*' ( 1. F)) * (m '*' ( 1. F))) " )) by A11, A12, VECTSP_2: 11

          .= ((((i * n) + (j * m)) '*' ( 1. F)) * (((n * m) '*' ( 1. F)) " )) by Th66

          .= ((((i * n) + (j * m)) '*' ( 1. F)) * (( 1. F) * (((n * m) '*' ( 1. F)) " )))

          .= ((((i * n) + (j * m)) '*' ( 1. F)) * (((((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " ) * ((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F))) * (((m * n) '*' ( 1. F)) " ))) by A8, VECTSP_2:def 2

          .= ((((i * n) + (j * m)) '*' ( 1. F)) * ((((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " ) * ((((m * n) '*' ( 1. F)) " ) * ((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F))))) by GROUP_1:def 3

          .= (((((i * n) + (j * m)) '*' ( 1. F)) * (((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) '*' ( 1. F)) " ) * ((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)))) by GROUP_1:def 3

          .= (((((i * n) + (j * m)) '*' ( 1. F)) * (((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) '*' ( 1. F)) " ) * ((((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " ) " ))) by A8, VECTSP_1: 24

          .= (((((i * n) + (j * m)) '*' ( 1. F)) * (((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) '*' ( 1. F)) * (((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " )) " )) by A9, A10, VECTSP_2: 11;

          

           A14: (f . (x + y)) = ((c . ( numerator (x + y))) / (c . ( denominator (x + y)))) by Def11

          .= ((( numerator (x + y)) '*' ( 1. F)) * ((( denominator (x + y)) '*' ( 1. F)) " )) by A3, Def8

          .= (((((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n))) '*' ( 1. F)) * ((( denominator (x + y)) '*' ( 1. F)) " )) by Th35

          .= (((((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n))) '*' ( 1. F)) * ((((m * n) div (((i * n) + (j * m)) gcd (m * n))) '*' ( 1. F)) " )) by Th35;

          per cases ;

            suppose ((i * n) + (j * m)) <> 0 ;

            

            hence (f . (x + y)) = (((((i * n) + (j * m)) '*' ( 1. F)) * (((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) div (((i * n) + (j * m)) gcd (m * n))) '*' ( 1. F)) " )) by A14, A5, A6, Th96

            .= ((f . x) + (f . y)) by A13, A5, A7, Th96;

          end;

            suppose

             A15: ((i * n) + (j * m)) = 0 ;

            ((m * n) * 0 ) = 0 ;

            then

             A16: (m * n) divides 0 & (m * n) divides (m * n);

            for a be Integer st a divides 0 & a divides (m * n) holds a divides (m * n);

            then (((i * n) + (j * m)) gcd (m * n)) = (m * n) by A16, A15, INT_2:def 2;

            

            hence (f . (x + y)) = (((((i * n) + (j * m)) div (m * n)) '*' ( 1. F)) * ((1 '*' ( 1. F)) " )) by A14, INT_1: 49

            .= (((((i * n) + (j * m)) div (m * n)) '*' ( 1. F)) * (( 1. F) " )) by Th59

            .= ( [\( 0 / (m * n))/] '*' ( 1. F)) by A15

            .= ( 0 '*' ( 1. F)) by INT_1: 25

            .= ((( 0. F) * (((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) '*' ( 1. F)) * (((((i * n) + (j * m)) gcd (m * n)) '*' ( 1. F)) " )) " )) by Th58

            .= ((f . x) + (f . y)) by A13, A15, Th58;

          end;

        end;

        hereby

          let x,y be Element of F_Rat ;

          reconsider x1 = x, y1 = y as Rational;

          set m = ( denominator x1), n = ( denominator y1);

          set i = ( numerator x1), j = ( numerator y1);

          

           A17: (c . ( numerator x)) = (( numerator x) '*' ( 1. F)) by Def8;

          

           A18: (c . ( numerator y)) = (( numerator y) '*' ( 1. F)) by Def8;

          

           A19: (c . ( numerator (x * y))) = (( numerator (x * y)) '*' ( 1. F)) by Def8;

          

           A20: ( Char F) = 0 by Def6;

          

           A21: ((i * j) gcd (m * n)) <> 0 by INT_2: 5;

          

           A22: ((i * j) gcd (m * n)) divides (i * j) by INT_2:def 2;

          

           A23: ((i * j) gcd (m * n)) divides (m * n) by INT_2:def 2;

          

           A24: (((i * j) gcd (m * n)) '*' ( 1. F)) <> ( 0. F) by A20, A21, Def5;

          then

           A25: ((((i * j) gcd (m * n)) '*' ( 1. F)) " ) <> ( 0. F) by VECTSP_2: 13;

          

           A26: ((m * n) '*' ( 1. F)) <> ( 0. F) by A20, Def5;

          

           A27: (m '*' ( 1. F)) <> ( 0. F) by A20, Def5;

          

           A28: (n '*' ( 1. F)) <> ( 0. F) by A20, Def5;

          

           A29: ((f . x) * (f . y)) = ((f . x) * ((c . ( numerator y)) / (c . ( denominator y)))) by Def11

          .= (((c . ( numerator x)) / (c . ( denominator x))) * ((c . ( numerator y)) / (c . ( denominator y)))) by Def11

          .= (((i '*' ( 1. F)) * ((m '*' ( 1. F)) " )) * ((c . ( numerator y)) / (c . ( denominator y)))) by A17, Def8

          .= (((i '*' ( 1. F)) * ((m '*' ( 1. F)) " )) * ((j '*' ( 1. F)) / (n '*' ( 1. F)))) by A18, Def8

          .= ((i '*' ( 1. F)) * (((m '*' ( 1. F)) " ) * ((j '*' ( 1. F)) * ((n '*' ( 1. F)) " )))) by GROUP_1:def 3

          .= ((i '*' ( 1. F)) * ((((m '*' ( 1. F)) " ) * ((n '*' ( 1. F)) " )) * (j '*' ( 1. F)))) by GROUP_1:def 3

          .= (((i '*' ( 1. F)) * (j '*' ( 1. F))) * (((m '*' ( 1. F)) " ) * ((n '*' ( 1. F)) " ))) by GROUP_1:def 3

          .= (((i * j) '*' ( 1. F)) * (((m '*' ( 1. F)) " ) * ((n '*' ( 1. F)) " ))) by Th66

          .= (((i * j) '*' ( 1. F)) * (((m '*' ( 1. F)) * (n '*' ( 1. F))) " )) by A27, A28, VECTSP_2: 11

          .= (((i * j) '*' ( 1. F)) * (((m * n) '*' ( 1. F)) " )) by Th66

          .= (((i * j) '*' ( 1. F)) * (( 1. F) * (((m * n) '*' ( 1. F)) " )))

          .= (((i * j) '*' ( 1. F)) * ((((((i * j) gcd (m * n)) '*' ( 1. F)) " ) * (((i * j) gcd (m * n)) '*' ( 1. F))) * (((m * n) '*' ( 1. F)) " ))) by A24, VECTSP_2:def 2

          .= (((i * j) '*' ( 1. F)) * (((((i * j) gcd (m * n)) '*' ( 1. F)) " ) * ((((m * n) '*' ( 1. F)) " ) * (((i * j) gcd (m * n)) '*' ( 1. F))))) by GROUP_1:def 3

          .= ((((i * j) '*' ( 1. F)) * ((((i * j) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) '*' ( 1. F)) " ) * (((i * j) gcd (m * n)) '*' ( 1. F)))) by GROUP_1:def 3

          .= ((((i * j) '*' ( 1. F)) * ((((i * j) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) '*' ( 1. F)) " ) * (((((i * j) gcd (m * n)) '*' ( 1. F)) " ) " ))) by A24, VECTSP_1: 24

          .= ((((i * j) '*' ( 1. F)) * ((((i * j) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) '*' ( 1. F)) * ((((i * j) gcd (m * n)) '*' ( 1. F)) " )) " )) by A25, A26, VECTSP_2: 11;

          

           A30: (f . (x * y)) = ((c . ( numerator (x * y))) / (c . ( denominator (x * y)))) by Def11

          .= ((( numerator (x * y)) '*' ( 1. F)) * ((( denominator (x * y)) '*' ( 1. F)) " )) by A19, Def8

          .= ((((i * j) div ((i * j) gcd (m * n))) '*' ( 1. F)) * ((( denominator (x * y)) '*' ( 1. F)) " )) by Th39

          .= ((((i * j) div ((i * j) gcd (m * n))) '*' ( 1. F)) * ((((m * n) div ((i * j) gcd (m * n))) '*' ( 1. F)) " )) by Th39;

          per cases ;

            suppose (i * j) <> 0 ;

            

            hence (f . (x * y)) = ((((i * j) '*' ( 1. F)) * ((((i * j) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) div ((i * j) gcd (m * n))) '*' ( 1. F)) " )) by A30, A21, A22, Th96

            .= ((f . x) * (f . y)) by A29, A21, A23, Th96;

          end;

            suppose

             A31: (i * j) = 0 ;

            ((m * n) * 0 ) = 0 ;

            then

             A32: (m * n) divides 0 & (m * n) divides (m * n);

            for a be Integer st a divides 0 & a divides (m * n) holds a divides (m * n);

            then ((i * j) gcd (m * n)) = (m * n) by A32, A31, INT_2:def 2;

            

            hence (f . (x * y)) = ((((i * j) div (m * n)) '*' ( 1. F)) * ((1 '*' ( 1. F)) " )) by A30, INT_1: 49

            .= ((((i * j) div (m * n)) '*' ( 1. F)) * (( 1. F) " )) by Th59

            .= ( [\( 0 / (m * n))/] '*' ( 1. F)) by A31

            .= ( 0 '*' ( 1. F)) by INT_1: 25

            .= ((( 0. F) * ((((i * j) gcd (m * n)) '*' ( 1. F)) " )) * ((((m * n) '*' ( 1. F)) * ((((i * j) gcd (m * n)) '*' ( 1. F)) " )) " )) by Th58

            .= ((f . x) * (f . y)) by A29, A31, Th58;

          end;

        end;

      end;

    end

    registration

      cluster -> F_Rat -monomorphic for 0 -characteristic Field;

      coherence

      proof

        let F be 0 -characteristic Field;

        take ( canHom_Rat F);

        thus thesis;

      end;

    end

    theorem :: RING_3:98

    

     Th97: for F be Field holds ( canHom_Int F) = (( canHom_Rat F) | INT )

    proof

      let F be Field;

      set f = ( canHom_Int F);

      set g = ( canHom_Rat F);

      ( dom g) = RAT by FUNCT_2:def 1;

      then

       A1: ( dom (g | INT )) = INT by RELAT_1: 62, NUMBERS: 14;

      now

        let x be object;

        assume

         A2: x in ( dom f);

        then

        reconsider y = x as Element of INT.Ring ;

        reconsider r = y as Element of F_Rat by NUMBERS: 14;

        

         A3: (f . ( 1_ I)) = ( 1_ F) by GROUP_1:def 13;

        

        thus (f . x) = ((f . ( numerator r)) / ( 1_ F)) by RAT_1: 17

        .= ((f . ( numerator r)) / (f . ( denominator r))) by A3, RAT_1: 17

        .= (g . x) by Def11

        .= ((g | INT ) . x) by A2, FUNCT_1: 49;

      end;

      hence thesis by FUNCT_2:def 1, A1;

    end;

    registration

      cluster 0 -characteristic F_Rat -homomorphic for Field;

      existence ;

    end

    theorem :: RING_3:99

    

     Th98: for F be 0 -characteristic F_Rat -homomorphic Field, f be Homomorphism of F_Rat , F holds f = ( canHom_Rat F)

    proof

      let F be 0 -characteristic F_Rat -homomorphic Field, f be Homomorphism of F_Rat , F;

      set g = ( canHom_Rat F);

      

       A1: f is unity-preserving;

      

       A2: f is multiplicative;

      

       A3: g is unity-preserving;

      

       A4: ( dom f) = the carrier of F_Rat by FUNCT_2:def 1

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

      defpred P[ Integer] means for j be Element of F_Rat st j = $1 holds (f . j) = (g . j);

      

       A5: ( 0. F_Rat ) = 0 ;

      

      then (f . 0 ) = ( 0. F) by RING_2: 6

      .= (g . 0 ) by A5, RING_2: 6;

      then

       A6: P[ 0 ];

       A7:

      now

        let u be Integer;

        assume

         A8: P[u];

        reconsider uu = u as Element of F_Rat by RAT_1:def 2;

        now

          let k be Integer;

          assume k = (u - 1);

          then

           A9: k = (uu - ( 1. F_Rat ));

          

          hence (f . k) = ((f . uu) - (f . ( 1. F_Rat ))) by RING_2: 8

          .= ((g . uu) - (g . ( 1_ F_Rat ))) by A8, A1, A3

          .= (g . k) by A9, RING_2: 8;

        end;

        hence P[(u - 1)];

        now

          let k be Integer;

          assume k = (u + 1);

          then

           A10: k = (uu + ( 1. F_Rat ));

          

          hence (f . k) = ((f . uu) + (f . ( 1. F_Rat ))) by VECTSP_1:def 20

          .= ((g . uu) + (g . ( 1_ F_Rat ))) by A8, A1, A3

          .= (g . k) by A10, VECTSP_1:def 20;

        end;

        hence P[(u + 1)];

      end;

      

       A11: for i be Integer holds P[i] from INT_1:sch 4( A6, A7);

      

       A12: for i be Integer, j be Element of F_Rat st j = i holds (f . j) = (( canHom_Int F) . i)

      proof

        let i be Integer, j be Element of F_Rat ;

        assume

         A13: j = i;

        

         A14: ( canHom_Int F) = (( canHom_Rat F) | INT ) by Th97;

        

        thus (f . j) = (g . i) by A13, A11

        .= (( canHom_Int F) . i) by A14, INT_1:def 2, FUNCT_1: 49;

      end;

      now

        let x be object;

        assume x in ( dom f);

        then

        reconsider a = x as Element of F_Rat ;

        reconsider a1 = ( numerator a) as Element of F_Rat by RAT_1:def 2;

        reconsider a2 = ( denominator a) as Element of F_Rat by RAT_1:def 2;

        

         A15: a2 <> ( 0. F_Rat );

        (g . a) = ((( canHom_Int F) . ( numerator a)) / (( canHom_Int F) . ( denominator a))) by Def11

        .= ((f . a1) / (( canHom_Int F) . ( denominator a))) by A12

        .= ((f . a1) / (f . a2)) by A12

        .= ((f . a1) * (f . (a2 " ))) by A15, QUOFIELD: 52

        .= (f . (a1 * (a2 " ))) by A2

        .= (f . (( numerator a) * (( denominator a) " ))) by GAUSSINT: 15

        .= (f . a) by RAT_1: 15;

        hence (f . x) = (g . x);

      end;

      hence thesis by A4;

    end;

    registration

      cluster F_Rat -> F_Rat -homomorphic;

      coherence ;

    end

    registration

      let F be 0 -characteristic Field;

      cluster ( PrimeField F) -> F_Rat -homomorphic;

      coherence ;

    end

    theorem :: RING_3:100

    for f be Homomorphism of F_Rat , F_Rat holds f = ( id F_Rat )

    proof

      let f be Homomorphism of F_Rat , F_Rat ;

      ( id F_Rat ) = ( canHom_Rat F_Rat ) by Th98;

      hence thesis by Th98;

    end;

    definition

      let F be Field, S be F -homomorphic Field, f be Homomorphism of F, S;

      :: original: Image

      redefine

      func Image f -> strict Subfield of S ;

      coherence

      proof

        set I = ( Image f);

        the carrier of I = ( rng f) & the addF of I = (the addF of S || ( rng f)) & the multF of I = (the multF of S || ( rng f)) & ( 1. I) = ( 1. S) & ( 0. I) = ( 0. S) by RING_2:def 6;

        hence thesis by EC_PF_1:def 1;

      end;

    end

    registration

      let F be 0 -characteristic Field;

      cluster ( canHom_Rat ( PrimeField F)) -> onto;

      coherence

      proof

        set K = ( PrimeField F);

        

        thus the carrier of K = the carrier of ( Image ( canHom_Rat K)) by EC_PF_1:def 2

        .= ( rng ( canHom_Rat K)) by RING_2:def 6;

      end;

    end

    theorem :: RING_3:101

    

     Th100: for F be 0 -characteristic Field holds ( F_Rat ,( PrimeField F)) are_isomorphic

    proof

      let F be 0 -characteristic Field;

      take ( canHom_Rat ( PrimeField F));

      thus thesis;

    end;

    theorem :: RING_3:102

    ( PrimeField F_Rat ) = F_Rat by GAUSSINT: 26;

    theorem :: RING_3:103

    for F be 0 -characteristic Field holds F includes F_Rat by Th71;

    theorem :: RING_3:104

    for F be 0 -characteristic Field, E be Field st F includes E holds E includes F_Rat

    proof

      let F be 0 -characteristic Field, E be Field;

      assume F includes E;

      then F is E -monomorphic by Th71;

      

      then ( Char E) = ( Char F) by Th87

      .= 0 by Def6;

      then E is 0 -characteristic;

      hence thesis by Th71;

    end;

    theorem :: RING_3:105

    

     Th104: for p be Prime, R be p -characteristic Ring, i be Integer holds (i '*' ( 1. R)) = ((i mod p) '*' ( 1. R))

    proof

      let p be Prime, R be p -characteristic Ring, i be Integer;

      ( Char R) = p by Def6;

      then

       A1: (p '*' ( 1. R)) = ( 0. R) by Def5;

      

       A2: (((i div p) * p) '*' ( 1. R)) = (((i div p) '*' ( 1. R)) * (p '*' ( 1. R))) by Th66

      .= ( 0. R) by A1;

      

      thus (i '*' ( 1. R)) = ((((i div p) * p) + (i mod p)) '*' ( 1. R)) by INT_1: 59

      .= (( 0. R) + ((i mod p) '*' ( 1. R))) by A2, Th61

      .= ((i mod p) '*' ( 1. R));

    end;

    definition

      let p be Prime, F be Field;

      :: RING_3:def12

      func canHom_Z/ (p,F) -> Function of ( Z/ p), F equals (( canHom_Int F) | the carrier of ( Z/ p));

      coherence

      proof

        set f = (( canHom_Int F) | the carrier of ( Z/ p));

        now

          let x be object;

          assume x in the carrier of ( Z/ p);

          then

          reconsider x1 = x as natural Number;

          x1 in INT by NUMBERS: 17, ORDINAL1:def 12;

          hence x in ( dom ( canHom_Int F)) by FUNCT_2:def 1;

        end;

        then the carrier of ( Z/ p) c= ( dom ( canHom_Int F));

        then

         A1: ( dom f) = the carrier of ( Z/ p) by RELAT_1: 62;

        now

          let x be object;

          assume

           A2: x in the carrier of ( Z/ p);

          then (f . x) = (( canHom_Int F) . x) by FUNCT_1: 49;

          then (f . x) in ( rng ( canHom_Int F)) by A1, A2, FUNCT_2: 4;

          hence (f . x) in the carrier of F;

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    

     Lm14: for p be Prime, F be Field, x be Element of ( Z/ p), y be Element of INT.Ring st x = y holds (( canHom_Z/ (p,F)) . x) = (y '*' ( 1. F))

    proof

      let p be Prime, F be Field, x be Element of ( Z/ p), y be Element of INT.Ring ;

      assume x = y;

      

      hence (( canHom_Z/ (p,F)) . x) = (( canHom_Int F) . y) by FUNCT_1: 49

      .= (y '*' ( 1. F)) by Def8;

    end;

    registration

      let p be Prime, F be Field;

      cluster ( canHom_Z/ (p,F)) -> unity-preserving;

      coherence

      proof

        set f = ( canHom_Z/ (p,F));

        set c = ( canHom_Int F);

        ( 1_ ( Z/ p)) = ( 1_ INT.Ring ) by INT_3: 14, INT_2:def 4;

        

        hence (f . ( 1_ ( Z/ p))) = (c . ( 1_ INT.Ring )) by FUNCT_1: 49

        .= ( 1_ F) by GROUP_1:def 13;

      end;

    end

    registration

      let p be Prime, F be p -characteristic Field;

      cluster ( canHom_Z/ (p,F)) -> additive multiplicative;

      coherence

      proof

        set f = ( canHom_Z/ (p,F));

        hereby

          let x,y be Element of ( Z/ p);

          reconsider x1 = x, y1 = y as Element of INT.Ring by ORDINAL1:def 12, NUMBERS: 17;

          

           A1: (x + y) = ((x1 + y1) mod p) by GR_CY_1:def 4;

          reconsider z = ((x1 + y1) mod p) as Element of INT.Ring by INT_1:def 2;

          

          thus ((f . x) + (f . y)) = ((x1 '*' ( 1. F)) + (f . y)) by Lm14

          .= ((x1 '*' ( 1. F)) + (y1 '*' ( 1. F))) by Lm14

          .= ((x1 + y1) '*' ( 1. F)) by Th61

          .= (z '*' ( 1. F)) by Th104

          .= (f . (x + y)) by Lm14, A1;

        end;

        hereby

          let x,y be Element of ( Z/ p);

          reconsider x1 = x, y1 = y as Element of INT.Ring by ORDINAL1:def 12, NUMBERS: 17;

          

           A2: (x * y) = ((x1 * y1) mod p) by INT_3:def 10;

          reconsider z = ((x1 * y1) mod p) as Element of INT.Ring by INT_1:def 2;

          

          thus ((f . x) * (f . y)) = ((x1 '*' ( 1. F)) * (f . y)) by Lm14

          .= ((x1 '*' ( 1. F)) * (y1 '*' ( 1. F))) by Lm14

          .= ((x1 * y1) '*' ( 1. F)) by Th66

          .= (z '*' ( 1. F)) by Th104

          .= (f . (x * y)) by Lm14, A2;

        end;

      end;

    end

    registration

      let p be Prime;

      cluster -> ( Z/ p) -monomorphic for p -characteristic Field;

      coherence

      proof

        let F be p -characteristic Field;

        take ( canHom_Z/ (p,F));

        thus thesis;

      end;

    end

    registration

      let p be Prime;

      cluster p -characteristic( Z/ p) -homomorphic for Field;

      existence ;

      cluster ( Z/ p) -> ( Z/ p) -homomorphic;

      coherence ;

    end

    theorem :: RING_3:106

    

     Th105: for p be Prime, F be p -characteristic( Z/ p) -homomorphic Field, f be Homomorphism of ( Z/ p), F holds f = ( canHom_Z/ (p,F))

    proof

      let p be Prime, F be p -characteristic( Z/ p) -homomorphic Field, f be Homomorphism of ( Z/ p), F;

      set g = ( canHom_Z/ (p,F));

      

       A1: f is unity-preserving;

      

       A2: g is unity-preserving additive multiplicative;

      

       A3: ( dom f) = the carrier of ( Z/ p) by FUNCT_2:def 1

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

      

       A4: ( 1. ( Z/ p)) = 1 by INT_3: 14, INT_2:def 4;

      reconsider p1 = (p - 1) as Element of NAT by INT_1: 3;

      

       A5: (p1 + 1) = p;

      defpred P[ Nat] means for j be Element of ( Z/ p) st j = $1 holds (f . j) = (g . j);

      (f . 0 ) = (f . ( 0. ( Z/ p))) by NAT_1: 44, SUBSET_1:def 8

      .= ( 0. F) by RING_2: 6

      .= (g . ( 0. ( Z/ p))) by RING_2: 6

      .= (g . 0 ) by NAT_1: 44, SUBSET_1:def 8;

      then

       A6: P[ 0 ];

      

       A7: for k be Element of NAT st 0 <= k & k < p1 holds P[k] implies P[(k + 1)]

      proof

        let k be Element of NAT ;

        assume

         A8: 0 <= k & k < p1;

        assume

         A9: P[k];

        reconsider e = 1 as Element of ( Segm p) by A4;

        k < p by A5, A8, NAT_1: 13;

        then

        reconsider z = k as Element of ( Z/ p) by NAT_1: 44;

        reconsider z0 = z as Element of ( Segm p);

        

         A10: (k + 1) < (p1 + 1) by A8, XREAL_1: 6;

        then

        reconsider z1 = (k + 1) as Element of ( Segm p) by NAT_1: 44;

        reconsider z1 as Element of ( Z/ p);

        

         A11: (z + ( 1. ( Z/ p))) = (( addint p) . (k,1)) by INT_3: 14, INT_2:def 4

        .= (z0 + e) by A10, INT_3: 7

        .= (k + 1);

        (f . z1) = ((f . z) + (f . ( 1. ( Z/ p)))) by A11, VECTSP_1:def 20

        .= ((g . z) + (g . ( 1. ( Z/ p)))) by A9, A1, A2

        .= (g . z1) by A11, A2;

        hence P[(k + 1)];

      end;

      

       A12: for k be Element of NAT st 0 <= k & k <= p1 holds P[k] from INT_1:sch 7( A6, A7);

      now

        let x be object;

        assume x in ( dom f);

        then

        reconsider a = x as Element of ( Segm p);

        a < (p1 + 1) by NAT_1: 44;

        then a <= (p - 1) by NAT_1: 13;

        hence (f . x) = (g . x) by A12;

      end;

      hence thesis by A3;

    end;

    theorem :: RING_3:107

    for p be Prime, f be Homomorphism of ( Z/ p), ( Z/ p) holds f = ( id ( Z/ p))

    proof

      let p be Prime;

      let f be Homomorphism of ( Z/ p), ( Z/ p);

      ( id ( Z/ p)) = ( canHom_Z/ (p,( Z/ p))) by Th105;

      hence thesis by Th105;

    end;

    registration

      let p be Prime, F be p -characteristic Field;

      cluster ( PrimeField F) -> ( Z/ p) -homomorphic;

      coherence ;

    end

    registration

      let p be Prime, F be p -characteristic Field;

      cluster ( canHom_Z/ (p,( PrimeField F))) -> onto;

      coherence

      proof

        set K = ( PrimeField F);

        

        thus the carrier of K = the carrier of ( Image ( canHom_Z/ (p,K))) by EC_PF_1:def 2

        .= ( rng ( canHom_Z/ (p,K))) by RING_2:def 6;

      end;

    end

    theorem :: RING_3:108

    

     Th107: for p be Prime, F be p -characteristic Field holds (( Z/ p),( PrimeField F)) are_isomorphic

    proof

      let p be Prime;

      let F be p -characteristic Field;

      take ( canHom_Z/ (p,( PrimeField F)));

      thus thesis;

    end;

    theorem :: RING_3:109

    for p be Prime, F be strict Subfield of ( Z/ p) holds F = ( Z/ p) by EC_PF_1:def 2;

    theorem :: RING_3:110

    for p be Prime holds ( PrimeField ( Z/ p)) = ( Z/ p) by EC_PF_1:def 2;

    theorem :: RING_3:111

    for p be Prime, F be p -characteristic Field holds F includes ( Z/ p) by Th71;

    theorem :: RING_3:112

    for p be Prime, F be p -characteristic Field, E be Field st F includes E holds E includes ( Z/ p)

    proof

      let p be Prime, F be p -characteristic Field, E be Field;

      assume F includes E;

      then F is E -monomorphic by Th71;

      

      then ( Char E) = ( Char F) by Th87

      .= p by Def6;

      then E is p -characteristic;

      hence thesis by Th71;

    end;

    registration

      let p be Prime;

      cluster ( Z/ p) -> prime;

      coherence ;

    end

    theorem :: RING_3:113

    for F be Field holds ( Char F) = 0 iff (( PrimeField F), F_Rat ) are_isomorphic

    proof

      let F be Field;

       A1:

      now

        assume ( Char F) = 0 ;

        then F is 0 -characteristic;

        hence (( PrimeField F), F_Rat ) are_isomorphic by Th100;

      end;

      now

        assume (( PrimeField F), F_Rat ) are_isomorphic ;

        then ex f be Function of F_Rat , ( PrimeField F) st f is RingIsomorphism by QUOFIELD:def 23;

        then ( PrimeField F) is F_Rat -isomorphic;

        then

         A2: ( PrimeField F) is 0 -characteristic;

        ( PrimeField F) is Subring of F by Lm1;

        hence ( Char F) = 0 by A2, Th88;

      end;

      hence thesis by A1;

    end;

    theorem :: RING_3:114

    for p be Prime, F be Field holds ( Char F) = p iff (( PrimeField F),( Z/ p)) are_isomorphic

    proof

      let p be Prime, F be Field;

       A1:

      now

        assume ( Char F) = p;

        then F is p -characteristic;

        hence (( PrimeField F),( Z/ p)) are_isomorphic by Th107;

      end;

      now

        assume (( PrimeField F),( Z/ p)) are_isomorphic ;

        then ex f be Function of ( Z/ p), ( PrimeField F) st f is RingIsomorphism by QUOFIELD:def 23;

        then ( PrimeField F) is ( Z/ p) -isomorphic;

        then

         A2: ( PrimeField F) is p -characteristic;

        ( PrimeField F) is Subring of F by Lm1;

        hence ( Char F) = p by A2, Th88;

      end;

      hence thesis by A1;

    end;

    theorem :: RING_3:115

    for F be strict Field holds F is prime iff ((F, F_Rat ) are_isomorphic or ex p be Prime st (F,( Z/ p)) are_isomorphic )

    proof

      let F be strict Field;

      thus F is prime implies (F, F_Rat ) are_isomorphic or ex p be Prime st (F,( Z/ p)) are_isomorphic

      proof

        assume

         A1: F is prime;

        per cases by Th85;

          suppose ( Char F) = 0 ;

          then F is 0 -characteristic;

          then (( PrimeField F), F_Rat ) are_isomorphic by Th100;

          hence thesis by EC_PF_1:def 2, A1;

        end;

          suppose ( Char F) is prime;

          then

          consider p be Prime such that

           A2: ( Char F) = p;

          F is p -characteristic by A2;

          then

           A3: (( PrimeField F),( Z/ p)) are_isomorphic by Th107;

          (( PrimeField F),F) are_isomorphic by EC_PF_1:def 2, A1;

          hence thesis by A3, Th43;

        end;

      end;

      assume

       A4: (F, F_Rat ) are_isomorphic or ex p be Prime st (F,( Z/ p)) are_isomorphic ;

      per cases by A4;

        suppose (F, F_Rat ) are_isomorphic ;

        then

        consider f be Function of F, F_Rat such that

         A5: f is RingIsomorphism;

        

         A6: F_Rat is F -isomorphic by A5;

        then

        reconsider EK1 = F_Rat as F -homomorphic Field;

        reconsider f as Homomorphism of F, EK1 by A5;

        now

          let K be Field;

          assume

           A7: K is strict Subfield of F;

          then

          reconsider EK = F_Rat as K -homomorphic Field by A6, Th56;

          reconsider g = (f | K) as Homomorphism of K, EK by A7, Th57;

          

           A8: ( Image g) = F_Rat by EC_PF_1:def 2;

          

           A9: the carrier of K c= the carrier of F by A7, EC_PF_1:def 1;

          now

            let x be object;

            assume x in the carrier of F;

            then

            reconsider a = x as Element of the carrier of F;

            (f . a) in ( Image g) by A8;

            then (f . a) in ( rng g) by RING_2:def 6;

            then

            consider y be object such that

             A10: y in ( dom g) & (g . y) = (f . a) by FUNCT_1:def 3;

            reconsider y as Element of the carrier of K by A10;

            

             A11: y in the carrier of F by A9;

            ((f | the carrier of K) . y) = (f . y) by FUNCT_1: 49;

            then a = y by A10, A11, FUNCT_2: 19;

            hence x in the carrier of K;

          end;

          then the carrier of F c= the carrier of K;

          then

           A12: the carrier of F = the carrier of K by A7, EC_PF_1:def 1;

          the addF of K = (the addF of F || the carrier of K) & the multF of K = (the multF of F || the carrier of K) & ( 1. F) = ( 1. K) & ( 0. F) = ( 0. K) by A7, EC_PF_1:def 1;

          hence K = F by A7, A12;

        end;

        hence thesis by EC_PF_1:def 2;

      end;

        suppose ex p be Prime st (F,( Z/ p)) are_isomorphic ;

        then

        consider p be Prime such that

         A13: (F,( Z/ p)) are_isomorphic ;

        consider f be Function of F, ( Z/ p) such that

         A14: f is RingIsomorphism by A13;

        

         A15: ( Z/ p) is F -isomorphic by A14;

        then

        reconsider EK1 = ( Z/ p) as F -homomorphic Field;

        reconsider f as Homomorphism of F, EK1 by A14;

        now

          let K be Field;

          assume

           A16: K is strict Subfield of F;

          then

          reconsider EK = ( Z/ p) as K -homomorphic Field by A15, Th56;

          reconsider g = (f | K) as Homomorphism of K, EK by A16, Th57;

          

           A17: ( Image g) = ( Z/ p) by EC_PF_1:def 2;

          

           A18: the carrier of K c= the carrier of F by A16, EC_PF_1:def 1;

          now

            let x be object;

            assume x in the carrier of F;

            then

            reconsider a = x as Element of the carrier of F;

            (f . a) in ( Image g) by A17;

            then (f . a) in ( rng g) by RING_2:def 6;

            then

            consider y be object such that

             A19: y in ( dom g) & (g . y) = (f . a) by FUNCT_1:def 3;

            reconsider y as Element of the carrier of K by A19;

            

             A20: y in the carrier of F by A18;

            ((f | the carrier of K) . y) = (f . y) by FUNCT_1: 49;

            then a = y by A19, A20, FUNCT_2: 19;

            hence x in the carrier of K;

          end;

          then the carrier of F c= the carrier of K;

          then

           A21: the carrier of F = the carrier of K by A16, EC_PF_1:def 1;

          the addF of K = (the addF of F || the carrier of K) & the multF of K = (the multF of F || the carrier of K) & ( 1. F) = ( 1. K) & ( 0. F) = ( 0. K) by A16, EC_PF_1:def 1;

          hence K = F by A16, A21;

        end;

        hence thesis by EC_PF_1:def 2;

      end;

    end;