zmodul02.miz



    begin

    reserve x,y,y1,y2 for set;

    reserve R for Ring;

    reserve V for LeftMod of R;

    reserve u,v,w for VECTOR of V;

    reserve F,G,H,I for FinSequence of V;

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

    reserve f,f9,g for sequence of V;

    definition

      let R be Ring;

      let V be LeftMod of R;

      let a be Element of R;

      :: ZMODUL02:def1

      func a * V -> non empty Subset of V equals the set of all (a * v) where v be Element of V;

      correctness

      proof

        set S = the set of all (a * v) where v be Element of V;

         A1:

        now

          let x be object;

          assume x in S;

          then ex v be Element of V st x = (a * v);

          hence x in the carrier of V;

        end;

        (a * ( 0. V)) in S;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    definition

      let R be Ring;

      let V be LeftMod of R;

      let a be Element of R;

      :: ZMODUL02:def2

      func Zero_ (a,V) -> Element of (a * V) equals ( 0. V);

      correctness

      proof

        ( 0. V) = (a * ( 0. V)) by VECTSP_1: 14;

        then ( 0. V) in (a * V);

        hence thesis;

      end;

    end

    definition

      let R be Ring;

      let V be LeftMod of R;

      let a be Element of R;

      :: ZMODUL02:def3

      func Add_ (a,V) -> Function of [:(a * V), (a * V):], (a * V) equals (the addF of V | [:(a * V), (a * V):]);

      correctness

      proof

        set adds = (the addF of V | [:(a * V), (a * V):]);

         [:(a * V), (a * V):] c= [:the carrier of V, the carrier of V:] by ZFMISC_1: 96;

        then [:(a * V), (a * V):] c= ( dom the addF of V) by FUNCT_2:def 1;

        then

         A1: ( dom adds) = [:(a * V), (a * V):] by RELAT_1: 62;

        for z be object st z in [:(a * V), (a * V):] holds (adds . z) in (a * V)

        proof

          let z be object such that

           A2: z in [:(a * V), (a * V):];

          consider x,y be object such that

           A3: (x in (a * V)) & y in (a * V) & z = [x, y] by A2, ZFMISC_1:def 2;

          consider v be Element of V such that

           A4: x = (a * v) by A3;

          consider w be Element of V such that

           A5: y = (a * w) by A3;

          (adds . z) = ((a * v) + (a * w)) by A2, A3, A4, A5, FUNCT_1: 49

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

          hence (adds . z) in (a * V);

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    definition

      let R be commutative Ring;

      let V be VectSp of R;

      let a be Element of R;

      :: ZMODUL02:def4

      func Mult_ (a,V) -> Function of [:the carrier of R, (a * V):], (a * V) equals (the lmult of V | [:the carrier of R, (a * V):]);

      correctness

      proof

        set I = the carrier of R;

        set scmult = (the lmult of V | [:the carrier of R, (a * V):]);

         [:I, (a * V):] c= [:I, the carrier of V:] by ZFMISC_1: 96;

        then [:I, (a * V):] c= ( dom the lmult of V) by FUNCT_2:def 1;

        then

         A1: ( dom scmult) = [:I, (a * V):] by RELAT_1: 62;

        for z be object st z in [:I, (a * V):] holds (scmult . z) in (a * V)

        proof

          let z be object such that

           A2: z in [:I, (a * V):];

          consider x,y be object such that

           A3: x in I & y in (a * V) & z = [x, y] by A2, ZFMISC_1:def 2;

          reconsider i = x as Element of R by A3;

          consider v be Element of V such that

           A4: y = (a * v) by A3;

          (scmult . z) = (i * (a * v)) by A2, A3, A4, FUNCT_1: 49

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

          .= ((a * i) * v)

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

          hence (scmult . z) in (a * V);

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    definition

      let R be commutative Ring;

      let V be LeftMod of R;

      let a be Element of R;

      :: ZMODUL02:def5

      func a (*) V -> Subspace of V equals ModuleStr (# (a * V), ( Add_ (a,V)), ( Zero_ (a,V)), ( Mult_ (a,V)) #);

      coherence

      proof

        set V1 = (a * V);

        set Z0 = ( Zero_ (a,V));

        set AV1 = ( Add_ (a,V));

        set MV1 = ( Mult_ (a,V));

        Z0 = ( 0. V) & AV1 = (the addF of V || V1) & MV1 = (the lmult of V | [:the carrier of R, V1:]);

        hence thesis by ZMODUL01: 40;

      end;

    end

    definition

      ::$Canceled

    end

    theorem :: ZMODUL02:1

    

     Th1: for p be Element of INT.Ring , V be Z_Module, W be Submodule of V, x be VECTOR of ( VectQuot (V,W)) st W = (p (*) V) holds (p * x) = ( 0. ( VectQuot (V,W)))

    proof

      let p be Element of INT.Ring , V be Z_Module, W be Submodule of V, x be VECTOR of ( VectQuot (V,W)) such that

       A1: W = (p (*) V);

      

       A2: x is Element of ( CosetSet (V,W)) by VECTSP10:def 6;

      then x in the set of all A where A be Coset of W;

      then

      consider xx be Coset of W such that

       A3: xx = x;

      consider v be VECTOR of V such that

       A4: xx = (v + W) by VECTSP_4:def 6;

      (p * v) in the carrier of W by A1;

      then

       A5: (p * v) in W;

      

      thus (p * x) = (( lmultCoset (V,W)) . (p,x)) by VECTSP10:def 6

      .= ((p * v) + W) by A2, A3, A4, VECTSP10:def 5

      .= ( zeroCoset (V,W)) by A5, ZMODUL01: 63

      .= ( 0. ( VectQuot (V,W))) by VECTSP10:def 6;

    end;

    theorem :: ZMODUL02:2

    

     Th2: for p,i be Element of INT.Ring , V be Z_Module, W be Submodule of V, x be VECTOR of ( VectQuot (V,W)) st p <> 0 & W = (p (*) V) holds (i * x) = ((i mod p) * x)

    proof

      let p,i be Element of INT.Ring , V be Z_Module, W be Submodule of V, x be VECTOR of ( VectQuot (V,W)) such that

       A1: p <> 0 and

       A2: W = (p (*) V);

      consider j be Element of INT.Ring such that

       A3: j = (i div p);

      

      thus (i * x) = (((j * p) + (i mod p)) * x) by A1, A3, INT_1: 59

      .= (((j * p) * x) + ((i mod p) * x)) by VECTSP_1:def 15

      .= ((j * (p * x)) + ((i mod p) * x)) by VECTSP_1:def 16

      .= (( 0. ( VectQuot (V,W))) + ((i mod p) * x)) by A2, Th1, ZMODUL01: 1

      .= ((i mod p) * x) by RLVECT_1: 4;

    end;

    

     Lem1: for i be Integer holds i in the carrier of INT.Ring by INT_1:def 2;

    theorem :: ZMODUL02:3

    for p,q be Element of INT.Ring , V be Z_Module, W be Submodule of V, v be VECTOR of V st W = (p (*) V) & p > 1 & q > 1 & (p,q) are_coprime holds (q * v) = ( 0. V) implies (v + W) = ( 0. ( VectQuot (V,W)))

    proof

      let p,q be Element of INT.Ring , V be Z_Module, W be Submodule of V, v be VECTOR of V such that

       A1: W = (p (*) V) and

       A2: p > 1 & q > 1 & (p,q) are_coprime ;

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

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

      then

      reconsider x = (v + W) as VECTOR of ( VectQuot (V,W)) by VECTSP10:def 6;

      p in NAT & q in NAT by A2, INT_1: 3;

      then

      reconsider pp = p, qq = q as Nat;

      consider i,j be Integer such that

       A3: ((i * pp) + (j * qq)) = 1 by A2, EULER_1: 10;

      

       a3: ((i * pp) + (j * qq)) = ( 1. INT.Ring ) by A3;

      reconsider i, j as Element of INT.Ring by Lem1;

      assume

       A4: (q * v) = ( 0. V);

      

       A5: x is Element of ( CosetSet (V,W)) by VECTSP10:def 6;

      

       A6: (q * x) = (( lmultCoset (V,W)) . (q,x)) by VECTSP10:def 6

      .= (( 0. V) + W) by A4, A5, VECTSP10:def 5

      .= ( zeroCoset (V,W)) by ZMODUL01: 59

      .= ( 0. ( VectQuot (V,W))) by VECTSP10:def 6;

      (((i * p) + (j * q)) * x) = (((i * p) * x) + ((j * q) * x)) by VECTSP_1:def 15

      .= (((i * p) * x) + (j * (q * x))) by VECTSP_1:def 16

      .= (((i * p) * x) + ( 0. ( VectQuot (V,W)))) by A6, ZMODUL01: 1

      .= ((i * p) * x) by RLVECT_1: 4

      .= (i * (p * x)) by VECTSP_1:def 16

      .= ( 0. ( VectQuot (V,W))) by A1, Th1, ZMODUL01: 1;

      hence ( 0. ( VectQuot (V,W))) = (v + W) by VECTSP_1:def 17, a3;

    end;

    registration

      cluster -> integer for Element of INT.Ring ;

      coherence ;

    end

    registration

      cluster prime for Element of INT.Ring ;

      existence

      proof

        2 in INT by NUMBERS: 17;

        then

        reconsider p = 2 as Element of INT.Ring ;

        take p;

        p is prime by INT_2: 28;

        hence thesis;

      end;

    end

    registration

      cluster prime -> natural for integer Number;

      coherence

      proof

        let p be integer Number;

        assume p is prime;

        then p > 1 by INT_2:def 4;

        then p >= 0 ;

        then p in NAT by INT_1: 3;

        hence thesis;

      end;

    end

    definition

      let p be prime Element of INT.Ring ;

      let V be Z_Module;

      :: ZMODUL02:def11

      func Mult_Mod_pV (V,p) -> Function of [:the carrier of ( GF p), the carrier of ( VectQuot (V,(p (*) V))):], the carrier of ( VectQuot (V,(p (*) V))) means

      : Def11: for a be Element of ( GF p), i be Element of INT.Ring , x be Element of ( VectQuot (V,(p (*) V))) st a = (i mod p) holds (it . (a,x)) = ((i mod p) * x);

      existence

      proof

        defpred P[ Element of ( GF p), Element of ( VectQuot (V,(p (*) V))), Element of ( VectQuot (V,(p (*) V)))] means for i be Element of INT.Ring st $1 = (i mod p) holds $3 = ((i mod p) * $2);

        

         A1: for a be Element of ( GF p) holds for x be Element of ( VectQuot (V,(p (*) V))) holds ex z be Element of ( VectQuot (V,(p (*) V))) st P[a, x, z]

        proof

          let a be Element of ( GF p), x be Element of ( VectQuot (V,(p (*) V)));

          consider i be Nat such that

           A2: a = (i mod p) by EC_PF_1: 13;

          i in INT by INT_1:def 2;

          then

          reconsider i as Element of INT.Ring ;

          reconsider z = ((i mod p) * x) as Element of ( VectQuot (V,(p (*) V)));

           P[a, x, z] by A2;

          hence thesis;

        end;

        consider f be Function of [:the carrier of ( GF p), the carrier of ( VectQuot (V,(p (*) V))):], the carrier of ( VectQuot (V,(p (*) V))) such that

         A3: for a be Element of ( GF p) holds for x be Element of ( VectQuot (V,(p (*) V))) holds P[a, x, (f . (a,x))] from BINOP_1:sch 3( A1);

        take f;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let f1,f2 be Function of [:the carrier of ( GF p), the carrier of ( VectQuot (V,(p (*) V))):], the carrier of ( VectQuot (V,(p (*) V)));

        assume

         A4: for a be Element of ( GF p), i be Element of INT.Ring , x be Element of ( VectQuot (V,(p (*) V))) st a = (i mod p) holds (f1 . (a,x)) = ((i mod p) * x);

        assume

         A5: for a be Element of ( GF p), i be Element of INT.Ring , x be Element of ( VectQuot (V,(p (*) V))) st a = (i mod p) holds (f2 . (a,x)) = ((i mod p) * x);

        let a,x be set;

        assume

         A6: a in the carrier of ( GF p) & x in the carrier of ( VectQuot (V,(p (*) V)));

        then

        reconsider a0 = a as Element of ( GF p);

        reconsider x0 = x as Element of ( VectQuot (V,(p (*) V))) by A6;

        consider i be Nat such that

         A7: a0 = (i mod p) by EC_PF_1: 13;

        reconsider i as Element of INT.Ring by Lem1;

        

        thus (f1 . (a,x)) = ((i mod p) * x0) by A4, A7

        .= (f2 . (a,x)) by A5, A7;

      end;

    end

    definition

      let p be prime Element of INT.Ring , V be Z_Module;

      :: ZMODUL02:def12

      func Z_MQ_VectSp (V,p) -> non empty strict ModuleStr over ( GF p) equals ModuleStr (# the carrier of ( VectQuot (V,(p (*) V))), the addF of ( VectQuot (V,(p (*) V))), the ZeroF of ( VectQuot (V,(p (*) V))), ( Mult_Mod_pV (V,p)) #);

      coherence ;

    end

    registration

      let p be prime Element of INT.Ring , V be Z_Module;

      cluster ( Z_MQ_VectSp (V,p)) -> scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian;

      coherence

      proof

        set M = ( Z_MQ_VectSp (V,p));

        set F = ( GF p);

        set AD = the addF of ( VectQuot (V,(p (*) V)));

        set ML = ( lmultCoset (V,(p (*) V)));

        thus M is scalar-distributive

        proof

          let x,y be Element of F, v be Element of M;

          consider i be Nat such that

           A1: x = (i mod p) by EC_PF_1: 13;

          reconsider i as Element of INT.Ring by Lem1;

          consider j be Nat such that

           A2: y = (j mod p) by EC_PF_1: 13;

          reconsider j as Element of INT.Ring by Lem1;

          reconsider v1 = v as Element of ( VectQuot (V,(p (*) V)));

          

           A3: (x + y) = ((i + j) mod p) by A1, A2, EC_PF_1: 15

          .= (((i mod p) + (j mod p)) mod p) by EULER_2: 6;

          

           A4: (x * v) = ((i mod p) * v1) by Def11, A1;

          

           A5: (y * v) = ((j mod p) * v1) by Def11, A2;

          ((((i mod p) + (j mod p)) mod p) * v1) = (((i mod p) + (j mod p)) * v1) by Th2

          .= (((i mod p) * v1) + ((j mod p) * v1)) by VECTSP_1:def 15;

          hence thesis by A3, A4, A5, Def11;

        end;

        thus M is vector-distributive

        proof

          let x be Element of F, v,w be Element of M;

          consider i be Nat such that

           A6: x = (i mod p) by EC_PF_1: 13;

          reconsider i as Element of INT.Ring by Lem1;

          reconsider v1 = v, w1 = w as Element of ( VectQuot (V,(p (*) V)));

          

           A7: (x * w) = ((i mod p) * w1) by Def11, A6;

          

          thus (x * (v + w)) = ((i mod p) * (v1 + w1)) by Def11, A6

          .= (((i mod p) * v1) + ((i mod p) * w1)) by VECTSP_1:def 14

          .= ((x * v) + (x * w)) by A6, A7, Def11;

        end;

        thus M is scalar-associative

        proof

          let x,y be Element of F, v be Element of M;

          consider i be Nat such that

           A8: x = (i mod p) by EC_PF_1: 13;

          reconsider i as Element of INT.Ring by Lem1;

          consider j be Nat such that

           A9: y = (j mod p) by EC_PF_1: 13;

          reconsider j as Element of INT.Ring by Lem1;

          reconsider v1 = v as Element of ( VectQuot (V,(p (*) V)));

          

           A10: (x * y) = ((i * j) mod p) by A8, A9, EC_PF_1: 18;

          

           A11: (y * v) = ((j mod p) * v1) by Def11, A9;

          

           A12: (x * (y * v)) = ((i mod p) * ((j mod p) * v1)) by A8, A11, Def11;

          (((i * j) mod p) * v1) = ((i * j) * v1) by Th2

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

          .= (i * ((j mod p) * v1)) by Th2

          .= ((i mod p) * ((j mod p) * v1)) by Th2;

          hence thesis by A10, A12, Def11;

        end;

        thus M is scalar-unital

        proof

          let v be Element of M;

          reconsider v1 = v as Element of ( VectQuot (V,(p (*) V)));

          consider i be Nat such that

           A13: ( 1. F) = (i mod p) by EC_PF_1: 13;

          reconsider i as Element of INT.Ring by Lem1;

          

          thus (( 1. F) * v) = ((i mod p) * v1) by Def11, A13

          .= (( 1. INT.Ring ) * v1) by A13, EC_PF_1: 12

          .= v by VECTSP_1:def 17;

        end;

        thus M is add-associative

        proof

          let u,v,w be Element of M;

          reconsider u1 = u, v1 = v, w1 = w as Element of ( VectQuot (V,(p (*) V)));

          

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

          .= (u1 + (v1 + w1)) by RLVECT_1:def 3

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

        end;

        thus M is right_zeroed

        proof

          let u be Element of M;

          reconsider u1 = u as Element of ( VectQuot (V,(p (*) V)));

          

          thus (u + ( 0. M)) = (u1 + ( 0. ( VectQuot (V,(p (*) V)))))

          .= u by RLVECT_1:def 4;

        end;

        thus M is right_complementable

        proof

          let v be Element of M;

          reconsider v1 = v as Element of ( VectQuot (V,(p (*) V)));

          reconsider w = ( - v1) as Element of M;

          take w;

          

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

          .= ( 0. ( VectQuot (V,(p (*) V)))) by RLVECT_1: 5

          .= ( 0. M);

        end;

        let v,w be Element of M;

        reconsider v1 = v, w1 = w as Element of ( VectQuot (V,(p (*) V)));

        

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

        .= (w1 + v1)

        .= (w + v);

      end;

    end

    definition

      let p be prime Element of INT.Ring , V be Z_Module, v be VECTOR of V;

      :: ZMODUL02:def13

      func ZMtoMQV (V,p,v) -> Vector of ( Z_MQ_VectSp (V,p)) equals (v + (p (*) V));

      correctness

      proof

        set vq = (v + (p (*) V));

        vq is Coset of (p (*) V) by VECTSP_4:def 6;

        then vq in the set of all A where A be Coset of (p (*) V);

        then vq is Element of ( CosetSet (V,(p (*) V)));

        hence thesis by VECTSP10:def 6;

      end;

    end

    definition

      let R be Ring;

      let X be LeftMod of R;

      :: ZMODUL02:def14

      func Mult_INT* (X) -> Function of [:the carrier of R, the carrier of X:], the carrier of X equals the lmult of X;

      correctness ;

    end

    definition

      let R be Ring;

      let X be LeftMod of R;

      :: ZMODUL02:def15

      func modetrans (X) -> non empty strict ModuleStr over R equals ModuleStr (# the carrier of X, the addF of X, the ZeroF of X, ( Mult_INT* X) #);

      coherence ;

    end

    registration

      let R be Ring;

      let X be LeftMod of R;

      cluster ( modetrans X) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        set X0 = the carrier of X;

        set Z0 = the ZeroF of X;

        set ADD = the addF of X;

        set LMLT = ( Mult_INT* X);

        set XP = ModuleStr (# X0, ADD, Z0, LMLT #);

        

         A1: XP is vector-distributive

        proof

          let x be Scalar of R;

          let v,w be Element of XP;

          set x1 = x;

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

          

          thus (x * (v + w)) = (x1 * (v1 + w1))

          .= ((x1 * v1) + (x1 * w1)) by VECTSP_1:def 14

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

        end;

        

         A2: XP is scalar-distributive

        proof

          let x,y be Scalar of R;

          let v be Element of XP;

          set x1 = x, y1 = y;

          reconsider v1 = v as Element of X;

          

          thus ((x + y) * v) = ((x1 + y1) * v1)

          .= ((x1 * v1) + (y1 * v1)) by VECTSP_1:def 15

          .= ((x * v) + (y * v));

        end;

        

         A3: XP is scalar-associative

        proof

          let x,y be Scalar of R;

          let v be Element of XP;

          set x1 = x, y1 = y;

          reconsider v1 = v as Element of X;

          

          thus ((x * y) * v) = ((x1 * y1) * v1)

          .= (x1 * (y1 * v1)) by VECTSP_1:def 16

          .= (x * (y * v));

        end;

        

         A4: XP is scalar-unital

        proof

          let v be Element of XP;

          reconsider v1 = v as Element of X;

          

          thus (( 1. R) * v) = (( 1. R) * v1)

          .= v1 by VECTSP_1:def 17

          .= v;

        end;

         A5:

        now

          let u,v,w be Element of XP;

          reconsider u1 = u, v1 = v, w1 = w as Element of X;

          

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

          .= ((u1 + v1) + w1) by RLVECT_1:def 3

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

        end;

         A6:

        now

          let v be Element of XP;

          reconsider v1 = v as Element of X;

          

          thus (v + ( 0. XP)) = (v1 + ( 0. X))

          .= v by RLVECT_1:def 4;

        end;

         A7:

        now

          let v be Element of XP;

          reconsider v1 = v as Element of X;

          consider w1 be Element of X such that

           A8: (v1 + w1) = ( 0. X) by ALGSTR_0:def 11;

          reconsider w = w1 as Element of XP;

          (v + w) = ( 0. XP) by A8;

          hence v is right_complementable;

        end;

        now

          let v,w be Element of XP;

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

          

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

          .= (w1 + v1)

          .= (w + v);

        end;

        hence thesis by A1, A2, A3, A4, A5, A6, A7;

      end;

    end

    definition

      ::$Canceled

    end

    ::$Canceled

    begin

    reserve K,L,L1,L2,L3 for Linear_Combination of V;

    theorem :: ZMODUL02:8

    for R be Ring holds for V be LeftMod of R, L be Linear_Combination of V, v be Element of V holds (L . v) = ( 0. R) iff not v in ( Carrier L)

    proof

      let R be Ring;

      let V be LeftMod of R, L be Linear_Combination of V, v be Element of V;

      thus (L . v) = ( 0. R) implies not v in ( Carrier L)

      proof

        assume

         A1: (L . v) = ( 0. R);

        assume not thesis;

        then ex u be Element of V st u = v & (L . u) <> ( 0. R);

        hence thesis by A1;

      end;

      assume not v in ( Carrier L);

      hence thesis;

    end;

    theorem :: ZMODUL02:9

    for R be Ring holds for V be LeftMod of R, v be Element of V holds (( ZeroLC V) . v) = ( 0. R)

    proof

      let R be Ring;

      let V be LeftMod of R, v be Element of V;

      ( Carrier ( ZeroLC V)) = {} & not v in {} by VECTSP_6:def 3;

      hence thesis;

    end;

    reserve a,b for Element of R;

    reserve G,H1,H2,F,F1,F2,F3 for FinSequence of V;

    reserve A,B for Subset of V,

v1,v2,v3,u1,u2,u3 for Vector of V,

f for Function of V, R,

i for Element of NAT ;

    reserve l,l1,l2 for Linear_Combination of A;

    theorem :: ZMODUL02:10

    A c= B implies l is Linear_Combination of B by VECTSP_6: 4;

    theorem :: ZMODUL02:11

    

     Th11: ( ZeroLC V) is Linear_Combination of A by VECTSP_6: 5;

    theorem :: ZMODUL02:12

    for l be Linear_Combination of ( {} the carrier of V) holds l = ( ZeroLC V) by VECTSP_6: 6;

    theorem :: ZMODUL02:13

    i in ( dom F) & v = (F . i) implies ((f (#) F) . i) = ((f . v) * v) by VECTSP_6: 8;

    theorem :: ZMODUL02:14

    (f (#) ( <*> the carrier of V)) = ( <*> the carrier of V) by VECTSP_6: 9;

    theorem :: ZMODUL02:15

    (f (#) <*v*>) = <*((f . v) * v)*> by VECTSP_6: 10;

    theorem :: ZMODUL02:16

    (f (#) <*v1, v2*>) = <*((f . v1) * v1), ((f . v2) * v2)*> by VECTSP_6: 11;

    theorem :: ZMODUL02:17

    (f (#) <*v1, v2, v3*>) = <*((f . v1) * v1), ((f . v2) * v2), ((f . v3) * v3)*> by VECTSP_6: 12;

    theorem :: ZMODUL02:18

    R is non degenerated implies (A <> {} & A is linearly-closed iff for l holds ( Sum l) in A) by VECTSP_6: 14;

    theorem :: ZMODUL02:19

    ( Sum ( ZeroLC V)) = ( 0. V) by VECTSP_6: 15;

    theorem :: ZMODUL02:20

    for l be Linear_Combination of ( {} the carrier of V) holds ( Sum l) = ( 0. V) by VECTSP_6: 16;

    theorem :: ZMODUL02:21

    for l be Linear_Combination of {v} holds ( Sum l) = ((l . v) * v) by VECTSP_6: 17;

    theorem :: ZMODUL02:22

    

     Th22: v1 <> v2 implies for l be Linear_Combination of {v1, v2} holds ( Sum l) = (((l . v1) * v1) + ((l . v2) * v2)) by VECTSP_6: 18;

    theorem :: ZMODUL02:23

    ( Carrier L) = {} implies ( Sum L) = ( 0. V) by VECTSP_6: 19;

    theorem :: ZMODUL02:24

    

     Th24: ( Carrier L) = {v} implies ( Sum L) = ((L . v) * v) by VECTSP_6: 20;

    theorem :: ZMODUL02:25

    ( Carrier L) = {v1, v2} & v1 <> v2 implies ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2)) by VECTSP_6: 21;

    theorem :: ZMODUL02:26

    ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2)) by VECTSP_6: 23;

    theorem :: ZMODUL02:27

    

     Th27: L1 is Linear_Combination of A & L2 is Linear_Combination of A implies (L1 + L2) is Linear_Combination of A by VECTSP_6: 24;

    theorem :: ZMODUL02:28

    

     Th28: (L1 + (L2 + L3)) = ((L1 + L2) + L3) by VECTSP_6: 26;

    registration

      let R, V, L;

      reduce (L + ( ZeroLC V)) to L;

      reducibility by VECTSP_6: 27;

    end

    theorem :: ZMODUL02:29

    for V be Z_Module, a be Element of INT.Ring , L be Linear_Combination of V holds a <> ( 0. INT.Ring ) implies ( Carrier (a * L)) = ( Carrier L)

    proof

      let V be Z_Module, a be Element of INT.Ring , L be Linear_Combination of V;

      set R = INT.Ring ;

      set T = { u where u be Vector of V : ((a * L) . u) <> ( 0. R) };

      set S = { v where v be Vector of V : (L . v) <> ( 0. R) };

      assume

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

      T = S

      proof

        thus T c= S

        proof

          let x be object;

          assume x in T;

          then

          consider u be Vector of V such that

           A2: x = u and

           A3: ((a * L) . u) <> ( 0. R);

          ((a * L) . u) = (a * (L . u)) by VECTSP_6:def 9;

          then (L . u) <> ( 0. R) by A3;

          hence thesis by A2;

        end;

        let x be object;

        assume x in S;

        then

        consider v be Vector of V such that

         A4: x = v and

         A5: (L . v) <> ( 0. R);

        ((a * L) . v) = (a * (L . v)) by VECTSP_6:def 9;

        then ((a * L) . v) <> ( 0. R) by A1, A5;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL02:30

    (( 0. R) * L) = ( ZeroLC V) by VECTSP_6: 30;

    theorem :: ZMODUL02:31

    

     Th31: L is Linear_Combination of A implies (a * L) is Linear_Combination of A by VECTSP_6: 31;

    theorem :: ZMODUL02:32

    

     Th32: ((a + b) * L) = ((a * L) + (b * L)) by VECTSP_6: 32;

    theorem :: ZMODUL02:33

    

     Th33: (a * (L1 + L2)) = ((a * L1) + (a * L2)) by VECTSP_6: 33;

    theorem :: ZMODUL02:34

    

     Th34: (a * (b * L)) = ((a * b) * L) by VECTSP_6: 34;

    registration

      let R, V, L;

      reduce (( 1. R) * L) to L;

      reducibility by VECTSP_6: 35;

    end

    theorem :: ZMODUL02:35

    (( - L) . v) = ( - (L . v)) by VECTSP_6: 36;

    theorem :: ZMODUL02:36

    (L1 + L2) = ( ZeroLC V) implies L2 = ( - L1) by VECTSP_6: 37;

    theorem :: ZMODUL02:37

    ( Carrier ( - L)) = ( Carrier L) by VECTSP_6: 38;

    theorem :: ZMODUL02:38

    L is Linear_Combination of A implies ( - L) is Linear_Combination of A by VECTSP_6: 39;

    theorem :: ZMODUL02:39

    ((L1 - L2) . v) = ((L1 . v) - (L2 . v)) by VECTSP_6: 40;

    theorem :: ZMODUL02:40

    ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier L2)) by VECTSP_6: 41;

    theorem :: ZMODUL02:41

    L1 is Linear_Combination of A & L2 is Linear_Combination of A implies (L1 - L2) is Linear_Combination of A by VECTSP_6: 42;

    theorem :: ZMODUL02:42

    

     Th42: (L - L) = ( ZeroLC V) by VECTSP_6: 43;

    definition

      let R, V;

      :: ZMODUL02:def29

      func LinComb (V) -> set means

      : Def29: x in it iff x is Linear_Combination of V;

      existence

      proof

        defpred P[ object] means $1 is Linear_Combination of V;

        consider A be set such that

         A1: for x be object holds x in A iff x in ( Funcs (the carrier of V,the carrier of R)) & P[x] from XBOOLE_0:sch 1;

        take A;

        let x;

        thus x in A implies x is Linear_Combination of V by A1;

        assume x is Linear_Combination of V;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be set;

        assume

         A2: for x holds x in D1 iff x is Linear_Combination of V;

        assume

         A3: for x holds x in D2 iff x is Linear_Combination of V;

        thus D1 c= D2

        proof

          let x be object;

          assume x in D1;

          then x is Linear_Combination of V by A2;

          hence thesis by A3;

        end;

        let x be object;

        assume x in D2;

        then x is Linear_Combination of V by A3;

        hence thesis by A2;

      end;

    end

    registration

      let R, V;

      cluster ( LinComb V) -> non empty;

      coherence

      proof

        set x = the Linear_Combination of V;

        x in ( LinComb V) by Def29;

        hence thesis;

      end;

    end

    reserve e,e1,e2 for Element of ( LinComb V);

    definition

      let R, V, e;

      :: ZMODUL02:def30

      func @ e -> Linear_Combination of V equals e;

      coherence by Def29;

    end

    definition

      let R, V, L;

      :: ZMODUL02:def31

      func @ L -> Element of ( LinComb V) equals L;

      coherence by Def29;

    end

    definition

      let R, V;

      :: ZMODUL02:def32

      func LCAdd (V) -> BinOp of ( LinComb V) means

      : Def32: for e1, e2 holds (it . (e1,e2)) = (( @ e1) + ( @ e2));

      existence

      proof

        deffunc F( Element of ( LinComb V), Element of ( LinComb V)) = ( @ (( @ $1) + ( @ $2)));

        consider o be BinOp of ( LinComb V) such that

         A1: for e1, e2 holds (o . (e1,e2)) = F(e1,e2) from BINOP_1:sch 4;

        take o;

        let e1, e2;

        

        thus (o . (e1,e2)) = ( @ (( @ e1) + ( @ e2))) by A1

        .= (( @ e1) + ( @ e2));

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( LinComb V);

        assume

         A2: for e1, e2 holds (o1 . (e1,e2)) = (( @ e1) + ( @ e2));

        assume

         A3: for e1, e2 holds (o2 . (e1,e2)) = (( @ e1) + ( @ e2));

        now

          let e1, e2;

          

          thus (o1 . (e1,e2)) = (( @ e1) + ( @ e2)) by A2

          .= (o2 . (e1,e2)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let R, V;

      :: ZMODUL02:def33

      func LCMult (V) -> Function of [:the carrier of R, ( LinComb V):], ( LinComb V) means

      : Def33: for a, e holds (it . [a, e]) = (a * ( @ e));

      existence

      proof

        defpred P[ Element of R, Element of ( LinComb V), set] means ex a st a = $1 & $3 = (a * ( @ $2));

        

         A1: for x be Element of R, e1 holds ex e2 st P[x, e1, e2]

        proof

          let x be Element of R, e1;

          take ( @ (x * ( @ e1)));

          take x;

          thus thesis;

        end;

        consider g be Function of [:the carrier of R, ( LinComb V):], ( LinComb V) such that

         A2: for x be Element of R, e holds P[x, e, (g . (x,e))] from BINOP_1:sch 3( A1);

        take g;

        let a, e;

        reconsider a0 = a as Element of R;

        ex b st b = a0 & (g . (a0,e)) = (b * ( @ e)) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let g1,g2 be Function of [:the carrier of R, ( LinComb V):], ( LinComb V);

        assume

         A3: for a, e holds (g1 . [a, e]) = (a * ( @ e));

        assume

         A4: for a, e holds (g2 . [a, e]) = (a * ( @ e));

        now

          let x be Element of R, e;

          

          thus (g1 . (x,e)) = (x * ( @ e)) by A3

          .= (g2 . (x,e)) by A4;

        end;

        hence thesis;

      end;

    end

    definition

      let R, V;

      :: ZMODUL02:def34

      func LC_Z_Module V -> ModuleStr over R equals ModuleStr (# ( LinComb V), ( LCAdd V), ( @ ( ZeroLC V)), ( LCMult V) #);

      coherence ;

    end

    registration

      let R, V;

      cluster ( LC_Z_Module V) -> strict non empty;

      coherence ;

    end

    registration

      let R, V;

      cluster ( LC_Z_Module V) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        set S = ( LC_Z_Module V);

         A1:

        now

          let v,u be Vector of S, K, L;

          

           A2: ( @ ( @ K)) = K & ( @ ( @ L)) = L;

          assume v = K & u = L;

          hence (v + u) = (K + L) by A2, Def32;

        end;

        thus S is Abelian

        proof

          let u,v be Element of S;

          reconsider K = u, L = v as Linear_Combination of V by Def29;

          

          thus (u + v) = (K + L) by A1

          .= (L + K)

          .= (v + u) by A1;

        end;

        thus S is add-associative

        proof

          let u,v,w be Element of S;

          reconsider L = u, K = v, M = w as Linear_Combination of V by Def29;

          

           A3: (v + w) = (K + M) by A1;

          (u + v) = (L + K) by A1;

          

          hence ((u + v) + w) = ((L + K) + M) by A1

          .= (L + (K + M)) by Th28

          .= (u + (v + w)) by A1, A3;

        end;

        thus S is right_zeroed

        proof

          let v be Element of S;

          reconsider K = v as Linear_Combination of V by Def29;

          

          thus (v + ( 0. S)) = (K + ( ZeroLC V)) by A1

          .= v;

        end;

        thus S is right_complementable

        proof

          let v be Element of S;

          reconsider K = v as Linear_Combination of V by Def29;

          ( - K) in the carrier of S by Def29;

          then ( - K) in S;

          then ( - K) = ( vector (S,( - K))) by RLVECT_2:def 1;

          

          then (v + ( vector (S,( - K)))) = (K - K) by A1

          .= ( 0. S) by Th42;

          hence ex w be Vector of S st (v + w) = ( 0. S);

        end;

         A4:

        now

          let v be Vector of S, L, a;

          

           A5: ( @ ( @ L)) = L;

          assume v = L;

          hence (a * v) = (a * L) by A5, Def33;

        end;

        thus S is vector-distributive

        proof

          let a be Element of R;

          let v,w be Vector of S;

          reconsider K = v, M = w as Linear_Combination of V by Def29;

          

           A6: (a * v) = (a * K) & (a * w) = (a * M) by A4;

          (v + w) = (K + M) by A1;

          

          then (a * (v + w)) = (a * (K + M)) by A4

          .= ((a * K) + (a * M)) by Th33

          .= ((a * v) + (a * w)) by A1, A6;

          hence thesis;

        end;

        thus S is scalar-distributive

        proof

          let a,b be Element of R;

          let v be Vector of S;

          reconsider K = v as Linear_Combination of V by Def29;

          

           A7: (a * v) = (a * K) & (b * v) = (b * K) by A4;

          ((a + b) * v) = ((a + b) * K) by A4

          .= ((a * K) + (b * K)) by Th32

          .= ((a * v) + (b * v)) by A1, A7;

          hence thesis;

        end;

        thus S is scalar-associative

        proof

          let a,b be Element of R;

          let v be Vector of S;

          reconsider K = v as Linear_Combination of V by Def29;

          

           A8: (b * v) = (b * K) by A4;

          ((a * b) * v) = ((a * b) * K) by A4

          .= (a * (b * K)) by Th34

          .= (a * (b * v)) by A4, A8;

          hence thesis;

        end;

        let v be Vector of S;

        reconsider K = v as Linear_Combination of V by Def29;

        

        thus (( 1. R) * v) = (( 1. R) * K) by A4

        .= v;

      end;

    end

    theorem :: ZMODUL02:43

    the carrier of ( LC_Z_Module V) = ( LinComb V);

    theorem :: ZMODUL02:44

    ( 0. ( LC_Z_Module V)) = ( ZeroLC V);

    theorem :: ZMODUL02:45

    the addF of ( LC_Z_Module V) = ( LCAdd V);

    theorem :: ZMODUL02:46

    the lmult of ( LC_Z_Module V) = ( LCMult V);

    theorem :: ZMODUL02:47

    

     Th47: (( vector (( LC_Z_Module V),L1)) + ( vector (( LC_Z_Module V),L2))) = (L1 + L2)

    proof

      set v2 = ( vector (( LC_Z_Module V),L2));

      

       A1: L1 = ( @ ( @ L1)) & L2 = ( @ ( @ L2));

      L2 in the carrier of ( LC_Z_Module V) by Def29;

      then

       A2: L2 in ( LC_Z_Module V);

      L1 in the carrier of ( LC_Z_Module V) by Def29;

      then L1 in ( LC_Z_Module V);

      

      hence (( vector (( LC_Z_Module V),L1)) + ( vector (( LC_Z_Module V),L2))) = (( LCAdd V) . [L1, v2]) by RLVECT_2:def 1

      .= (( LCAdd V) . (( @ L1),( @ L2))) by A2, RLVECT_2:def 1

      .= (L1 + L2) by A1, Def32;

    end;

    theorem :: ZMODUL02:48

    

     Th48: (a * ( vector (( LC_Z_Module V),L))) = (a * L)

    proof

      

       A1: ( @ ( @ L)) = L;

      L in the carrier of ( LC_Z_Module V) by Def29;

      then L in ( LC_Z_Module V);

      

      hence (a * ( vector (( LC_Z_Module V),L))) = (( LCMult V) . [a, ( @ L)]) by RLVECT_2:def 1

      .= (a * L) by A1, Def33;

    end;

    theorem :: ZMODUL02:49

    

     Th49: ( - ( vector (( LC_Z_Module V),L))) = ( - L)

    proof

      

      thus ( - ( vector (( LC_Z_Module V),L))) = (( - ( 1. R)) * ( vector (( LC_Z_Module V),L))) by ZMODUL01: 2

      .= ( - L) by Th48;

    end;

    theorem :: ZMODUL02:50

    (( vector (( LC_Z_Module V),L1)) - ( vector (( LC_Z_Module V),L2))) = (L1 - L2)

    proof

      ( - L2) in ( LinComb V) by Def29;

      then

       A1: ( - L2) in ( LC_Z_Module V);

      ( - ( vector (( LC_Z_Module V),L2))) = ( - L2) by Th49

      .= ( vector (( LC_Z_Module V),( - L2))) by A1, RLVECT_2:def 1;

      hence thesis by Th47;

    end;

    definition

      let R, V, A;

      :: ZMODUL02:def35

      func LC_Z_Module (A) -> strict Submodule of ( LC_Z_Module V) means the carrier of it = the set of all l;

      existence

      proof

        set X = the set of all l;

        X c= the carrier of ( LC_Z_Module V)

        proof

          let x be object;

          assume x in X;

          then ex l st x = l;

          hence thesis by Def29;

        end;

        then

        reconsider X as Subset of ( LC_Z_Module V);

        

         A1: X is linearly-closed

        proof

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

          proof

            let v,u be Vector of ( LC_Z_Module V);

            assume that

             A2: v in X and

             A3: u in X;

            consider l1 such that

             A4: v = l1 by A2;

            consider l2 such that

             A5: u = l2 by A3;

            

             A6: u = ( vector (( LC_Z_Module V),l2)) by A5, RLVECT_2:def 1, RLVECT_1: 1;

            v = ( vector (( LC_Z_Module V),l1)) by A4, RLVECT_2:def 1, RLVECT_1: 1;

            then (v + u) = (l1 + l2) by A6, Th47;

            then (v + u) is Linear_Combination of A by Th27;

            hence thesis;

          end;

          let a be Element of R;

          let v be Vector of ( LC_Z_Module V);

          assume v in X;

          then

          consider l such that

           A7: v = l;

          (a * v) = (a * ( vector (( LC_Z_Module V),l))) by A7, RLVECT_2:def 1, RLVECT_1: 1

          .= (a * l) by Th48;

          then (a * v) is Linear_Combination of A by Th31;

          hence thesis;

        end;

        ( ZeroLC V) is Linear_Combination of A by Th11;

        then ( ZeroLC V) in X;

        hence thesis by A1, ZMODUL01: 50;

      end;

      uniqueness by ZMODUL01: 45;

    end

    begin

    reserve W,W1,W2,W3 for Submodule of V;

    reserve v,v1,v2,u for Vector of V;

    reserve A,B,C for Subset of V;

    reserve T for finite Subset of V;

    reserve L,L1,L2 for Linear_Combination of V;

    reserve l for Linear_Combination of A;

    reserve F,G,H for FinSequence of V;

    reserve f,g for Function of V, R;

    theorem :: ZMODUL02:51

    (f (#) (F ^ G)) = ((f (#) F) ^ (f (#) G)) by VECTSP_6: 13;

    theorem :: ZMODUL02:52

    ( Sum (L1 + L2)) = (( Sum L1) + ( Sum L2)) by VECTSP_6: 44;

    theorem :: ZMODUL02:53

    ( Sum (a * L)) = (a * ( Sum L)) by MOD_3: 3;

    theorem :: ZMODUL02:54

    ( Sum ( - L)) = ( - ( Sum L)) by VECTSP_6: 46;

    theorem :: ZMODUL02:55

    ( Sum (L1 - L2)) = (( Sum L1) - ( Sum L2)) by VECTSP_6: 47;

    theorem :: ZMODUL02:56

    R is commutative & A c= B & B is linearly-independent implies A is linearly-independent by VECTSP_7: 1;

    theorem :: ZMODUL02:57

    

     Th57: R is non degenerated & A is linearly-independent implies not ( 0. V) in A by VECTSP_7: 2;

    theorem :: ZMODUL02:58

    ( {} the carrier of V) is linearly-independent;

    registration

      let R be Ring;

      let V be LeftMod of R;

      cluster linearly-independent for Subset of V;

      existence

      proof

        take ( {} the carrier of V);

        thus thesis;

      end;

    end

    theorem :: ZMODUL02:59

    R is non degenerated & V is Mult-cancelable implies ( {v} is linearly-independent iff v <> ( 0. V))

    proof

      assume

       A1: R is non degenerated & V is Mult-cancelable;

      thus {v} is linearly-independent implies v <> ( 0. V)

      proof

        assume {v} is linearly-independent;

        then not ( 0. V) in {v} by Th57, A1;

        hence thesis by TARSKI:def 1;

      end;

      assume

       A2: v <> ( 0. V);

      let l be Linear_Combination of {v};

      

       A3: ( Carrier l) c= {v} by VECTSP_6:def 4;

      assume

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

      now

        per cases by A3, ZFMISC_1: 33;

          suppose ( Carrier l) = {} ;

          hence thesis;

        end;

          suppose

           A5: ( Carrier l) = {v};

          then

           A6: ( 0. V) = ((l . v) * v) by A4, Th24;

          now

            assume v in ( Carrier l);

            then ex u st v = u & (l . u) <> ( 0. R);

            hence contradiction by A2, A6, A1;

          end;

          hence thesis by A5, TARSKI:def 1;

        end;

      end;

      hence thesis;

    end;

    registration

      let R be non degenerated Ring;

      let V be LeftMod of R;

      cluster {( 0. V)} -> linearly-dependent;

      coherence

      proof

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

        hence thesis by Th57;

      end;

    end

    theorem :: ZMODUL02:60

    

     Th60: R is commutative non degenerated & {v1, v2} is linearly-independent implies v1 <> ( 0. V) by VECTSP_7: 4;

    theorem :: ZMODUL02:61

    R is commutative non degenerated implies {v, ( 0. V)} is linearly-dependent by Th60;

    theorem :: ZMODUL02:62

    

     Th62: R = INT.Ring & V is Mult-cancelable implies (v1 <> v2 & {v1, v2} is linearly-independent iff v2 <> ( 0. V) & for a,b be Element of R st b <> ( 0. R) holds (b * v1) <> (a * v2))

    proof

      assume

       A1: R = INT.Ring & V is Mult-cancelable;

      thus v1 <> v2 & {v1, v2} is linearly-independent implies v2 <> ( 0. V) & for a,b be Element of R st b <> ( 0. R) holds (b * v1) <> (a * v2)

      proof

        set N0 = ( 0. R), N1 = ( - ( 1. R));

        deffunc F( Element of V) = ( 0. R);

        assume that

         A2: v1 <> v2 and

         A3: {v1, v2} is linearly-independent;

        thus v2 <> ( 0. V) by A3, Th60, A1;

        let a,b be Element of R;

        assume

         A4: b <> ( 0. R);

        set Na = a;

        set Nb = ( - b);

        consider f such that

         A5: (f . v1) = Nb & (f . v2) = Na and

         A6: for v be Element of V st v <> v1 & v <> v2 holds (f . v) = F(v) from FUNCT_2:sch 7( A2);

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

        now

          let v;

          assume not v in {v1, v2};

          then v <> v1 & v <> v2 by TARSKI:def 2;

          hence (f . v) = ( 0. R) by A6;

        end;

        then

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

        ( Carrier f) c= {v1, v2}

        proof

          let x be object;

          assume x in ( Carrier f);

          then

           A7: ex u st x = u & (f . u) <> ( 0. R);

          assume not x in {v1, v2};

          then x <> v1 & x <> v2 by TARSKI:def 2;

          hence thesis by A6, A7;

        end;

        then

        reconsider f as Linear_Combination of {v1, v2} by VECTSP_6:def 4;

        Nb <> ( 0. R) by A4, VECTSP_1: 28;

        then (f . v1) <> ( 0. R) by A5;

        then

         A8: v1 in ( Carrier f);

        set w = (a * v2);

        assume

         A9: (b * v1) = (a * v2);

        ( Sum f) = ((Nb * v1) + (Na * v2)) by A2, A5, Th22

        .= ((b * ( - v1)) + (Na * v2)) by ZMODUL01: 5, A1

        .= (( - w) + w) by A9, ZMODUL01: 6, A1

        .= ( - (w - w)) by RLVECT_1: 33

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

        .= ( 0. V) by RLVECT_1: 12;

        then ( Carrier f) = {} by VECTSP_7:def 1, A3;

        hence thesis by A8;

      end;

      assume

       A10: v2 <> ( 0. V);

      assume

       A11: for a,b be Element of R st b <> ( 0. R) holds (b * v1) <> (a * v2);

      

       A12: (( 1. R) * v2) = v2 & (( 1. R) * v1) = v1 by VECTSP_1:def 17;

      hence v1 <> v2 by A11, A1;

      let l be Linear_Combination of {v1, v2};

      assume that

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

       A14: ( Carrier l) <> {} ;

      

       A15: ( 0. V) = (((l . v1) * v1) + ((l . v2) * v2)) by A11, A12, A13, Th22, A1;

      set x = the Element of ( Carrier l);

      ( Carrier l) c= {v1, v2} by VECTSP_6:def 4;

      then

       A16: x in {v1, v2} by A14;

      x in ( Carrier l) by A14;

      then

       A17: ex u st x = u & (l . u) <> ( 0. R);

      now

        per cases by A17, A16, TARSKI:def 2;

          suppose

           A18: (l . v1) <> ( 0. R);

          ((l . v1) * v1) = ( - ((l . v2) * v2)) by A15, RLVECT_1: 6

          .= (( - ( 1. R)) * ((l . v2) * v2)) by ZMODUL01: 2

          .= ((( - ( 1. R)) * (l . v2)) * v2) by VECTSP_1:def 16;

          hence thesis by A11, A18;

        end;

          suppose

           A19: (l . v2) <> ( 0. R) & (l . v1) = ( 0. R);

          ( 0. V) = (((l . v1) * v1) + ((l . v2) * v2)) by A11, A12, A13, Th22, A1

          .= (( 0. V) + ((l . v2) * v2)) by A19, ZMODUL01: 1, A1

          .= ((l . v2) * v2) by RLVECT_1: 4;

          hence thesis by A1, A10, A19;

        end;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL02:63

    R = INT.Ring & V is Mult-cancelable implies (v1 <> v2 & {v1, v2} is linearly-independent iff for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = ( 0. R) & b = ( 0. R))

    proof

      assume

       A1: R = INT.Ring & V is Mult-cancelable;

      thus v1 <> v2 & {v1, v2} is linearly-independent implies for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = ( 0. R) & b = ( 0. R)

      proof

        assume

         A2: v1 <> v2 & {v1, v2} is linearly-independent;

        let a, b;

        assume that

         A3: ((a * v1) + (b * v2)) = ( 0. V) and

         A4: a <> ( 0. R) or b <> ( 0. R);

        now

          per cases by A4;

            suppose

             A5: a <> ( 0. R);

            (a * v1) = ( - (b * v2)) by A3, RLVECT_1: 6

            .= (( - ( 1. R)) * (b * v2)) by ZMODUL01: 2

            .= ((( - ( 1. R)) * b) * v2) by VECTSP_1:def 16;

            hence thesis by A1, A2, A5, Th62;

          end;

            suppose

             A6: b <> ( 0. R);

            (b * v2) = ( - (a * v1)) by A3, RLVECT_1: 6

            .= (( - ( 1. R)) * (a * v1)) by ZMODUL01: 2

            .= ((( - ( 1. R)) * a) * v1) by VECTSP_1:def 16;

            hence thesis by A1, A2, A6, Th62;

          end;

        end;

        hence thesis;

      end;

      assume

       A7: for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = ( 0. R) & b = ( 0. R);

       A8:

      now

        let a, b;

        assume

         A9: b <> ( 0. R);

        assume (b * v1) = (a * v2);

        then (b * v1) = (( 0. V) + (a * v2)) by RLVECT_1: 4;

        

        then ( 0. V) = ((b * v1) - (a * v2)) by RLSUB_2: 61

        .= ((b * v1) + (a * ( - v2))) by A1, ZMODUL01: 6

        .= ((b * v1) + (( - a) * v2)) by A1, ZMODUL01: 5;

        hence contradiction by A9, A7;

      end;

      now

        assume

         A10: v2 = ( 0. V);

        ( 0. V) = (( 0. V) + ( 0. V)) by RLVECT_1: 4

        .= ((( 0. R) * v1) + ( 0. V)) by ZMODUL01: 1, A1

        .= ((( 0. R) * v1) + (( 1. R) * v2)) by A1, A10, ZMODUL01: 1;

        hence contradiction by A7, A1;

      end;

      hence thesis by A8, A1, Th62;

    end;

    theorem :: ZMODUL02:64

    x in ( Lin A) iff ex l st x = ( Sum l) by MOD_3: 4;

    theorem :: ZMODUL02:65

    

     Th65: x in A implies x in ( Lin A) by MOD_3: 5;

    theorem :: ZMODUL02:66

    for x be object holds x in ( (0). V) iff x = ( 0. V)

    proof

      let x be object;

      thus x in ( (0). V) implies x = ( 0. V)

      proof

        assume x in ( (0). V);

        then x in the carrier of ( (0). V);

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

        hence thesis by TARSKI:def 1;

      end;

      thus thesis by ZMODUL01: 33;

    end;

    theorem :: ZMODUL02:67

    ( Lin ( {} the carrier of V)) = ( (0). V) by MOD_3: 6;

    theorem :: ZMODUL02:68

    ( Lin A) = ( (0). V) implies A = {} or A = {( 0. V)} by MOD_3: 7;

    theorem :: ZMODUL02:69

    for V be strict LeftMod of R, A be Subset of V holds A = the carrier of V implies ( Lin A) = V

    proof

      let V be strict LeftMod of R, A be Subset of V;

      assume A = the carrier of V;

      then for v be Vector of V holds v in ( Lin A) iff v in ( (Omega). V) by Th65;

      hence thesis by ZMODUL01: 46;

    end;

    

     Lm3: W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule of (W2 /\ W3)

    proof

      assume

       A1: W1 is Submodule of W2 & W1 is Submodule of W3;

      now

        let v;

        assume v in W1;

        then v in W2 & v in W3 by A1, ZMODUL01: 23;

        hence v in (W2 /\ W3) by ZMODUL01: 94;

      end;

      hence thesis by ZMODUL01: 44;

    end;

    

     Lm4: W1 is Submodule of W3 & W2 is Submodule of W3 implies (W1 + W2) is Submodule of W3

    proof

      assume

       A1: W1 is Submodule of W3 & W2 is Submodule of W3;

      now

        let v;

        assume v in (W1 + W2);

        then

        consider v1, v2 such that

         A2: v1 in W1 & v2 in W2 and

         A3: v = (v1 + v2) by ZMODUL01: 92;

        v1 in W3 & v2 in W3 by A1, A2, ZMODUL01: 23;

        hence v in W3 by A3, ZMODUL01: 36;

      end;

      hence thesis by ZMODUL01: 44;

    end;

    theorem :: ZMODUL02:70

    A c= B implies ( Lin A) is Submodule of ( Lin B) by MOD_3: 10;

    theorem :: ZMODUL02:71

    for V be strict Z_Module, A,B be Subset of V holds ( Lin A) = V & A c= B implies ( Lin B) = V by MOD_3: 11;

    theorem :: ZMODUL02:72

    ( Lin (A \/ B)) = (( Lin A) + ( Lin B)) by MOD_3: 12;

    theorem :: ZMODUL02:73

    ( Lin (A /\ B)) is Submodule of (( Lin A) /\ ( Lin B)) by MOD_3: 13;

    begin

    theorem :: ZMODUL02:74

    W1 is Submodule of W3 implies (W1 /\ W2) is Submodule of W3

    proof

      

       A1: (W1 /\ W2) is Submodule of W1 by ZMODUL01: 105;

      assume W1 is Submodule of W3;

      hence thesis by A1, ZMODUL01: 42;

    end;

    theorem :: ZMODUL02:75

    W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule of (W2 /\ W3) by Lm3;

    theorem :: ZMODUL02:76

    W1 is Submodule of W3 & W2 is Submodule of W3 implies (W1 + W2) is Submodule of W3 by Lm4;

    theorem :: ZMODUL02:77

    W1 is Submodule of W2 implies W1 is Submodule of (W2 + W3)

    proof

      

       A1: W2 is Submodule of (W2 + W3) by ZMODUL01: 97;

      assume W1 is Submodule of W2;

      hence thesis by A1, ZMODUL01: 42;

    end;