zmodul07.miz



    begin

    reserve x,y,y1,y2 for object;

    reserve V for Z_Module;

    reserve W,W1,W2 for Submodule of V;

    reserve u,v for VECTOR of V;

    reserve i,j,k,n for Element of NAT ;

    theorem :: ZMODUL07:1

    

     LMThFRat31X: for n be Integer st n <> 0 & n <> ( - 1) & n <> ( - 2) holds not (n / (n + 1)) in INT

    proof

      let n be Integer;

      assume

       AS: n <> 0 & n <> ( - 1) & n <> ( - 2);

      consider m be Nat such that

       A0: n = m or n = ( - m) by INT_1: 2;

      per cases by A0;

        suppose n = m;

        hence not (n / (n + 1)) in INT by AS, NAT_1: 16, NAT_D: 33;

      end;

        suppose

         D1: n = ( - m);

        

        then

         D2: (n / (n + 1)) = (( - m) / ( - (m - 1)))

        .= (m / (m - 1)) by XCMPLX_1: 191

        .= (((m - 1) / (m - 1)) + (1 / (m - 1)));

        

         D32: m <> 0 & m <> 1 & m <> 2 by D1, AS;

        then 1 <= m by NAT_1: 14;

        then 1 < m by AS, D1, XXREAL_0: 1;

        then (1 + 1) <= m by NAT_1: 13;

        then 2 < m by AS, D1, XXREAL_0: 1;

        then (2 + 1) <= m by NAT_1: 13;

        then

         D3: ((2 + 1) - 1) <= (m - 1) by XREAL_1: 9;

        then

         D31: 1 < (m - 1) & (m - 1) <> 0 by XXREAL_0: 2;

        

         D4: (n / (n + 1)) = (1 + (1 / (m - 1))) by D2, D3, XCMPLX_1: 60;

        thus not (n / (n + 1)) in INT

        proof

          assume (n / (n + 1)) in INT ;

          then

          reconsider k = (n / (n + 1)) as Integer;

          

           D5: (k - 1) = (1 / (m - 1)) by D4;

          reconsider j = (m - 1) as Nat by D32;

           not (1 / j) is Integer by D31, NAT_D: 33;

          hence contradiction by D5;

        end;

      end;

    end;

    registration

      cluster prime non zero for Element of INT.Ring ;

      existence

      proof

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

        p <> ( 0. INT.Ring );

        hence thesis by STRUCT_0:def 12, INT_2: 28;

      end;

    end

    registration

      cluster prime -> non zero for Element of INT.Ring ;

      coherence ;

    end

    

     LmDOMRNG: for V,W be non empty 1-sorted, T be Function of V, W holds ( dom T) = ( [#] V) & ( rng T) c= ( [#] W)

    proof

      let V,W be non empty 1-sorted, T be Function of V, W;

      T is Element of ( Funcs (( [#] V),( [#] W))) by FUNCT_2: 8;

      hence thesis by FUNCT_2: 92;

    end;

    theorem :: ZMODUL07:2

    

     LmTF1: for V be Z_Module, A be Subset of V st A is linearly-independent holds ex B be Subset of V st A c= B & B is linearly-independent & (for v be VECTOR of V holds ex a be Element of INT.Ring st a <> 0 & (a * v) in ( Lin B))

    proof

      let V be Z_Module, A be Subset of V such that

       A1: A is linearly-independent;

      defpred P[ set] means ex B be Subset of V st B = $1 & A c= B & B is linearly-independent;

      consider Q be set such that

       A2: for Z be set holds Z in Q iff Z in ( bool the carrier of V) & P[Z] from XFAMILY:sch 1;

       A3:

      now

        let Z be set;

        assume that

         A4: Z <> {} and

         A5: Z c= Q and

         A6: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X be set such that

           A7: x in X and

           A8: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A2, A5, A8;

          hence thesis by A7;

        end;

        then

        reconsider W as Subset of V;

        

         A9: W is linearly-independent

        proof

          deffunc Q( object) = { C where C be Subset of V : $1 in C & C in Z };

          let l be Linear_Combination of W;

          assume that

           A10: ( Sum l) = ( 0. V) and

           A11: ( Carrier l) <> {} ;

          consider f be Function such that

           A12: ( dom f) = ( Carrier l) and

           A13: for x be object st x in ( Carrier l) holds (f . x) = Q(x) from FUNCT_1:sch 3;

          reconsider M = ( rng f) as non empty set by A11, A12, RELAT_1: 42;

          set F = the Choice_Function of M;

          set S = ( rng F);

           A14:

          now

            assume {} in M;

            then

            consider x be object such that

             A15: x in ( dom f) and

             A16: (f . x) = {} by FUNCT_1:def 3;

            ( Carrier l) c= W by VECTSP_6:def 4;

            then

            consider X be set such that

             A17: x in X and

             A18: X in Z by A12, A15, TARSKI:def 4;

            reconsider X as Subset of V by A2, A5, A18;

            X in { C where C be Subset of V : x in C & C in Z } by A17, A18;

            hence contradiction by A12, A13, A15, A16;

          end;

          then

           A19: ( dom F) = M by RLVECT_3: 28;

          then ( dom F) is finite by A12, FINSET_1: 8;

          then

           A20: S is finite by FINSET_1: 8;

           A21:

          now

            let X be set;

            assume X in S;

            then

            consider x be object such that

             A22: x in ( dom F) and

             A23: (F . x) = X by FUNCT_1:def 3;

            consider y be object such that

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

            reconsider x as set by TARSKI: 1;

            

             A25: x = Q(y) by A12, A13, A24;

            X in x by A14, A22, A23, ORDERS_1: 89;

            then ex C be Subset of V st C = X & y in C & C in Z by A25;

            hence X in Z;

          end;

           A26:

          now

            let X,Y be set;

            assume X in S & Y in S;

            then X in Z & Y in Z by A21;

            hence X c= Y or Y c= X by A6, ORDINAL1:def 8, XBOOLE_0:def 9;

          end;

          S <> {} by A19, RELAT_1: 42;

          then ( union S) in Z by A20, A21, A26, CARD_2: 62;

          then

          consider B be Subset of V such that

           A27: B = ( union S) and A c= B and

           A28: B is linearly-independent by A2, A5;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A29: x in ( Carrier l);

            then

             A30: (f . x) = { C where C be Subset of V : x in C & C in Z } by A13;

            

             A31: (f . x) in M by A12, A29, FUNCT_1:def 3;

            then (F . X) in X by A14, ORDERS_1: 89;

            then

             A32: ex C be Subset of V st (F . X) = C & x in C & C in Z by A30;

            (F . X) in S by A19, A31, FUNCT_1:def 3;

            hence thesis by A32, TARSKI:def 4;

          end;

          then l is Linear_Combination of B by A27, VECTSP_6:def 4;

          hence thesis by A10, A11, A28;

        end;

        set x = the Element of Z;

        x in Q by A4, A5;

        then

         A33: ex B be Subset of V st B = x & A c= B & B is linearly-independent by A2;

        x c= W by A4, ZFMISC_1: 74;

        hence ( union Z) in Q by A2, A9, A33, XBOOLE_1: 1;

      end;

      Q <> {} by A1, A2;

      then

      consider X be set such that

       A34: X in Q and

       A35: for Z be set st Z in Q & Z <> X holds not X c= Z by A3, ORDERS_1: 67;

      consider B be Subset of V such that

       A36: B = X and

       A37: A c= B and

       A38: B is linearly-independent by A2, A34;

      take B;

      thus A c= B & B is linearly-independent by A37, A38;

      assume not for v be VECTOR of V holds ex a be Element of INT.Ring st a <> 0 & (a * v) in ( Lin B);

      then

      consider v be VECTOR of V such that

       A39: for a be Element of INT.Ring st a <> 0 holds not (a * v) in ( Lin B);

      

       A40: (B \/ {v}) is linearly-independent

      proof

        let l be Linear_Combination of (B \/ {v});

        assume

         A41: ( Sum l) = ( 0. V);

        now

          per cases ;

            suppose

             B1: v in ( Carrier l);

            reconsider i0 = 0 as Element of INT.Ring ;

            deffunc G( VECTOR of V) = i0;

            deffunc L( VECTOR of V) = (l . $1);

            consider f be Function of V, INT.Ring such that

             A42: (f . v) = i0 and

             A43: for u be VECTOR of V st u <> v holds (f . u) = L(u) from FUNCT_2:sch 6;

            reconsider f as Element of ( Funcs (the carrier of V,the carrier of INT.Ring )) by FUNCT_2: 8;

            now

              let u be VECTOR of V;

              assume not u in (( Carrier l) \ {v});

              then not u in ( Carrier l) or u in {v} by XBOOLE_0:def 5;

              then (l . u) = ( 0. INT.Ring ) & u <> v or u = v by TARSKI:def 1;

              hence (f . u) = ( 0. INT.Ring ) by A42, A43;

            end;

            then

            reconsider f as Linear_Combination of V by VECTSP_6:def 1;

            ( Carrier f) c= B

            proof

              let x be object;

              

               A44: ( Carrier l) c= (B \/ {v}) by VECTSP_6:def 4;

              assume x in ( Carrier f);

              then

              consider u be VECTOR of V such that

               A45: u = x and

               A46: (f . u) <> ( 0. INT.Ring );

              (f . u) = (l . u) by A42, A43, A46;

              then u in ( Carrier l) by A46;

              then u in B or u in {v} by A44, XBOOLE_0:def 3;

              hence thesis by A42, A45, A46, TARSKI:def 1;

            end;

            then

            reconsider f as Linear_Combination of B by VECTSP_6:def 4;

            reconsider lv = ( - (l . v)) as Element of INT.Ring ;

            consider g be Function of V, INT.Ring such that

             A47: (g . v) = lv and

             A48: for u be VECTOR of V st u <> v holds (g . u) = G(u) from FUNCT_2:sch 6;

            reconsider g as Element of ( Funcs (the carrier of V,the carrier of INT.Ring )) by FUNCT_2: 8;

            now

              let u be VECTOR of V;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (g . u) = ( 0. INT.Ring ) by A48;

            end;

            then

            reconsider g as Linear_Combination of V by VECTSP_6:def 1;

            ( Carrier g) c= {v}

            proof

              let x be object;

              assume x in ( Carrier g);

              then ex u be VECTOR of V st x = u & (g . u) <> ( 0. INT.Ring );

              then x = v by A48;

              hence thesis by TARSKI:def 1;

            end;

            then

            reconsider g as Linear_Combination of {v} by VECTSP_6:def 4;

            (f - g) = l

            proof

              let u be VECTOR of V;

              now

                per cases ;

                  suppose

                   A50: v = u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by ZMODUL02: 39

                  .= (l . u) by A42, A47, A50;

                end;

                  suppose

                   A51: v <> u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by ZMODUL02: 39

                  .= ((l . u) - (g . u)) by A43, A51

                  .= ((l . u) - 0 ) by A48, A51

                  .= (l . u);

                end;

              end;

              hence thesis;

            end;

            then ( 0. V) = (( Sum f) - ( Sum g)) by A41, ZMODUL02: 55;

            

            then

             B2: ( Sum f) = (( 0. V) + ( Sum g)) by RLSUB_2: 61

            .= (( - (l . v)) * v) by A47, ZMODUL02: 21;

            ( - (l . v)) <> 0 by B1, ZMODUL02: 8;

            hence thesis by A39, B2, ZMODUL02: 64;

          end;

            suppose

             A52: not v in ( Carrier l);

            ( Carrier l) c= B

            proof

              let x be object;

              assume

               A53: x in ( Carrier l);

              ( Carrier l) c= (B \/ {v}) by VECTSP_6:def 4;

              then x in B or x in {v} by A53, XBOOLE_0:def 3;

              hence thesis by A52, A53, TARSKI:def 1;

            end;

            then l is Linear_Combination of B by VECTSP_6:def 4;

            hence thesis by A38, A41;

          end;

        end;

        hence thesis;

      end;

      v in {v} by TARSKI:def 1;

      then

       A54: v in (B \/ {v}) by XBOOLE_0:def 3;

       not (( 1. INT.Ring ) * v) in ( Lin B) by A39;

      then not v in ( Lin B) by VECTSP_1:def 17;

      then

       A55: not v in B by ZMODUL02: 65;

      B c= (B \/ {v}) by XBOOLE_1: 7;

      then (B \/ {v}) in Q by A2, A37, A40, XBOOLE_1: 1;

      hence contradiction by A35, A36, A54, A55, XBOOLE_1: 7;

    end;

    theorem :: ZMODUL07:3

    

     LmTF1C: for V be Z_Module, I be finite Subset of V, W be Submodule of V st for v be VECTOR of V st v in I holds ex a be Element of INT.Ring st a <> ( 0. INT.Ring ) & (a * v) in W holds ex a be Element of INT.Ring st a <> ( 0. INT.Ring ) & for v be VECTOR of V st v in I holds (a * v) in W

    proof

      let V be Z_Module, I be finite Subset of V, W be Submodule of V;

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

      

       P1: P[ 0 ]

      proof

        let I be finite Subset of V;

        assume that

         A0: ( card I) = 0 and for v be VECTOR of V st v in I holds ex a be Element of INT.Ring st a <> ( 0. INT.Ring ) & (a * v) in W;

        reconsider a = ( 1. INT.Ring ) as Element of INT.Ring ;

        take a;

        thus a <> ( 0. INT.Ring );

        thus for v be VECTOR of V st v in I holds (a * v) in W by A0;

      end;

      

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

      proof

        let n be Nat such that

         B1: P[n];

        let I be finite Subset of V;

        assume that

         A0: ( card I) = (n + 1) and

         A1: for v be VECTOR of V st v in I holds ex a be Element of INT.Ring st a <> ( 0. INT.Ring ) & (a * v) in W;

        I is non empty by A0;

        then

        consider u be object such that

         B3: u in I by XBOOLE_0:def 1;

        reconsider u as VECTOR of V by B3;

        set Iu = (I \ {u});

         {u} is Subset of I by B3, SUBSET_1: 41;

        

        then

         B6: ( card Iu) = ((n + 1) - ( card {u})) by A0, CARD_2: 44

        .= ((n + 1) - 1) by CARD_1: 30

        .= n;

        reconsider Iu as finite Subset of V;

        for v be VECTOR of V st v in Iu holds ex a be Element of INT.Ring st a <> ( 0. INT.Ring ) & (a * v) in W

        proof

          let v be VECTOR of V;

          assume v in Iu;

          then v in I & not v in {u} by XBOOLE_0:def 5;

          hence thesis by A1;

        end;

        then

        consider b be Element of INT.Ring such that

         A3: b <> ( 0. INT.Ring ) and

         A4: for v be VECTOR of V st v in Iu holds (b * v) in W by B1, B6;

        consider au be Element of INT.Ring such that

         A5: au <> ( 0. INT.Ring ) and

         A6: (au * u) in W by A1, B3;

        set a = (au * b);

        take a;

        thus a <> ( 0. INT.Ring ) by A3, A5;

        thus for v be VECTOR of V st v in I holds (a * v) in W

        proof

          let v be VECTOR of V;

          assume

           D1: v in I;

          per cases ;

            suppose v = u;

            

            then (a * v) = ((b * au) * u)

            .= (b * (au * u)) by VECTSP_1:def 16;

            hence (a * v) in W by A6, ZMODUL01: 37;

          end;

            suppose v <> u;

            then

             D3: (b * v) in W by A4, D1, ZFMISC_1: 56;

            (a * v) = (au * (b * v)) by VECTSP_1:def 16;

            hence (a * v) in W by D3, ZMODUL01: 37;

          end;

        end;

      end;

      

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

      assume

       X2: for v be VECTOR of V st v in I holds ex a be Element of INT.Ring st a <> ( 0. INT.Ring ) & (a * v) in W;

      ( card I) is Nat;

      hence thesis by X1, X2;

    end;

    

     LmTF1B: for V be Z_Module, I be finite Subset of V, W be Submodule of V, a be Element of INT.Ring st a <> ( 0. INT.Ring ) & for v be VECTOR of V st v in I holds (a * v) in W holds for v be VECTOR of V st v in ( Lin I) holds (a * v) in W

    proof

      let V be Z_Module, I be finite Subset of V, W be Submodule of V, a be Element of INT.Ring ;

      assume that a <> ( 0. INT.Ring ) and

       AS2: for v be VECTOR of V st v in I holds (a * v) in W;

      defpred P[ Nat] means for I be finite Subset of V st ( card I) = $1 & for v be VECTOR of V st v in I holds (a * v) in W holds for v be VECTOR of V st v in ( Lin I) holds (a * v) in W;

      

       P1: P[ 0 ]

      proof

        let I be finite Subset of V;

        assume that

         A0: ( card I) = 0 and for v be VECTOR of V st v in I holds (a * v) in W;

        I = ( {} the carrier of V) by A0;

        then

         P1: ( Lin I) = ( (0). V) by ZMODUL02: 67;

        thus for v be VECTOR of V st v in ( Lin I) holds (a * v) in W

        proof

          let v be VECTOR of V;

          assume v in ( Lin I);

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

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

          

          then (a * v) = ( 0. V) by ZMODUL01: 1

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

          hence (a * v) in W;

        end;

      end;

      

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

      proof

        let n be Nat such that

         B1: P[n];

        let I be finite Subset of V;

        assume that

         A0: ( card I) = (n + 1) and

         A1: for v be VECTOR of V st v in I holds (a * v) in W;

        I is non empty by A0;

        then

        consider u be object such that

         B3: u in I by XBOOLE_0:def 1;

        reconsider u as VECTOR of V by B3;

        set Iu = (I \ {u});

         {u} is Subset of I by B3, SUBSET_1: 41;

        

        then

         B6: ( card Iu) = ((n + 1) - ( card {u})) by A0, CARD_2: 44

        .= ((n + 1) - 1) by CARD_1: 30

        .= n;

        reconsider Iu as finite Subset of V;

        set Ku = {u};

        

         E1: I = (Iu \/ Ku) by B3, XBOOLE_1: 45, ZFMISC_1: 31;

        

         E3: ( Lin I) = (( Lin Iu) + ( Lin Ku)) by E1, ZMODUL02: 72;

        

         A4: for v be VECTOR of V st v in Iu holds (a * v) in W

        proof

          let v be VECTOR of V;

          assume v in Iu;

          then v in I & not v in {u} by XBOOLE_0:def 5;

          hence thesis by A1;

        end;

        thus for v be VECTOR of V st v in ( Lin I) holds (a * v) in W

        proof

          let v be VECTOR of V;

          assume v in ( Lin I);

          then

          consider v1,v2 be VECTOR of V such that

           F1: v1 in ( Lin Iu) and

           F2: v2 in ( Lin Ku) and

           F3: v = (v1 + v2) by E3, ZMODUL01: 92;

          

           F4: (a * v1) in W by F1, A4, B1, B6;

          consider i be Element of INT.Ring such that

           F5: v2 = (i * u) by F2, ZMODUL06: 19;

          

           F6: (a * v2) = ((a * i) * u) by F5, VECTSP_1:def 16

          .= ((i * a) * u)

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

          

           F7: (a * v2) in W by A1, B3, F6, ZMODUL01: 37;

          (a * v) = (a * (v1 + v2)) = ((a * v1) + (a * v2)) by F3, VECTSP_1:def 14;

          hence (a * v) in W by ZMODUL01: 36, F7, F4;

        end;

      end;

      

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

      ( card I) is Nat;

      hence thesis by X1, AS2;

    end;

    theorem :: ZMODUL07:4

    

     LmTF1D: for V be finite-rank free Z_Module, I be linearly-independent Subset of V holds I is finite

    proof

      let V be finite-rank free Z_Module, I be linearly-independent Subset of V;

      set IV = the Basis of V;

      ( card I) c= ( card IV) by ZMODUL04: 20;

      hence thesis;

    end;

    registration

      let V be finite-rank free Z_Module;

      cluster linearly-independent -> finite for Subset of V;

      coherence by LmTF1D;

    end

    

     LmTF1A: for V be finite-rank free Z_Module, A be Subset of V st A is linearly-independent holds ex B be finite Subset of V, a be Element of INT.Ring st a <> ( 0. INT.Ring ) & A c= B & B is linearly-independent & for v be VECTOR of V holds (a * v) in ( Lin B)

    proof

      let V be finite-rank free Z_Module, A be Subset of V;

      assume A is linearly-independent;

      then

      consider B be Subset of V such that

       P1: A c= B and

       P2: B is linearly-independent and

       P3: for v be VECTOR of V holds ex a be Element of INT.Ring st a <> ( 0. INT.Ring ) & (a * v) in ( Lin B) by LmTF1;

      reconsider B as finite Subset of V by P2;

      consider I be finite Subset of V such that

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

      

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

      for v be VECTOR of V st v in I holds ex a be Element of INT.Ring st a <> ( 0. INT.Ring ) & (a * v) in ( Lin B) by P3;

      then

      consider a be Element of INT.Ring such that

       B1: a <> ( 0. INT.Ring ) and

       B2: for v be VECTOR of V st v in I holds (a * v) in ( Lin B) by LmTF1C;

      take B, a;

      thus a <> ( 0. INT.Ring ) & A c= B & B is linearly-independent by P1, B1, P2;

      thus for v be VECTOR of V holds (a * v) in ( Lin B)

      proof

        let v be VECTOR of V;

        v in ( (Omega). V);

        hence thesis by A2, B1, B2, LmTF1B;

      end;

    end;

    theorem :: ZMODUL07:5

    

     LmRankSX11: for V be finite-rank free Z_Module, A be linearly-independent Subset of V holds ex I be finite linearly-independent Subset of V, a be Element of INT.Ring st a <> ( 0. INT.Ring ) & A c= I & (a (*) V) is Submodule of ( Lin I)

    proof

      let V be finite-rank free Z_Module, A be linearly-independent Subset of V;

      consider I be finite Subset of V, a be Element of INT.Ring such that

       P0: a <> ( 0. INT.Ring ) and

       P1: A c= I and

       P2: I is linearly-independent and

       P3: for v be VECTOR of V holds (a * v) in ( Lin I) by LmTF1A;

      reconsider I as finite linearly-independent Subset of V by P2;

      take I, a;

      thus a <> ( 0. INT.Ring ) & A c= I by P0, P1;

      for v be VECTOR of V st v in (a (*) V) holds v in ( Lin I)

      proof

        let v be VECTOR of V;

        assume v in (a (*) V);

        then

        consider w be VECTOR of V such that

         P4: v = (a * w);

        thus v in ( Lin I) by P3, P4;

      end;

      hence (a (*) V) is Submodule of ( Lin I) by ZMODUL01: 44;

    end;

    theorem :: ZMODUL07:6

    

     LmRankSX1: for V be finite-rank free Z_Module, A be linearly-independent Subset of V holds ex I be finite linearly-independent Subset of V st A c= I & ( rank V) = ( card I)

    proof

      let V be finite-rank free Z_Module, A be linearly-independent Subset of V;

      consider I be finite linearly-independent Subset of V, a be Element of INT.Ring such that

       A1: a <> 0 & A c= I & (a (*) V) is Submodule of ( Lin I) by LmRankSX11;

      take I;

      

       A3: V is finite-rank free Submodule of V by ZMODUL01: 32;

      ( rank (a (*) V)) <= ( rank ( Lin I)) by A1, ZMODUL05: 2;

      then

       A2: ( rank V) <= ( rank ( Lin I)) by A1, A3, ZMODUL06: 52;

      ( rank ( Lin I)) <= ( rank V) by ZMODUL05: 2;

      then ( rank ( Lin I)) = ( rank V) by A2, XXREAL_0: 1;

      hence thesis by A1, ZMODUL05: 3;

    end;

    theorem :: ZMODUL07:7

    

     LmRankSX2: for V be torsion-free Z_Module, W1,W2 be finite-rank free Submodule of V, I1 be Basis of W1 holds ex I be finite linearly-independent Subset of V st I is Subset of (W1 + W2) & I1 c= I & ( rank (W1 + W2)) = ( rank ( Lin I))

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Submodule of V, I1 be Basis of W1;

      

       A2: W1 is Submodule of (W1 + W2) by ZMODUL01: 97;

      then I1 c= the carrier of W1 & the carrier of W1 c= the carrier of (W1 + W2) by VECTSP_4:def 2;

      then I1 c= the carrier of (W1 + W2);

      then

      reconsider II1 = I1 as Subset of (W1 + W2);

      reconsider II1 as finite Subset of (W1 + W2);

      reconsider II1 as finite linearly-independent Subset of (W1 + W2) by A2, VECTSP_7:def 3, ZMODUL03: 15;

      consider II be finite linearly-independent Subset of (W1 + W2) such that

       A3: II1 c= II & ( rank (W1 + W2)) = ( card II) by LmRankSX1;

      II c= the carrier of (W1 + W2) & the carrier of (W1 + W2) c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider I = II as Subset of V by XBOOLE_1: 1;

      reconsider I as finite linearly-independent Subset of V by ZMODUL03: 15;

      ( rank (W1 + W2)) = ( rank ( Lin I)) by A3, ZMODUL05: 3;

      hence thesis by A3;

    end;

    theorem :: ZMODUL07:8

    for V be torsion-free Z_Module, W1,W2 be finite-rank free Submodule of V st W2 is Submodule of W1 holds ex W3 be finite-rank free Submodule of V st ( rank W1) = (( rank W2) + ( rank W3)) & (W2 /\ W3) = ( (0). V) & W3 is Submodule of W1

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Submodule of V such that

       A0: W2 is Submodule of W1;

      set III2 = the Basis of W2;

      III2 c= the carrier of W2 & the carrier of W2 c= the carrier of W1 by A0, VECTSP_4:def 2;

      then

      reconsider II2 = III2 as Subset of W1 by XBOOLE_1: 1;

      reconsider II2 as finite linearly-independent Subset of W1 by A0, VECTSP_7:def 3, ZMODUL03: 15;

      consider II1 be finite linearly-independent Subset of W1 such that

       A1: II2 c= II1 & ( rank W1) = ( card II1) by LmRankSX1;

      II1 c= the carrier of W1 & the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

      then II1 c= the carrier of V;

      then

      reconsider I1 = II1 as Subset of V;

      reconsider I1 as finite Subset of V;

      reconsider I1 as finite linearly-independent Subset of V by ZMODUL03: 15;

      set II3 = (II1 \ II2);

      II2 c= the carrier of W1 & the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

      then II2 c= the carrier of V;

      then

      reconsider I2 = II2 as Subset of V;

      reconsider I2 as finite Subset of V;

      reconsider I2 as finite linearly-independent Subset of V by ZMODUL03: 15;

      II3 c= the carrier of W1 & the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

      then II3 c= the carrier of V;

      then

      reconsider I3 = II3 as Subset of V;

      II3 is linearly-independent by XBOOLE_1: 36, ZMODUL02: 56;

      then

      reconsider I3 as linearly-independent Subset of V by ZMODUL03: 15;

      reconsider I3 as finite linearly-independent Subset of V;

      

       A3: (W2 /\ ( Lin I3)) = ( (0). V)

      proof

        

         B1: ( (Omega). W2) = ( Lin III2) by VECTSP_7:def 3

        .= ( Lin I2) by ZMODUL03: 20;

        reconsider W2s = ( (Omega). W2) as finite-rank free Submodule of V by ZMODUL01: 42;

        ( (Omega). ( Lin I3)) = ( Lin I3);

        then

         B2: (W2 /\ ( Lin I3)) = (( Lin I2) /\ ( Lin I3)) by B1, ZMODUL04: 23;

        I2 c= I1 & I3 = (I1 \ I2) by A1;

        hence (W2 /\ ( Lin I3)) = ( (0). V) by B2, ZMODUL06: 4;

      end;

      ( card II3) = (( card II1) - ( card II2)) by A1, CARD_2: 44

      .= (( rank W1) - ( rank W2)) by A1, ZMODUL03:def 5;

      then

       A6: ( rank ( Lin I3)) = (( rank W1) - ( rank W2)) by ZMODUL05: 3;

      

       A11: ( Lin I3) is Submodule of ( Lin I1) by XBOOLE_1: 36, ZMODUL02: 70;

      ( Lin II1) is Submodule of W1;

      then

       A7: ( Lin I1) is Submodule of W1 by ZMODUL03: 20;

      take ( Lin I3);

      thus thesis by A3, A6, A7, A11, ZMODUL01: 42;

    end;

    theorem :: ZMODUL07:9

    for V be torsion-free Z_Module, W1,W2 be finite-rank free Submodule of V holds ex W3 be finite-rank free Submodule of V st ( rank (W1 + W2)) = (( rank W1) + ( rank W3)) & (W1 /\ W3) = ( (0). V) & W3 is Submodule of (W1 + W2)

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Submodule of V;

      set I1 = the Basis of W1;

      consider I be finite linearly-independent Subset of V such that

       A1: I is Subset of (W1 + W2) & I1 c= I & ( rank (W1 + W2)) = ( rank ( Lin I)) by LmRankSX2;

      set I2 = (I \ I1);

      I1 c= the carrier of W1 & the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

      then I1 c= the carrier of V;

      then

      reconsider II1 = I1 as Subset of V;

      reconsider II1 as finite Subset of V;

      

       A10: II1 is linearly-independent by VECTSP_7:def 3, ZMODUL03: 15;

      reconsider II2 = I2 as finite linearly-independent Subset of V by XBOOLE_1: 36, ZMODUL02: 56;

      

       A3: (W1 /\ ( Lin II2)) = ( (0). V)

      proof

        

         B1: ( (Omega). W1) = ( Lin I1) by VECTSP_7:def 3

        .= ( Lin II1) by ZMODUL03: 20;

        reconsider W1s = ( (Omega). W1) as finite-rank free Submodule of V by ZMODUL01: 42;

        ( (Omega). ( Lin II2)) = ( Lin II2);

        then (W1 /\ ( Lin II2)) = (( Lin II1) /\ ( Lin II2)) by B1, ZMODUL04: 23;

        hence thesis by A1, A10, ZMODUL06: 4;

      end;

      

       A4: ( card I) = ( rank (W1 + W2)) by A1, ZMODUL05: 3;

      ( card II2) = (( card I) - ( card I1)) by A1, CARD_2: 44

      .= (( rank (W1 + W2)) - ( rank W1)) by A4, ZMODUL03:def 5;

      then

       A6: ( rank ( Lin II2)) = (( rank (W1 + W2)) - ( rank W1)) by ZMODUL05: 3;

      

       A11: ( Lin II2) is Submodule of ( Lin I) by XBOOLE_1: 36, ZMODUL02: 70;

      reconsider II = I as Subset of (W1 + W2) by A1;

      ( Lin II) is Submodule of (W1 + W2);

      then

       A7: ( Lin I) is Submodule of (W1 + W2) by ZMODUL03: 20;

      take ( Lin II2);

      thus thesis by A3, A6, A7, A11, ZMODUL01: 42;

    end;

    theorem :: ZMODUL07:10

    for V be finite-rank free Z_Module, W1,W2 be Submodule of V holds ( rank (W1 /\ W2)) >= ((( rank W1) + ( rank W2)) - ( rank V))

    proof

      let V be finite-rank free Z_Module, W1,W2 be Submodule of V;

      

       A1: ( rank (W1 + W2)) <= ( rank V) & (( rank V) + (( rank (W1 /\ W2)) - ( rank V))) = ( rank (W1 /\ W2)) by ZMODUL05: 2;

      ((( rank W1) + ( rank W2)) - ( rank V)) = ((( rank (W1 + W2)) + ( rank (W1 /\ W2))) - ( rank V)) by ZMODUL06: 62

      .= (( rank (W1 + W2)) + (( rank (W1 /\ W2)) - ( rank V)));

      hence thesis by A1, XREAL_1: 6;

    end;

    definition

      let V be LeftMod of INT.Ring ;

      :: ZMODUL07:def1

      func torsion_part (V) -> strict Subspace of V means

      : defTorsionPart: the carrier of it = { v where v be Vector of V : v is torsion };

      existence

      proof

        set X = { v where v be Vector of V : v is torsion };

        

         A1: for x be object st x in X holds x in the carrier of V

        proof

          let x be object such that

           B1: x in X;

          consider y be Vector of V such that

           B2: y = x & y is torsion by B1;

          thus x in the carrier of V by B2;

        end;

        

         A2: for x be Vector of V st x in X holds x is torsion

        proof

          let x be Vector of V such that

           B1: x in X;

          consider y be Vector of V such that

           B2: y = x & y is torsion by B1;

          thus thesis by B2;

        end;

        X c= the carrier of V by A1;

        then

        reconsider X as Subset of V;

        

         A4: for v,u be Vector of V st v in X & u in X holds (v + u) in X

        proof

          let v,u be Vector of V such that

           B1: v in X & u in X;

          v is torsion & u is torsion by A2, B1;

          then (v + u) is torsion by ZMODUL06: 5;

          hence thesis;

        end;

        for i be Element of INT.Ring , v be Vector of V st v in X holds (i * v) in X

        proof

          let i be Element of INT.Ring , v be Vector of V such that

           B1: v in X;

          (i * v) is torsion by A2, B1, ZMODUL06: 8;

          hence thesis;

        end;

        then

         A6: X is linearly-closed by A4;

        ( 0. V) in X;

        then

        reconsider X as non empty Subset of V;

        consider W be strict Subspace of V such that

         A7: X = the carrier of W by A6, ZMODUL01: 50;

        take W;

        thus thesis by A7;

      end;

      uniqueness by ZMODUL01: 45;

    end

    theorem :: ZMODUL07:11

    

     LmTP1: for V be Z_Module, v be Vector of V holds v is torsion iff v in ( torsion_part V)

    proof

      let V be Z_Module, v be Vector of V;

      set W = ( torsion_part V);

      hereby

        assume v is torsion;

        then v in { v where v be Vector of V : v is torsion };

        hence v in W by defTorsionPart;

      end;

      assume v in W;

      then v in { v where v be Vector of V : v is torsion } by defTorsionPart;

      then

      consider vv be Vector of V such that

       A2: vv = v & vv is torsion;

      thus v is torsion by A2;

    end;

    theorem :: ZMODUL07:12

    for V be Z_Module holds V is torsion-free iff ( torsion_part V) = ( (0). V)

    proof

      let V be Z_Module;

      set W = ( torsion_part V);

      hereby

        assume

         A1: V is torsion-free;

        for x be object holds x in the carrier of W implies x in {( 0. V)}

        proof

          let x be object;

          assume

           B11: x in the carrier of W;

          then

           B1: x in W;

          reconsider xx = x as VECTOR of V by B11, ZMODUL01: 25;

          xx is torsion by B1, LmTP1;

          then x = ( 0. V) by A1;

          hence x in {( 0. V)} by TARSKI:def 1;

        end;

        then

         A3: the carrier of W c= {( 0. V)};

        ( 0. V) in W by ZMODUL01: 33;

        then {( 0. V)} c= the carrier of W by ZFMISC_1: 31;

        hence W = ( (0). V) by A3, XBOOLE_0:def 10, VECTSP_4:def 3;

      end;

      assume W = ( (0). V);

      then

       A2: the carrier of W = {( 0. V)} by VECTSP_4:def 3;

      for v be VECTOR of V holds v is torsion implies v = ( 0. V)

      proof

        let v be VECTOR of V;

        assume v is torsion;

        then v in W by LmTP1;

        hence v = ( 0. V) by A2, TARSKI:def 1;

      end;

      hence V is torsion-free;

    end;

    

     ThTF1: for V be Z_Module holds ( VectQuot (V,( torsion_part V))) is torsion-free

    proof

      let V be Z_Module;

      set W = ( torsion_part V);

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

      for v be Vector of ZQ st v <> ( 0. ZQ) holds not v is torsion

      proof

        let v be Vector of ZQ;

        assume

         AS: v <> ( 0. ZQ);

        assume v is torsion;

        then

        consider i be Element of INT.Ring such that

         P1: i <> 0 & (i * v) = ( 0. ZQ);

        

         P3: v is Element of ( CosetSet (V,W)) by VECTSP10:def 6;

        then v in ( CosetSet (V,W));

        then ex A be Coset of W st v = A;

        then

        consider a be VECTOR of V such that

         A3: v = (a + W) by VECTSP_4:def 6;

        

         A4: (i * v) = (( lmultCoset (V,W)) . (i,v)) by VECTSP10:def 6

        .= ((i * a) + W) by VECTSP10:def 5, A3, P3;

        (i * v) = ( zeroCoset (V,W)) by P1, VECTSP10:def 6

        .= the carrier of W;

        then (i * a) in W by ZMODUL01: 63, A4;

        then (i * a) in { v where v be VECTOR of V : v is torsion } by defTorsionPart;

        then ex w be VECTOR of V st (i * a) = w & w is torsion;

        then

        consider j be Element of INT.Ring such that

         A5: j <> 0 & (j * (i * a)) = ( 0. V);

        ((j * i) * a) = ( 0. V) by A5, VECTSP_1:def 16;

        then a is torsion by A5, P1;

        then a in { v where v be VECTOR of V : v is torsion };

        then a in W by defTorsionPart;

        then v = ( zeroCoset (V,W)) by A3, ZMODUL01: 63;

        hence contradiction by AS, VECTSP10:def 6;

      end;

      hence thesis;

    end;

    registration

      let V be Z_Module;

      cluster ( VectQuot (V,( torsion_part V))) -> torsion-free;

      coherence by ThTF1;

    end

    definition

      let R be Ring;

      let V be LeftMod of R;

      let W be Subspace of V;

      :: ZMODUL07:def2

      func ZQMorph (V,W) -> linear-transformation of V, ( VectQuot (V,W)) means

      : defMophVW: for v be Element of V holds (it . v) = (v + W);

      existence

      proof

        defpred P[ Element of V, Element of ( VectQuot (V,W))] means $2 = ($1 + W);

        

         A11: for v be Element of V holds ex y be Element of ( VectQuot (V,W)) st P[v, y]

        proof

          let v be Element of V;

          reconsider y = (v + W) as Coset of W by VECTSP_4:def 6;

          y in ( CosetSet (V,W));

          then

          reconsider y as Element of ( VectQuot (V,W)) by VECTSP10:def 6;

          take y;

          thus thesis;

        end;

        consider f be Function of V, ( VectQuot (V,W)) such that

         A15: for v be Element of V holds P[v, (f . v)] from FUNCT_2:sch 3( A11);

        for x,y be Vector of V holds (f . (x + y)) = ((f . x) + (f . y))

        proof

          let x,y be Vector of V;

          

           A2: (f . x) = (x + W) by A15;

          

           A3: (f . y) = (y + W) by A15;

          reconsider A = (x + W) as Element of ( CosetSet (V,W)) by A2, VECTSP10:def 6;

          reconsider B = (y + W) as Element of ( CosetSet (V,W)) by A3, VECTSP10:def 6;

          

          thus (f . (x + y)) = ((x + y) + W) by A15

          .= (( addCoset (V,W)) . (A,B)) by VECTSP10:def 3

          .= ((f . x) + (f . y)) by A2, A3, VECTSP10:def 6;

        end;

        then

         A16: f is additive;

        for a be Element of R, x be Element of V holds (f . (a * x)) = (a * (f . x))

        proof

          let a be Element of R, x be Element of V;

          

           A2: (f . x) = (x + W) by A15;

          reconsider A = (x + W) as Element of ( CosetSet (V,W)) by A2, VECTSP10:def 6;

          

          thus (f . (a * x)) = ((a * x) + W) by A15

          .= (( lmultCoset (V,W)) . (a,A)) by VECTSP10:def 5

          .= (a * (f . x)) by A2, VECTSP10:def 6;

        end;

        then f is homogeneous;

        hence thesis by A15, A16;

      end;

      uniqueness

      proof

        let f1,f2 be linear-transformation of V, ( VectQuot (V,W));

        assume

         AS1: for v be Element of V holds (f1 . v) = (v + W);

        assume

         AS2: for v be Element of V holds (f2 . v) = (v + W);

        for v be Element of V holds (f1 . v) = (f2 . v)

        proof

          let v be Element of V;

          

          thus (f1 . v) = (v + W) by AS1

          .= (f2 . v) by AS2;

        end;

        hence f1 = f2 by FUNCT_2:def 8;

      end;

    end

    registration

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V;

      cluster ( ZQMorph (V,W)) -> onto;

      coherence

      proof

        for y be object st y in the carrier of ( VectQuot (V,W)) holds ex x be object st x in the carrier of V & y = (( ZQMorph (V,W)) . x)

        proof

          let y be object;

          assume y in the carrier of ( VectQuot (V,W));

          then

          reconsider A = y as Element of ( CosetSet (V,W)) by VECTSP10:def 6;

          A in ( CosetSet (V,W));

          then

          consider A0 be Coset of W such that

           P0: A = A0;

          consider v be VECTOR of V such that

           P1: A0 = (v + W) by VECTSP_4:def 6;

          (( ZQMorph (V,W)) . v) = y by P0, P1, defMophVW;

          hence thesis;

        end;

        then ( rng ( ZQMorph (V,W))) = the carrier of ( VectQuot (V,W)) by FUNCT_2: 10;

        hence thesis by FUNCT_2:def 3;

      end;

    end

    theorem :: ZMODUL07:13

    for V,W be Z_Module, T be linear-transformation of V, W, s be FinSequence of V, t be FinSequence of W st ( len s) = ( len t) & for i be Element of NAT st i in ( dom s) holds ex si be VECTOR of V st si = (s . i) & (t . i) = (T . si) holds ( Sum t) = (T . ( Sum s))

    proof

      let V,W be Z_Module, T be linear-transformation of V, W;

      

       XX: T is additive;

      defpred P[ Nat] means for s be FinSequence of V, t be FinSequence of W st ( len s) = $1 & ( len s) = ( len t) & for i be Element of NAT st i in ( dom s) holds ex si be VECTOR of V st si = (s . i) & (t . i) = (T . si) holds ( Sum t) = (T . ( Sum s));

      

       A1: P[ 0 ]

      proof

        let s be FinSequence of V, t be FinSequence of W;

        assume that

         A2: ( len s) = 0 & ( len s) = ( len t) and for i be Element of NAT st i in ( dom s) holds ex si be VECTOR of V st si = (s . i) & (t . i) = (T . si);

        s = ( <*> the carrier of V) by A2;

        then ( Sum s) = ( 0. V) by RLVECT_1: 43;

        then

         A3: (T . ( Sum s)) = ( 0. W) by ZMODUL05: 19;

        t = ( <*> the carrier of W) by A2;

        hence thesis by A3, RLVECT_1: 43;

      end;

      

       A4: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A5: P[k];

        now

          let s be FinSequence of V, t be FinSequence of W;

          assume that

           A6: ( len s) = (k + 1) & ( len s) = ( len t) and

           A7: for i be Element of NAT st i in ( dom s) holds ex si be VECTOR of V st si = (s . i) & (t . i) = (T . si);

          reconsider s1 = (s | k) as FinSequence of V;

          

           A8: ( dom s) = ( Seg (k + 1)) by A6, FINSEQ_1:def 3;

          

           A9: ( dom t) = ( Seg (k + 1)) by A6, FINSEQ_1:def 3;

          

           A10: ( len s1) = k by A6, FINSEQ_1: 59, NAT_1: 11;

          

           A11: ( dom s1) = ( Seg ( len s1)) by FINSEQ_1:def 3

          .= ( Seg k) by A6, FINSEQ_1: 59, NAT_1: 11;

          then

           A12: s1 = (s | ( dom s1)) by FINSEQ_1:def 15;

          reconsider t1 = (t | k) as FinSequence of W;

          

           A13: ( dom t1) = ( Seg ( len t1)) by FINSEQ_1:def 3

          .= ( Seg k) by A6, FINSEQ_1: 59, NAT_1: 11;

          then

           A14: t1 = (t | ( dom t1)) by FINSEQ_1:def 15;

          k in NAT by ORDINAL1:def 12;

          then

           A15: ( len t1) = k by A13, FINSEQ_1:def 3;

          (s . ( len s)) in ( rng s) by A6, A8, FINSEQ_1: 4, FUNCT_1: 3;

          then

          reconsider vs = (s . ( len s)) as Element of V;

          (t . ( len t)) in ( rng t) by A6, A9, FINSEQ_1: 4, FUNCT_1: 3;

          then

          reconsider vt = (t . ( len t)) as Element of W;

          

           A16: ( len s1) = k & ( len s1) = ( len t1) by A10, A13, FINSEQ_1:def 3;

          

           A17: for i be Element of NAT st i in ( dom s1) holds ex si be VECTOR of V st si = (s1 . i) & (t1 . i) = (T . si)

          proof

            let i be Element of NAT ;

            assume

             A18: i in ( dom s1);

            ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5, NAT_1: 11;

            then

            consider si be VECTOR of V such that

             A19: si = (s . i) & (t . i) = (T . si) by A7, A11, A8, A18;

            take si;

            thus si = (s1 . i) by A12, A18, A19, FUNCT_1: 49;

            thus (t1 . i) = (T . si) by A14, A11, A13, A18, A19, FUNCT_1: 49;

          end;

          

           A20: ( Sum t1) = (T . ( Sum s1)) by A5, A16, A17;

          

           A21: ( len s) = (( len s1) + 1) by A6, FINSEQ_1: 59, NAT_1: 11;

          consider ssi be VECTOR of V such that

           A22: ssi = (s . ( len s)) & (t . ( len s)) = (T . ssi) by A6, A7, A8, FINSEQ_1: 4;

          

          thus ( Sum t) = (( Sum t1) + vt) by A6, A14, A15, RLVECT_1: 38

          .= (T . (( Sum s1) + vs)) by A6, A20, A22, XX

          .= (T . ( Sum s)) by A12, A21, RLVECT_1: 38;

        end;

        hence P[(k + 1)];

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A1, A4);

      hence thesis;

    end;

    registration

      let V be finitely-generated Z_Module, W be Submodule of V;

      cluster ( VectQuot (V,W)) -> finitely-generated;

      coherence

      proof

        consider A be finite Subset of V such that

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

        set T = ( ZQMorph (V,W));

        reconsider B = (T .: A) as finite Subset of ( VectQuot (V,W));

        

         A2: (T .: the carrier of ( Lin A)) c= the carrier of ( Lin B) by ZMODUL06: 40;

        

         A3: ( rng T) = the carrier of ( VectQuot (V,W)) by FUNCT_2:def 3;

        

         X1: ( rng T) = (T .: ( dom T)) by RELAT_1: 113

        .= (T .: the carrier of ( Lin A)) by A1, FUNCT_2:def 1;

        the carrier of ( Lin B) c= the carrier of ( VectQuot (V,W)) by VECTSP_4:def 2;

        hence thesis by A2, A3, X1, XBOOLE_0:def 10, ZMODUL01: 47;

      end;

    end

    registration

      let V be finitely-generated Z_Module;

      cluster ( VectQuot (V,( torsion_part V))) -> free;

      correctness ;

    end

    begin

    definition

      :: ZMODUL07:def3

      func Rat-Module -> ModuleStr over INT.Ring equals ModuleStr (# the carrier of F_Rat , the addF of F_Rat , the ZeroF of F_Rat , ( Int-mult-left F_Rat ) #);

      coherence ;

    end

    registration

      cluster Rat-Module -> non empty;

      coherence ;

    end

    registration

      cluster Rat-Module -> Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital;

      correctness

      proof

        set ZS = Rat-Module ;

        reconsider ZS as non empty ModuleStr over INT.Ring ;

        set AG = the carrier of F_Rat ;

        set MLI = ( Int-mult-left F_Rat );

        

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

        proof

          let v,w be Element of ZS;

          reconsider v1 = v, w1 = w as Element of F_Rat ;

          

          thus (v + w) = (v1 + w1)

          .= (w1 + v1)

          .= (w + v);

        end;

        

         A2: 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 u1 = u, v1 = v, w1 = w as Element of F_Rat ;

          

          thus ((u + v) + w) = ((u1 + v1) + w1)

          .= (u1 + (v1 + w1))

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

        end;

        

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

        proof

          let v be Element of ZS;

          reconsider v1 = v as Element of F_Rat ;

          

          thus (v + ( 0. ZS)) = (v1 + ( 0. F_Rat ))

          .= v;

        end;

        

         A6: for v be Vector of ZS holds v is right_complementable

        proof

          let v be Vector of ZS;

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

          reconsider v1 = v as Element of F_Rat ;

          set i0 = ( 0. INT.Ring );

          set i1 = ( 1. INT.Ring );

          set i2 = ( - ( 1. INT.Ring ));

          ( 0. F_Rat ) = (MLI . ((i1 + i2),v1)) by ZMODUL01: 152

          .= ((MLI . (i1,v1)) + (MLI . (i2,v1))) by ZMODUL01: 159

          .= (v + (( - ( 1. INT.Ring )) * v)) by ZMODUL01: 155;

          hence thesis;

        end;

        

         A8: for a,b be Element of INT.Ring , v be Vector of ZS holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a,b be Element of INT.Ring ;

          let v be Vector of ZS;

          reconsider a1 = a, b1 = b as Element of INT.Ring ;

          reconsider v1 = v as Element of F_Rat ;

          

          thus ((a + b) * v) = ((MLI . (a1,v1)) + (MLI . (b1,v1))) by ZMODUL01: 159

          .= ((a * v) + (b * v));

        end;

        for a be Element of INT.Ring , v,w be Vector of ZS holds (a * (v + w)) = ((a * v) + (a * w))

        proof

          let a be Element of INT.Ring ;

          let v,w be Vector of ZS;

          reconsider a1 = a as Element of INT.Ring ;

          reconsider v1 = v, w1 = w as Element of F_Rat ;

          

          thus (a * (v + w)) = (MLI . (a,(v1 + w1)))

          .= ((MLI . (a1,v1)) + (MLI . (a1,w1))) by ZMODUL01: 161

          .= ((a * v) + (a * w));

        end;

        hence thesis by A1, A2, A5, A6, A8, ZMODUL01: 163, ZMODUL01: 155, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

      end;

    end

    theorem :: ZMODUL07:14

    

     LMTFRat1: for v be Element of F_Rat , v1 be Rational st v = v1 holds for n be Nat holds (( Nat-mult-left F_Rat ) . (n,v)) = (n * v1)

    proof

      let v be Element of F_Rat , v1 be Rational;

      assume

       A1: v = v1;

      defpred P[ Nat] means (( Nat-mult-left F_Rat ) . ($1,v)) = ($1 * v1);

      (( Nat-mult-left F_Rat ) . ( 0 ,v)) = ( 0. F_Rat ) by BINOM:def 3

      .= ( 0 * v1);

      then

       X1: P[ 0 ];

      

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

      proof

        let n be Nat;

        assume

         X22: P[n];

        (( Nat-mult-left F_Rat ) . ((n + 1),v)) = (v + (( Nat-mult-left F_Rat ) . (n,v))) by BINOM:def 3

        .= (v1 + (n * v1)) by A1, X22

        .= ((n + 1) * v1);

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: ZMODUL07:15

    

     LMTFRat2: for x be Integer, v be Element of F_Rat , v1 be Rational st v = v1 holds (( Int-mult-left F_Rat ) . (x,v)) = (x * v1)

    proof

      let x be Integer, v be Element of F_Rat , v1 be Rational;

      assume

       A1: v = v1;

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

      per cases ;

        suppose

         C1: x >= 0 ;

        then

        reconsider x0 = x as Element of NAT by INT_1: 3;

        

        thus (( Int-mult-left F_Rat ) . (x,v)) = (( Nat-mult-left F_Rat ) . (xx,v)) by C1, ZMODUL01:def 20

        .= (x0 * v1) by LMTFRat1, A1

        .= (x * v1);

      end;

        suppose

         C2: x < 0 ;

        then

        reconsider x0 = ( - x) as Element of NAT by INT_1: 3;

        

        thus (( Int-mult-left F_Rat ) . (x,v)) = (( Nat-mult-left F_Rat ) . (( - xx),( - v))) by C2, ZMODUL01:def 20

        .= (x0 * ( - v1)) by A1, LMTFRat1

        .= (x * v1);

      end;

    end;

    registration

      cluster Rat-Module -> torsion-free;

      correctness

      proof

        set V = Rat-Module ;

        for v be VECTOR of V st v <> ( 0. V) holds not v is torsion

        proof

          let v be VECTOR of V;

          assume

           AS: v <> ( 0. V);

          assume v is torsion;

          then

          consider i be Element of INT.Ring such that

           P1: i <> ( 0. INT.Ring ) & (i * v) = ( 0. V);

          reconsider v1 = v as Rational;

          (i * v1) = 0 by LMTFRat2, P1;

          hence contradiction by AS, P1;

        end;

        hence thesis;

      end;

    end

    registration

      cluster Rat-Module -> non trivial;

      correctness ;

    end

    theorem :: ZMODUL07:16

    

     LMThFRat31: for s be Element of Rat-Module holds ( Lin {s}) <> Rat-Module

    proof

      set ZS = Rat-Module ;

      let s be Element of ZS;

      assume

       AS: ( Lin {s}) = ZS;

      consider m,n be Integer such that

       P2: n <> 0 & s = (m / n) by RAT_1: 1;

      per cases ;

        suppose

         N1: n = ( - 1);

        reconsider t = (1 / 2) as Element of ZS by RAT_1:def 1;

        t in ( Lin {s}) by AS;

        then

        consider l be Linear_Combination of {s} such that

         P3: t = ( Sum l) by ZMODUL02: 64;

        

         P4: ( Sum l) = ((l . s) * s) by ZMODUL02: 21;

        reconsider k = (l . s) as Integer;

        (1 / 2) = (k * ( - m)) by N1, P2, P3, P4, LMTFRat2

        .= ( - (k * m));

        hence contradiction by NAT_D: 33;

      end;

        suppose

         N0: n <> ( - 1);

        per cases ;

          suppose

           C1: m = 1 or m = ( - 1);

          per cases by C1;

            suppose

             D1: m = 1;

            per cases ;

              suppose

               XD3: n = ( - 2);

              reconsider t = ( - (1 / 3)) as Element of ZS by RAT_1:def 2;

              t in ( Lin {s}) by AS;

              then

              consider l be Linear_Combination of {s} such that

               P3: t = ( Sum l) by ZMODUL02: 64;

              

               P4: ( Sum l) = ((l . s) * s) by ZMODUL02: 21;

              reconsider k = (l . s) as Integer;

              

               P5: ( - (1 / 3)) = (k / n) by D1, P2, P3, P4, LMTFRat2;

              k = ((k / n) * n) by P2, XCMPLX_1: 87

              .= (2 / 3) by P5, XD3;

              hence contradiction by NAT_D: 33;

            end;

              suppose

               XD2: n <> ( - 2);

              reconsider t = (1 / (n + 1)) as Element of ZS by RAT_1:def 1;

              t in ( Lin {s}) by AS;

              then

              consider l be Linear_Combination of {s} such that

               P3: t = ( Sum l) by ZMODUL02: 64;

              

               P4: ( Sum l) = ((l . s) * s) by ZMODUL02: 21;

              reconsider k = (l . s) as Integer;

              

               P5: (1 / (n + 1)) = (k / n) by D1, P2, P3, P4, LMTFRat2;

              k = (n / (n + 1)) by P2, P5, XCMPLX_1: 87;

              hence contradiction by LMThFRat31X, N0, XD2, P2;

            end;

          end;

            suppose

             D2: m = ( - 1);

            per cases ;

              suppose

               XD3: n = ( - 2);

              reconsider t = (1 / 3) as Element of ZS by RAT_1:def 1;

              t in ( Lin {s}) by AS;

              then

              consider l be Linear_Combination of {s} such that

               P3: t = ( Sum l) by ZMODUL02: 64;

              

               P4: ( Sum l) = ((l . s) * s) by ZMODUL02: 21;

              reconsider k = (l . s) as Integer;

              

               P5: (1 / 3) = (k * (m / n)) by P2, P3, P4, LMTFRat2

              .= ( - (k / n)) by D2;

              k = ((k / n) * n) by P2, XCMPLX_1: 87

              .= (2 / 3) by P5, XD3;

              hence contradiction by NAT_D: 33;

            end;

              suppose

               XD2: n <> ( - 2);

              reconsider t = (( - 1) / (n + 1)) as Element of ZS by RAT_1:def 1;

              t in ( Lin {s}) by AS;

              then

              consider l be Linear_Combination of {s} such that

               P3: t = ( Sum l) by ZMODUL02: 64;

              

               P4: ( Sum l) = ((l . s) * s) by ZMODUL02: 21;

              reconsider k = (l . s) as Integer;

              (( - 1) / (n + 1)) = (k * (m / n)) by P2, P3, P4, LMTFRat2

              .= ( - (k / n)) by D2;

              then k = (n / (n + 1)) by P2, XCMPLX_1: 87;

              hence contradiction by LMThFRat31X, N0, P2, XD2;

            end;

          end;

        end;

          suppose

           C2: m <> 1 & m <> ( - 1);

          reconsider t = ((m + 1) / n) as Element of ZS by RAT_1:def 1;

          t in ( Lin {s}) by AS;

          then

          consider l be Linear_Combination of {s} such that

           P3: t = ( Sum l) by ZMODUL02: 64;

          

           P4: ( Sum l) = ((l . s) * s) by ZMODUL02: 21;

          reconsider k = (l . s) as Integer;

          

           P5: ((m + 1) / n) = (k * (m / n)) by P2, P3, P4, LMTFRat2;

          (m + 1) = (((m + 1) / n) * n) by P2, XCMPLX_1: 87

          .= (k * ((m / n) * n)) by P5

          .= (k * m) by P2, XCMPLX_1: 87;

          then (m * (k - 1)) = 1;

          hence contradiction by C2, INT_1: 9;

        end;

      end;

    end;

    theorem :: ZMODUL07:17

    

     LMThFRat32: for s,t be Element of Rat-Module st s <> t holds not {s, t} is linearly-independent

    proof

      set ZS = Rat-Module ;

      let s,t be Element of ZS;

      assume

       AS: s <> t;

      assume

       P1: {s, t} is linearly-independent;

      consider m,n be Integer such that

       P2: n <> 0 & s = (m / n) by RAT_1: 1;

      consider p,q be Integer such that

       P3: q <> 0 & t = (p / q) by RAT_1: 1;

      reconsider b = (n * p) as Element of INT.Ring by INT_1:def 2;

      reconsider a = (q * m) as Element of INT.Ring by INT_1:def 2;

      

       P4: p <> ( 0. INT.Ring ) by AS, P1, P3, ZMODUL02: 62;

      (b * s) = ((n * p) * (m / n)) by LMTFRat2, P2

      .= (p * m) by P2, XCMPLX_1: 90

      .= ((q * m) * (p / q)) by P3, XCMPLX_1: 90

      .= (a * t) by LMTFRat2, P3;

      hence contradiction by AS, P1, P2, P4, ZMODUL02: 62;

    end;

    registration

      cluster Rat-Module -> non free;

      correctness

      proof

        set ZS = Rat-Module ;

        assume ZS is free;

        then

        consider A be Subset of ZS such that

         p1: A is base;

        per cases ;

          suppose

           P2: not (ex s,t be Element of ZS st s in A & t in A & s <> t);

          A <> {}

          proof

            assume A = {} ;

            then A = ( {} the carrier of ZS);

            then ( Lin A) = ( (0). ZS) by ZMODUL02: 67;

            hence contradiction by p1;

          end;

          then

          consider s be object such that

           P21: s in A by XBOOLE_0:def 1;

          reconsider s as Element of ZS by P21;

          

           P23: {s} c= A by ZFMISC_1: 31, P21;

          now

            let z be object;

            assume

             P22: z in A;

            then

            reconsider z0 = z as Element of ZS;

            z0 = s by P21, P22, P2;

            hence z in {s} by TARSKI:def 1;

          end;

          then A c= {s};

          then A = {s} by P23, XBOOLE_0:def 10;

          hence contradiction by p1, LMThFRat31;

        end;

          suppose ex s,t be Element of ZS st s in A & t in A & s <> t;

          then

          consider s,t be Element of ZS such that

           P4: s in A & t in A & s <> t;

           {s, t} c= A by ZFMISC_1: 32, P4;

          hence contradiction by p1, P4, LMThFRat32, ZMODUL02: 56;

        end;

      end;

    end

    theorem :: ZMODUL07:18

    for A be finite Subset of Rat-Module holds ex n be Integer st n <> 0 & for s be Element of Rat-Module st s in ( Lin A) holds ex m be Integer st s = (m / n)

    proof

      set ZS = Rat-Module ;

      defpred P[ Nat] means for A be finite Subset of ZS st ( card A) = $1 holds ex n be Integer st n <> 0 & for s be Element of ZS st s in ( Lin A) holds ex m be Integer st s = (m / n);

      

       P0: P[ 0 ]

      proof

        let A be finite Subset of ZS;

        assume ( card A) = 0 ;

        then

         P2: A = ( {} the carrier of ZS);

        

         P3: the carrier of ( (0). ZS) = {( 0. ZS)} by VECTSP_4:def 3;

        reconsider n = 1 as Integer;

        take n;

        thus n <> 0 ;

        let s be Element of ZS;

        assume s in ( Lin A);

        then

         P4: s in ( (0). ZS) by P2, ZMODUL02: 67;

        reconsider m = 0 as Integer;

        take m;

        thus s = (m / n) by P3, P4, TARSKI:def 1;

      end;

      

       P1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         P11: P[k];

        let A be finite Subset of ZS;

        assume

         B3: ( card A) = (k + 1);

        then A <> {} ;

        then

        consider v be object such that

         B4: v in A by XBOOLE_0: 7;

        reconsider v as VECTOR of ZS by B4;

        set Av = (A \ {v});

        

         B6: {v} is Subset of A by B4, SUBSET_1: 41;

        

        then ( card Av) = ((k + 1) - ( card {v})) by B3, CARD_2: 44

        .= ((k + 1) - 1) by CARD_1: 30

        .= k;

        then

        consider nk be Integer such that

         B8: nk <> 0 & for s be Element of ZS st s in ( Lin Av) holds ex mk be Integer st s = (mk / nk) by P11;

        consider mv,nv be Integer such that

         B9: nv <> 0 & v = (mv / nv) by RAT_1: 1;

        reconsider n = (nk * nv) as Integer;

        take n;

        thus n <> 0 by B8, B9;

        A = (Av \/ {v}) by B6, XBOOLE_1: 45;

        then

         B11: ( Lin A) = (( Lin Av) + ( Lin {v})) by ZMODUL02: 72;

        let s be Element of ZS;

        assume s in ( Lin A);

        then

        consider sk,sv be VECTOR of ZS such that

         B12: sk in ( Lin Av) & sv in ( Lin {v}) & s = (sk + sv) by ZMODUL01: 92, B11;

        consider mk be Integer such that

         B13: sk = (mk / nk) by B8, B12;

        consider l be Linear_Combination of {v} such that

         B14: sv = ( Sum l) by B12, ZMODUL02: 64;

        

         B15: ( Sum l) = ((l . v) * v) by ZMODUL02: 21;

        reconsider k = (l . v) as Integer;

        

         B16: sv = (k * (mv / nv)) by B9, B14, B15, LMTFRat2;

        reconsider m = ((mk * nv) + ((k * mv) * nk)) as Integer;

        take m;

        reconsider s1 = (mk / nk) as Rational;

        reconsider ss1 = s1 as Element of F_Rat by RAT_1:def 1;

        reconsider mn = (mv / nv) as Rational;

        reconsider s2 = (k * mn) as Rational;

        reconsider ss2 = s2 as Element of F_Rat by RAT_1:def 2;

        reconsider sss1 = ss1, sss2 = ss2 as Element of F_Real by TARSKI:def 3, GAUSSINT: 13;

        

         XX1: (ss1 + ss2) = (sss1 + sss2)

        .= ((mk / nk) + (k * (mv / nv)));

        

        thus s = (((mk * nv) / (nk * nv)) + ((k * mv) / nv)) by B9, B12, B13, B16, XX1, XCMPLX_1: 91

        .= (((mk * nv) / (nk * nv)) + (((k * mv) * nk) / (nv * nk))) by B8, XCMPLX_1: 91

        .= (m / n);

      end;

      

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

      let A be finite Subset of ZS;

      ( card A) is Nat;

      hence ex n be Integer st n <> 0 & for s be Element of ZS st s in ( Lin A) holds ex m be Integer st s = (m / n) by P2;

    end;

    registration

      cluster Rat-Module -> non finitely-generated;

      correctness ;

    end

    theorem :: ZMODUL07:19

    for A be finite Subset of Rat-Module holds ( rank ( Lin A)) <= 1

    proof

      set ZS = Rat-Module ;

      defpred P[ Nat] means for A be finite Subset of ZS st ( card A) = $1 holds ( rank ( Lin A)) <= 1;

      

       A1: P[ 0 ]

      proof

        let A be finite Subset of ZS such that

         B1: ( card A) = 0 ;

        A = ( {} the carrier of ZS) by B1;

        

        then ( Lin A) = ( (0). ZS) by ZMODUL02: 67

        .= ( (0). ( Lin A)) by ZMODUL01: 51;

        then ( (Omega). ( Lin A)) = ( (0). ( Lin A));

        hence thesis by ZMODUL05: 1;

      end;

      

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

      proof

        let n be Nat such that

         B1: P[n];

        let A be finite Subset of ZS such that

         B2: ( card A) = (n + 1);

        A <> {} by B2;

        then

        consider x be object such that

         B3: x in A by XBOOLE_0: 7;

        reconsider x as VECTOR of ZS by B3;

        

         B5: ( card (A \ {x})) = (( card A) - ( card {x})) by B3, ZFMISC_1: 31, CARD_2: 44

        .= ((n + 1) - 1) by B2, CARD_1: 30

        .= n;

        

         B6: (( Lin (A \ {x})) + ( Lin {x})) = ( Lin ((A \ {x}) \/ {x})) by ZMODUL02: 72

        .= ( Lin (A \/ {x})) by XBOOLE_1: 39

        .= ( Lin A) by B3, ZFMISC_1: 40;

        per cases by B1, B5, NAT_1: 25;

          suppose ( rank ( Lin (A \ {x}))) = 0 ;

          

          then

           C2: ( (Omega). ( Lin (A \ {x}))) = ( (0). ( Lin (A \ {x}))) by ZMODUL05: 1

          .= ( (0). ZS) by ZMODUL01: 51;

          per cases ;

            suppose x = ( 0. ZS);

            then ( Lin {x}) = ( (0). ZS) by ZMODUL06: 22;

            then (( Lin (A \ {x})) + ( Lin {x})) = ( (0). ZS) by C2, ZMODUL01: 99;

            then ( (Omega). ( Lin A)) = ( (0). ( Lin A)) by B6, ZMODUL01: 51;

            hence thesis by ZMODUL05: 1;

          end;

            suppose

             D1: x <> ( 0. ZS);

            reconsider Linx = ( Lin {x}) as free Submodule of ZS;

            x in ( Lin A) by B3, ZMODUL02: 65;

            then

            reconsider xx = x as VECTOR of ( Lin A);

            ( Lin A) = ( Lin {x}) by B6, C2, ZMODUL01: 99

            .= ( Lin {xx}) by ZMODUL03: 20;

            then

             D3: ( (Omega). ( Lin A)) = ( Lin {xx});

            xx <> ( 0. ( Lin A)) by D1, ZMODUL01: 26;

            hence thesis by D3, ZMODUL05: 5;

          end;

        end;

          suppose ( rank ( Lin (A \ {x}))) = 1;

          then

          consider axl be VECTOR of ( Lin (A \ {x})) such that

           C2: axl <> ( 0. ( Lin (A \ {x}))) & ( (Omega). ( Lin (A \ {x}))) = ( Lin {axl}) by ZMODUL05: 5;

          reconsider ax = axl as VECTOR of ZS by ZMODUL01: 25;

          

           C3: ax <> ( 0. ZS) by C2, ZMODUL01: 26;

          

           C4: ( Lin (A \ {x})) = ( Lin {ax}) by C2, ZMODUL03: 20;

          

           C5: {ax} is linearly-independent by C3, ZMODUL02: 59;

          per cases ;

            suppose x = ( 0. ZS);

            then ( Lin {x}) = ( (0). ZS) by ZMODUL06: 22;

            then (( Lin (A \ {x})) + ( Lin {x})) = ( Lin (A \ {x})) by ZMODUL01: 99;

            hence thesis by B1, B5, B6;

          end;

            suppose x = ax;

            then (( Lin (A \ {x})) + ( Lin {x})) = ( Lin (A \ {x})) by C4, ZMODUL01: 95;

            hence thesis by B1, B5, B6;

          end;

            suppose

             D1: x <> ( 0. ZS) & x <> ax;

            then

             D2: {x} is linearly-independent by ZMODUL02: 59;

             {ax, x} is linearly-dependent by D1, LMThFRat32;

            then

             D3: ( {ax} \/ {x}) is linearly-dependent by ENUMSET1: 1;

            ( {ax} /\ {x}) = {} by D1, XBOOLE_0:def 7, ZFMISC_1: 11;

            then

             D4: (( Lin {ax}) /\ ( Lin {x})) <> ( (0). ZS) by C5, D2, D3, ZMODUL06: 23;

            consider y be VECTOR of ZS such that

             D5: y <> ( 0. ZS) & (( Lin {ax}) + ( Lin {x})) = ( Lin {y}) by C3, D1, D4, ZMODUL06: 28;

            

             D6: y <> ( 0. ( Lin A)) by D5, ZMODUL01: 26;

            y in ( Lin A) by B6, C4, D5, ZMODUL06: 20;

            then

            reconsider yy = y as VECTOR of ( Lin A);

            ( (Omega). ( Lin A)) = ( Lin {yy}) by B6, C4, D5, ZMODUL03: 20;

            hence thesis by D6, ZMODUL05: 5;

          end;

        end;

      end;

      

       A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      let A be finite Subset of ZS;

      set n = ( card A);

       P[n] by A3;

      hence thesis;

    end;

    begin

    reserve V,W for finite-rank free Z_Module;

    reserve T for linear-transformation of V, W;

    registration

      let W be finite-rank free Z_Module, V be Z_Module;

      let T be linear-transformation of V, W;

      cluster ( im T) -> finite-rank free;

      correctness ;

    end

    definition

      let W be finite-rank free Z_Module;

      let V be Z_Module;

      let T be linear-transformation of V, W;

      :: ZMODUL07:def4

      func rank (T) -> Nat equals ( rank ( im T));

      coherence ;

    end

    definition

      let V be finite-rank free Z_Module;

      let W be Z_Module;

      let T be linear-transformation of V, W;

      :: ZMODUL07:def5

      func nullity (T) -> Nat equals ( rank ( ker T));

      coherence ;

    end

    theorem :: ZMODUL07:20

    

     ZM05Th35: for V be finite-rank free Z_Module, A be Subset of V, B be linearly-independent Subset of V, T be linear-transformation of V, W st ( rank V) = ( card B) & A is Basis of ( ker T) & A c= B holds (T | (B \ A)) is one-to-one

    proof

      let V be finite-rank free Z_Module, A be Subset of V, B be linearly-independent Subset of V, T be linear-transformation of V, W such that ( rank V) = ( card B) and

       A1: A is Basis of ( ker T) and

       A2: A c= B;

      reconsider A9 = A as Subset of V;

      set f = (T | (B \ A));

      let x1,x2 be object such that

       A3: x1 in ( dom f) and

       A4: x2 in ( dom f) and

       A5: (f . x1) = (f . x2) and

       A6: x1 <> x2;

      x2 in ( dom T) by A4, RELAT_1: 57;

      then

      reconsider x2 as Element of V;

      x1 in ( dom T) by A3, RELAT_1: 57;

      then

      reconsider x1 as Element of V;

      

       A7: not x1 in (A9 \/ {x2})

      proof

        assume

         A8: x1 in (A9 \/ {x2});

        per cases by A8, XBOOLE_0:def 3;

          suppose x1 in A9;

          hence contradiction by A3, XBOOLE_0:def 5;

        end;

          suppose x1 in {x2};

          hence contradiction by A6, TARSKI:def 1;

        end;

      end;

      

       A9: (f . x2) = (T . x2) by A4, FUNCT_1: 49;

      reconsider A as Subset of ( ker T) by A1;

      reconsider A as Basis of ( ker T) by A1;

      

       A10: ( ker T) = ( Lin A) by VECTSP_7:def 3;

      (f . x1) = (T . x1) by A3, FUNCT_1: 49;

      then (x1 - x2) in ( ker T) by A5, A9, ZMODUL05: 27;

      then (x1 - x2) in ( Lin A9) by A10, ZMODUL03: 20;

      then

       A11: x1 in ( Lin (A9 \/ {x2})) by ZMODUL05: 28;

      ( {x2} \/ {x1}) = {x1, x2} by ENUMSET1: 1;

      then

       A12: ((A9 \/ {x2}) \/ {x1}) = (A9 \/ {x1, x2}) by XBOOLE_1: 4;

       {x1, x2} c= B

      proof

        let z be object such that

         A13: z in {x1, x2};

        per cases by A13, TARSKI:def 2;

          suppose z = x1;

          hence thesis by A3, XBOOLE_0:def 5;

        end;

          suppose z = x2;

          hence thesis by A4, XBOOLE_0:def 5;

        end;

      end;

      then (A9 \/ {x1, x2}) c= B by A2, XBOOLE_1: 8;

      hence thesis by A7, A11, A12, ZMODUL02: 56, ZMODUL05: 32;

    end;

    theorem :: ZMODUL07:21

    

     ZM05Th59: for V be finite-rank free Z_Module, A be Subset of V, B be linearly-independent Subset of V, T be linear-transformation of V, W, l be Linear_Combination of (B \ A) st ( rank V) = ( card B) & A is Basis of ( ker T) & A c= B holds (T . ( Sum l)) = ( Sum (T @* l))

    proof

      let V be finite-rank free Z_Module, A be Subset of V, B be linearly-independent Subset of V, T be linear-transformation of V, W, l be Linear_Combination of (B \ A);

      assume ( rank V) = ( card B) & A is Basis of ( ker T) & A c= B;

      then

       A1: (T | (B \ A)) is one-to-one by ZM05Th35;

      

       A2: ((T | (B \ A)) | ( Carrier l)) = (T | ( Carrier l)) by RELAT_1: 74, VECTSP_6:def 4;

      then

       A3: (T | ( Carrier l)) is one-to-one by A1, FUNCT_1: 52;

      consider G be FinSequence of V such that

       A4: G is one-to-one and

       A5: ( rng G) = ( Carrier l) and

       A6: ( Sum l) = ( Sum (l (#) G)) by VECTSP_6:def 6;

      set H = (T * G);

      reconsider H as FinSequence of W;

      

       A7: ( rng H) = (T .: ( Carrier l)) by A5, RELAT_1: 127

      .= ( Carrier (T @* l)) by A3, ZMODUL05: 56;

      ( dom T) = ( [#] V) by LmDOMRNG;

      then H is one-to-one by A1, A2, A4, A5, FUNCT_1: 52, RANKNULL: 1;

      then

       A8: ( Sum (T @* l)) = ( Sum ((T @* l) (#) H)) by A7, VECTSP_6:def 6;

      (T * (l (#) G)) = ((T @* l) (#) H) by A3, A5, ZMODUL05: 55;

      hence thesis by A6, A8, ZMODUL05: 16;

    end;

    theorem :: ZMODUL07:22

    

     LMTh441: for R be Ring holds for V,W be LeftMod of R, T be linear-transformation of V, W, A be Subset of V st A c= the carrier of ( ker T) holds ( Lin (T .: A)) = ( (0). W)

    proof

      let R be Ring;

      let V,W be LeftMod of R, T be linear-transformation of V, W, A be Subset of V;

      assume

       A1: A c= the carrier of ( ker T);

      per cases ;

        suppose A = {} ;

        then (T .: A) = ( {} the carrier of W);

        hence ( Lin (T .: A)) = ( (0). W) by MOD_3: 6;

      end;

        suppose A <> {} ;

        then

        consider a be object such that

         A6: a in A by XBOOLE_0:def 1;

        

         A8: a in ( ker T) by A1, A6;

        reconsider a as Vector of V by A6;

        

         A9: (T . a) = ( 0. W) by A8, RANKNULL: 10;

        for x be object holds x in (T .: A) iff x in {( 0. W)}

        proof

          let x be object;

          hereby

            assume x in (T .: A);

            then

            consider z be Element of V such that

             A4: z in A & x = (T . z) by FUNCT_2: 65;

            z in ( ker T) by A1, A4;

            then (T . z) = ( 0. W) by RANKNULL: 10;

            hence x in {( 0. W)} by TARSKI:def 1, A4;

          end;

          assume x in {( 0. W)};

          then x = (T . a) by A9, TARSKI:def 1;

          hence x in (T .: A) by FUNCT_2: 35, A6;

        end;

        then (T .: A) = {( 0. W)} by TARSKI: 2;

        hence ( Lin (T .: A)) = ( (0). W) by ZMODUL06: 22;

      end;

    end;

    theorem :: ZMODUL07:23

    

     LMTh44: for R be Ring holds for V,W be LeftMod of R, T be linear-transformation of V, W, A,B,X be Subset of V st A c= the carrier of ( ker T) & X = (B \/ A) holds ( Lin (T .: X)) = ( Lin (T .: B))

    proof

      let R be Ring;

      let V,W be LeftMod of R, T be linear-transformation of V, W, A,B,X be Subset of V;

      assume that

       A1: A c= the carrier of ( ker T) and

       A2: X = (B \/ A);

      

       P1: (T .: X) = ((T .: B) \/ (T .: A)) by A2, RELAT_1: 120;

      

      thus ( Lin (T .: X)) = (( Lin (T .: B)) + ( Lin (T .: A))) by P1, MOD_3: 12

      .= (( Lin (T .: B)) + ( (0). W)) by LMTh441, A1

      .= ( Lin (T .: B)) by VECTSP_5: 9;

    end;

    theorem :: ZMODUL07:24

    

     Th44: for V,W be finite-rank free Z_Module, T be linear-transformation of V, W holds ( rank V) = (( rank T) + ( nullity T))

    proof

      let V,W be finite-rank free Z_Module, T be linear-transformation of V, W;

      set A = the finite Basis of ( ker T);

      reconsider A9 = A as Subset of V by ZMODUL05: 29;

      reconsider A9 as finite linearly-independent Subset of V by VECTSP_7:def 3, ZMODUL03: 15;

      consider B9 be finite linearly-independent Subset of V, a be Element of INT.Ring such that

       A1: a <> ( 0. INT.Ring ) & A9 c= B9 & (a (*) V) is Submodule of ( Lin B9) by LmRankSX11;

      

       X1: V is finite-rank free Submodule of V by ZMODUL01: 32;

      ( rank (a (*) V)) <= ( rank ( Lin B9)) by A1, ZMODUL05: 2;

      then

       X2: ( rank V) <= ( rank ( Lin B9)) by A1, X1, ZMODUL06: 52;

      ( rank ( Lin B9)) <= ( rank V) by ZMODUL05: 2;

      then ( rank ( Lin B9)) = ( rank V) by X2, XXREAL_0: 1;

      then

       X0: ( rank V) = ( card B9) by ZMODUL05: 3;

      reconsider X = (B9 \ A9) as finite Subset of B9 by XBOOLE_1: 36;

      reconsider X as finite Subset of V;

      

       A2: B9 = (A9 \/ X) by A1, XBOOLE_1: 45;

      reconsider C = (T .: X) as finite Subset of W;

      

       A3: (T | X) is one-to-one by A1, X0, ZM05Th35;

      C is linearly-independent

      proof

        assume C is linearly-dependent;

        then

        consider l be Linear_Combination of C such that

         A5: ( Carrier l) <> {} and

         A6: ( Sum l) = ( 0. W);

        ex m be Linear_Combination of X st l = (T @* m)

        proof

          reconsider l9 = l as Linear_Combination of (T .: X);

          set m = (T # l9);

          take m;

          thus thesis by A3, ZMODUL05: 60;

        end;

        then

        consider m be Linear_Combination of (B9 \ A9) such that

         A7: l = (T @* m);

        (T . ( Sum m)) = ( 0. W) by A1, A6, A7, X0, ZM05Th59;

        then ( Sum m) in ( ker T) by ZMODUL05: 20;

        then ( Sum m) in ( Lin A) by VECTSP_7:def 3;

        then ( Sum m) in ( Lin A9) by ZMODUL03: 20;

        then

        consider n be Linear_Combination of A9 such that

         A8: ( Sum m) = ( Sum n) by ZMODUL02: 64;

        

         A9: ( Carrier (m - n)) c= (( Carrier m) \/ ( Carrier n)) & ((B9 \ A9) \/ A9) = B9 by A1, ZMODUL02: 40, XBOOLE_1: 45;

        

         A10: ( Carrier m) c= (B9 \ A9) & ( Carrier n) c= A by VECTSP_6:def 4;

        then (( Carrier m) \/ ( Carrier n)) c= ((B9 \ A9) \/ A) by XBOOLE_1: 13;

        then ( Carrier (m - n)) c= B9 by A9;

        then

        reconsider o = (m - n) as Linear_Combination of B9 by VECTSP_6:def 4;

        (( Sum m) - ( Sum n)) = ( 0. V) by A8, VECTSP_1: 19;

        then ( Sum (m - n)) = ( 0. V) by ZMODUL02: 55;

        then

         A12: ( Carrier o) = {} by VECTSP_7:def 1;

        A9 misses (B9 \ A9) by XBOOLE_1: 79;

        then ( Carrier (m - n)) = (( Carrier m) \/ ( Carrier n)) by A10, XBOOLE_1: 64, ZMODUL05: 48;

        then ( Carrier m) = {} by A12;

        then (T .: ( Carrier m)) = {} ;

        hence thesis by A5, A7, XBOOLE_1: 3, ZMODUL05:def 8;

      end;

      then

      reconsider C as finite linearly-independent Subset of W;

      ( dom T) = ( [#] V) by LmDOMRNG;

      then X c= ( dom (T | X)) by RELAT_1: 62;

      then (X,((T | X) .: X)) are_equipotent by A3, CARD_1: 33;

      then (X,C) are_equipotent by RELAT_1: 129;

      then

       A13: ( card C) = ( card X) by CARD_1: 5;

      reconsider aT = (a (*) ( im T)) as Submodule of W by ZMODUL01: 42;

      

       L1: ( Lin (T .: B9)) = ( Lin (T .: X)) by A2, LMTh44;

      for v be VECTOR of W st v in aT holds v in ( Lin C)

      proof

        let v be VECTOR of W;

        assume v in aT;

        then

        consider tw be VECTOR of ( im T) such that

         X1: v = (a * tw);

        tw is VECTOR of W & tw in ( im T) by ZMODUL01: 25;

        then

        consider w be VECTOR of V such that

         X2: tw = (T . w) by ZMODUL05: 23;

        

         X3: v = (a * (T . w)) by X1, X2, ZMODUL01: 29

        .= (T . (a * w)) by MOD_2:def 2;

        (a * w) in (a * V);

        then

        reconsider aw = (a * w) as VECTOR of (a (*) V);

        aw in (a (*) V);

        then aw in ( Lin B9) by A1, ZMODUL01: 24;

        then (T . aw) in (T .: the carrier of ( Lin B9)) by FUNCT_2: 35;

        hence v in ( Lin C) by L1, X3, TARSKI:def 3, ZMODUL06: 40;

      end;

      then (a (*) ( im T)) is Submodule of ( Lin C) by ZMODUL01: 44;

      then ( rank (a (*) ( im T))) <= ( rank ( Lin C)) by ZMODUL05: 2;

      then

       X4: ( rank ( im T)) <= ( rank ( Lin C)) by A1, ZMODUL06: 52;

      reconsider CC = C as Subset of ( im T) by ZMODUL05: 22;

      ( Lin CC) is Submodule of ( im T);

      then ( Lin C) is Submodule of ( im T) by ZMODUL03: 20;

      then ( rank ( Lin C)) <= ( rank ( im T)) by ZMODUL05: 2;

      

      then

       X5: ( rank T) = ( rank ( Lin C)) by X4, XXREAL_0: 1

      .= ( card C) by ZMODUL05: 3;

      ( nullity T) = ( card A) by ZMODUL03:def 5;

      hence thesis by A2, A13, X0, X5, CARD_2: 40, XBOOLE_1: 79;

    end;

    theorem :: ZMODUL07:25

    for V,W be finite-rank free Z_Module, T be linear-transformation of V, W st T is one-to-one holds ( rank V) = ( rank T)

    proof

      let V,W be finite-rank free Z_Module, T be linear-transformation of V, W;

      assume T is one-to-one;

      then ( ker T) = ( (0). V) by ZMODUL05: 25;

      then

       A1: ( nullity T) = 0 by ZMODUL05: 26;

      ( rank V) = (( rank T) + ( nullity T)) by Th44

      .= ( rank T) by A1;

      hence thesis;

    end;

    definition

      let R be Ring;

      let V,W be LeftMod of R;

      let T be linear-transformation of V, W;

      :: ZMODUL07:def6

      func Zdecom (T) -> linear-transformation of ( VectQuot (V,( ker T))), ( im T) means

      : defdecom: it is bijective & for v be Element of V holds (it . (( ZQMorph (V,( ker T))) . v)) = (T . v);

      existence

      proof

        set KT = ( ker T);

        

         XX: T is additive & T is homogeneous;

        

         YY: ( rng ( ZQMorph (V,KT))) = the carrier of ( VectQuot (V,KT)) by FUNCT_2:def 3;

        defpred P[ object, object] means ex v be Element of V st $1 = (( ZQMorph (V,KT)) . v) & $2 = (T . v);

        

         A11: for z be Element of ( VectQuot (V,KT)) holds ex y be Element of ( im T) st P[z, y]

        proof

          let z be Element of ( VectQuot (V,KT));

          consider v be Element of V such that

           A12: z = (( ZQMorph (V,KT)) . v) by FUNCT_2: 113, YY;

          set y = (T . v);

          ( dom T) = ( [#] V) by LmDOMRNG;

          then y in (T .: ( [#] V)) by FUNCT_1:def 6;

          then y in ( [#] ( im T)) by RANKNULL:def 2;

          then

          reconsider y = (T . v) as Element of ( im T);

          take y;

          thus thesis by A12;

        end;

        consider f be Function of the carrier of ( VectQuot (V,KT)), the carrier of ( im T) such that

         A15: for z be Element of ( VectQuot (V,KT)) holds P[z, (f . z)] from FUNCT_2:sch 3( A11);

        

         A16: for v be Element of V holds (f . (( ZQMorph (V,KT)) . v)) = (T . v)

        proof

          let v1 be Element of V;

          set z = (( ZQMorph (V,KT)) . v1);

          reconsider z as Element of ( VectQuot (V,KT));

          consider v2 be Element of V such that

           Q1: z = (( ZQMorph (V,KT)) . v2) & (f . z) = (T . v2) by A15;

          (( ZQMorph (V,KT)) . v1) = (v1 + KT) by defMophVW;

          then

           Q3: (v1 + KT) = (v2 + KT) by Q1, defMophVW;

          

           Q4: v1 in (v1 + KT) by VECTSP_4: 44;

          

           A23: v2 in (v1 + KT) by Q3, VECTSP_4: 44;

          ((T . v1) - (T . v2)) = (T . (v1 - v2)) by ZMODUL05: 18

          .= ( 0. W) by A23, Q4, VECTSP_4: 63, RANKNULL: 10;

          hence thesis by Q1, RLVECT_1: 21;

        end;

        for x,y be Vector of ( VectQuot (V,( ker T))) holds (f . (x + y)) = ((f . x) + (f . y))

        proof

          let x,y be Vector of ( VectQuot (V,KT));

          consider v be Element of V such that

           A17: x = (( ZQMorph (V,KT)) . v) by FUNCT_2: 113, YY;

          consider w be Element of V such that

           A18: y = (( ZQMorph (V,KT)) . w) by FUNCT_2: 113, YY;

          

           A19: (( ZQMorph (V,KT)) . v) = (v + KT) by defMophVW;

          

           A20: (( ZQMorph (V,KT)) . w) = (w + KT) by defMophVW;

          reconsider A = (v + KT) as Element of ( CosetSet (V,KT)) by A19, VECTSP10:def 6;

          reconsider B = (w + KT) as Element of ( CosetSet (V,KT)) by A20, VECTSP10:def 6;

          (x + y) = (( addCoset (V,KT)) . (A,B)) by A17, A18, A19, A20, VECTSP10:def 6

          .= ((v + w) + KT) by VECTSP10:def 3;

          then

           A22: (x + y) = (( ZQMorph (V,KT)) . (v + w)) by defMophVW;

          

           A23: (T . v) = (f . x) by A16, A17;

          

           A24: (T . w) = (f . y) by A16, A18;

          

          thus (f . (x + y)) = (T . (v + w)) by A16, A22

          .= ((T . v) + (T . w)) by XX

          .= ((f . x) + (f . y)) by A23, A24, VECTSP_4: 13;

        end;

        then

         A25: f is additive;

        for a be Element of R, x be Element of ( VectQuot (V,KT)) holds (f . (a * x)) = (a * (f . x))

        proof

          let a be Element of R, x be Element of ( VectQuot (V,KT));

          consider v be Element of V such that

           A2: x = (( ZQMorph (V,KT)) . v) & (f . x) = (T . v) by A15;

          (( ZQMorph (V,KT)) . (a * v)) = (a * x) by A2, MOD_2:def 2;

          

          hence (f . (a * x)) = (T . (a * v)) by A16

          .= (a * (T . v)) by XX

          .= (a * (f . x)) by A2, VECTSP_4: 14;

        end;

        then

         A17: f is homogeneous;

        for y be object st y in the carrier of ( im T) holds ex x be object st x in the carrier of ( VectQuot (V,KT)) & y = (f . x)

        proof

          let y be object;

          assume

           LA0: y in the carrier of ( im T);

          the carrier of ( im T) c= the carrier of W by VECTSP_4:def 2;

          then

          reconsider y0 = y as Element of W by LA0;

          y0 in ( im T) by LA0;

          then

          consider v be Element of V such that

           LA1: y0 = (T . v) by RANKNULL: 13;

          (f . (( ZQMorph (V,KT)) . v)) = y by A16, LA1;

          hence thesis;

        end;

        then ( rng f) = the carrier of ( im T) by FUNCT_2: 10;

        then

         A18: f is onto by FUNCT_2:def 3;

        for x1,x2 be object st x1 in the carrier of ( VectQuot (V,KT)) & x2 in the carrier of ( VectQuot (V,KT)) & (f . x1) = (f . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume

           A19: x1 in the carrier of ( VectQuot (V,KT)) & x2 in the carrier of ( VectQuot (V,KT)) & (f . x1) = (f . x2);

          reconsider xx1 = x1 as Element of ( VectQuot (V,KT)) by A19;

          reconsider xx2 = x2 as Element of ( VectQuot (V,KT)) by A19;

          consider v1 be Element of V such that

           A20: xx1 = (( ZQMorph (V,KT)) . v1) & (f . xx1) = (T . v1) by A15;

          consider v2 be Element of V such that

           A21: xx2 = (( ZQMorph (V,KT)) . v2) & (f . xx2) = (T . v2) by A15;

          

           A23: (v1 - v2) in ( ker T) by A19, A20, A21, RANKNULL: 17;

          

           A24: (( ZQMorph (V,KT)) . v1) = (v1 + KT) by defMophVW;

          

           A25: (( ZQMorph (V,KT)) . v2) = (v2 + KT) by defMophVW;

          ((v1 - v2) + v2) = (v1 - (v2 - v2)) by RLVECT_1: 29

          .= (v1 - ( 0. V)) by RLVECT_1: 15

          .= v1;

          then v1 in (v2 + KT) by A23;

          hence thesis by A24, A25, A21, A20, VECTSP_4: 55;

        end;

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

        hence thesis by A18, A16, A17, A25;

      end;

      uniqueness

      proof

        let f1,f2 be linear-transformation of ( VectQuot (V,( ker T))), ( im T);

        assume

         AS1: f1 is one-to-one & f1 is onto & for v be Element of V holds (f1 . (( ZQMorph (V,( ker T))) . v)) = (T . v);

        assume

         AS2: f2 is one-to-one & f2 is onto & for v be Element of V holds (f2 . (( ZQMorph (V,( ker T))) . v)) = (T . v);

        

         YY: ( rng ( ZQMorph (V,( ker T)))) = the carrier of ( VectQuot (V,( ker T))) by FUNCT_2:def 3;

        for v be Element of ( VectQuot (V,( ker T))) holds (f1 . v) = (f2 . v)

        proof

          let v be Element of ( VectQuot (V,( ker T)));

          consider z be Element of V such that

           A12: v = (( ZQMorph (V,( ker T))) . z) by FUNCT_2: 113, YY;

          

          thus (f1 . v) = (T . z) by A12, AS1

          .= (f2 . v) by A12, AS2;

        end;

        hence f1 = f2 by FUNCT_2:def 8;

      end;

    end

    theorem :: ZMODUL07:26

    for R be Ring holds for V,W be LeftMod of R, T be linear-transformation of V, W holds T = (( Zdecom T) * ( ZQMorph (V,( ker T))))

    proof

      let R be Ring;

      let V,W be LeftMod of R;

      let T be linear-transformation of V, W;

      set g = (( Zdecom T) * ( ZQMorph (V,( ker T))));

      

       A1: ( dom g) = the carrier of V by FUNCT_2:def 1;

      the carrier of ( im T) c= the carrier of W by VECTSP_4:def 2;

      then ( rng g) c= the carrier of W;

      then

      reconsider g as Function of V, W by FUNCT_2: 2, A1;

      for z be Element of V holds (T . z) = (g . z)

      proof

        let z be Element of V;

        

        thus (T . z) = (( Zdecom T) . (( ZQMorph (V,( ker T))) . z)) by defdecom

        .= (g . z) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2:def 8;

    end;

    theorem :: ZMODUL07:27

    

     LMFirst1: for R be Ring holds for V,U,W be LeftMod of R, f be linear-transformation of V, U, g be linear-transformation of U, W holds (g * f) is linear-transformation of V, W

    proof

      let R be Ring;

      let V,U,W be LeftMod of R, f be linear-transformation of V, U, g be linear-transformation of U, W;

      set gf = (g * f);

      for a be Element of R, x be Element of V holds (gf . (a * x)) = (a * (gf . x))

      proof

        let a be Element of R, x be Element of V;

        

         P3: f is homogeneous;

        

         P4: g is homogeneous;

        

        thus (gf . (a * x)) = (g . (f . (a * x))) by FUNCT_2: 15

        .= (g . (a * (f . x))) by P3

        .= (a * (g . (f . x))) by P4

        .= (a * (gf . x)) by FUNCT_2: 15;

      end;

      then gf is homogeneous;

      hence thesis;

    end;

    definition

      let R be Ring;

      let V,U,W be LeftMod of R, f be linear-transformation of V, U, g be linear-transformation of U, W;

      :: original: *

      redefine

      func g * f -> linear-transformation of V, W ;

      correctness by LMFirst1;

    end

    theorem :: ZMODUL07:28

    

     LMFirst2: for R be Ring holds for V,W be LeftMod of R, f be linear-transformation of V, W holds the carrier of ( ker f) = (f " {( 0. W)})

    proof

      let R be Ring;

      let V,W be LeftMod of R, f be linear-transformation of V, W;

      

       A0: ( [#] ( ker f)) = { u where u be Element of V : (f . u) = ( 0. W) } by RANKNULL:def 1;

      for x be object holds x in the carrier of ( ker f) iff x in (f " {( 0. W)})

      proof

        let x be object;

        hereby

          assume x in the carrier of ( ker f);

          then

          consider v be Vector of V such that

           A2: x = v & (f . v) = ( 0. W) by A0;

          (f . x) in {( 0. W)} by A2, TARSKI:def 1;

          hence x in (f " {( 0. W)}) by FUNCT_2: 38, A2;

        end;

        assume

         A11: x in (f " {( 0. W)});

        then

         A1: x in the carrier of V & (f . x) in {( 0. W)} by FUNCT_2: 38;

        reconsider v = x as Vector of V by A11;

        (f . v) = ( 0. W) by A1, TARSKI:def 1;

        hence x in the carrier of ( ker f) by A0;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ZMODUL07:29

    

     LMFirst3: for R be Ring holds for V,U,W be LeftMod of R, f be linear-transformation of V, U, g be linear-transformation of U, W holds the carrier of ( ker (g * f)) = (f " the carrier of ( ker g))

    proof

      let R be Ring;

      let V,U,W be LeftMod of R, f be linear-transformation of V, U, g be linear-transformation of U, W;

      

      thus the carrier of ( ker (g * f)) = ((g * f) " {( 0. W)}) by LMFirst2

      .= (f " (g " {( 0. W)})) by RELAT_1: 146

      .= (f " the carrier of ( ker g)) by LMFirst2;

    end;

    theorem :: ZMODUL07:30

    

     LMFirst4: for R be Ring holds for V,W be LeftMod of R, f be linear-transformation of V, W st f is onto holds ( im f) = ( (Omega). W)

    proof

      let R be Ring;

      let V,W be LeftMod of R, f be linear-transformation of V, W;

      assume f is onto;

      then

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

      

       B2: ( dom f) = the carrier of V by FUNCT_2:def 1;

      the carrier of ( im f) = ( [#] ( im f))

      .= (f .: ( [#] V)) by RANKNULL:def 2

      .= the carrier of ( (Omega). W) by B1, B2, RELAT_1: 113;

      hence thesis by VECTSP_4: 29;

    end;

    theorem :: ZMODUL07:31

    

     LMFirst5: for R be Ring holds for V be LeftMod of R, W be Subspace of V holds ( ker ( ZQMorph (V,W))) = ( (Omega). W)

    proof

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V;

      set f = ( ZQMorph (V,W));

      reconsider Ws = ( (Omega). W) as strict Subspace of V by VECTSP_4: 26;

      for x be object holds x in (f " {( 0. ( VectQuot (V,W)))}) iff x in the carrier of W

      proof

        let x be object;

        hereby

          assume

           A11: x in (f " {( 0. ( VectQuot (V,W)))});

          then

           A1: x in the carrier of V & (f . x) in {( 0. ( VectQuot (V,W)))} by FUNCT_2: 38;

          reconsider v = x as Vector of V by A11;

          (f . v) = ( 0. ( VectQuot (V,W))) by A1, TARSKI:def 1

          .= ( zeroCoset (V,W)) by VECTSP10:def 6

          .= the carrier of W;

          then (v + W) = the carrier of W by defMophVW;

          then v in W by VECTSP_4: 49;

          hence x in the carrier of W;

        end;

        assume

         B1: x in the carrier of W;

        

         B4: the carrier of W c= the carrier of V by VECTSP_4:def 2;

        then

        reconsider v = x as Vector of V by B1;

        

         B2: v in W by B1;

        (f . v) = (v + W) by defMophVW

        .= ( zeroCoset (V,W)) by B2, VECTSP_4: 49

        .= ( 0. ( VectQuot (V,W))) by VECTSP10:def 6;

        then (f . x) in {( 0. ( VectQuot (V,W)))} by TARSKI:def 1;

        hence x in (f " {( 0. ( VectQuot (V,W)))}) by B1, B4, FUNCT_2: 38;

      end;

      then (f " {( 0. ( VectQuot (V,W)))}) = the carrier of W by TARSKI: 2;

      then ( ker f) = Ws by LMFirst2, VECTSP_4: 29;

      hence thesis;

    end;

    theorem :: ZMODUL07:32

    

     LmStrict11a: for R be Ring holds for V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V, v be Vector of V st Ws = ( (Omega). W) holds (v + W) = (v + Ws)

    proof

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V, v be Vector of V such that

       A1: Ws = ( (Omega). W);

      for x be object holds x in (v + W) iff x in (v + Ws)

      proof

        let x be object;

        hereby

          assume

           B1: x in (v + W);

          then

          reconsider xx = x as Vector of V;

          consider u be Vector of V such that

           B2: xx = (v + u) & u in W by B1;

          u in Ws by A1, B2;

          hence x in (v + Ws) by B2;

        end;

        assume

         B1: x in (v + Ws);

        then

        reconsider xx = x as Vector of V;

        consider u be Vector of V such that

         B2: xx = (v + u) & u in Ws by B1;

        u in W by A1, B2;

        hence x in (v + W) by B2;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ZMODUL07:33

    

     LmStrict11: for R be Ring holds for V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V, A be object st Ws = ( (Omega). W) holds A is Coset of W iff A is Coset of Ws

    proof

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V, A be object such that

       A1: Ws = ( (Omega). W);

      hereby

        assume A is Coset of W;

        then

        consider v be Vector of V such that

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

        A = (v + Ws) by A1, B1, LmStrict11a;

        hence A is Coset of Ws by VECTSP_4:def 6;

      end;

      assume A is Coset of Ws;

      then

      consider v be Vector of V such that

       B1: A = (v + Ws) by VECTSP_4:def 6;

      A = (v + W) by A1, B1, LmStrict11a;

      hence A is Coset of W by VECTSP_4:def 6;

    end;

    theorem :: ZMODUL07:34

    

     LmStrict1: for R be Ring holds for V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V st Ws = ( (Omega). W) holds ( CosetSet (V,W)) = ( CosetSet (V,Ws))

    proof

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V such that

       A1: Ws = ( (Omega). W);

      for A be object holds A in ( CosetSet (V,W)) iff A in ( CosetSet (V,Ws))

      proof

        let A be object;

        hereby

          assume A in ( CosetSet (V,W));

          then

          consider AA be Coset of W such that

           C1: A = AA;

          AA is Coset of Ws by A1, LmStrict11;

          hence A in ( CosetSet (V,Ws)) by C1;

        end;

        assume A in ( CosetSet (V,Ws));

        then

        consider AA be Coset of Ws such that

         C1: A = AA;

        AA is Coset of W by A1, LmStrict11;

        hence A in ( CosetSet (V,W)) by C1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ZMODUL07:35

    

     LmStrict2: for R be Ring holds for V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V st Ws = ( (Omega). W) holds ( addCoset (V,W)) = ( addCoset (V,Ws))

    proof

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V;

      assume

       AS: Ws = ( (Omega). W);

      set f1 = ( addCoset (V,W));

      set f2 = ( addCoset (V,Ws));

      set C = ( CosetSet (V,W));

      set Cs = ( CosetSet (V,Ws));

      

       A14: ( CosetSet (V,W)) = ( CosetSet (V,Ws)) by AS, LmStrict1;

      now

        let A,B be Element of C;

        A in C;

        then

        consider A1 be Coset of W such that

         A17: A1 = A;

        consider a be Vector of V such that

         A18: A1 = (a + W) by VECTSP_4:def 6;

        B in C;

        then

        consider B1 be Coset of W such that

         A19: B1 = B;

        consider b be Vector of V such that

         A20: B1 = (b + W) by VECTSP_4:def 6;

        reconsider As = A as Element of Cs by AS, LmStrict1;

        

         A21: As = (a + Ws) by AS, A17, A18, LmStrict11a;

        reconsider Bs = B as Element of Cs by AS, LmStrict1;

        

         A22: Bs = (b + Ws) by AS, A19, A20, LmStrict11a;

        

        thus (f1 . (A,B)) = ((a + b) + W) by A17, A19, A18, A20, VECTSP10:def 3

        .= ((a + b) + Ws) by LmStrict11a, AS

        .= (f2 . (A,B)) by A21, A22, VECTSP10:def 3;

      end;

      hence thesis by A14, BINOP_1: 2;

    end;

    theorem :: ZMODUL07:36

    

     LmStrict3: for R be Ring holds for V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V st Ws = ( (Omega). W) holds ( lmultCoset (V,W)) = ( lmultCoset (V,Ws))

    proof

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V;

      assume

       AS: Ws = ( (Omega). W);

      set f1 = ( lmultCoset (V,W));

      set f2 = ( lmultCoset (V,Ws));

      set C = ( CosetSet (V,W));

      set Cs = ( CosetSet (V,Ws));

      

       A14: ( CosetSet (V,W)) = ( CosetSet (V,Ws)) by AS, LmStrict1;

      now

        let z be Element of R;

        let A be Element of C;

        A in C;

        then

        consider A1 be Coset of W such that

         A17: A1 = A;

        consider a be Vector of V such that

         A18: A1 = (a + W) by VECTSP_4:def 6;

        reconsider As = A as Element of Cs by AS, LmStrict1;

        

         A21: As = (a + Ws) by AS, A17, A18, LmStrict11a;

        

        thus (f1 . (z,A)) = ((z * a) + W) by A17, A18, VECTSP10:def 5

        .= ((z * a) + Ws) by LmStrict11a, AS

        .= (f2 . (z,A)) by A21, VECTSP10:def 5;

      end;

      hence thesis by A14, BINOP_1: 2;

    end;

    theorem :: ZMODUL07:37

    

     ThStrict1: for R be Ring holds for V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V st Ws = ( (Omega). W) holds ( VectQuot (V,W)) = ( VectQuot (V,Ws))

    proof

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V such that

       A1: Ws = ( (Omega). W);

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

      set Z2 = ( VectQuot (V,Ws));

      

       A2: the carrier of Z1 = ( CosetSet (V,W)) by VECTSP10:def 6

      .= ( CosetSet (V,Ws)) by A1, LmStrict1

      .= the carrier of Z2 by VECTSP10:def 6;

      

       A3: the addF of Z1 = ( addCoset (V,W)) by VECTSP10:def 6

      .= ( addCoset (V,Ws)) by A1, LmStrict2

      .= the addF of Z2 by VECTSP10:def 6;

      

       A4: ( 0. Z1) = ( zeroCoset (V,W)) by VECTSP10:def 6

      .= ( zeroCoset (V,Ws)) by A1

      .= ( 0. Z2) by VECTSP10:def 6;

      the lmult of Z1 = ( lmultCoset (V,W)) by VECTSP10:def 6

      .= ( lmultCoset (V,Ws)) by A1, LmStrict3

      .= the lmult of Z2 by VECTSP10:def 6;

      hence thesis by A2, A3, A4;

    end;

    theorem :: ZMODUL07:38

    for R be Ring holds for V,U be LeftMod of R, V1 be Submodule of V, U1 be Submodule of U, f be linear-transformation of V, U st f is onto & the carrier of V1 = (f " the carrier of U1) holds ex F be linear-transformation of ( VectQuot (V,V1)), ( VectQuot (U,U1)) st F is bijective

    proof

      let R be Ring;

      let V,U be LeftMod of R, V1 be Submodule of V, U1 be Submodule of U, f be linear-transformation of V, U;

      assume

       AS: f is onto & the carrier of V1 = (f " the carrier of U1);

      set g = ( ZQMorph (U,U1));

      reconsider V1s = ( (Omega). V1) as strict Submodule of V by ZMODUL01: 42;

      

       P2: (g * f) is onto by AS, FUNCT_2: 27;

      

       P5: ( VectQuot (V,V1)) = ( VectQuot (V,V1s)) by ThStrict1;

      the carrier of ( ker (g * f)) = (f " the carrier of ( ker g)) by LMFirst3

      .= (f " the carrier of ( (Omega). U1)) by LMFirst5

      .= the carrier of V1s by AS;

      then

       P3: ( ker (g * f)) = V1s by ZMODUL01: 45;

      

       P4: ( im (g * f)) = ( (Omega). ( VectQuot (U,U1))) by P2, LMFirst4

      .= ( VectQuot (U,U1));

      then

      reconsider F = ( Zdecom (g * f)) as linear-transformation of ( VectQuot (V,V1)), ( VectQuot (U,U1)) by P3, P5;

      take F;

      ( Zdecom (g * f)) is bijective by defdecom;

      hence F is bijective by P4;

    end;

    theorem :: ZMODUL07:39

    for R be Ring holds for V be LeftMod of R, W1,W2 be Submodule of V, U1 be Submodule of (W1 + W2), U2 be strict Submodule of W1 st U1 = W2 & U2 = (W1 /\ W2) holds ex F be linear-transformation of ( VectQuot ((W1 + W2),U1)), ( VectQuot (W1,U2)) st F is bijective

    proof

      let R be Ring;

      let V be LeftMod of R, W1,W2 be Submodule of V, U1 be Submodule of (W1 + W2), U2 be strict Submodule of W1 such that

       A1: U1 = W2 & U2 = (W1 /\ W2);

      set Z1 = ( VectQuot ((W1 + W2),U1));

      set Z2 = ( VectQuot (W1,U2));

      defpred P[ object, object] means ex v be Element of (W1 + W2) st $1 = v & $2 = (v + U1);

      

       A2: for z be Element of W1 holds ex y be Element of Z1 st P[z, y]

      proof

        let z be Element of W1;

        reconsider zv = z as Element of V by ZMODUL01: 25;

        zv in W1;

        then zv in (W1 + W2) by ZMODUL01: 93;

        then

        reconsider zz = zv as Element of (W1 + W2);

        set y = (zz + U1);

        y is Coset of U1 by VECTSP_4:def 6;

        then y in ( CosetSet ((W1 + W2),U1));

        then

        reconsider yy = y as Element of Z1 by VECTSP10:def 6;

        take yy;

        thus thesis;

      end;

      consider f be Function of the carrier of W1, the carrier of Z1 such that

       A3: for z be Element of W1 holds P[z, (f . z)] from FUNCT_2:sch 3( A2);

      f is linear-transformation of W1, Z1

      proof

        for x,y be Element of W1 holds (f . (x + y)) = ((f . x) + (f . y))

        proof

          let x,y be Element of W1;

          consider xx be Element of (W1 + W2) such that

           C1: x = xx & (f . x) = (xx + U1) by A3;

          consider yy be Element of (W1 + W2) such that

           C2: y = yy & (f . y) = (yy + U1) by A3;

          consider xy be Element of (W1 + W2) such that

           C3: (x + y) = xy & (f . (x + y)) = (xy + U1) by A3;

          reconsider xv = x, yv = y as Element of V by ZMODUL01: 25;

          (xx + U1) is Coset of U1 & (yy + U1) is Coset of U1 by VECTSP_4:def 6;

          then (xx + U1) in ( CosetSet ((W1 + W2),U1)) & (yy + U1) in ( CosetSet ((W1 + W2),U1));

          then

          reconsider xU = (xx + U1), yU = (yy + U1) as Element of ( CosetSet ((W1 + W2),U1));

          

           C4: (xx + yy) = (xv + yv) by C1, C2, ZMODUL01: 28

          .= xy by C3, ZMODUL01: 28;

          

          thus ((f . x) + (f . y)) = (( addCoset ((W1 + W2),U1)) . (xU,yU)) by C1, C2, VECTSP10:def 6

          .= (f . (x + y)) by C3, C4, VECTSP10:def 3;

        end;

        then

         B1: f is additive;

        for a be Element of R, x be Element of W1 holds (f . (a * x)) = (a * (f . x))

        proof

          let a be Element of R, x be Element of W1;

          consider xx be Element of (W1 + W2) such that

           C1: x = xx & (f . x) = (xx + U1) by A3;

          consider ax be Element of (W1 + W2) such that

           C2: (a * x) = ax & (f . (a * x)) = (ax + U1) by A3;

          reconsider xv = x as Element of V by ZMODUL01: 25;

          

           C3: (a * xx) = (a * xv) by C1, ZMODUL01: 29

          .= ax by C2, ZMODUL01: 29;

          (xx + U1) is Coset of U1 by VECTSP_4:def 6;

          then (xx + U1) in ( CosetSet ((W1 + W2),U1));

          then

          reconsider xU = (xx + U1) as Element of ( CosetSet ((W1 + W2),U1));

          

          thus (f . (a * x)) = (( lmultCoset ((W1 + W2),U1)) . (a,xU)) by C2, C3, VECTSP10:def 5

          .= (a * (f . x)) by C1, VECTSP10:def 6;

        end;

        then f is homogeneous;

        hence thesis by B1;

      end;

      then

      reconsider f as linear-transformation of W1, Z1;

      

       A4: ( ker f) = U2

      proof

        for v be Element of W1 holds v in ( ker f) iff v in U2

        proof

          let v be Element of W1;

          hereby

            assume v in ( ker f);

            then

             C1: (f . v) = ( 0. Z1) by RANKNULL: 10;

            consider vv be Element of (W1 + W2) such that

             C2: v = vv & (f . v) = (vv + U1) by A3;

            (vv + U1) = ( zeroCoset ((W1 + W2),U1)) by C1, C2, VECTSP10:def 6

            .= the carrier of U1;

            then

             C3: v in W2 by A1, C2, ZMODUL01: 63;

            v in W1;

            hence v in U2 by A1, C3, ZMODUL01: 94;

          end;

          assume

           C1: v in U2;

          consider vv be Element of (W1 + W2) such that

           C2: v = vv & (f . v) = (vv + U1) by A3;

          vv in U1 by A1, C1, C2, ZMODUL01: 94;

          

          then (f . v) = ( zeroCoset ((W1 + W2),U1)) by C2, ZMODUL01: 63

          .= ( 0. Z1) by VECTSP10:def 6;

          hence v in ( ker f) by RANKNULL: 10;

        end;

        hence thesis by ZMODUL01: 46;

      end;

      

       A5: ( im f) = ( VectQuot ((W1 + W2),U1))

      proof

        for y be object st y in the carrier of Z1 holds (f " {y}) <> {}

        proof

          let y be object such that

           C2: y in the carrier of Z1;

          y in ( CosetSet ((W1 + W2),U1)) by C2, VECTSP10:def 6;

          then

          consider yy be Coset of U1 such that

           C8: y = yy;

          consider z be Element of (W1 + W2) such that

           C3: y = (z + U1) by C8, VECTSP_4:def 6;

          z in (W1 + W2);

          then

          consider z1,z2 be Element of V such that

           C4: z1 in W1 & z2 in W2 & z = (z1 + z2) by ZMODUL01: 92;

          reconsider zz1 = z1 as Element of W1 by C4;

          consider zzz1 be Element of (W1 + W2) such that

           C6: zz1 = zzz1 & (f . zz1) = (zzz1 + U1) by A3;

          z2 in (W1 + W2) by C4, ZMODUL01: 93;

          then

          reconsider zzz2 = z2 as Element of (W1 + W2);

          

           C7: z = (zzz1 + zzz2) by C4, C6, ZMODUL01: 28;

          y = (f . zz1) by A1, C3, C4, C6, C7, ZMODUL01: 65;

          then (f . zz1) in {y} by TARSKI:def 1;

          hence (f " {y}) <> {} by FUNCT_2: 38;

        end;

        then

         B1: ( rng f) = the carrier of Z1 by FUNCT_2: 41;

        

         B2: ( dom f) = the carrier of W1 by FUNCT_2:def 1;

        the carrier of ( im f) = ( [#] ( im f))

        .= (f .: ( [#] W1)) by RANKNULL:def 2

        .= the carrier of Z1 by B1, B2, RELAT_1: 113;

        hence thesis by ZMODUL01: 47;

      end;

      reconsider F = ( Zdecom f) as linear-transformation of Z2, Z1 by A4, A5;

      consider FI be linear-transformation of Z1, Z2 such that

       X1: FI = (F " ) & FI is bijective by A4, A5, defdecom, ZMODUL06: 42;

      take FI;

      thus thesis by X1;

    end;

    theorem :: ZMODUL07:40

    for R be Ring holds for V be LeftMod of R, W1 be Submodule of V, W2 be Submodule of W1, U1 be Submodule of V, U2 be Submodule of ( VectQuot (V,U1)) st U1 = W2 & U2 = ( VectQuot (W1,W2)) holds ex F be linear-transformation of ( VectQuot (( VectQuot (V,U1)),U2)), ( VectQuot (V,W1)) st F is bijective

    proof

      let R be Ring;

      let V be LeftMod of R, W1 be Submodule of V, W2 be Submodule of W1, U1 be Submodule of V, U2 be Submodule of ( VectQuot (V,U1));

      assume

       A1: U1 = W2 & U2 = ( VectQuot (W1,W2));

      set Z1 = ( VectQuot (( VectQuot (V,U1)),U2));

      set Z2 = ( VectQuot (V,W1));

      

       YY: ( rng ( ZQMorph (V,U1))) = the carrier of ( VectQuot (V,U1)) by FUNCT_2:def 3;

      defpred P[ object, object] means ex v be Element of V st $1 = (v + U1) & $2 = (v + W1);

      

       A2: for z be Element of ( VectQuot (V,U1)) holds ex y be Element of ( VectQuot (V,W1)) st P[z, y]

      proof

        let z be Element of ( VectQuot (V,U1));

        consider v be Element of V such that

         A17: z = (( ZQMorph (V,U1)) . v) by FUNCT_2: 113, YY;

        

         A19: (( ZQMorph (V,U1)) . v) = (v + U1) by defMophVW;

        set y = (v + W1);

        y is Coset of W1 by VECTSP_4:def 6;

        then y in ( CosetSet (V,W1));

        then

        reconsider y as Element of ( VectQuot (V,W1)) by VECTSP10:def 6;

        take y;

        thus thesis by A17, A19;

      end;

      consider f be Function of ( VectQuot (V,U1)), ( VectQuot (V,W1)) such that

       A3: for z be Element of ( VectQuot (V,U1)) holds P[z, (f . z)] from FUNCT_2:sch 3( A2);

      f is linear-transformation of ( VectQuot (V,U1)), ( VectQuot (V,W1))

      proof

        for x,y be Element of ( VectQuot (V,U1)) holds (f . (x + y)) = ((f . x) + (f . y))

        proof

          let x,y be Element of ( VectQuot (V,U1));

          consider xx be Element of V such that

           C1: x = (xx + U1) & (f . x) = (xx + W1) by A3;

          consider yy be Element of V such that

           C2: y = (yy + U1) & (f . y) = (yy + W1) by A3;

          consider xy be Element of V such that

           C3: (x + y) = (xy + U1) & (f . (x + y)) = (xy + W1) by A3;

          reconsider xU = (xx + U1), yU = (yy + U1) as Element of ( CosetSet (V,U1)) by C1, C2, VECTSP10:def 6;

          reconsider fxU = (xx + W1), fyU = (yy + W1) as Element of ( CosetSet (V,W1)) by C1, C2, VECTSP10:def 6;

          (xy + U1) = (( addCoset (V,U1)) . (xU,yU)) by C3, C1, C2, VECTSP10:def 6

          .= ((xx + yy) + U1) by VECTSP10:def 3;

          then (xx + yy) in (xy + U1) by ZMODUL01: 58;

          then

          consider w be Vector of V such that

           D21: (xx + yy) = (xy + w) & w in U1;

          w in W1 by A1, D21, ZMODUL01: 24;

          then

           D3: (xx + yy) in (xy + W1) by D21;

          (xx + yy) in ((xx + yy) + W1) by ZMODUL01: 58;

          then

           C4: (xy + W1) = ((xx + yy) + W1) by D3, ZMODUL01: 68;

          

          thus ((f . x) + (f . y)) = (( addCoset (V,W1)) . (fxU,fyU)) by C1, C2, VECTSP10:def 6

          .= (f . (x + y)) by C4, C3, VECTSP10:def 3;

        end;

        then

         B1: f is additive;

        for a be Element of R, x be Element of ( VectQuot (V,U1)) holds (f . (a * x)) = (a * (f . x))

        proof

          let a be Element of R, x be Element of ( VectQuot (V,U1));

          consider xx be Element of V such that

           C1: x = (xx + U1) & (f . x) = (xx + W1) by A3;

          consider ax be Element of V such that

           C3: (a * x) = (ax + U1) & (f . (a * x)) = (ax + W1) by A3;

          reconsider xU = (xx + U1) as Element of ( CosetSet (V,U1)) by C1, VECTSP10:def 6;

          reconsider fxU = (xx + W1) as Element of ( CosetSet (V,W1)) by C1, VECTSP10:def 6;

          (ax + U1) = (( lmultCoset (V,U1)) . (a,xU)) by C3, C1, VECTSP10:def 6

          .= ((a * xx) + U1) by VECTSP10:def 5;

          then (a * xx) in (ax + U1) by ZMODUL01: 58;

          then

          consider w be Vector of V such that

           D21: (a * xx) = (ax + w) & w in U1;

          w in W1 by A1, D21, ZMODUL01: 24;

          then

           D3: (a * xx) in (ax + W1) by D21;

          (a * xx) in ((a * xx) + W1) by ZMODUL01: 58;

          then

           C4: (ax + W1) = ((a * xx) + W1) by D3, ZMODUL01: 68;

          

          thus (a * (f . x)) = (( lmultCoset (V,W1)) . (a,fxU)) by C1, VECTSP10:def 6

          .= (f . (a * x)) by C4, C3, VECTSP10:def 5;

        end;

        then f is homogeneous;

        hence thesis by B1;

      end;

      then

      reconsider f as linear-transformation of ( VectQuot (V,U1)), ( VectQuot (V,W1));

      

       A4: ( ker f) = U2

      proof

        for v be Element of ( VectQuot (V,U1)) holds v in ( ker f) iff v in U2

        proof

          let v be Element of ( VectQuot (V,U1));

          hereby

            assume v in ( ker f);

            then

             C1: (f . v) = ( 0. ( VectQuot (V,W1))) by RANKNULL: 10;

            consider vv be Element of V such that

             C2: v = (vv + U1) & (f . v) = (vv + W1) by A3;

            (vv + W1) = ( zeroCoset (V,W1)) by C1, C2, VECTSP10:def 6

            .= the carrier of W1;

            then vv in W1 by ZMODUL01: 63;

            then

            reconsider vv1 = vv as Vector of W1;

            for x be object holds x in (vv + U1) iff x in (vv1 + W2)

            proof

              let x be object;

              hereby

                assume x in (vv + U1);

                then

                consider w3 be Vector of V such that

                 X1: x = (vv + w3) & w3 in U1;

                w3 in W1 by A1, X1, ZMODUL01: 24;

                then

                reconsider ww3 = w3 as Vector of W1;

                

                 X2: (vv + w3) = (vv1 + ww3) by ZMODUL01: 28;

                thus x in (vv1 + W2) by A1, X1, X2;

              end;

              assume x in (vv1 + W2);

              then

              consider w2 be Vector of W1 such that

               X1: x = (vv1 + w2) & w2 in W2;

              w2 in V by A1, X1, ZMODUL01: 24;

              then

              reconsider ww2 = w2 as Vector of V;

              

               X2: (vv + ww2) = (vv1 + w2) by ZMODUL01: 28;

              thus x in (vv + U1) by A1, X1, X2;

            end;

            then v = (vv1 + W2) by C2, TARSKI: 2;

            then v is Coset of W2 by VECTSP_4:def 6;

            then v in ( CosetSet (W1,W2));

            hence v in U2 by A1, VECTSP10:def 6;

          end;

          assume v in U2;

          then v in ( CosetSet (W1,W2)) by A1, VECTSP10:def 6;

          then ex A be Coset of W2 st v = A;

          then

          consider vv1 be Vector of W1 such that

           X1: v = (vv1 + W2) by VECTSP_4:def 6;

          consider vv be Element of V such that

           C2: v = (vv + U1) & (f . v) = (vv + W1) by A3;

          vv in (vv1 + W2) by C2, X1, ZMODUL01: 58;

          then vv in W1;

          

          then (f . v) = ( zeroCoset (V,W1)) by C2, ZMODUL01: 63

          .= ( 0. ( VectQuot (V,W1))) by VECTSP10:def 6;

          hence v in ( ker f) by RANKNULL: 10;

        end;

        hence thesis by A1, ZMODUL01: 46;

      end;

      

       A5: ( im f) = ( VectQuot (V,W1))

      proof

        for y be object st y in the carrier of ( VectQuot (V,W1)) holds (f " {y}) <> {}

        proof

          let y be object such that

           C2: y in the carrier of ( VectQuot (V,W1));

          y in ( CosetSet (V,W1)) by C2, VECTSP10:def 6;

          then

          consider yy be Coset of W1 such that

           C8: y = yy;

          consider z be Element of V such that

           C3: y = (z + W1) by C8, VECTSP_4:def 6;

          (z + U1) is Coset of U1 by VECTSP_4:def 6;

          then (z + U1) in ( CosetSet (V,U1));

          then

          reconsider y1 = (z + U1) as Vector of ( VectQuot (V,U1)) by VECTSP10:def 6;

          consider z1 be Element of V such that

           C6: y1 = (z1 + U1) & (f . y1) = (z1 + W1) by A3;

          z1 in (z1 + U1) by ZMODUL01: 58;

          then

          consider w be Vector of V such that

           D21: z1 = (z + w) & w in U1 by C6;

          w in W1 by A1, D21, ZMODUL01: 24;

          then

           D3: z1 in (z + W1) by D21;

          z1 in (z1 + W1) by ZMODUL01: 58;

          then y = (f . y1) by C3, C6, D3, ZMODUL01: 68;

          then (f . y1) in {y} by TARSKI:def 1;

          hence (f " {y}) <> {} by FUNCT_2: 38;

        end;

        then

         B1: ( rng f) = the carrier of ( VectQuot (V,W1)) by FUNCT_2: 41;

        

         B2: ( dom f) = the carrier of ( VectQuot (V,U1)) by FUNCT_2:def 1;

        the carrier of ( im f) = ( [#] ( im f))

        .= (f .: ( [#] ( VectQuot (V,U1)))) by RANKNULL:def 2

        .= the carrier of ( VectQuot (V,W1)) by B1, B2, RELAT_1: 113;

        hence thesis by ZMODUL01: 47;

      end;

      reconsider F = ( Zdecom f) as linear-transformation of Z1, Z2 by A4, A5;

      take F;

      thus thesis by A4, A5, defdecom;

    end;

    registration

      let V be Z_Module;

      let a be non zero Element of INT.Ring ;

      cluster ( VectQuot (V,(a (*) V))) -> torsion;

      correctness

      proof

        set W = (a (*) V);

        for x be Vector of ( VectQuot (V,W)) holds x is torsion

        proof

          let x be Vector of ( VectQuot (V,W));

          a <> ( 0. INT.Ring );

          then a <> 0 ;

          

          then (a * x) = ((a mod a) * x) by ZMODUL02: 2

          .= ( 0. ( VectQuot (V,W))) by INT_1: 50, ZMODUL01: 1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: ZMODUL07:41

    

     ThTrivial1: for R be Ring holds for V be trivial LeftMod of R holds ( (Omega). V) = ( (0). V)

    proof

      let R be Ring;

      let V be trivial LeftMod of R;

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

      then

      consider v be Vector of V such that

       A1: v in ( (Omega). V) & v <> ( 0. V) by ZMODUL04: 24;

      reconsider v as Vector of V;

      V is non trivial by A1;

      hence contradiction;

    end;

    theorem :: ZMODUL07:42

    

     ThTrivial2: for R be Ring holds for V be LeftMod of R, v be Vector of V st v <> ( 0. V) holds ( Lin {v}) is non trivial

    proof

      let R be Ring;

      let V be LeftMod of R, v be Vector of V such that

       A1: v <> ( 0. V);

       {v} <> {( 0. V)} by A1, ZFMISC_1: 3;

      then ( Lin {v}) <> ( (0). V) by MOD_3: 7;

      then ( (Omega). ( Lin {v})) <> ( (0). ( Lin {v})) by VECTSP_4: 36;

      hence thesis by ThTrivial1;

    end;

    theorem :: ZMODUL07:43

    

     LMCLUS1: ex V be Z_Module, p be Element of INT.Ring st p <> ( 0. INT.Ring ) & ( VectQuot (V,(p (*) V))) is non trivial

    proof

      reconsider V = ModuleStr (# the carrier of INT.Ring , the addF of INT.Ring , the ZeroF of INT.Ring , ( Int-mult-left INT.Ring ) #) as Z_Module by ZMODUL01: 164;

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

      take V, p;

      thus p <> ( 0. INT.Ring );

      thus ( VectQuot (V,(p (*) V))) is non trivial

      proof

        reconsider i = ( 1. INT.Ring ) as Vector of V;

        (i + (p (*) V)) is Coset of (p (*) V) by VECTSP_4:def 6;

        then (i + (p (*) V)) in ( CosetSet (V,(p (*) V)));

        then

        reconsider B = (i + (p (*) V)) as Element of ( CosetSet (V,(p (*) V)));

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

        u <> ( 0. ( VectQuot (V,(p (*) V))))

        proof

          assume u = ( 0. ( VectQuot (V,(p (*) V))));

          

          then (i + (p (*) V)) = ( zeroCoset (V,(p (*) V))) by VECTSP10:def 6

          .= the carrier of (p (*) V);

          then i in (p (*) V) by ZMODUL01: 63;

          then

          consider w be Vector of V such that

           P1: i = (p * w);

          reconsider w0 = w as Element of INT.Ring ;

          (p * w) = (p * w0) by ZMODUL06: 14;

          then (1 / 2) = w0 by P1;

          hence contradiction by NAT_D: 33;

        end;

        hence thesis;

      end;

    end;

    registration

      cluster non trivial for torsion Z_Module;

      correctness

      proof

        consider V be Z_Module, p be Element of INT.Ring such that

         A1: p <> ( 0. INT.Ring ) & ( VectQuot (V,(p (*) V))) is non trivial by LMCLUS1;

        reconsider pp = p as non zero Element of INT.Ring by A1, STRUCT_0:def 12;

        set W = ( VectQuot (V,(pp (*) V)));

        W is non trivial by A1;

        hence thesis;

      end;

    end

    registration

      cluster non torsion-free for Z_Module;

      correctness

      proof

        set V = the non trivial torsion Z_Module;

        set v = the non zero Vector of V;

        take V;

        thus thesis;

      end;

    end

    registration

      let V be non torsion-free Z_Module;

      cluster non zero torsion for Vector of V;

      correctness

      proof

        ex v be Vector of V st v is non zero torsion

        proof

          assume

           B1: for v be Vector of V holds v is zero or v is non torsion;

          for v be Vector of V st v <> ( 0. V) holds v is non torsion

          proof

            let v be Vector of V such that

             C1: v <> ( 0. V);

            v is non zero by C1;

            hence thesis by B1;

          end;

          then V is torsion-free;

          hence contradiction;

        end;

        then

        consider v be Vector of V such that

         A1: v is non zero torsion;

        take v;

        thus thesis by A1;

      end;

    end

    registration

      cluster non trivial for finitely-generated Z_Module;

      correctness

      proof

        set V = the non trivial Z_Module;

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

        then

        consider v be Vector of V such that

         A1: v in ( (Omega). V) & v <> ( 0. V) by ZMODUL04: 24;

        take ( Lin {v});

        thus thesis by A1, ThTrivial2;

      end;

    end

    theorem :: ZMODUL07:44

    

     ThTFX: for V be Z_Module holds V is torsion-free iff ( (Omega). V) is torsion-free

    proof

      let V be Z_Module;

      thus V is torsion-free implies ( (Omega). V) is torsion-free;

      assume

       A1: ( (Omega). V) is torsion-free;

      for v be Vector of V st v <> ( 0. V) holds v is non torsion

      proof

        let v be Vector of V such that

         B1: v <> ( 0. V);

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

        

         B2: vv is non torsion by A1, B1;

        for i be Element of INT.Ring st i <> ( 0. INT.Ring ) holds (i * v) <> ( 0. V)

        proof

          let i be Element of INT.Ring such that

           C1: i <> ( 0. INT.Ring );

          (i * vv) <> ( 0. ( (Omega). V)) by B2, C1;

          hence thesis;

        end;

        hence thesis;

      end;

      hence V is torsion-free;

    end;

    registration

      cluster -> non trivial for non torsion-free Z_Module;

      correctness

      proof

        let V be non torsion-free Z_Module;

        assume V is trivial;

        then ( (Omega). V) = ( (0). V) by ThTrivial1;

        hence contradiction by ThTFX;

      end;

    end

    registration

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

      correctness

      proof

        set V = the non trivial torsion-free Z_Module;

        set v = the non zero Vector of V;

        take ( Lin {v});

        v <> ( 0. V);

        hence thesis by ThTrivial2;

      end;

    end

    registration

      let V be non trivial finitely-generated torsion-free Z_Module, p be prime Element of INT.Ring ;

      cluster ( VectQuot (V,(p (*) V))) -> non trivial;

      coherence

      proof

        set I = the Basis of V;

        ( card I) > 0

        proof

          assume ( card I) <= 0 ;

          then I = ( {} the carrier of V);

          then ( Lin I) = ( (0). V) by ZMODUL02: 67;

          then ( (Omega). V) = ( (0). V) by VECTSP_7:def 3;

          hence contradiction;

        end;

        then I is non empty;

        then

        consider v be object such that

         A1: v in I by XBOOLE_0:def 1;

        reconsider v as Vector of V by A1;

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

        then ( (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 A1, ZMODUL06: 24;

        then

         A6: v is non torsion by ZMODUL06:def 3;

        reconsider pp = p as Element of INT.Ring ;

        assume ( VectQuot (V,(p (*) V))) is trivial;

        

        then (( ZQMorph (V,(p (*) V))) . v) = ( 0. ( VectQuot (V,(p (*) V))))

        .= ( zeroCoset (V,(p (*) V))) by VECTSP10:def 6

        .= the carrier of (p (*) V);

        then (v + (p (*) V)) = the carrier of (p (*) V) by defMophVW;

        then v in (p (*) V) by ZMODUL01: 63;

        then

        consider u be Vector of V such that

         A3: v = (pp * u);

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

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

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

        then

        consider u1,u2 be Vector of V such that

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

        

         B5: v = ((pp * u1) + (pp * u2)) by A3, B4, VECTSP_1:def 14;

        

         B6: (pp * u1) in ( Lin (I \ {v})) by B4, ZMODUL01: 37;

        

         B7: (pp * u2) in ( Lin {v}) by B4, ZMODUL01: 37;

        consider iu2 be Element of INT.Ring such that

         B8: u2 = (iu2 * v) by B4, ZMODUL06: 19;

        

         B9: (pp * u2) = ((pp * iu2) * v) by B8, VECTSP_1:def 16;

        

         B10: V is_the_direct_sum_of (( Lin (I \ {v})),( Lin {v})) by A1, ZMODUL04: 33;

        

         B11: v = ((( 1. INT.Ring ) * v) + ( 0. V)) by VECTSP_1:def 17;

        

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

        ( 0. V) in ( Lin (I \ {v})) by ZMODUL01: 33;

        then ((( 1. INT.Ring ) * v) - ((pp * iu2) * v)) = (((pp * iu2) * v) - ((pp * iu2) * v)) by B5, B11, B6, B7, B9, B10, B12, ZMODUL01: 134;

        then ((( 1. INT.Ring ) - (pp * iu2)) * v) = (((pp * iu2) * v) - ((pp * iu2) * v)) by ZMODUL01: 9;

        then (( 1. INT.Ring ) - (pp * iu2)) = 0 by A6, RLVECT_1: 15;

        then (1 / p) is Integer by XCMPLX_1: 89;

        hence contradiction by INT_2:def 4, NAT_D: 33;

      end;

    end

    registration

      cluster finitely-generated for torsion Z_Module;

      correctness

      proof

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

        set p = the prime Element of INT.Ring ;

        reconsider pp = p as non zero Element of INT.Ring ;

        set W = ( VectQuot (V,(pp (*) V)));

        W is torsion;

        hence thesis;

      end;

    end

    registration

      cluster non trivial for finitely-generated torsion Z_Module;

      correctness

      proof

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

        set p = the prime Element of INT.Ring ;

        reconsider pp = p as prime non zero Element of INT.Ring ;

        set W = ( VectQuot (V,(pp (*) V)));

        W is non trivial;

        hence thesis;

      end;

    end

    registration

      let V be non trivial finitely-generated torsion-free Z_Module, p be prime Element of INT.Ring ;

      cluster ( VectQuot (V,(p (*) V))) -> finitely-generated torsion;

      correctness ;

    end

    registration

      let V be non torsion Z_Module;

      cluster ( VectQuot (V,( torsion_part V))) -> non trivial;

      correctness

      proof

        assume

         AS: ( VectQuot (V,( torsion_part V))) is trivial;

        consider v be Vector of V such that

         P1: not v is torsion by ZMODUL06:def 2;

        (v + ( torsion_part V)) is Coset of ( torsion_part V) by VECTSP_4:def 6;

        then (v + ( torsion_part V)) in ( CosetSet (V,( torsion_part V)));

        then

        reconsider B = (v + ( torsion_part V)) as Element of ( CosetSet (V,( torsion_part V)));

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

        u = ( 0. ( VectQuot (V,( torsion_part V)))) by AS

        .= ( zeroCoset (V,( torsion_part V))) by VECTSP10:def 6

        .= the carrier of ( torsion_part V);

        then v in ( torsion_part V) by ZMODUL01: 63;

        then v in { v where v be Vector of V : v is torsion } by defTorsionPart;

        then ex u be Vector of V st v = u & u is torsion;

        hence contradiction by P1;

      end;

    end