zmodul08.miz



    begin

    definition

      let V be Z_Module, v be Vector of V;

      :: ZMODUL08:def1

      attr v is divisible means

      : defDivisibleVector: for a be Element of INT.Ring st a <> ( 0. INT.Ring ) holds ex u be Vector of V st (a * u) = v;

    end

    registration

      let V be Z_Module;

      cluster ( 0. V) -> divisible;

      correctness

      proof

        for a be Element of INT.Ring st a <> 0 holds ex u be Vector of V st (a * u) = ( 0. V)

        proof

          let a be Element of INT.Ring such that a <> 0 ;

          take ( 0. V);

          thus thesis by ZMODUL01: 1;

        end;

        hence thesis;

      end;

    end

    registration

      let V be Z_Module;

      cluster divisible for Vector of V;

      correctness

      proof

        take ( 0. V);

        thus thesis;

      end;

    end

    theorem :: ZMODUL08:1

    for V be Z_Module, v,u be divisible Vector of V holds (v + u) is divisible

    proof

      let V be Z_Module, v,u be divisible Vector of V;

      thus for a be Element of INT.Ring st a <> ( 0. INT.Ring ) holds ex w be Vector of V st (v + u) = (a * w)

      proof

        let a be Element of INT.Ring such that

         A1: a <> ( 0. INT.Ring );

        consider v1 be Vector of V such that

         A2: v = (a * v1) by A1, defDivisibleVector;

        consider u1 be Vector of V such that

         A3: u = (a * u1) by A1, defDivisibleVector;

        take (v1 + u1);

        thus (v + u) = (a * (v1 + u1)) by A2, A3, VECTSP_1:def 14;

      end;

    end;

    theorem :: ZMODUL08:2

    for V be Z_Module, v be divisible Vector of V holds ( - v) is divisible

    proof

      let V be Z_Module, v be divisible Vector of V;

      thus for a be Element of INT.Ring st a <> ( 0. INT.Ring ) holds ex w be Vector of V st ( - v) = (a * w)

      proof

        let a be Element of INT.Ring such that

         A1: a <> ( 0. INT.Ring );

        consider u be Vector of V such that

         A2: v = (a * u) by A1, defDivisibleVector;

        take ( - u);

        thus ( - v) = (a * ( - u)) by A2, ZMODUL01: 6;

      end;

    end;

    theorem :: ZMODUL08:3

    for V be Z_Module, v be divisible Vector of V, i be Element of INT.Ring holds (i * v) is divisible

    proof

      let V be Z_Module, v be divisible Vector of V, i be Element of INT.Ring ;

      thus for a be Element of INT.Ring st a <> ( 0. INT.Ring ) holds ex w be Vector of V st (i * v) = (a * w)

      proof

        let a be Element of INT.Ring such that

         A1: a <> ( 0. INT.Ring );

        consider v1 be Vector of V such that

         A2: v = (a * v1) by A1, defDivisibleVector;

        take (i * v1);

        

        thus (i * v) = ((i * a) * v1) by A2, VECTSP_1:def 16

        .= (a * (i * v1)) by VECTSP_1:def 16;

      end;

    end;

    definition

      let V be Z_Module;

      :: ZMODUL08:def2

      attr V is divisible means

      : defDivisibleModule: for v be Vector of V holds v is divisible;

    end

    registration

      let V be Z_Module;

      cluster ( (0). V) -> divisible;

      correctness

      proof

        thus for x be Vector of ( (0). V) holds x is divisible

        proof

          let x be Vector of ( (0). V);

          x in ( (0). V);

          

          then x = ( 0. V) by ZMODUL02: 66

          .= ( 0. ( (0). V)) by ZMODUL01: 26;

          hence thesis;

        end;

      end;

    end

    registration

      cluster Rat-Module -> divisible;

      correctness

      proof

        set V = Rat-Module ;

        for v be Vector of V holds v is divisible

        proof

          let v be Vector of V;

          for a be Element of INT.Ring st a <> ( 0. INT.Ring ) holds ex u be Vector of V st (a * u) = v

          proof

            let a be Element of INT.Ring ;

            assume

             AS: a <> ( 0. INT.Ring );

            reconsider v1 = v as Element of F_Rat ;

            set u1 = ((1 / a) * v1);

            reconsider u1 as Element of F_Rat by RAT_1:def 2;

            reconsider u = u1 as Vector of V;

            take u;

            

            thus (a * u) = (a * u1) by ZMODUL07: 15

            .= v by AS, XCMPLX_1: 109;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      cluster divisible for Z_Module;

      correctness

      proof

        set ZR = Rat-Module ;

        take ZR;

        thus thesis;

      end;

    end

    registration

      let V be Z_Module;

      cluster divisible for Submodule of V;

      correctness

      proof

        ( (0). V) is divisible;

        hence thesis;

      end;

    end

    registration

      cluster non finitely-generated for divisible Z_Module;

      correctness

      proof

        reconsider ZR = Rat-Module as divisible Z_Module;

        take ZR;

        thus thesis;

      end;

    end

    theorem :: ZMODUL08:4

    

     LMLT11: (( Int-mult-left F_Rat ) | [: INT , INT :]) = ( Int-mult-left INT.Ring )

    proof

      set ad = (( Int-mult-left F_Rat ) | [: INT , INT :]);

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

      then

       A2: [: INT , INT :] c= ( dom ( Int-mult-left F_Rat )) by FUNCT_2:def 1;

      

       A3: ( dom ( Int-mult-left INT.Ring )) = [: INT , INT :] by FUNCT_2:def 1;

      for z be object st z in ( dom ad) holds (ad . z) = (( Int-mult-left INT.Ring ) . 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 ZFMISC_1:def 2;

        reconsider x1 = x, y1 = y as Element of INT.Ring by A5;

        reconsider y2 = y1 as Element of F_Rat by RAT_1:def 2;

        reconsider y3 = y1 as Element of INT.Ring ;

        

        thus (ad . z) = (( Int-mult-left F_Rat ) . (x1,y1)) by A4, A5, FUNCT_1: 49

        .= (x1 * y2) by ZMODUL07: 15

        .= (( Int-mult-left INT.Ring ) . (x1,y3)) by ZMODUL06: 14

        .= (( Int-mult-left INT.Ring ) . z) by A5;

      end;

      hence thesis by A2, A3, FUNCT_1: 2, RELAT_1: 62;

    end;

    

     LMLT12: ( addreal || INT ) = addint

    proof

      set ad = ( addreal || INT );

       [: INT , INT :] c= [: REAL , REAL :] by NUMBERS: 15, ZFMISC_1: 96;

      then

       A1: [: INT , INT :] c= ( dom addreal ) 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) = ( addreal . (x1,y1)) by A4, A5, A2, FUNCT_1: 49

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

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

        .= ( addint . z) by A5;

      end;

      hence thesis by A1, A3, FUNCT_1: 2, RELAT_1: 62;

    end;

    theorem :: ZMODUL08:5

     ModuleStr (# the carrier of INT.Ring , the addF of INT.Ring , the ZeroF of INT.Ring , ( Int-mult-left INT.Ring ) #) is Submodule of Rat-Module

    proof

      set W = ModuleStr (# the carrier of INT.Ring , the addF of INT.Ring , the ZeroF of INT.Ring , ( Int-mult-left INT.Ring ) #);

      set V = Rat-Module ;

      

       G1: W is Z_Module by ZMODUL01: 164;

      

       P2: ( 0. W) = ( 0. V);

      (the addF of V || the carrier of W) = the addF of W by LMLT12, GAUSSINT: 13, NUMBERS: 14, RELAT_1: 74, ZFMISC_1: 96;

      hence thesis by G1, P2, LMLT11, NUMBERS: 14, VECTSP_4:def 2;

    end;

    theorem :: ZMODUL08:6

    

     LMLT2: for V be divisible Z_Module, W be Submodule of V holds ( VectQuot (V,W)) is divisible

    proof

      let V be divisible Z_Module, W be Submodule of V;

      set VW = ( VectQuot (V,W));

      

       X0: the carrier of VW = ( CosetSet (V,W)) by VECTSP10:def 6;

      for vw be Vector of VW holds vw is divisible

      proof

        let vw be Vector of VW;

        for a be Element of INT.Ring st a <> 0 holds ex u be Vector of VW st (a * u) = vw

        proof

          let a be Element of INT.Ring ;

          assume

           AS: a <> 0 ;

          vw in ( CosetSet (V,W)) by X0;

          then

          consider A be Coset of W such that

           X1: vw = A;

          consider v be Vector of V such that

           X2: A = (v + W) by VECTSP_4:def 6;

          v is divisible by defDivisibleModule;

          then

          consider u0 be Vector of V such that

           X3: (a * u0) = v by AS;

          (u0 + W) is Coset of W by VECTSP_4:def 6;

          then (u0 + W) in ( CosetSet (V,W));

          then

          reconsider B = (u0 + W) as Element of ( CosetSet (V,W));

          reconsider u = B as Vector of ( VectQuot (V,W)) by VECTSP10:def 6;

          take u;

          

          thus (a * u) = (( lmultCoset (V,W)) . (a,B)) by VECTSP10:def 6

          .= vw by X1, X2, X3, VECTSP10:def 5;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      cluster non trivial for divisible Z_Module;

      correctness

      proof

        reconsider ZR = Rat-Module as divisible Z_Module;

        take ZR;

        reconsider v = 1 as Element of F_Rat ;

        thus ZR is non trivial;

      end;

    end

    theorem :: ZMODUL08:7

    for V be Z_Module holds V is divisible iff ( (Omega). V) is divisible

    proof

      let V be Z_Module;

      hereby

        assume

         A1: V is divisible;

        for vv be Vector of ( (Omega). V) holds vv is divisible

        proof

          let vv be Vector of ( (Omega). V);

          reconsider v = vv as Vector of V;

          

           B1: v is divisible by A1;

          for a be Element of INT.Ring st a <> 0 holds ex uu be Vector of ( (Omega). V) st (a * uu) = vv

          proof

            let a be Element of INT.Ring such that

             C1: a <> 0 ;

            consider u be Vector of V such that

             C2: (a * u) = v by B1, C1;

            reconsider uu = u as Vector of ( (Omega). V);

            take uu;

            thus thesis by C2;

          end;

          hence thesis;

        end;

        hence ( (Omega). V) is divisible;

      end;

      assume

       A1: ( (Omega). V) is divisible;

      for v be Vector of V holds v is divisible

      proof

        let v be Vector of V;

        reconsider vv = v as Vector of ( (Omega). V);

        

         B1: vv is divisible by A1;

        for a be Element of INT.Ring st a <> 0 holds ex u be Vector of V st (a * u) = v

        proof

          let a be Element of INT.Ring such that

           C1: a <> 0 ;

          consider uu be Vector of ( (Omega). V) such that

           C2: (a * uu) = vv by B1, C1;

          reconsider u = uu as Vector of V;

          take u;

          thus thesis by C2;

        end;

        hence thesis;

      end;

      hence V is divisible;

    end;

    theorem :: ZMODUL08:8

    

     LmFGND1: for V be Z_Module, v be Vector of V st v is non torsion holds ( Lin {v}) is non divisible

    proof

      let V be Z_Module, v be Vector of V such that

       A1: v is non torsion;

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

      assume

       A2: ( Lin {v}) is divisible;

      v in ( Lin {v}) by ZMODUL06: 20;

      then

      reconsider vv = v as Vector of ( Lin {v});

      vv is divisible by A2;

      then

      consider uu be Vector of ( Lin {v}) such that

       A3: (i2 * uu) = vv;

      reconsider u = uu as Vector of V by ZMODUL01: 25;

      u in ( Lin {v});

      then

      consider i be Element of INT.Ring such that

       A4: u = (i * v) by ZMODUL06: 19;

      reconsider i3 = i as Integer;

      v = (i2 * (i * v)) by A3, A4, ZMODUL01: 29

      .= ((i2 * i) * v) by VECTSP_1:def 16;

      then (((i2 * i) * v) - v) = ( 0. V) by RLVECT_1: 15;

      then (((i2 * i) * v) - (( 1. INT.Ring ) * v)) = ( 0. V) by VECTSP_1:def 17;

      then

       A5: (((i2 * i) - ( 1. INT.Ring )) * v) = ( 0. V) by ZMODUL01: 9;

      ((2 * i3) - 1) <> 0

      proof

        assume ((2 * i3) - 1) = 0 ;

        then (1 / 2) is Integer;

        hence contradiction by NAT_D: 33;

      end;

      hence contradiction by A1, A5;

    end;

    theorem :: ZMODUL08:9

    

     LmFGND2: for V be Z_Module, v be Vector of V st v is torsion & v <> ( 0. V) holds ( Lin {v}) is non divisible

    proof

      let V be Z_Module, v be Vector of V such that

       A1: v is torsion & v <> ( 0. V);

      consider i be Element of INT.Ring such that

       A2: i <> 0 & (i * v) = ( 0. V) by A1;

      assume

       A3: ( Lin {v}) is divisible;

      v in ( Lin {v}) by ZMODUL06: 20;

      then

      reconsider vv = v as Vector of ( Lin {v});

      vv is divisible by A3;

      then

      consider uu be Vector of ( Lin {v}) such that

       A4: (i * uu) = vv by A2;

      reconsider u = uu as Vector of V by ZMODUL01: 25;

      u in ( Lin {v});

      then

      consider b be Element of INT.Ring such that

       A5: u = (b * v) by ZMODUL06: 19;

      vv = (i * (b * v)) by A4, A5, ZMODUL01: 29

      .= ((i * b) * v) by VECTSP_1:def 16

      .= (b * (i * v)) by VECTSP_1:def 16

      .= ( 0. V) by A2, ZMODUL01: 1;

      hence contradiction by A1;

    end;

    registration

      let V be non trivial Z_Module, v be non zero Vector of V;

      cluster ( Lin {v}) -> non divisible;

      correctness

      proof

        per cases ;

          suppose v is torsion;

          hence thesis by LmFGND2;

        end;

          suppose v is non torsion;

          hence thesis by LmFGND1;

        end;

      end;

    end

    registration

      let V be non trivial Z_Module;

      cluster non divisible for Submodule of V;

      correctness

      proof

        set v = the non zero Vector of V;

        ( Lin {v}) is non divisible;

        hence thesis;

      end;

    end

    theorem :: ZMODUL08:10

    

     LmFGND3: for V be non trivial finitely-generated torsion-free Z_Module holds V is non divisible

    proof

      let V be non trivial finitely-generated torsion-free Z_Module;

      consider I be finite Subset of V such that

       A1: I is Basis of V by ZMODUL03:def 3;

      ( (Omega). V) <> ( (0). V);

      then ( Lin I) <> ( (0). V) by A1, VECTSP_7:def 3;

      then I <> ( {} the carrier of V) by ZMODUL02: 67;

      then

      consider v be object such that

       A3: v in I by XBOOLE_0:def 1;

      reconsider v as Vector of V by A3;

      

       A4: V is Submodule of V & I is linearly-independent & ( (Omega). V) = ( Lin I) by A1, ZMODUL01: 32, VECTSP_7:def 3;

      then

       A5: ( (Omega). V) = (( Lin (I \ {v})) + ( Lin {v})) & (( Lin (I \ {v})) /\ ( Lin {v})) = ( (0). V) & ( Lin (I \ {v})) is free & ( Lin {v}) is free & v <> ( 0. V) by A3, ZMODUL06: 24;

      ((I \ {v}) \/ {v}) = (I \/ {v}) by XBOOLE_1: 39

      .= I by A3, XBOOLE_1: 12, ZFMISC_1: 31;

      then

       B3: ( Lin I) = (( Lin (I \ {v})) + ( Lin {v})) by ZMODUL02: 72;

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

      v is non divisible

      proof

        assume v is divisible;

        then

        consider u be Vector of V such that

         C1: (i2 * u) = v;

        u in ( Lin I) by A4;

        then

        consider u1,u2 be Vector of V such that

         C2: u1 in ( Lin (I \ {v})) & u2 in ( Lin {v}) & u = (u1 + u2) by B3, ZMODUL01: 92;

        consider iu2 be Element of INT.Ring such that

         C3: u2 = (iu2 * v) by C2, ZMODUL06: 19;

        

         C4: u1 <> ( 0. V)

        proof

          assume u1 = ( 0. V);

          then v = ((i2 * iu2) * v) by C1, C2, C3, VECTSP_1:def 16;

          then (((i2 * iu2) * v) - v) = ( 0. V) by RLVECT_1: 15;

          then (((i2 * iu2) * v) - (( 1. INT.Ring ) * v)) = ( 0. V) by VECTSP_1:def 17;

          then

           D1: (((i2 * iu2) - ( 1. INT.Ring )) * v) = ( 0. V) by ZMODUL01: 9;

          reconsider iiu2 = iu2 as Integer;

          ((2 * iiu2) - 1) <> 0

          proof

            assume ((2 * iiu2) - 1) = 0 ;

            then (1 / 2) is Integer;

            hence contradiction by NAT_D: 33;

          end;

          then v is torsion by D1;

          hence contradiction by A5, ZMODUL06:def 3;

        end;

        v = ((i2 * u1) + (i2 * u2)) by C1, C2, VECTSP_1:def 14

        .= ((i2 * u1) + ((i2 * iu2) * v)) by C3, VECTSP_1:def 16;

        

        then (v - ((i2 * iu2) * v)) = ((i2 * u1) + (((i2 * iu2) * v) - ((i2 * iu2) * v))) by RLVECT_1: 28

        .= ((i2 * u1) + ( 0. V)) by RLVECT_1: 15

        .= (i2 * u1);

        then ((( 1. INT.Ring ) * v) - ((i2 * iu2) * v)) = (i2 * u1) by VECTSP_1:def 17;

        then

         C5: ((( 1. INT.Ring ) - (i2 * iu2)) * v) = (i2 * u1) by ZMODUL01: 9;

        i2 <> ( 0. INT.Ring );

        then

         C6: (i2 * u1) <> ( 0. V) by C4, ZMODUL01:def 7;

        

         C7: (i2 * u1) in ( Lin (I \ {v})) by C2, ZMODUL01: 37;

        ((( 1. INT.Ring ) - (i2 * iu2)) * v) in ( Lin {v}) by ZMODUL06: 21;

        hence contradiction by A5, C5, C6, C7, ZMODUL01: 94, ZMODUL02: 66;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL08:11

    

     LmTM1: for V be non trivial finitely-generated torsion Z_Module holds ex i be Element of INT.Ring st i <> 0 & for v be Vector of V holds (i * v) = ( 0. V)

    proof

      let V be non trivial finitely-generated torsion Z_Module;

      defpred P[ Nat] means for I be finite Subset of V st ( card I) = $1 holds ex i be Element of INT.Ring st i <> 0 & for v be Vector of V st v in ( Lin I) holds (i * v) = ( 0. V);

      

       P1: P[ 0 ]

      proof

        let I be finite Subset of V;

        assume ( card I) = 0 ;

        then

         A2: I = ( {} the carrier of V);

        reconsider i = 1 as Element of INT.Ring ;

        take i;

        thus i <> 0 ;

        thus for v be Vector of V st v in ( Lin I) holds (i * v) = ( 0. V)

        proof

          let v be Vector of V;

          assume v in ( Lin I);

          then v in ( (0). V) by A2, ZMODUL02: 67;

          then v in {( 0. V)} by VECTSP_4:def 3;

          then v = ( 0. V) by TARSKI:def 1;

          hence (i * v) = ( 0. V) by ZMODUL01: 1;

        end;

      end;

      

       P2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A0: P[n];

        thus P[(n + 1)]

        proof

          let I be finite Subset of V;

          assume

           A1: ( card I) = (n + 1);

          then I <> {} ;

          then

          consider v be object such that

           A3: v in I by XBOOLE_0:def 1;

          reconsider v as Vector of V by A3;

          ((I \ {v}) \/ {v}) = (I \/ {v}) by XBOOLE_1: 39

          .= I by A3, ZFMISC_1: 40;

          then

           A4: ( Lin I) = (( Lin (I \ {v})) + ( Lin {v})) by ZMODUL02: 72;

          

           A5: ( card (I \ {v})) = (( card I) - ( card {v})) by A3, CARD_2: 44, ZFMISC_1: 31

          .= (( card I) - 1) by CARD_1: 30

          .= n by A1;

          reconsider J = (I \ {v}) as finite Subset of V;

          consider j be Element of INT.Ring such that

           B8: j <> 0 & for v be Vector of V st v in ( Lin J) holds (j * v) = ( 0. V) by A0, A5;

          v is torsion by ZMODUL06:def 2;

          then

          consider k be Element of INT.Ring such that

           A8: k <> 0 & (k * v) = ( 0. V);

          reconsider i = (j * k) as Element of INT.Ring ;

          take i;

          thus i <> 0 by A8, B8;

          thus for w be Vector of V st w in ( Lin I) holds (i * w) = ( 0. V)

          proof

            let w be Vector of V;

            assume w in ( Lin I);

            then

            consider u1,u2 be Vector of V such that

             A10: u1 in ( Lin (I \ {v})) & u2 in ( Lin {v}) & w = (u1 + u2) by A4, ZMODUL01: 92;

            consider iu2 be Element of INT.Ring such that

             A11: u2 = (iu2 * v) by A10, ZMODUL06: 19;

            

            thus (i * w) = ((i * u1) + (i * u2)) by A10, VECTSP_1:def 14

            .= ((k * (j * u1)) + ((j * k) * u2)) by VECTSP_1:def 16

            .= ((k * ( 0. V)) + ((j * k) * u2)) by B8, A10

            .= ((k * ( 0. V)) + (j * (k * u2))) by VECTSP_1:def 16

            .= ((k * ( 0. V)) + (j * ((k * iu2) * v))) by A11, VECTSP_1:def 16

            .= ((k * ( 0. V)) + (j * (iu2 * (k * v)))) by VECTSP_1:def 16

            .= (( 0. V) + (j * (iu2 * ( 0. V)))) by A8, ZMODUL01: 1

            .= (( 0. V) + (j * ( 0. V))) by ZMODUL01: 1

            .= ( 0. V) by ZMODUL01: 1;

          end;

        end;

      end;

      

       X1: for n be Nat holds P[n] from NAT_1:sch 2( P1, P2);

      consider I be finite Subset of V such that

       A1: ( Lin I) = the ModuleStr of V by ZMODUL03:def 4;

      ( card I) is Nat;

      then

      consider i be Element of INT.Ring such that

       X2: i <> 0 & for v be Vector of V st v in ( Lin I) holds (i * v) = ( 0. V) by X1;

      take i;

      thus i <> 0 by X2;

      thus for v be Vector of V holds (i * v) = ( 0. V)

      proof

        let v be Vector of V;

        v in ( Lin I) by A1;

        hence (i * v) = ( 0. V) by X2;

      end;

    end;

    theorem :: ZMODUL08:12

    

     LmFGND41: for V be non trivial finitely-generated torsion Z_Module, i be Element of INT.Ring st i <> 0 & for v be Vector of V holds (i * v) = ( 0. V) holds V is non divisible

    proof

      let V be non trivial finitely-generated torsion Z_Module, i be Element of INT.Ring such that

       A1: i <> 0 & for v be Vector of V holds (i * v) = ( 0. V);

      assume

       AS: V is divisible;

      set v = the non zero Vector of V;

      v is divisible by AS;

      then

      consider u be Vector of V such that

       A2: (i * u) = v by A1;

      thus contradiction by A1, A2;

    end;

    theorem :: ZMODUL08:13

    

     LmFGND4: for V be non trivial finitely-generated torsion Z_Module holds V is non divisible

    proof

      let V be non trivial finitely-generated torsion Z_Module;

      consider i be Element of INT.Ring such that

       A1: i <> 0 & for v be Vector of V holds (i * v) = ( 0. V) by LmTM1;

      thus thesis by A1, LmFGND41;

    end;

    registration

      cluster non divisible for non trivial finitely-generated torsion Z_Module;

      correctness

      proof

        set V = the non trivial finitely-generated torsion Z_Module;

        take V;

        thus thesis by LmFGND4;

      end;

    end

    theorem :: ZMODUL08:14

    

     ThFGND: for V be non trivial finitely-generated Z_Module holds V is non divisible

    proof

      let V be non trivial finitely-generated Z_Module;

      per cases ;

        suppose V is torsion;

        hence thesis by LmFGND4;

      end;

        suppose

         B2: V is non torsion;

        assume V is divisible;

        then ( VectQuot (V,( torsion_part V))) is divisible by LMLT2;

        hence contradiction by B2, LmFGND3;

      end;

    end;

    registration

      cluster -> non finitely-generated for non trivial divisible Z_Module;

      correctness by ThFGND;

    end

    registration

      let V be non trivial non divisible Z_Module;

      cluster non divisible for non zero Vector of V;

      correctness

      proof

        thus ex v be non zero Vector of V st v is non divisible

        proof

          assume

           AS: for v be non zero Vector of V holds v is divisible;

          for v be Vector of V holds v is divisible

          proof

            let v be Vector of V;

            per cases ;

              suppose v = ( 0. V);

              hence thesis;

            end;

              suppose v <> ( 0. V);

              then v is non zero;

              hence thesis by AS;

            end;

          end;

          hence contradiction by defDivisibleModule;

        end;

      end;

    end

    registration

      let V be non trivial finite-rank free Z_Module;

      cluster ( rank V) -> non zero;

      correctness

      proof

        assume ( rank V) is zero;

        then ( (Omega). V) = ( (0). V) by ZMODUL05: 1;

        hence contradiction;

      end;

    end

    theorem :: ZMODUL08:15

    

     LmND1: for V be non trivial free Z_Module, v be non zero Vector of V, I be Basis of V holds ex L be Linear_Combination of I, u be Vector of V st v = ( Sum L) & u in I & (L . u) <> 0

    proof

      let V be non trivial free Z_Module, v be non zero Vector of V, I be Basis of V;

      

       A1: I is linearly-independent & ( (Omega). V) = ( Lin I) by VECTSP_7:def 3;

      v in ( Lin I) by A1;

      then

      consider L be Linear_Combination of I such that

       A2: v = ( Sum L) by ZMODUL02: 64;

      ( Carrier L) <> {}

      proof

        assume ( Carrier L) = {} ;

        then ( Sum L) = ( 0. V) by ZMODUL02: 23;

        hence contradiction by A2;

      end;

      then

      consider uu be object such that

       A3: uu in ( Carrier L) by XBOOLE_0:def 1;

      consider u be Vector of V such that

       A4: u = uu & (L . u) <> 0 by A3;

      

       A5: ( Carrier L) c= I by VECTSP_6:def 4;

      take L, u;

      thus thesis by A2, A3, A4, A5;

    end;

    theorem :: ZMODUL08:16

    

     ThND1: for V be non trivial free Z_Module, v be non zero Vector of V holds v is non divisible

    proof

      let V be non trivial free Z_Module, v be non zero Vector of V;

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

      set I = the Basis of V;

      

       A1: I is linearly-independent & ( (Omega). V) = ( Lin I) by VECTSP_7:def 3;

      consider L be Linear_Combination of I, u be Vector of V such that

       A2: v = ( Sum L) & u in I & (L . u) <> 0 by LmND1;

      assume v is divisible;

      then

      consider w be Vector of V such that

       A5: ((i2 * (L . u)) * w) = v by A2;

      w in ( Lin I) by A1;

      then

      consider Lw be Linear_Combination of I such that

       A6: w = ( Sum Lw) by ZMODUL02: 64;

      reconsider Luw = ((i2 * (L . u)) * Lw) as Linear_Combination of I by ZMODUL02: 31;

      

       A8: ( Sum Luw) = ( Sum L) by A2, A5, A6, ZMODUL02: 53;

      ( Carrier Luw) c= I & ( Carrier L) c= I by VECTSP_6:def 4;

      then Luw = L by A8, VECTSP_7:def 3, ZMODUL03: 3;

      

      then (L . u) = ((i2 * (L . u)) * (Lw . u)) by VECTSP_6:def 9

      .= ((i2 * (Lw . u)) * (L . u));

      then (i2 * (Lw . u)) = 1 by A2, XCMPLX_1: 7;

      hence contradiction by INT_1: 9;

    end;

    registration

      cluster -> non divisible for non trivial free Z_Module;

      correctness

      proof

        let V be non trivial free Z_Module;

        set v = the non zero Vector of V;

        v is non divisible by ThND1;

        hence thesis;

      end;

    end

    theorem :: ZMODUL08:17

    

     LmND2: for V be non trivial free Z_Module, v be non zero Vector of V holds ex a be Element of INT.Ring st a in NAT & for b be Element of INT.Ring , u be Vector of V st b > a holds v <> (b * u)

    proof

      let V be non trivial free Z_Module, v be non zero Vector of V;

      set I = the Basis of V;

      

       A1: I is linearly-independent & ( (Omega). V) = ( Lin I) by VECTSP_7:def 3;

      consider L be Linear_Combination of I, w be Vector of V such that

       A2: v = ( Sum L) & w in I & (L . w) <> 0 by LmND1;

      reconsider a = |.(L . w).| as Element of INT.Ring ;

      

       A3: for b be Element of INT.Ring , u be Vector of V st b > a holds v <> (b * u)

      proof

        let b be Element of INT.Ring , u be Vector of V such that

         B0: b > a;

        assume

         B1: v = (b * u);

        u in ( Lin I) by A1;

        then

        consider Lu be Linear_Combination of I such that

         B2: u = ( Sum Lu) by ZMODUL02: 64;

        reconsider Lnu = (b * Lu) as Linear_Combination of I by ZMODUL02: 31;

        

         B4: ( Sum Lnu) = ( Sum L) by A2, B1, B2, ZMODUL02: 53;

        ( Carrier Lnu) c= I & ( Carrier L) c= I by VECTSP_6:def 4;

        then

         B5: Lnu = L by B4, VECTSP_7:def 3, ZMODUL03: 3;

        

         B6: (Lnu . w) = (b * (Lu . w)) by VECTSP_6:def 9;

        reconsider ib = b as Integer;

         |.(L . w).| <> 0 by A2, ABSVALUE: 2;

        then

         B8: |.(L . w).| > 0 by COMPLEX1: 46;

        

         N3: 0 <= b by B0, COMPLEX1: 46;

         |.(L . w).| = ( |.b.| * |.(Lu . w).|) by B5, B6, COMPLEX1: 65

        .= (ib * |.(Lu . w).|) by N3, ABSVALUE:def 1;

        hence contradiction by B0, B8, INT_1:def 3, INT_2: 27;

      end;

      take a;

      thus thesis by A3, COMPLEX1: 46, INT_1: 3;

    end;

    theorem :: ZMODUL08:18

    for V be non trivial free Z_Module, v be non zero Vector of V holds ex a be Element of INT.Ring , u be Vector of V st a in NAT & a <> 0 & v = (a * u) & for b be Element of INT.Ring , w be Vector of V st b > a holds v <> (b * w)

    proof

      let V be non trivial free Z_Module, v be non zero Vector of V;

      defpred P[ Nat] means ex u be Vector of V, k be Element of INT.Ring st k = $1 & v = (k * u);

      consider a be Element of INT.Ring such that

       A1: a in NAT & for b be Element of INT.Ring , u be Vector of V st b > a holds v <> (b * u) by LmND2;

      reconsider na = a as Nat by A1;

      

       A2: for k be Nat st P[k] holds k <= na by A1;

      

       A3: ex k be Nat st P[k]

      proof

        take 1;

        v = (( 1. INT.Ring ) * v) by VECTSP_1:def 17;

        hence thesis;

      end;

      consider a0 be Nat such that

       A4: P[a0] & for n be Nat st P[n] holds n <= a0 from NAT_1:sch 6( A2, A3);

      reconsider a = a0 as Element of INT.Ring by INT_1:def 2;

      consider u be Vector of V such that

       A5: v = (a * u) by A4;

      take a, u;

      thus a in NAT by ORDINAL1:def 12;

      thus a <> 0

      proof

        assume a = 0 ;

        then v = ( 0. V) by A5, ZMODUL01: 1;

        hence contradiction;

      end;

      thus v = (a * u) by A5;

      thus for b be Element of INT.Ring , w be Vector of V st b > a holds v <> (b * w)

      proof

        let b be Element of INT.Ring , w be Vector of V such that

         B1: b > a;

        b in NAT by B1, INT_1: 3;

        then

        reconsider bn = b as Nat;

         not P[bn] by A4, B1;

        hence thesis;

      end;

    end;

    begin

    definition

      let V be torsion-free Z_Module;

      :: ZMODUL08:def3

      func EMbedding (V) -> strict Z_Module means

      : defEmbedding: the carrier of it = ( rng ( MorphsZQ V)) & the ZeroF of it = ( zeroCoset V) & the addF of it = (( addCoset V) || ( rng ( MorphsZQ V))) & the lmult of it = (( lmultCoset V) | [: INT , ( rng ( MorphsZQ V)):]);

      existence

      proof

        set EZV = ( Z_MQ_VectSp V);

        

         D1: EZV = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

        

         AX: EZV is scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian non empty;

        set Cl = ( rng ( MorphsZQ V));

        set Add = (( addCoset V) || Cl);

        set Mlt = (( lmultCoset V) | [:the carrier of INT.Ring , ( rng ( MorphsZQ V)):]);

        

         X0: Cl c= the carrier of EZV;

        ( dom ( addCoset V)) = [:the carrier of EZV, the carrier of EZV:] by D1, FUNCT_2:def 1;

        then

         X3: ( dom Add) = [:Cl, Cl:] by RELAT_1: 62;

        for x be object st x in [:Cl, Cl:] holds (Add . x) in Cl

        proof

          let x be object;

          assume

           X40: x in [:Cl, Cl:];

          then

          consider v,w be object such that

           X41: v in Cl & w in Cl & x = [v, w] by ZFMISC_1:def 2;

          consider a be object such that

           X43: a in the carrier of V & v = (( MorphsZQ V) . a) by X41, FUNCT_2: 11;

          reconsider a as Vector of V by X43;

          

           X44: v = ( Class (( EQRZM V), [a, 1])) by ZMODUL04:def 6, X43;

          consider b be object such that

           X45: b in the carrier of V & w = (( MorphsZQ V) . b) by X41, FUNCT_2: 11;

          reconsider b as Vector of V by X45;

          

           X46: w = ( Class (( EQRZM V), [b, 1])) by ZMODUL04:def 6, X45;

          (Add . x) = (( addCoset V) . (v,w)) by X40, X41, FUNCT_1: 49

          .= ( Class (( EQRZM V), [((( 1. INT.Ring ) * a) + (( 1. INT.Ring ) * b)), (( 1. INT.Ring ) * ( 1. INT.Ring ))])) by D1, X41, X44, X46, ZMODUL04:def 2

          .= ( Class (( EQRZM V), [(a + (( 1. INT.Ring ) * b)), 1])) by VECTSP_1:def 17

          .= ( Class (( EQRZM V), [(a + b), 1])) by VECTSP_1:def 17

          .= (( MorphsZQ V) . (a + b)) by ZMODUL04:def 6;

          hence (Add . x) in Cl by FUNCT_2: 4;

        end;

        then

        reconsider Add as BinOp of Cl by X3, FUNCT_2: 3;

        ( dom ( lmultCoset V)) = [:the carrier of F_Rat , the carrier of EZV:] by FUNCT_2:def 1, D1;

        then

         Y3: ( dom Mlt) = [:the carrier of INT.Ring , Cl:] by RELAT_1: 62, NUMBERS: 14, ZFMISC_1: 96;

        for x be object st x in [:the carrier of INT.Ring , Cl:] holds (Mlt . x) in Cl

        proof

          let x be object;

          assume

           X40: x in [:the carrier of INT.Ring , Cl:];

          then

          consider i,w be object such that

           X41: i in INT & w in Cl & x = [i, w] by ZFMISC_1:def 2;

          consider b be object such that

           X45: b in the carrier of V & w = (( MorphsZQ V) . b) by X41, FUNCT_2: 11;

          reconsider b as Vector of V by X45;

          reconsider i as Element of INT.Ring by X41;

          reconsider j = i as Element of F_Rat by NUMBERS: 14;

          

           X47: j = (i / 1) & 1 <> 0 ;

          

           X46: w = ( Class (( EQRZM V), [b, 1])) by ZMODUL04:def 6, X45;

          (Mlt . x) = (( lmultCoset V) . (j,w)) by X40, X41, FUNCT_1: 49

          .= ( Class (( EQRZM V), [(i * b), (1 * 1)])) by D1, X41, X46, X47, ZMODUL04:def 4

          .= (( MorphsZQ V) . (i * b)) by ZMODUL04:def 6;

          hence (Mlt . x) in Cl by FUNCT_2: 4;

        end;

        then

        reconsider Mlt = (( lmultCoset V) | [:the carrier of INT.Ring , Cl:]) as Function of [:the carrier of INT.Ring , Cl:], ( rng ( MorphsZQ V)) by Y3, FUNCT_2: 3;

        

         X1: (( MorphsZQ V) . ( 0. V)) = ( 0. EZV) by ZMODUL04:def 6

        .= ( zeroCoset V) by D1;

        reconsider z = ( zeroCoset V) as Element of Cl by X1, FUNCT_2: 4;

        set ZS = ModuleStr (# Cl, Add, z, Mlt #);

        reconsider ZS as non empty ModuleStr over INT.Ring ;

        

         LM2: for x,y be Vector of ZS, v,w be Vector of EZV st x = v & y = w holds (x + y) = (v + w)

        proof

          let x,y be Vector of ZS, v,w be Vector of EZV;

          assume

           L0: x = v & y = w;

          

          thus (x + y) = (( addCoset V) . [x, y]) by FUNCT_1: 49

          .= (v + w) by D1, L0;

        end;

        

         LM3: for i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of EZV st i = j & x = v holds (i * x) = (j * v)

        proof

          let i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of EZV;

          assume

           L0: i = j & x = v;

          

          thus (i * x) = (( lmultCoset V) . [i, x]) by FUNCT_1: 49

          .= (j * v) by D1, L0;

        end;

        ZS is Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring

        proof

          

           P1: for x be Element of INT.Ring , v,w be Element of ZS holds (x * (v + w)) = ((x * v) + (x * w))

          proof

            let x be Element of INT.Ring , v,w be Element of ZS;

            reconsider y = x as Element of F_Rat by NUMBERS: 14;

            reconsider s = v, t = w as Vector of EZV by X0;

            

             P1: (v + w) = (s + t) by LM2;

            

             P2: (x * v) = (y * s) & (x * w) = (y * t) by LM3;

            

            thus (x * (v + w)) = (y * (s + t)) by P1, LM3

            .= ((y * s) + (y * t)) by AX

            .= ((x * v) + (x * w)) by LM2, P2;

          end;

          

           P2: for x,y be Element of INT.Ring , v be Element of ZS holds ((x + y) * v) = ((x * v) + (y * v))

          proof

            let x,y be Element of INT.Ring , v be Element of ZS;

            reconsider p = x, q = y as Element of F_Rat by NUMBERS: 14;

            reconsider p1 = p, q1 = q as Rational;

            reconsider s = v as Vector of EZV by X0;

            

             P1: (x * v) = (p * s) by LM3;

            

             P2: (y * v) = (q * s) by LM3;

            

            thus ((x + y) * v) = ((p + q) * s) by LM3

            .= ((p * s) + (q * s)) by AX

            .= ((x * v) + (y * v)) by P1, P2, LM2;

          end;

          

           P3: for x,y be Element of INT.Ring , v be Element of ZS holds ((x * y) * v) = (x * (y * v))

          proof

            let x,y be Element of INT.Ring , v be Element of ZS;

            reconsider p = x, q = y as Element of F_Rat by NUMBERS: 14;

            reconsider p1 = p, q1 = q as Rational;

            reconsider s = v as Vector of EZV by X0;

            

             P1: (y * v) = (q * s) by LM3;

            

            thus ((x * y) * v) = ((p * q) * s) by LM3

            .= (p * (q * s)) by AX

            .= (x * (y * v)) by P1, LM3;

          end;

          

           P4: for v be Element of ZS holds (( 1. INT.Ring ) * v) = v

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of EZV by X0;

            

            thus (( 1. INT.Ring ) * v) = (( 1. F_Rat ) * s) by LM3

            .= v by AX;

          end;

          

           P5: for v be Element of ZS holds v is right_complementable

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of EZV by X0;

            reconsider i1 = ( 1. F_Rat ) as Rational;

            

             P5: ( - s) = (( - ( 1. F_Rat )) * s) by VECTSP_1: 14;

            

             P1: (( - ( 1. INT.Ring )) * v) = (( - ( 1. F_Rat )) * s) by LM3;

            (v + (( - ( 1. INT.Ring )) * v)) = (s - s) by P1, P5, LM2

            .= ( 0. EZV) by RLVECT_1: 15

            .= ( 0. ZS) by D1;

            hence v is right_complementable;

          end;

          

           P6: for v,w be Element of ZS holds (v + w) = (w + v)

          proof

            let v,w be Element of ZS;

            reconsider s = v, t = w as Vector of EZV by X0;

            

            thus (v + w) = (s + t) by LM2

            .= (w + v) by LM2;

          end;

          

           P7: for u,v,w be Element of ZS holds ((u + v) + w) = (u + (v + w))

          proof

            let u,v,w be Element of ZS;

            reconsider z = u, s = v, t = w as Vector of EZV by X0;

            

             P1: (u + v) = (z + s) by LM2;

            

             P2: (v + w) = (s + t) by LM2;

            

            thus ((u + v) + w) = ((z + s) + t) by P1, LM2

            .= (z + (s + t)) by RLVECT_1:def 3

            .= (u + (v + w)) by LM2, P2;

          end;

          for v be Element of ZS holds (v + ( 0. ZS)) = v

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of EZV by X0;

            

            thus (v + ( 0. ZS)) = (s + ( 0. EZV)) by LM2, D1

            .= v;

          end;

          hence thesis by P1, P2, P3, P4, P5, P6, P7, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

        end;

        then

        reconsider ZS as strict Z_Module;

        take ZS;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: ZMODUL08:19

    

     SB01: for V be torsion-free Z_Module holds (for x be Vector of ( EMbedding V) holds x is Vector of ( Z_MQ_VectSp V)) & ( 0. ( EMbedding V)) = ( 0. ( Z_MQ_VectSp V)) & (for x,y be Vector of ( EMbedding V), v,w be Vector of ( Z_MQ_VectSp V) st x = v & y = w holds (x + y) = (v + w)) & for i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ( EMbedding V), v be Vector of ( Z_MQ_VectSp V) st i = j & x = v holds (i * x) = (j * v)

    proof

      let V be torsion-free Z_Module;

      set EZV = ( Z_MQ_VectSp V);

      

       D1: EZV = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

      set ZS = ( EMbedding V);

      

       AS1: the carrier of ZS = ( rng ( MorphsZQ V)) & the ZeroF of ZS = ( zeroCoset V) & the addF of ZS = (( addCoset V) || ( rng ( MorphsZQ V))) & the lmult of ZS = (( lmultCoset V) | [:the carrier of INT.Ring , ( rng ( MorphsZQ V)):]) by defEmbedding;

      set Cl = the carrier of ZS;

      set Add = (( addCoset V) || Cl);

      set Mlt = (( lmultCoset V) | [:the carrier of INT.Ring , ( rng ( MorphsZQ V)):]);

      Cl c= the carrier of EZV by AS1;

      hence for x be Vector of ZS holds x is Vector of EZV;

      thus ( 0. ZS) = ( 0. EZV) by D1, defEmbedding;

      thus for x,y be Vector of ZS, v,w be Vector of EZV st x = v & y = w holds (x + y) = (v + w)

      proof

        let x,y be Vector of ZS, v,w be Vector of EZV;

        assume

         L0: x = v & y = w;

        

        thus (x + y) = (( addCoset V) . [x, y]) by AS1, FUNCT_1: 49

        .= (v + w) by D1, L0;

      end;

      thus for i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of EZV st i = j & x = v holds (i * x) = (j * v)

      proof

        let i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of EZV;

        assume

         L0: i = j & x = v;

        

        thus (i * x) = (( lmultCoset V) . [i, x]) by AS1, FUNCT_1: 49

        .= (j * v) by D1, L0;

      end;

    end;

    theorem :: ZMODUL08:20

    

     SB02: for V be torsion-free Z_Module holds (for v,w be Vector of ( Z_MQ_VectSp V) st v in ( EMbedding V) & w in ( EMbedding V) holds (v + w) in ( EMbedding V)) & for j be Element of F_Rat , v be Vector of ( Z_MQ_VectSp V) st j in INT & v in ( EMbedding V) holds (j * v) in ( EMbedding V)

    proof

      let V be torsion-free Z_Module;

      set EZV = ( Z_MQ_VectSp V);

      set ZS = ( EMbedding V);

      set Cl = the carrier of ZS;

      set Add = (( addCoset V) || Cl);

      set Mlt = (( lmultCoset V) | [:the carrier of INT.Ring , ( rng ( MorphsZQ V)):]);

      thus for v,w be Vector of ( Z_MQ_VectSp V) st v in ( EMbedding V) & w in ( EMbedding V) holds (v + w) in ( EMbedding V)

      proof

        let v,w be Vector of ( Z_MQ_VectSp V);

        assume

         B1: v in ( EMbedding V) & w in ( EMbedding V);

        reconsider v1 = v, w1 = w as Vector of ( EMbedding V) by B1;

        (v + w) = (v1 + w1) by SB01;

        hence thesis;

      end;

      thus for j be Element of F_Rat , v be Vector of ( Z_MQ_VectSp V) st j in INT & v in ( EMbedding V) holds (j * v) in ( EMbedding V)

      proof

        let j be Element of F_Rat , v be Vector of ( Z_MQ_VectSp V);

        assume

         B1: j in INT & v in ( EMbedding V);

        then

        reconsider v1 = v as Vector of ( EMbedding V);

        reconsider i = j as Element of INT.Ring by B1;

        (j * v) = (i * v1) by SB01;

        hence thesis;

      end;

    end;

    theorem :: ZMODUL08:21

    

     SB03: for V be torsion-free Z_Module holds ex T be linear-transformation of V, ( EMbedding V) st T is bijective & T = ( MorphsZQ V) & (for v be Vector of V holds (T . v) = ( Class (( EQRZM V), [v, 1])))

    proof

      let V be torsion-free Z_Module;

      set T = ( MorphsZQ V);

      ( rng T) = the carrier of ( EMbedding V) by defEmbedding;

      then

      reconsider T0 = T as Function of V, ( EMbedding V) by FUNCT_2: 6;

      

       B0: T0 is additive

      proof

        let x,y be Element of V;

        thus (T0 . (x + y)) = ((T0 . x) + (T0 . y))

        proof

          

           L1: (T . (x + y)) = ((T . x) + (T . y)) by ZMODUL04:def 6;

          reconsider v = (T0 . x), w = (T0 . y) as Vector of ( EMbedding V);

          thus (T0 . (x + y)) = ((T0 . x) + (T0 . y)) by L1, SB01;

        end;

      end;

      for x be Vector of V, i be Element of INT.Ring holds (T0 . (i * x)) = (i * (T0 . x))

      proof

        let x be Vector of V, i be Element of INT.Ring ;

        thus (T0 . (i * x)) = (i * (T0 . x))

        proof

          reconsider j = i as Element of F_Rat by NUMBERS: 14;

          

           L1: (T . (i * x)) = (j * (T . x)) by ZMODUL04:def 6;

          reconsider v = (T0 . x) as Vector of ( EMbedding V);

          thus (T0 . (i * x)) = (i * (T0 . x)) by L1, SB01;

        end;

      end;

      then T0 is additive homogeneous by B0;

      then

      reconsider T0 as linear-transformation of V, ( EMbedding V);

      take T0;

      

       SS: T0 is one-to-one by ZMODUL04:def 6;

      ( rng T0) = the carrier of ( EMbedding V) by defEmbedding;

      then T0 is onto by FUNCT_2:def 3;

      hence T0 is bijective by SS;

      thus T0 = ( MorphsZQ V);

      thus thesis by ZMODUL04:def 6;

    end;

    theorem :: ZMODUL08:22

    for V be torsion-free Z_Module, vv be Vector of ( EMbedding V) holds ex v be Vector of V st (( MorphsZQ V) . v) = vv

    proof

      let V be torsion-free Z_Module, vv be Vector of ( EMbedding V);

      set Z = ( EMbedding V);

      consider T be linear-transformation of V, Z such that

       A1: T is bijective & T = ( MorphsZQ V) & (for v be Element of V holds (T . v) = ( Class (( EQRZM V), [v, 1]))) by SB03;

      vv in the carrier of Z;

      then vv in ( rng ( MorphsZQ V)) by A1, FUNCT_2:def 3;

      then

      consider v be object such that

       A2: v in the carrier of V & vv = (( MorphsZQ V) . v) by FUNCT_2: 11;

      reconsider v as Vector of V by A2;

      take v;

      thus thesis by A2;

    end;

    definition

      let V be torsion-free Z_Module;

      :: ZMODUL08:def4

      func DivisibleMod (V) -> strict Z_Module means

      : defDivisibleMod: the carrier of it = ( Class ( EQRZM V)) & the ZeroF of it = ( zeroCoset V) & the addF of it = ( addCoset V) & the lmult of it = (( lmultCoset V) | [: INT , ( Class ( EQRZM V)):]);

      existence

      proof

        set Z = ( Z_MQ_VectSp V);

        reconsider Z as VectSp of F_Rat ;

        set Mlt = (( lmultCoset V) | [: INT , ( Class ( EQRZM V)):]);

        ( dom ( lmultCoset V)) = [:the carrier of F_Rat , ( Class ( EQRZM V)):] by FUNCT_2:def 1;

        then

         Y3: ( dom Mlt) = [: INT , ( Class ( EQRZM V)):] by NUMBERS: 14, RELAT_1: 62, ZFMISC_1: 96;

        

         Z1: Z = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

        

         Z2: ( 0. Z) = ( zeroCoset V) by Z1;

        for x be object st x in [: INT , ( Class ( EQRZM V)):] holds (Mlt . x) in ( Class ( EQRZM V))

        proof

          let x be object;

          assume

           X40: x in [: INT , ( Class ( EQRZM V)):];

          then

          consider i,w be object such that

           X41: i in INT & w in ( Class ( EQRZM V)) & x = [i, w] by ZFMISC_1:def 2;

          reconsider i as Element of INT by X41;

          reconsider j = i as Element of F_Rat by NUMBERS: 14;

          reconsider b = w as Element of Z by X41, Z1;

          

           X46: (Mlt . x) = (( lmultCoset V) . (j,w)) by X40, X41, FUNCT_1: 49;

           [j, w] in [:the carrier of F_Rat , ( Class ( EQRZM V)):] by X41, ZFMISC_1: 87;

          hence thesis by X46, FUNCT_2: 5;

        end;

        then

        reconsider Mlt as Function of [:the carrier of INT.Ring , ( Class ( EQRZM V)):], ( Class ( EQRZM V)) by Y3, FUNCT_2: 3;

        set ZS = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), Mlt #);

        reconsider ZS as non empty ModuleStr over INT.Ring ;

        

         LM2: for x,y be Vector of ZS, v,w be Vector of Z st x = v & y = w holds (x + y) = (v + w) by Z1;

        

         LM3: for i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of Z st i = j & x = v holds (i * x) = (j * v)

        proof

          let i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of Z;

          assume

           L0: i = j & x = v;

          

          thus (i * x) = (( lmultCoset V) . [i, x]) by FUNCT_1: 49

          .= (j * v) by L0, Z1;

        end;

        ZS is Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring

        proof

          

           P1: for x be Element of INT.Ring holds for v,w be Element of ZS holds (x * (v + w)) = ((x * v) + (x * w))

          proof

            let x be Element of INT.Ring , v,w be Element of ZS;

            reconsider y = x as Element of F_Rat by NUMBERS: 14;

            reconsider s = v, t = w as Vector of Z by Z1;

            

             P2: (x * v) = (y * s) & (x * w) = (y * t) by LM3;

            

            thus (x * (v + w)) = (y * (s + t)) by Z1, LM3

            .= ((y * s) + (y * t)) by VECTSP_1:def 14

            .= ((x * v) + (x * w)) by P2, Z1;

          end;

          

           P2: for x,y be Element of INT.Ring holds for v be Element of ZS holds ((x + y) * v) = ((x * v) + (y * v))

          proof

            let x,y be Element of INT.Ring , v be Element of ZS;

            reconsider p = x, q = y as Element of F_Rat by NUMBERS: 14;

            reconsider p1 = p, q1 = q as Rational;

            reconsider s = v as Vector of Z by Z1;

            

             P2: (y * v) = (q * s) by LM3;

            

            thus ((x + y) * v) = ((p + q) * s) by LM3

            .= ((p * s) + (q * s)) by VECTSP_1:def 15

            .= ((x * v) + (y * v)) by P2, Z1, LM3;

          end;

          

           P3: for x,y be Element of INT.Ring holds for v be Element of ZS holds ((x * y) * v) = (x * (y * v))

          proof

            let x,y be Element of INT.Ring , v be Element of ZS;

            reconsider p = x, q = y as Element of F_Rat by NUMBERS: 14;

            reconsider p1 = p, q1 = q as Rational;

            reconsider s = v as Vector of Z by Z1;

            

             P1: (y * v) = (q * s) by LM3;

            

            thus ((x * y) * v) = ((p * q) * s) by LM3

            .= (p * (q * s)) by VECTSP_1:def 16

            .= (x * (y * v)) by P1, LM3;

          end;

          

           P4: for v be Element of ZS holds (( 1. INT.Ring ) * v) = v

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of Z by Z1;

            

            thus (( 1. INT.Ring ) * v) = (( 1. F_Rat ) * s) by LM3

            .= v by VECTSP_1:def 17;

          end;

          

           P5: for v be Element of ZS holds v is right_complementable

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of Z by Z1;

            reconsider i1 = ( 1. F_Rat ) as Rational;

            

             P5: ( - s) = (( - ( 1. F_Rat )) * s) by VECTSP_1: 14;

            (v + (( - ( 1. INT.Ring )) * v)) = (s - s) by P5, Z1, LM3

            .= ( 0. ZS) by Z2, RLVECT_1: 15;

            hence v is right_complementable;

          end;

          

           P6: for v,w be Element of ZS holds (v + w) = (w + v)

          proof

            let v,w be Element of ZS;

            reconsider s = v, t = w as Vector of Z by Z1;

            

            thus (v + w) = (s + t) by Z1

            .= (w + v) by LM2;

          end;

          

           P7: for u,v,w be Element of ZS holds ((u + v) + w) = (u + (v + w))

          proof

            let u,v,w be Element of ZS;

            reconsider z = u, s = v, t = w as Vector of Z by Z1;

            

            thus ((u + v) + w) = ((z + s) + t) by Z1

            .= (z + (s + t)) by RLVECT_1:def 3

            .= (u + (v + w)) by Z1;

          end;

          for v be Element of ZS holds (v + ( 0. ZS)) = v

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of Z by Z1;

            

            thus (v + ( 0. ZS)) = (s + ( 0. Z)) by Z1

            .= v;

          end;

          hence thesis by P1, P2, P3, P4, P5, P6, P7, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

        end;

        then

        reconsider ZS as strict Z_Module;

        take ZS;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: ZMODUL08:23

    

     ThDivisible1: for V be torsion-free Z_Module holds for v be Vector of ( DivisibleMod V) holds for a be Element of INT.Ring st a <> 0 holds ex u be Vector of ( DivisibleMod V) st (a * u) = v

    proof

      let V be torsion-free Z_Module;

      thus for v be Vector of ( DivisibleMod V) holds for a be Element of INT.Ring st a <> 0 holds ex u be Vector of ( DivisibleMod V) st (a * u) = v

      proof

        let v be Vector of ( DivisibleMod V);

        assume

         AS: ex a be Element of INT.Ring st a <> 0 & for u be Vector of ( DivisibleMod V) holds (a * u) <> v;

        consider a be Element of INT.Ring such that

         B1: a <> 0 & for u be Vector of ( DivisibleMod V) holds (a * u) <> v by AS;

        reconsider vv = v as Element of ( Class ( EQRZM V)) by defDivisibleMod;

        set Z = ( Z_MQ_VectSp V);

        reconsider Z as VectSp of F_Rat ;

        

         BX: Z = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

        reconsider vv as Element of Z by BX;

        reconsider aa = a as Element of F_Rat by NUMBERS: 14;

        

         B2: aa <> ( 0. F_Rat ) by B1;

        reconsider ai = (aa " ) as Element of F_Rat ;

        

         B3: (aa * ai) = ( 1. F_Rat ) by B2, VECTSP_1:def 10;

        set uu = (ai * vv);

        reconsider uu as Element of Z;

        reconsider u = uu as Element of ( DivisibleMod V) by BX, defDivisibleMod;

        (aa * uu) = ((aa * ai) * vv) by VECTSP_1:def 16

        .= vv by B3, VECTSP_1:def 17;

        

        then v = ((( lmultCoset V) | [: INT , ( Class ( EQRZM V)):]) . [a, u]) by BX, FUNCT_1: 49, ZFMISC_1: 87

        .= (a * u) by defDivisibleMod;

        hence contradiction by B1;

      end;

    end;

    registration

      let V be torsion-free Z_Module;

      cluster ( DivisibleMod V) -> divisible;

      correctness

      proof

        thus for v be Vector of ( DivisibleMod V) holds v is divisible by ThDivisible1;

      end;

    end

    theorem :: ZMODUL08:24

    

     ThDivisible2: for V be torsion-free Z_Module holds ( EMbedding V) is Submodule of ( DivisibleMod V)

    proof

      let V be torsion-free Z_Module;

      set EV = ( EMbedding V);

      set DV = ( DivisibleMod V);

      for x be object st x in the carrier of EV holds x in the carrier of DV

      proof

        let x be object such that

         B1: x in the carrier of EV;

        x in ( rng ( MorphsZQ V)) by B1, defEmbedding;

        then

        consider y be object such that

         B2: y in the carrier of V & (( MorphsZQ V) . y) = x by FUNCT_2: 11;

        reconsider y as Vector of V by B2;

        

         B3: ( Z_MQ_VectSp V) = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

        x in ( Class ( EQRZM V)) by B2, B3, FUNCT_2: 5;

        hence thesis by defDivisibleMod;

      end;

      then

       A1: the carrier of EV c= the carrier of DV;

      

       A2: ( 0. EV) = ( zeroCoset V) by defEmbedding

      .= ( 0. DV) by defDivisibleMod;

      

       A3: the addF of EV = (( addCoset V) || ( rng ( MorphsZQ V))) by defEmbedding

      .= (the addF of DV || ( rng ( MorphsZQ V))) by defDivisibleMod

      .= (the addF of DV || the carrier of EV) by defEmbedding;

      the lmult of EV = (the lmult of DV | [:the carrier of INT.Ring , ( rng ( MorphsZQ V)):])

      proof

        the carrier of EV c= ( Class ( EQRZM V)) by A1, defDivisibleMod;

        then

         B1: ( rng ( MorphsZQ V)) c= ( Class ( EQRZM V)) by defEmbedding;

        

        thus the lmult of EV = (( lmultCoset V) | [:the carrier of INT.Ring , ( rng ( MorphsZQ V)):]) by defEmbedding

        .= ((( lmultCoset V) | [:the carrier of INT.Ring , ( Class ( EQRZM V)):]) | [:the carrier of INT.Ring , ( rng ( MorphsZQ V)):]) by B1, RELAT_1: 74, ZFMISC_1: 96

        .= (the lmult of DV | [:the carrier of INT.Ring , ( rng ( MorphsZQ V)):]) by defDivisibleMod;

      end;

      then the lmult of EV = (the lmult of DV | [:the carrier of INT.Ring , the carrier of EV:]) by defEmbedding;

      hence thesis by A1, A2, A3, VECTSP_4:def 2;

    end;

    registration

      let V be finitely-generated torsion-free Z_Module;

      cluster ( EMbedding V) -> finitely-generated;

      correctness

      proof

        consider T be linear-transformation of V, ( EMbedding V) such that

         A1: T is bijective & T = ( MorphsZQ V) & (for v be Vector of V holds (T . v) = ( Class (( EQRZM V), [v, 1]))) by SB03;

        reconsider Z = ( EMbedding V) as free Z_Module by A1, ZMODUL06: 48;

        Z is finite-rank by A1, ZMODUL06: 50;

        hence thesis;

      end;

    end

    registration

      let V be non trivial torsion-free Z_Module;

      cluster ( EMbedding V) -> non trivial;

      correctness

      proof

        consider T be linear-transformation of V, ( EMbedding V) such that

         A1: T is bijective & T = ( MorphsZQ V) & (for v be Vector of V holds (T . v) = ( Class (( EQRZM V), [v, 1]))) by SB03;

        set v = the non zero Vector of V;

        (T . v) <> ( 0. ( EMbedding V))

        proof

          assume (T . v) = ( 0. ( EMbedding V));

          then (T . v) = (T . ( 0. V)) by ZMODUL05: 19;

          hence contradiction by A1, FUNCT_2: 19;

        end;

        then not (T . v) in ( (0). ( EMbedding V)) by ZMODUL02: 66;

        then ( (Omega). ( EMbedding V)) <> ( (0). ( EMbedding V));

        hence thesis by ZMODUL07: 41;

      end;

    end

    definition

      let G be Field;

      let V be VectSp of G;

      let W be Subset of V;

      let a be Element of G;

      :: ZMODUL08:def5

      func a * W -> Subset of V equals { (a * u) where u be Vector of V : u in W };

      coherence

      proof

        set Y = { (a * u) where u be Vector of V : u in W };

        defpred Sep[ object] means ex u be Vector of V st $1 = (a * u) & u in W;

        consider X be set such that

         A1: for x be object holds x in X iff x in the carrier of V & Sep[x] from XBOOLE_0:sch 1;

        X c= the carrier of V by A1;

        then

        reconsider X as Subset of V;

        

         A2: Y c= X

        proof

          let x be object;

          assume x in Y;

          then ex u be Vector of V st x = (a * u) & u in W;

          hence thesis by A1;

        end;

        X c= Y

        proof

          let x be object;

          assume x in X;

          then ex u be Vector of V st x = (a * u) & u in W by A1;

          hence thesis;

        end;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

    end

    definition

      let V be torsion-free Z_Module, r be Element of F_Rat ;

      :: ZMODUL08:def6

      func EMbedding (r,V) -> strict Z_Module means

      : defriV: the carrier of it = (r * ( rng ( MorphsZQ V))) & the ZeroF of it = ( zeroCoset V) & the addF of it = (( addCoset V) || (r * ( rng ( MorphsZQ V)))) & the lmult of it = (( lmultCoset V) | [:the carrier of INT.Ring , (r * ( rng ( MorphsZQ V))):]);

      existence

      proof

        set EZV = ( Z_MQ_VectSp V);

        

         D1: EZV = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

        

         AX: EZV is scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian non empty;

        

         BX: ( rng ( MorphsZQ V)) = the carrier of ( EMbedding V) by defEmbedding;

        set Cl = (r * ( rng ( MorphsZQ V)));

        set Add = (( addCoset V) || Cl);

        set Mlt = (( lmultCoset V) | [: INT , Cl:]);

        

         X0: Cl c= the carrier of EZV;

        ( dom ( addCoset V)) = [:the carrier of EZV, the carrier of EZV:] by D1, FUNCT_2:def 1;

        then

         X3: ( dom Add) = [:Cl, Cl:] by RELAT_1: 62;

        for x be object st x in [:Cl, Cl:] holds (Add . x) in Cl

        proof

          let x be object;

          assume

           X40: x in [:Cl, Cl:];

          then

          consider v0,w0 be object such that

           X41: v0 in Cl & w0 in Cl & x = [v0, w0] by ZFMISC_1:def 2;

          consider v be Vector of EZV such that

           X410: v0 = (r * v) & v in ( rng ( MorphsZQ V)) by X41;

          consider w be Vector of EZV such that

           X411: w0 = (r * w) & w in ( rng ( MorphsZQ V)) by X41;

          v in ( EMbedding V) & w in ( EMbedding V) by X410, X411, defEmbedding;

          then

           X42: (v + w) in ( EMbedding V) by SB02;

          (Add . x) = ((r * v) + (r * w)) by X40, X41, X410, X411, D1, FUNCT_1: 49

          .= (r * (v + w)) by VECTSP_1:def 14;

          hence (Add . x) in Cl by BX, X42;

        end;

        then

        reconsider Add as BinOp of Cl by X3, FUNCT_2: 3;

        ( dom ( lmultCoset V)) = [:the carrier of F_Rat , the carrier of EZV:] by FUNCT_2:def 1, D1;

        then

         Y3: ( dom Mlt) = [:the carrier of INT.Ring , Cl:] by RELAT_1: 62, NUMBERS: 14, ZFMISC_1: 96;

        for x be object st x in [:the carrier of INT.Ring , Cl:] holds (Mlt . x) in Cl

        proof

          let x be object;

          assume

           X40: x in [:the carrier of INT.Ring , Cl:];

          then

          consider i,w0 be object such that

           X41: i in INT & w0 in Cl & x = [i, w0] by ZFMISC_1:def 2;

          reconsider i1 = i as Integer by X41;

          reconsider i2 = i as Element of F_Rat by X41, NUMBERS: 14;

          consider w be Vector of EZV such that

           X411: w0 = (r * w) & w in ( rng ( MorphsZQ V)) by X41;

          w in ( EMbedding V) by X411, defEmbedding;

          then

           X42: (i2 * w) in ( EMbedding V) by SB02, X41;

          (Mlt . x) = (i2 * (r * w)) by D1, X40, X411, X41, FUNCT_1: 49

          .= ((i2 * r) * w) by VECTSP_1:def 16

          .= (r * (i2 * w)) by VECTSP_1:def 16;

          hence (Mlt . x) in Cl by BX, X42;

        end;

        then

        reconsider Mlt = (( lmultCoset V) | [:the carrier of INT.Ring , Cl:]) as Function of [:the carrier of INT.Ring , Cl:], Cl by Y3, FUNCT_2: 3;

        

         X1: (r * ( 0. EZV)) = ( 0. EZV) by VECTSP_1: 15;

        ( 0. EZV) = ( 0. ( EMbedding V)) by D1, defEmbedding;

        then

         X2: ( 0. EZV) in (r * ( rng ( MorphsZQ V))) by BX, X1;

        reconsider z = ( zeroCoset V) as Element of Cl by D1, X2;

        set ZS = ModuleStr (# Cl, Add, z, Mlt #);

        reconsider ZS as non empty ModuleStr over INT.Ring by X2;

        

         LM2: for x,y be Vector of ZS, v,w be Vector of EZV st x = v & y = w holds (x + y) = (v + w)

        proof

          let x,y be Vector of ZS, v,w be Vector of EZV;

          assume

           L0: x = v & y = w;

          

          thus (x + y) = (( addCoset V) . [x, y]) by FUNCT_1: 49

          .= (v + w) by D1, L0;

        end;

        

         LM3: for i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of EZV st i = j & x = v holds (i * x) = (j * v)

        proof

          let i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of EZV;

          assume

           L0: i = j & x = v;

          

          thus (i * x) = (( lmultCoset V) . [i, x]) by FUNCT_1: 49

          .= (j * v) by D1, L0;

        end;

        ZS is Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring

        proof

          

           P1: for x be Element of INT.Ring holds for v,w be Element of ZS holds (x * (v + w)) = ((x * v) + (x * w))

          proof

            let x be Element of INT.Ring , v,w be Element of ZS;

            reconsider y = x as Element of F_Rat by NUMBERS: 14;

            reconsider s = v, t = w as Vector of EZV by X0;

            

             P1: (v + w) = (s + t) by LM2;

            

             P2: (x * v) = (y * s) & (x * w) = (y * t) by LM3;

            

            thus (x * (v + w)) = (y * (s + t)) by P1, LM3

            .= ((y * s) + (y * t)) by AX

            .= ((x * v) + (x * w)) by LM2, P2;

          end;

          

           P2: for x,y be Element of INT.Ring holds for v be Element of ZS holds ((x + y) * v) = ((x * v) + (y * v))

          proof

            let x,y be Element of INT.Ring , v be Element of ZS;

            reconsider p = x, q = y as Element of F_Rat by NUMBERS: 14;

            reconsider p1 = p, q1 = q as Rational;

            reconsider s = v as Vector of EZV by X0;

            

             P1: (x * v) = (p * s) by LM3;

            

             P2: (y * v) = (q * s) by LM3;

            

            thus ((x + y) * v) = ((p + q) * s) by LM3

            .= ((p * s) + (q * s)) by AX

            .= ((x * v) + (y * v)) by P1, P2, LM2;

          end;

          

           P3: for x,y be Element of INT.Ring , v be Element of ZS holds ((x * y) * v) = (x * (y * v))

          proof

            let x,y be Element of INT.Ring , v be Element of ZS;

            reconsider p = x, q = y as Element of F_Rat by NUMBERS: 14;

            reconsider p1 = p, q1 = q as Rational;

            reconsider s = v as Vector of EZV by X0;

            

             P1: (y * v) = (q * s) by LM3;

            

            thus ((x * y) * v) = ((p * q) * s) by LM3

            .= (p * (q * s)) by AX

            .= (x * (y * v)) by P1, LM3;

          end;

          

           P4: for v be Element of ZS holds (( 1. INT.Ring ) * v) = v

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of EZV by X0;

            

            thus (( 1. INT.Ring ) * v) = (( 1. F_Rat ) * s) by LM3

            .= v by AX;

          end;

          

           P5: for v be Element of ZS holds v is right_complementable

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of EZV by X0;

            reconsider i1 = ( 1. F_Rat ) as Rational;

            

             P5: ( - s) = (( - ( 1. F_Rat )) * s) by VECTSP_1: 14;

            

             P1: (( - ( 1. INT.Ring )) * v) = (( - ( 1. F_Rat )) * s) by LM3;

            (v + (( - ( 1. INT.Ring )) * v)) = (s - s) by P1, P5, LM2

            .= ( 0. EZV) by RLVECT_1: 15

            .= ( 0. ZS) by D1;

            hence v is right_complementable;

          end;

          

           P6: for v,w be Element of ZS holds (v + w) = (w + v)

          proof

            let v,w be Element of ZS;

            reconsider s = v, t = w as Vector of EZV by X0;

            

            thus (v + w) = (s + t) by LM2

            .= (w + v) by LM2;

          end;

          

           P7: for u,v,w be Element of ZS holds ((u + v) + w) = (u + (v + w))

          proof

            let u,v,w be Element of ZS;

            reconsider z = u, s = v, t = w as Vector of EZV by X0;

            

             P1: (u + v) = (z + s) by LM2;

            

             P2: (v + w) = (s + t) by LM2;

            

            thus ((u + v) + w) = ((z + s) + t) by P1, LM2

            .= (z + (s + t)) by RLVECT_1:def 3

            .= (u + (v + w)) by LM2, P2;

          end;

          for v be Element of ZS holds (v + ( 0. ZS)) = v

          proof

            let v be Element of ZS;

            reconsider s = v as Vector of EZV by X0;

            

            thus (v + ( 0. ZS)) = (s + ( 0. EZV)) by LM2, D1

            .= v;

          end;

          hence thesis by P1, P2, P3, P4, P5, P6, P7, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

        end;

        then

        reconsider ZS as strict Z_Module;

        take ZS;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: ZMODUL08:25

    

     rSB01: for V be torsion-free Z_Module, r be Element of F_Rat holds (for x be Vector of ( EMbedding (r,V)) holds x is Vector of ( Z_MQ_VectSp V)) & ( 0. ( EMbedding (r,V))) = ( 0. ( Z_MQ_VectSp V)) & (for x,y be Vector of ( EMbedding (r,V)), v,w be Vector of ( Z_MQ_VectSp V) st x = v & y = w holds (x + y) = (v + w)) & for i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ( EMbedding (r,V)), v be Vector of ( Z_MQ_VectSp V) st i = j & x = v holds (i * x) = (j * v)

    proof

      let V be torsion-free Z_Module, r be Element of F_Rat ;

      set EZV = ( Z_MQ_VectSp V);

      

       D1: EZV = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

      set ZS = ( EMbedding (r,V));

      

       AS1: the carrier of ZS = (r * ( rng ( MorphsZQ V))) & the ZeroF of ZS = ( zeroCoset V) & the addF of ZS = (( addCoset V) || (r * ( rng ( MorphsZQ V)))) & the lmult of ZS = (( lmultCoset V) | [: INT , (r * ( rng ( MorphsZQ V))):]) by defriV;

      set Cl = the carrier of ZS;

      set Add = (( addCoset V) || Cl);

      set Mlt = (( lmultCoset V) | [: INT , (r * ( rng ( MorphsZQ V))):]);

      

       X0: Cl c= the carrier of EZV by AS1;

      thus for x be Vector of ZS holds x is Vector of EZV by X0;

      thus ( 0. ZS) = ( 0. EZV) by D1, defriV;

      thus for x,y be Vector of ZS, v,w be Vector of EZV st x = v & y = w holds (x + y) = (v + w)

      proof

        let x,y be Vector of ZS, v,w be Vector of EZV;

        assume

         L0: x = v & y = w;

        

        thus (x + y) = (( addCoset V) . [x, y]) by AS1, FUNCT_1: 49

        .= (v + w) by D1, L0;

      end;

      thus for i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of EZV st i = j & x = v holds (i * x) = (j * v)

      proof

        let i be Element of INT.Ring , j be Element of F_Rat , x be Vector of ZS, v be Vector of EZV;

        assume

         L0: i = j & x = v;

        

        thus (i * x) = (( lmultCoset V) . [i, x]) by AS1, FUNCT_1: 49

        .= (j * v) by D1, L0;

      end;

    end;

    theorem :: ZMODUL08:26

    for V be torsion-free Z_Module, r be Element of F_Rat holds (for v,w be Vector of ( Z_MQ_VectSp V) st v in ( EMbedding (r,V)) & w in ( EMbedding (r,V)) holds (v + w) in ( EMbedding (r,V))) & for j be Element of F_Rat , v be Vector of ( Z_MQ_VectSp V) st j in INT & v in ( EMbedding (r,V)) holds (j * v) in ( EMbedding (r,V))

    proof

      let V be torsion-free Z_Module, r be Element of F_Rat ;

      set EZV = ( Z_MQ_VectSp V);

      set ZS = ( EMbedding (r,V));

      set Cl = the carrier of ZS;

      set Add = (( addCoset V) || Cl);

      set Mlt = (( lmultCoset V) | [: INT , (r * ( rng ( MorphsZQ V))):]);

      thus for v,w be Vector of ( Z_MQ_VectSp V) st v in ( EMbedding (r,V)) & w in ( EMbedding (r,V)) holds (v + w) in ( EMbedding (r,V))

      proof

        let v,w be Vector of ( Z_MQ_VectSp V);

        assume

         B1: v in ( EMbedding (r,V)) & w in ( EMbedding (r,V));

        reconsider v1 = v, w1 = w as Vector of ( EMbedding (r,V)) by B1;

        (v + w) = (v1 + w1) by rSB01;

        hence thesis;

      end;

      thus for j be Element of F_Rat , v be Vector of ( Z_MQ_VectSp V) st j in INT & v in ( EMbedding (r,V)) holds (j * v) in ( EMbedding (r,V))

      proof

        let j be Element of F_Rat , v be Vector of ( Z_MQ_VectSp V);

        assume

         B1: j in INT & v in ( EMbedding (r,V));

        then

        reconsider v1 = v as Vector of ( EMbedding (r,V));

        reconsider i = j as Element of INT.Ring by B1;

        (j * v) = (i * v1) by rSB01;

        hence thesis;

      end;

    end;

    theorem :: ZMODUL08:27

    

     rSB03A: for V be torsion-free Z_Module, r be Element of F_Rat st r <> ( 0. F_Rat ) holds ex T be linear-transformation of ( EMbedding V), ( EMbedding (r,V)) st (for v be Element of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T . v) = (r * v)) & T is bijective

    proof

      let V be torsion-free Z_Module, r be Element of F_Rat ;

      assume

       AS: r <> ( 0. F_Rat );

      set EZV = ( Z_MQ_VectSp V);

      deffunc F( Vector of EZV) = (r * $1);

      consider T be Function of the carrier of EZV, the carrier of EZV such that

       P1: for x be Element of the carrier of EZV holds (T . x) = F(x) from FUNCT_2:sch 4;

      set T0 = (T | the carrier of ( EMbedding V));

      

       D0: the carrier of ( EMbedding V) = ( rng ( MorphsZQ V)) by defEmbedding;

      ( dom T) = the carrier of EZV by FUNCT_2:def 1;

      then

       P3: ( dom T0) = the carrier of ( EMbedding V) by D0, RELAT_1: 62;

      

       D1: the carrier of ( EMbedding (r,V)) = (r * ( rng ( MorphsZQ V))) by defriV;

      

       RX0: for y be object holds y in ( rng T0) iff y in the carrier of ( EMbedding (r,V))

      proof

        let y be object;

        hereby

          assume y in ( rng T0);

          then

          consider x be object such that

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

          reconsider x as Element of EZV by A2;

          (T0 . x) = (T . x) by FUNCT_1: 49, A2, P3

          .= (r * x) by P1;

          hence y in the carrier of ( EMbedding (r,V)) by A2, D0, D1, P3;

        end;

        assume y in the carrier of ( EMbedding (r,V));

        then y in (r * ( rng ( MorphsZQ V))) by defriV;

        then

        consider x be Vector of EZV such that

         A4: y = (r * x) & x in ( rng ( MorphsZQ V));

        

         A5: x in the carrier of ( EMbedding V) by A4, defEmbedding;

        (T0 . x) = (T . x) by FUNCT_1: 49, A5

        .= y by A4, P1;

        hence y in ( rng T0) by A5, P3, FUNCT_1:def 3;

      end;

      then ( rng T0) = the carrier of ( EMbedding (r,V)) by TARSKI: 2;

      then

      reconsider T0 as Function of ( EMbedding V), ( EMbedding (r,V)) by P3, FUNCT_2: 1;

      

       B0: T0 is additive

      proof

        let x,y be Element of ( EMbedding V);

        

         F1: x in ( EMbedding V) & y in ( EMbedding V);

        reconsider x0 = x, y0 = y as Vector of EZV by SB01;

        

         F2: (x0 + y0) in ( EMbedding V) by F1, SB02;

        

         F3: (T . x0) = (T0 . x) by FUNCT_1: 49;

        

         F4: (T . y0) = (T0 . y) by FUNCT_1: 49;

        

        thus (T0 . (x + y)) = (T0 . (x0 + y0)) by SB01

        .= (T . (x0 + y0)) by FUNCT_1: 49, F2

        .= (r * (x0 + y0)) by P1

        .= ((r * x0) + (r * y0)) by VECTSP_1:def 14

        .= ((T . x0) + (r * y0)) by P1

        .= ((T . x0) + (T . y0)) by P1

        .= ((T0 . x) + (T0 . y)) by rSB01, F3, F4;

      end;

      for x be Element of ( EMbedding V), i be Element of INT.Ring holds (T0 . (i * x)) = (i * (T0 . x))

      proof

        let x be Element of ( EMbedding V), i be Element of INT.Ring ;

        

         F1: x in ( EMbedding V);

        reconsider x0 = x as Vector of EZV by SB01;

        reconsider j = i as Element of F_Rat by NUMBERS: 14;

        

         F2: (j * x0) in ( EMbedding V) by F1, SB02;

        

         F3: (T . x0) = (T0 . x) by FUNCT_1: 49;

        

        thus (T0 . (i * x)) = (T0 . (j * x0)) by SB01

        .= (T . (j * x0)) by FUNCT_1: 49, F2

        .= (r * (j * x0)) by P1

        .= ((r * j) * x0) by VECTSP_1:def 16

        .= (j * (r * x0)) by VECTSP_1:def 16

        .= (i * (T0 . x)) by rSB01, F3, P1;

      end;

      then T0 is additive homogeneous by B0;

      then

      reconsider T0 as linear-transformation of ( EMbedding V), ( EMbedding (r,V));

      take T0;

      thus

       XX1: for v be Element of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T0 . v) = (r * v)

      proof

        let x be Element of ( Z_MQ_VectSp V);

        assume

         F1: x in ( EMbedding V);

        

        thus (T0 . x) = (T . x) by FUNCT_1: 49, F1

        .= (r * x) by P1;

      end;

      for x1,x2 be object st x1 in the carrier of ( EMbedding V) & x2 in the carrier of ( EMbedding V) & (T0 . x1) = (T0 . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         AS2: x1 in the carrier of ( EMbedding V) & x2 in the carrier of ( EMbedding V) & (T0 . x1) = (T0 . x2);

        then

        reconsider xx1 = x1, xx2 = x2 as Element of EZV by D0;

        

         Q0: xx1 in ( EMbedding V) & xx2 in ( EMbedding V) by AS2;

        

         Q1: (T0 . x1) = (r * xx1) by Q0, XX1;

        

         Q2: ((r " ) * (r * xx1)) = ((r " ) * (r * xx2)) by AS2, Q0, Q1, XX1;

        ((r " ) * (r * xx1)) = xx1 by AS, VECTSP_1: 20;

        hence x1 = x2 by Q2, AS, VECTSP_1: 20;

      end;

      then

       T1: T0 is one-to-one by FUNCT_2: 19;

      T0 is onto by RX0, FUNCT_2:def 3, TARSKI: 2;

      hence thesis by T1;

    end;

    theorem :: ZMODUL08:28

    

     ThEM1: for V be torsion-free Z_Module, v be Vector of V holds ( Class (( EQRZM V), [v, 1])) in ( EMbedding V)

    proof

      let V be torsion-free Z_Module, v be Vector of V;

      (( MorphsZQ V) . v) = ( Class (( EQRZM V), [v, 1])) by ZMODUL04:def 6;

      then ( Class (( EQRZM V), [v, 1])) in ( rng ( MorphsZQ V)) by FUNCT_2: 4;

      hence thesis by defEmbedding;

    end;

    theorem :: ZMODUL08:29

    

     ThDM1: for V be torsion-free Z_Module, v be Vector of ( DivisibleMod V) holds ex a be Element of INT.Ring st a <> 0 & (a * v) in ( EMbedding V)

    proof

      let V be torsion-free Z_Module, v be Vector of ( DivisibleMod V);

      

       A1: v in the carrier of ( DivisibleMod V);

      reconsider vv = v as Element of ( Class ( EQRZM V)) by defDivisibleMod;

      

       AX1: v in ( Class ( EQRZM V)) by A1, defDivisibleMod;

      v is Element of ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by defDivisibleMod;

      then

      consider a be Element of INT.Ring , z be Vector of V such that

       A2: a <> 0 & v = ( Class (( EQRZM V), [z, a])) by ZMODUL04: 5;

      reconsider aq = a as Element of F_Rat by NUMBERS: 14;

      

       A3: aq = (a / 1) & 1 <> 0 ;

      

       AX4: v in ( Class ( EQRZM V)) by A1, defDivisibleMod;

      (a * v) = ((( lmultCoset V) | [: INT , ( Class ( EQRZM V)):]) . (a,v)) by defDivisibleMod

      .= (( lmultCoset V) . (a,v)) by AX4, FUNCT_1: 49, ZFMISC_1: 87

      .= ( Class (( EQRZM V), [(a * z), (( 1. INT.Ring ) * a)])) by AX1, A2, A3, ZMODUL04:def 4

      .= ( Class (( EQRZM V), [z, ( 1. INT.Ring )])) by A2, ZMODUL04: 4;

      hence thesis by A2, ThEM1;

    end;

    registration

      let V be torsion-free Z_Module;

      cluster ( DivisibleMod V) -> torsion-free;

      correctness

      proof

        set D = ( DivisibleMod V);

        set Z = ( EMbedding V);

        assume D is non torsion-free;

        then

        consider v be Vector of D such that

         P1: v <> ( 0. D) & v is torsion;

        consider i be Element of INT.Ring such that

         P2: i <> 0 & (i * v) = ( 0. D) by P1;

        v in the carrier of D;

        then

         A1: v in ( Class ( EQRZM V)) by defDivisibleMod;

        reconsider vv = v as Element of ( Class ( EQRZM V)) by defDivisibleMod;

        v is Element of ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by defDivisibleMod;

        then

        consider a be Element of INT.Ring , z be Vector of V such that

         A2: a <> 0 & v = ( Class (( EQRZM V), [z, a])) by ZMODUL04: 5;

        reconsider iq = i as Element of F_Rat by NUMBERS: 14;

        

         A4: iq = (i / 1) & 1 <> 0 ;

        

         A6: (i * v) = ((( lmultCoset V) | [: INT , ( Class ( EQRZM V)):]) . (i,v)) by defDivisibleMod

        .= (( lmultCoset V) . (i,v)) by A1, FUNCT_1: 49, ZFMISC_1: 87

        .= ( Class (( EQRZM V), [(i * z), (( 1. INT.Ring ) * a)])) by A1, A2, A4, ZMODUL04:def 4

        .= ( Class (( EQRZM V), [(i * z), a]));

        

         A7: not a in { 0 } by A2, TARSKI:def 1;

        a in ( INT \ { 0 }) by A7, XBOOLE_0:def 5;

        then

         A8: [(i * z), a] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

        ( Class (( EQRZM V), [(i * z), a])) = ( zeroCoset V) by P2, A6, defDivisibleMod

        .= ( Class (( EQRZM V), [( 0. V), a])) by A2, ZMODUL04:def 3;

        then [ [(i * z), a], [( 0. V), a]] in ( EQRZM V) by A8, EQREL_1: 35;

        then (a * ( 0. V)) = (a * (i * z)) by ZMODUL04: 3;

        

        then

         A9: ( 0. V) = (a * (i * z)) by ZMODUL01: 1

        .= ((a * i) * z) by VECTSP_1:def 16;

        

         A10: z <> ( 0. V)

        proof

          assume z = ( 0. V);

          

          then v = ( zeroCoset V) by A2, ZMODUL04:def 3

          .= ( 0. D) by defDivisibleMod;

          hence contradiction by P1;

        end;

        z is torsion by P2, A2, A9;

        then V is non torsion-free by A10;

        hence contradiction;

      end;

    end

    registration

      let V be torsion-free Z_Module;

      cluster ( EMbedding V) -> torsion-free;

      correctness

      proof

        ( EMbedding V) is Submodule of ( DivisibleMod V) by ThDivisible2;

        hence thesis;

      end;

    end

    registration

      let V be free Z_Module;

      cluster ( EMbedding V) -> free;

      correctness

      proof

        consider T be linear-transformation of V, ( EMbedding V) such that

         A1: T is bijective & T = ( MorphsZQ V) & (for v be Vector of V holds (T . v) = ( Class (( EQRZM V), [v, 1]))) by SB03;

        thus thesis by A1, ZMODUL06: 48;

      end;

    end

    theorem :: ZMODUL08:30

    

     ThDivisibleX1: for V be torsion-free Z_Module holds (for v be Vector of ( Z_MQ_VectSp V) holds v is Vector of ( DivisibleMod V)) & (for v be Vector of ( DivisibleMod V) holds v is Vector of ( Z_MQ_VectSp V)) & ( 0. ( DivisibleMod V)) = ( 0. ( Z_MQ_VectSp V))

    proof

      let V be torsion-free Z_Module;

      

       A1: ( Z_MQ_VectSp V) = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

      thus for v be Vector of ( Z_MQ_VectSp V) holds v is Vector of ( DivisibleMod V) by A1, defDivisibleMod;

      thus for v be Vector of ( DivisibleMod V) holds v is Vector of ( Z_MQ_VectSp V) by A1, defDivisibleMod;

      thus ( 0. ( DivisibleMod V)) = ( 0. ( Z_MQ_VectSp V)) by A1, defDivisibleMod;

    end;

    theorem :: ZMODUL08:31

    

     ThDivisibleX2: for V be torsion-free Z_Module holds (for x,y be Vector of ( DivisibleMod V), v,u be Vector of ( Z_MQ_VectSp V) st x = v & y = u holds (x + y) = (v + u)) & (for z be Vector of ( DivisibleMod V), w be Vector of ( Z_MQ_VectSp V), a be Element of INT.Ring , aq be Element of F_Rat st z = w & a = aq holds (a * z) = (aq * w)) & (for z be Vector of ( DivisibleMod V), w be Vector of ( Z_MQ_VectSp V), aq be Element of F_Rat , a be Element of INT.Ring st a <> 0 & aq = a & (a * z) = (aq * w) holds z = w) & (for x be Vector of ( DivisibleMod V), v be Vector of ( Z_MQ_VectSp V), r be Element of F_Rat , m,n be Element of INT.Ring , mi,ni be Integer st m = mi & n = ni & x = v & r <> ( 0. F_Rat ) & n <> 0 & r = (mi / ni) holds ex y be Vector of ( DivisibleMod V) st x = (n * y) & (r * v) = (m * y))

    proof

      let V be torsion-free Z_Module;

      

       A1: ( Z_MQ_VectSp V) = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by ZMODUL04:def 5;

      thus for x,y be Vector of ( DivisibleMod V), v,u be Vector of ( Z_MQ_VectSp V) st x = v & y = u holds (x + y) = (v + u) by A1, defDivisibleMod;

      thus

       A2: for z be Vector of ( DivisibleMod V), w be Vector of ( Z_MQ_VectSp V), a be Element of INT.Ring , aq be Element of F_Rat st z = w & a = aq holds (a * z) = (aq * w)

      proof

        let z be Vector of ( DivisibleMod V), w be Vector of ( Z_MQ_VectSp V), a be Element of INT.Ring , aq be Element of F_Rat such that

         B1: z = w & a = aq;

        

        thus (a * z) = ((( lmultCoset V) | [: INT , ( Class ( EQRZM V)):]) . (a,z)) by defDivisibleMod

        .= (aq * w) by A1, B1, FUNCT_1: 49, ZFMISC_1: 87;

      end;

      thus

       A3: for z be Vector of ( DivisibleMod V), w be Vector of ( Z_MQ_VectSp V), aq be Element of F_Rat , a be Element of INT.Ring st a <> 0 & aq = a & (a * z) = (aq * w) holds z = w

      proof

        let z be Vector of ( DivisibleMod V), w be Vector of ( Z_MQ_VectSp V), aq be Element of F_Rat , a be Element of INT.Ring such that

         B1: a <> 0 & aq = a & (a * z) = (aq * w);

        assume

         B2: z <> w;

        reconsider ww = w as Vector of ( DivisibleMod V) by ThDivisibleX1;

        

         B4: (a * ww) = (a * z) by A2, B1;

        (a * (z - ww)) = ((a * z) - (a * ww)) by ZMODUL01: 8

        .= ( 0. ( DivisibleMod V)) by B4, RLVECT_1: 15;

        then (z - ww) is torsion by B1;

        hence contradiction by B2, RLVECT_1: 21, ZMODUL06:def 3;

      end;

      thus for x be Vector of ( DivisibleMod V), v be Vector of ( Z_MQ_VectSp V), r be Element of F_Rat , m,n be Element of INT.Ring , mi,ni be Integer st m = mi & n = ni & x = v & r <> ( 0. F_Rat ) & n <> 0 & r = (mi / ni) holds ex y be Vector of ( DivisibleMod V) st x = (n * y) & (r * v) = (m * y)

      proof

        let x be Vector of ( DivisibleMod V), v be Vector of ( Z_MQ_VectSp V), r be Element of F_Rat , m,n be Element of INT.Ring , mi,ni be Integer such that

         B1: m = mi & n = ni & x = v & r <> ( 0. F_Rat ) & n <> 0 & r = (mi / ni);

        consider y be Vector of ( DivisibleMod V) such that

         B2: (n * y) = x by B1, ThDivisible1;

        take y;

        reconsider mq = m, nq = n as Element of F_Rat by NUMBERS: 14;

        

         B3: (nq * r) = mq by B1, XCMPLX_1: 87;

        

         B4: (n * (m * y)) = ((n * m) * y) by VECTSP_1:def 16

        .= (m * x) by B2, VECTSP_1:def 16;

        (nq * (r * v)) = (mq * v) by B3, VECTSP_1:def 16;

        then (n * (m * y)) = (nq * (r * v)) by A2, B1, B4;

        hence thesis by A3, B1, B2;

      end;

    end;

    theorem :: ZMODUL08:32

    

     ThDivisible3: for V be torsion-free Z_Module, r be Element of F_Rat holds ( EMbedding (r,V)) is Submodule of ( DivisibleMod V)

    proof

      let V be torsion-free Z_Module, r be Element of F_Rat ;

      set Z = ( EMbedding (r,V));

      set D = ( DivisibleMod V);

      for x be object st x in the carrier of ( EMbedding (r,V)) holds x in the carrier of ( DivisibleMod V)

      proof

        let x be object such that

         B1: x in the carrier of ( EMbedding (r,V));

        x is Vector of ( Z_MQ_VectSp V) by B1, rSB01;

        then x is Vector of ( DivisibleMod V) by ThDivisibleX1;

        hence thesis;

      end;

      then

       A1: the carrier of Z c= the carrier of D;

      

       A2: the addF of Z = (( addCoset V) || (r * ( rng ( MorphsZQ V)))) by defriV

      .= (( addCoset V) || the carrier of Z) by defriV

      .= (the addF of D || the carrier of Z) by defDivisibleMod;

      

       A3: ( 0. Z) = ( zeroCoset V) by defriV

      .= ( 0. D) by defDivisibleMod;

      

       A4: [:the carrier of INT.Ring , the carrier of Z:] c= [:the carrier of INT.Ring , the carrier of D:] by A1, ZFMISC_1: 96;

      (the lmult of D | [:the carrier of INT.Ring , the carrier of Z:]) = ((( lmultCoset V) | [:the carrier of INT.Ring , ( Class ( EQRZM V)):]) | [:the carrier of INT.Ring , the carrier of Z:]) by defDivisibleMod

      .= ((( lmultCoset V) | [:the carrier of INT.Ring , the carrier of D:]) | [: INT , the carrier of Z:]) by defDivisibleMod

      .= (( lmultCoset V) | [:the carrier of INT.Ring , the carrier of Z:]) by A4, FUNCT_1: 51

      .= (( lmultCoset V) | [:the carrier of INT.Ring , (r * ( rng ( MorphsZQ V))):]) by defriV

      .= the lmult of Z by defriV;

      hence thesis by A1, A2, A3, VECTSP_4:def 2;

    end;

    registration

      let V be finitely-generated torsion-free Z_Module;

      let r be Element of F_Rat ;

      cluster ( EMbedding (r,V)) -> finitely-generated;

      correctness

      proof

        per cases ;

          suppose

           B1: r is zero;

          

           B2: for v be Vector of ( Z_MQ_VectSp V) st v in (r * ( rng ( MorphsZQ V))) holds v = ( 0. ( Z_MQ_VectSp V))

          proof

            let v be Vector of ( Z_MQ_VectSp V) such that

             C1: v in (r * ( rng ( MorphsZQ V)));

            consider u be Vector of ( Z_MQ_VectSp V) such that

             C2: v = (( 0. F_Rat ) * u) & u in ( rng ( MorphsZQ V)) by B1, C1;

            thus v = ( 0. ( Z_MQ_VectSp V)) by C2, VECTSP_1: 14;

          end;

          

           B3: ( EMbedding (r,V)) is strict Submodule of ( DivisibleMod V) by ThDivisible3;

          for v be Vector of ( DivisibleMod V) holds v in ( EMbedding (r,V)) iff v in ( (0). ( DivisibleMod V))

          proof

            let v be Vector of ( DivisibleMod V);

            hereby

              assume v in ( EMbedding (r,V));

              then v in (r * ( rng ( MorphsZQ V))) by defriV;

              

              then v = ( 0. ( Z_MQ_VectSp V)) by B2

              .= ( 0. ( DivisibleMod V)) by ThDivisibleX1;

              hence v in ( (0). ( DivisibleMod V)) by ZMODUL02: 66;

            end;

            assume v in ( (0). ( DivisibleMod V));

            

            then v = ( 0. ( DivisibleMod V)) by ZMODUL02: 66

            .= ( 0. ( EMbedding (r,V))) by B3, ZMODUL01: 26;

            hence thesis;

          end;

          hence thesis by B3, ZMODUL01: 46;

        end;

          suppose r is non zero;

          then

          consider T be linear-transformation of ( EMbedding V), ( EMbedding (r,V)) such that

           A1: (for v be Vector of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T . v) = (r * v)) & T is bijective by rSB03A;

          reconsider Z = ( EMbedding (r,V)) as free Z_Module by A1, ZMODUL06: 48;

          Z is finite-rank by A1, ZMODUL06: 50;

          hence thesis;

        end;

      end;

    end

    registration

      let V be non trivial torsion-free Z_Module;

      let r be non zero Element of F_Rat ;

      cluster ( EMbedding (r,V)) -> non trivial;

      correctness

      proof

        consider T be linear-transformation of ( EMbedding V), ( EMbedding (r,V)) such that

         A1: (for v be Element of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T . v) = (r * v)) & T is bijective by rSB03A;

        set v = the non zero Vector of ( EMbedding V);

        (T . v) <> ( 0. ( EMbedding (r,V)))

        proof

          assume (T . v) = ( 0. ( EMbedding (r,V)));

          then (T . v) = (T . ( 0. ( EMbedding V))) by ZMODUL05: 19;

          hence contradiction by A1, FUNCT_2: 19;

        end;

        then not (T . v) in ( (0). ( EMbedding (r,V))) by ZMODUL02: 66;

        then ( (Omega). ( EMbedding (r,V))) <> ( (0). ( EMbedding (r,V)));

        hence thesis by ZMODUL07: 41;

      end;

    end

    registration

      let V be torsion-free Z_Module;

      let r be Element of F_Rat ;

      cluster ( EMbedding (r,V)) -> torsion-free;

      correctness by ThDivisible3;

    end

    registration

      let V be free Z_Module;

      let r be non zero Element of F_Rat ;

      cluster ( EMbedding (r,V)) -> free;

      correctness

      proof

        consider T be linear-transformation of ( EMbedding V), ( EMbedding (r,V)) such that

         A1: (for v be Element of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T . v) = (r * v)) & T is bijective by rSB03A;

        thus thesis by A1, ZMODUL06: 48;

      end;

    end

    theorem :: ZMODUL08:33

    for V be non trivial free Z_Module, v be Vector of ( DivisibleMod V) holds ex a be Element of INT.Ring st a in NAT & a <> 0 & (a * v) in ( EMbedding V) & for b be Element of INT.Ring st b in NAT & b < a & b <> 0 holds not (b * v) in ( EMbedding V)

    proof

      let V be non trivial free Z_Module, v be Vector of ( DivisibleMod V);

      consider ai be Element of INT.Ring such that

       A2: ai <> 0 & (ai * v) in ( EMbedding V) by ThDM1;

      reconsider aiv = (ai * v) as Vector of ( EMbedding V) by A2;

      

       A3: ( |.ai.| * v) in ( EMbedding V)

      proof

        

         B1: ( EMbedding V) is Submodule of ( DivisibleMod V) by ThDivisible2;

        per cases by A2;

          suppose ai > 0 ;

          hence thesis by A2, ABSVALUE:def 1;

        end;

          suppose ai < 0 ;

          

          then ( |.ai.| * v) = (( - ai) * v) by ABSVALUE:def 1

          .= ( - (ai * v)) by ZMODUL01: 16

          .= ( - aiv) by B1, ZMODUL01: 30;

          hence thesis;

        end;

      end;

      reconsider ain = |.ai.| as Element of INT.Ring ;

      reconsider ainv = (ain * v) as Vector of ( EMbedding V) by A3;

      

       N1: |.ai.| in NAT by COMPLEX1: 46, INT_1: 3;

      then

      reconsider nai = |.ai.| as Nat;

      

       A4: ain <> 0 by A2, ABSVALUE: 2;

      defpred P[ Nat] means ex n be Element of INT.Ring st n = $1 & n in NAT & n <> 0 & (n * v) in ( EMbedding V);

      

       A6: ex k be Nat st P[k] by A3, A4, N1;

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

      then

      consider a0 be Nat such that

       A7: P[a0] & for b0 be Nat st P[b0] holds a0 <= b0;

      reconsider a = a0 as Element of INT.Ring by INT_1:def 2;

      take a;

      thus a in NAT by ORDINAL1:def 12;

      thus a <> 0 by A7;

      thus (a * v) in ( EMbedding V) by A7;

      thus for b be Element of INT.Ring st b in NAT & b < a & b <> 0 holds not (b * v) in ( EMbedding V) by A7;

    end;

    theorem :: ZMODUL08:34

    

     ThRankEM: for V be finite-rank free Z_Module holds ( rank ( EMbedding V)) = ( rank V)

    proof

      let V be finite-rank free Z_Module;

      consider T be linear-transformation of V, ( EMbedding V) such that

       A1: T is bijective & T = ( MorphsZQ V) & (for v be Vector of V holds (T . v) = ( Class (( EQRZM V), [v, 1]))) by SB03;

      thus thesis by A1, ZMODUL06: 51;

    end;

    theorem :: ZMODUL08:35

    

     ThRankrEM1: for V be finite-rank free Z_Module, r be non zero Element of F_Rat holds ( rank ( EMbedding (r,V))) = ( rank ( EMbedding V))

    proof

      let V be finite-rank free Z_Module, r be non zero Element of F_Rat ;

      consider T be linear-transformation of ( EMbedding V), ( EMbedding (r,V)) such that

       A1: (for v be Element of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T . v) = (r * v)) & T is bijective by rSB03A;

      thus thesis by A1, ZMODUL06: 51;

    end;

    theorem :: ZMODUL08:36

    for V be finite-rank free Z_Module, r be non zero Element of F_Rat holds ( rank ( EMbedding (r,V))) = ( rank V)

    proof

      let V be finite-rank free Z_Module, r be non zero Element of F_Rat ;

      

      thus ( rank ( EMbedding (r,V))) = ( rank ( EMbedding V)) by ThRankrEM1

      .= ( rank V) by ThRankEM;

    end;

    registration

      cluster -> infinite for non trivial torsion-free Z_Module;

      correctness

      proof

        let V be non trivial torsion-free Z_Module;

        set v = the non zero Vector of V;

        defpred P[ object, object] means for i be Element of INT.Ring st i = $1 holds $2 = (i * v);

        

         A1: for i be Element of INT.Ring holds ex w be Element of ( Lin {v}) st P[i, w]

        proof

          let i be Element of INT.Ring ;

          set w = (i * v);

          w in ( Lin {v}) by ZMODUL06: 21;

          then

          reconsider w as Element of ( Lin {v});

          take w;

          thus thesis;

        end;

        ex f be Function of INT.Ring , ( Lin {v}) st for i be Element of INT.Ring holds P[i, (f . i)] from FUNCT_2:sch 3( A1);

        then

        consider f be Function of INT.Ring , ( Lin {v}) such that

         A2: for i be Element of INT.Ring holds P[i, (f . i)];

        

         A3: ( dom f) = INT & ( rng f) c= the carrier of ( Lin {v}) by FUNCT_2:def 1;

        f is one-to-one

        proof

          for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

          proof

            let x1,x2 be object such that

             B1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

            reconsider xx1 = x1, xx2 = x2 as Element of INT.Ring by B1;

            (f . x1) = (xx1 * v) by A2;

            then (xx1 * v) = (xx2 * v) by A2, B1;

            then ((xx1 * v) - (xx2 * v)) = ( 0. V) by RLVECT_1: 15;

            then ((xx1 - xx2) * v) = ( 0. V) by ZMODUL01: 9;

            then (xx1 - xx2) = ( 0. INT.Ring ) by ZMODUL01:def 7;

            hence thesis;

          end;

          hence thesis by FUNCT_1:def 4;

        end;

        then

         A4: ( card INT ) c= ( card ( Lin {v})) by A3, CARD_1: 10;

        the carrier of ( Lin {v}) is Subset of the carrier of V by VECTSP_4:def 2;

        hence thesis by A4;

      end;

    end

    theorem :: ZMODUL08:37

    for V be Z_Module holds ex A be Subset of V st (A is linearly-independent & for v be Vector of V holds ex a be Element of INT.Ring st a in NAT & a > 0 & (a * v) in ( Lin A))

    proof

      let V be Z_Module;

      ( {} the carrier of V) is linearly-independent;

      then

      consider A be Subset of V such that

       A1: {} c= A & A is linearly-independent & (for v be Vector of V holds ex ai be Element of INT.Ring st ai <> 0 & (ai * v) in ( Lin A)) by ZMODUL07: 2;

      

       A2: for v be Vector of V holds ex a be Element of INT.Ring st a in NAT & a > 0 & (a * v) in ( Lin A)

      proof

        let v be Vector of V;

        consider ai be Element of INT.Ring such that

         B1: ai <> 0 & (ai * v) in ( Lin A) by A1;

        set a = |.ai.|;

        

         B2: a <> 0 by B1, ABSVALUE: 2;

        

         N1: a in NAT by COMPLEX1: 46, INT_1: 3;

        (a * v) in ( Lin A)

        proof

          per cases by B1;

            suppose ai > 0 ;

            hence thesis by B1, ABSVALUE:def 1;

          end;

            suppose ai < 0 ;

            then a = ( - ai) by ABSVALUE:def 1;

            then (a * v) = ( - (ai * v)) by ZMODUL01: 16;

            hence thesis by B1, ZMODUL01: 38;

          end;

        end;

        hence thesis by N1, B2;

      end;

      take A;

      thus thesis by A1, A2;

    end;

    theorem :: ZMODUL08:38

    for V be non trivial torsion-free Z_Module, v be non zero Vector of V, A be Subset of V, a be Element of INT.Ring st a in NAT & A is linearly-independent & a > 0 & (a * v) in ( Lin A) holds ex L be Linear_Combination of A, u be Vector of V st (a * v) = ( Sum L) & u in A & (L . u) <> 0

    proof

      let V be non trivial torsion-free Z_Module, v be non zero Vector of V, A be Subset of V, a be Element of INT.Ring such that

       A1: a in NAT & A is linearly-independent & a > 0 & (a * v) in ( Lin A);

      

       a1: a <> ( 0. INT.Ring ) by A1;

      consider L be Linear_Combination of A such that

       A2: (a * v) = ( Sum L) by A1, ZMODUL02: 64;

      ( Carrier L) <> {}

      proof

        assume ( Carrier L) = {} ;

        then ( Sum L) = ( 0. V) by ZMODUL02: 23;

        hence contradiction by a1, A2, ZMODUL01:def 7;

      end;

      then

      consider uu be object such that

       A3: uu in ( Carrier L) by XBOOLE_0:def 1;

      consider u be Vector of V such that

       A4: u = uu & (L . u) <> 0 by A3;

      

       A5: ( Carrier L) c= A by VECTSP_6:def 4;

      take L, u;

      thus thesis by A2, A3, A4, A5;

    end;

    theorem :: ZMODUL08:39

    

     ThDivisible4: for V be torsion-free Z_Module, i be non zero Integer, r1,r2 be non zero Element of F_Rat st r2 = (r1 / i) holds ( EMbedding (r1,V)) is Submodule of ( EMbedding (r2,V))

    proof

      let V be torsion-free Z_Module, i be non zero Integer, r1,r2 be non zero Element of F_Rat such that

       A1: r2 = (r1 / i);

      

       A2: for x be Vector of ( DivisibleMod V) st x in ( EMbedding (r1,V)) holds x in ( EMbedding (r2,V))

      proof

        let x be Vector of ( DivisibleMod V) such that

         B1: x in ( EMbedding (r1,V));

        consider T1 be linear-transformation of ( EMbedding V), ( EMbedding (r1,V)) such that

         B2: (for v be Element of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T1 . v) = (r1 * v)) & T1 is bijective by rSB03A;

        consider T2 be linear-transformation of ( EMbedding V), ( EMbedding (r2,V)) such that

         B3: (for v be Element of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T2 . v) = (r2 * v)) & T2 is bijective by rSB03A;

        reconsider ii = i as Element of INT.Ring by INT_1:def 2;

        reconsider ir = i as Element of F_Rat by INT_1:def 2, NUMBERS: 14;

        reconsider iv = (1 / i) as Element of F_Rat by RAT_1:def 1;

        x in ( rng T1) by B1, B2, FUNCT_2:def 3;

        then

        consider v be object such that

         B4: v in the carrier of ( EMbedding V) & x = (T1 . v) by FUNCT_2: 11;

        reconsider vv = v as Vector of ( Z_MQ_VectSp V) by B4, SB01;

        

         B5: vv in ( EMbedding V) by B4;

        then (T2 . vv) = (r2 * vv) by B3;

        then

        reconsider rv = (r2 * vv) as Vector of ( EMbedding (r2,V)) by B4, FUNCT_2: 5;

        

         B7: (ir * iv) = (i / i)

        .= ( 1. F_Rat ) by XCMPLX_1: 60;

        (ii * rv) = (ir * (r2 * vv)) by rSB01

        .= ((ir * r2) * vv) by VECTSP_1:def 16

        .= ((r1 * (ir * iv)) * vv) by A1

        .= x by B2, B4, B5, B7;

        hence thesis;

      end;

      ( EMbedding (r1,V)) is Submodule of ( DivisibleMod V) & ( EMbedding (r2,V)) is Submodule of ( DivisibleMod V) by ThDivisible3;

      hence thesis by A2, ZMODUL01: 44;

    end;

    theorem :: ZMODUL08:40

    for V be finite-rank free Z_Module, Z be Submodule of ( DivisibleMod V) holds Z is finitely-generated iff ex r be non zero Element of F_Rat st Z is Submodule of ( EMbedding (r,V))

    proof

      let V be finite-rank free Z_Module, Z be Submodule of ( DivisibleMod V);

      hereby

        assume

         AS: Z is finitely-generated;

        then

        reconsider ZX = Z as free Submodule of ( DivisibleMod V);

        reconsider ZX as finite-rank free Submodule of ( DivisibleMod V) by AS;

        defpred P[ Nat] means for ZZ be finite-rank free Submodule of ( DivisibleMod V) st ( rank ZZ) = $1 holds ex i be non zero Integer, r be non zero Element of F_Rat st ZZ is Submodule of ( EMbedding (r,V)) & r = (1 / i);

        

         B1: P[ 0 ]

        proof

          let ZZ be finite-rank free Submodule of ( DivisibleMod V) such that

           C0: ( rank ZZ) = 0 ;

          reconsider i = 1 as non zero Integer;

          reconsider r = (1 / i) as Element of F_Rat ;

          r is non zero;

          then

          reconsider r = (1 / i) as non zero Element of F_Rat ;

          

           C1: ( EMbedding (r,V)) is Submodule of ( DivisibleMod V) by ThDivisible3;

          

           C2: ( (Omega). ZZ) = ( (0). ZZ) by C0, ZMODUL05: 1

          .= ( (0). ( EMbedding (r,V))) by C1, ZMODUL01: 52;

          take i, r;

          ZZ is Submodule of ( (Omega). ZZ) by VECTSP_4: 41;

          hence thesis by C2, ZMODUL01: 42;

        end;

        

         B2: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat such that

           C1: P[n];

          let ZZ be finite-rank free Submodule of ( DivisibleMod V) such that

           C0: ( rank ZZ) = (n + 1);

          set I = the Basis of ZZ;

          

           C2: ( card I) = (n + 1) by C0, ZMODUL03:def 5;

          then I <> {} ;

          then

          consider v be object such that

           C3: v in I by XBOOLE_0:def 1;

          reconsider v as Vector of ZZ by C3;

          

           C4: ZZ is_the_direct_sum_of (( Lin (I \ {v})),( Lin {v})) by C3, ZMODUL04: 33;

          

           C5: ( card (I \ {v})) = (( card I) - ( card {v})) by C3, CARD_2: 44, ZFMISC_1: 31

          .= (( card I) - 1) by CARD_1: 30

          .= n by C2;

          I is linearly-independent by VECTSP_7:def 3;

          then (I \ {v}) is linearly-independent by XBOOLE_1: 36, ZMODUL02: 56;

          then

           C6: ( rank ( Lin (I \ {v}))) = n by C5, ZMODUL05: 3;

          ( Lin (I \ {v})) is Submodule of ( DivisibleMod V) by ZMODUL01: 42;

          then

          consider ix be non zero Integer, rx be non zero Element of F_Rat such that

           C7: ( Lin (I \ {v})) is Submodule of ( EMbedding (rx,V)) & rx = (1 / ix) by C1, C6;

          ex iy be non zero Integer, ry be non zero Element of F_Rat st ( Lin {v}) is Submodule of ( EMbedding (ry,V)) & ry = (1 / iy)

          proof

            reconsider vv = v as Vector of ( DivisibleMod V) by ZMODUL01: 25;

            consider iiy be Element of INT.Ring such that

             D1: iiy <> ( 0. INT.Ring ) & (iiy * vv) in ( EMbedding V) by ThDM1;

            reconsider iy = iiy as Integer;

            reconsider iy as non zero Integer by D1;

            reconsider ry = (1 / iy) as Element of F_Rat by RAT_1:def 1;

            ry is non zero;

            then

            reconsider ry as non zero Element of F_Rat ;

            take iy, ry;

            reconsider ivv = (iiy * vv) as Vector of ( Z_MQ_VectSp V) by D1, SB01;

            reconsider iv = ivv as Vector of ( DivisibleMod V);

            consider T be linear-transformation of ( EMbedding V), ( EMbedding (ry,V)) such that

             D7: (for v be Element of ( Z_MQ_VectSp V) st v in ( EMbedding V) holds (T . v) = (ry * v)) & T is bijective by rSB03A;

            consider y be Vector of ( DivisibleMod V) such that

             D8: iv = (iiy * y) & (ry * ivv) = (( 1. INT.Ring ) * y) by ThDivisibleX2;

            (T . ivv) = (ry * ivv) by D1, D7

            .= y by D8, VECTSP_1:def 17

            .= vv by D8, ZMODUL01: 10;

            then

             D3: vv in ( EMbedding (ry,V)) by D1, FUNCT_2: 5;

            

             D4: ( EMbedding (ry,V)) is Submodule of ( DivisibleMod V) by ThDivisible3;

            

             D5: for x be Vector of ( DivisibleMod V) st x in ( Lin {v}) holds x in ( EMbedding (ry,V))

            proof

              let x be Vector of ( DivisibleMod V) such that

               E1: x in ( Lin {v});

              consider a be Element of INT.Ring such that

               E2: x = (a * v) by E1, ZMODUL06: 19;

              (a * vv) in ( EMbedding (ry,V)) by D3, D4, ZMODUL01: 37;

              hence thesis by E2, ZMODUL01: 29;

            end;

            ( Lin {v}) is Submodule of ( DivisibleMod V) by ZMODUL01: 42;

            hence thesis by D4, D5, ZMODUL01: 44;

          end;

          then

          consider iy be non zero Integer, ry be non zero Element of F_Rat such that

           C8: ( Lin {v}) is Submodule of ( EMbedding (ry,V)) & ry = (1 / iy);

          reconsider i = (ix * iy) as non zero Integer;

          reconsider r = (1 / i) as Element of F_Rat by RAT_1:def 1;

          r is non zero;

          then

          reconsider r as non zero Element of F_Rat ;

          take i, r;

          r = (rx / iy) by C7, XCMPLX_1: 78;

          then ( EMbedding (rx,V)) is Submodule of ( EMbedding (r,V)) by ThDivisible4;

          then

           C9: ( Lin (I \ {v})) is Submodule of ( EMbedding (r,V)) by C7, ZMODUL01: 42;

          r = (ry / ix) by C8, XCMPLX_1: 78;

          then ( EMbedding (ry,V)) is Submodule of ( EMbedding (r,V)) by ThDivisible4;

          then

           C13: ( Lin {v}) is Submodule of ( EMbedding (r,V)) by C8, ZMODUL01: 42;

          reconsider LIv = ( Lin (I \ {v})), Lv = ( Lin {v}) as Submodule of ( DivisibleMod V) by ZMODUL01: 42;

          reconsider EMr = ( EMbedding (r,V)) as Submodule of ( DivisibleMod V) by ThDivisible3;

          

           C11: (LIv + Lv) is Submodule of EMr by C9, C13, ZMODUL02: 76;

          

           C12: ( (Omega). ZZ) is Submodule of ( EMbedding (r,V)) by C4, C11, ZMODUL06: 31;

          ZZ is Submodule of ( (Omega). ZZ) by VECTSP_4: 41;

          hence thesis by C12, ZMODUL01: 42;

        end;

        

         B3: for n be Nat holds P[n] from NAT_1:sch 2( B1, B2);

        set n = ( rank ZX);

         P[n] by B3;

        then

        consider i be non zero Integer, r be non zero Element of F_Rat such that

         B4: Z is Submodule of ( EMbedding (r,V)) & r = (1 / i);

        thus ex r be non zero Element of F_Rat st Z is Submodule of ( EMbedding (r,V)) by B4;

      end;

      given r be non zero Element of F_Rat such that

       B1: Z is Submodule of ( EMbedding (r,V));

      thus Z is finitely-generated by B1;

    end;