zmodul01.miz



    begin

    registration

      cluster -> integer for Element of INT.Ring ;

      coherence ;

    end

    registration

      let a,b be Element of INT.Ring , c,d be Integer;

      identify c * d with a * b when a = c, b = d;

      compatibility

      proof

        assume

         A1: a = c & b = d;

        ( multint . (a,b)) = ( multreal . (a,b)) by INT_3:def 1

        .= (c * d) by A1, BINOP_2:def 11;

        hence thesis;

      end;

      identify c + d with a + b when a = c, b = d;

      compatibility

      proof

        assume

         A2: a = c & b = d;

        ( addint . (a,b)) = ( addreal . (a,b)) by GR_CY_1:def 1

        .= (c + d) by A2, BINOP_2:def 9;

        hence thesis;

      end;

    end

    registration

      let a be Element of INT.Ring , b be Integer;

      identify - b with - a when a = b;

      compatibility

      proof

        reconsider b9 = ( - b) as Element of INT.Ring by INT_1:def 2;

        assume b = a;

        then (b9 + a) = ( 0. INT.Ring );

        hence thesis by RLVECT_1: 6;

      end;

    end

    definition

      ::$Canceled

    end

    definition

      mode Z_Module is LeftMod of INT.Ring ;

    end

    registration

      cluster ( TrivialLMod INT.Ring ) -> trivial non empty strict;

      coherence

      proof

        ( TrivialLMod INT.Ring ) = ModuleStr (# { 0 }, op2 , op0 , ( pr2 (the carrier of INT.Ring , { 0 })) #) by MOD_2:def 1;

        then the carrier of ( TrivialLMod INT.Ring ) = { 0 };

        hence thesis;

      end;

    end

    registration

      cluster strict for Z_Module;

      existence

      proof

        take ( TrivialLMod INT.Ring );

        thus thesis;

      end;

    end

    definition

      let R be Ring;

      let V be LeftMod of R;

      mode VECTOR of V is Element of V;

    end

    reserve R for Ring;

    reserve x,y,y1 for set;

    reserve a,b for Element of R;

    reserve V for LeftMod of R;

    reserve v,w for Vector of V;

    definition

      let R be Ring;

      let IT be LeftMod of R;

      :: ZMODUL01:def7

      attr IT is Mult-cancelable means for a be Element of R holds for v be Vector of IT st (a * v) = ( 0. IT) holds a = ( 0. R) or v = ( 0. IT);

    end

    theorem :: ZMODUL01:1

    

     Th1: for V be Z_Module holds for a be Element of INT.Ring , v be Vector of V holds a = ( 0. INT.Ring ) or v = ( 0. V) implies (a * v) = ( 0. V)

    proof

      let V be Z_Module;

      let a be Element of INT.Ring , v be Vector of V;

      set R = INT.Ring ;

      set N1 = ( 1. INT.Ring ), N0 = ( 0. INT.Ring );

      assume

       A1: a = ( 0. R) or v = ( 0. V);

      now

        per cases by A1;

          suppose

           A2: a = ( 0. R);

          (v + (N0 * v)) = ((N1 * v) + (N0 * v)) by VECTSP_1:def 17

          .= ((N1 + N0) * v) by VECTSP_1:def 15

          .= v by VECTSP_1:def 17

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

          hence thesis by A2, RLVECT_1: 8;

        end;

          suppose

           A3: v = ( 0. V);

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

          .= (a * ( 0. V)) by RLVECT_1: 4

          .= ((a * ( 0. V)) + ( 0. V)) by RLVECT_1: 4;

          hence thesis by A3, RLVECT_1: 8;

        end;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL01:2

    

     Th2: ( - v) = (( - ( 1. R)) * v) by VECTSP_1: 14;

    theorem :: ZMODUL01:3

    

     Th3: for V be Z_Module, v be Vector of V holds V is Mult-cancelable & v = ( - v) implies v = ( 0. V)

    proof

      let V be Z_Module, v be Vector of V;

      assume

       A1: V is Mult-cancelable;

      set a = ( 1. INT.Ring );

      assume v = ( - v);

      

      then ( 0. V) = (v + v) by RLVECT_1:def 10

      .= ((a * v) + v) by VECTSP_1:def 17

      .= ((a * v) + (a * v)) by VECTSP_1:def 17

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

      hence thesis by A1;

    end;

    theorem :: ZMODUL01:4

    for V be Z_Module, v be Vector of V holds V is Mult-cancelable & (v + v) = ( 0. V) implies v = ( 0. V)

    proof

      let V be Z_Module, v be Vector of V;

      assume

       A1: V is Mult-cancelable;

      assume (v + v) = ( 0. V);

      then v = ( - v) by RLVECT_1:def 10;

      hence thesis by A1, Th3;

    end;

    theorem :: ZMODUL01:5

    

     Th5: for V be Z_Module, a be Element of INT.Ring , v be Vector of V holds (a * ( - v)) = (( - a) * v)

    proof

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

      

      thus (a * ( - v)) = (a * (( - ( 1. INT.Ring )) * v)) by VECTSP_1: 14

      .= ((a * ( - ( 1. INT.Ring ))) * v) by VECTSP_1:def 16

      .= (( - a) * v);

    end;

    theorem :: ZMODUL01:6

    

     Th6: for V be Z_Module, a be Element of INT.Ring , v be Vector of V holds (a * ( - v)) = ( - (a * v))

    proof

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

      set i = ( 1. INT.Ring );

      

      thus (a * ( - v)) = (( - a) * v) by Th5

      .= ((( - i) * a) * v)

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

      .= ( - (a * v)) by Th2;

    end;

    theorem :: ZMODUL01:7

    for V be Z_Module, a be Element of INT.Ring , v be Vector of V holds (( - a) * ( - v)) = (a * v)

    proof

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

      

      thus (( - a) * ( - v)) = (( - ( - a)) * v) by Th5

      .= (a * v);

    end;

    theorem :: ZMODUL01:8

    

     Th8: for V be Z_Module, a be Element of INT.Ring , v,w be Vector of V holds (a * (v - w)) = ((a * v) - (a * w))

    proof

      let V be Z_Module, a be Element of INT.Ring , v,w be Vector of V;

      

      thus (a * (v - w)) = ((a * v) + (a * ( - w))) by VECTSP_1:def 14

      .= ((a * v) - (a * w)) by Th6;

    end;

    theorem :: ZMODUL01:9

    

     Th9: for V be Z_Module, a,b be Element of INT.Ring , v be Vector of V holds ((a - b) * v) = ((a * v) - (b * v))

    proof

      let V be Z_Module, a,b be Element of INT.Ring , v be Vector of V;

      

      thus ((a - b) * v) = ((a * v) + (( - b) * v)) by VECTSP_1:def 15

      .= ((a * v) + (b * ( - v))) by Th5

      .= ((a * v) - (b * v)) by Th6;

    end;

    theorem :: ZMODUL01:10

    for V be Z_Module, a be Element of INT.Ring , v,w be Vector of V holds V is Mult-cancelable & a <> ( 0. INT.Ring ) & (a * v) = (a * w) implies v = w

    proof

      let V be Z_Module, a be Element of INT.Ring , v,w be Vector of V;

      assume

       A1: V is Mult-cancelable;

      set R = INT.Ring ;

      assume that

       A2: a <> ( 0. R) and

       A3: (a * v) = (a * w);

      ( 0. V) = ((a * v) - (a * w)) by A3, RLVECT_1: 15

      .= (a * (v - w)) by Th8;

      then (v - w) = ( 0. V) by A2, A1;

      hence thesis by RLVECT_1: 21;

    end;

    theorem :: ZMODUL01:11

    for V be Z_Module, a,b be Element of INT.Ring , v be Vector of V holds V is Mult-cancelable & v <> ( 0. V) & (a * v) = (b * v) implies a = b

    proof

      let V be Z_Module, a,b be Element of INT.Ring , v be Vector of V;

      assume

       A1: V is Mult-cancelable;

      assume that

       A2: v <> ( 0. V) and

       A3: (a * v) = (b * v);

      ( 0. V) = ((a * v) - (b * v)) by A3, RLVECT_1: 15

      .= ((a - b) * v) by Th9;

      

      then (( - b) + a) = 0 by A2, A1

      .= ( 0. INT.Ring );

      hence thesis;

    end;

    reserve u,v,w for Vector of V;

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

    reserve j,k,n for Nat;

    reserve f,f9,g for sequence of V;

    

     Lm1: ( Sum ( <*> the carrier of V)) = ( 0. V)

    proof

      set S = ( <*> the carrier of V);

      ex f st ( Sum S) = (f . ( len S)) & (f . 0 ) = ( 0. V) & for j, v st j < ( len S) & v = (S . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      hence thesis;

    end;

    

     Lm2: ( len F) = 0 implies ( Sum F) = ( 0. V)

    proof

      assume ( len F) = 0 ;

      then F = ( <*> the carrier of V);

      hence thesis by Lm1;

    end;

    theorem :: ZMODUL01:12

    

     Th12: ( len F) = ( len G) & (for k, v st k in ( dom F) & v = (G . k) holds (F . k) = (a * v)) implies ( Sum F) = (a * ( Sum G))

    proof

      defpred P[ set] means for H, I st ( len H) = ( len I) & ( len H) = $1 & (for k, v st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (a * v)) holds ( Sum H) = (a * ( Sum I));

      

       A1: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

      now

        let n;

        assume

         A2: for H, I st ( len H) = ( len I) & ( len H) = n & for k, v st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (a * v) holds ( Sum H) = (a * ( Sum I));

        let H, I;

        assume that

         A3: ( len H) = ( len I) and

         A4: ( len H) = (n + 1) and

         A5: for k, v st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (a * v);

        reconsider p = (H | ( Seg n)), q = (I | ( Seg n)) as FinSequence of the carrier of V by FINSEQ_1: 18;

        

         A6: n <= (n + 1) by NAT_1: 12;

        then

         A7: ( len q) = n by A3, A4, FINSEQ_1: 17;

        

         A8: ( len p) = n by A4, A6, FINSEQ_1: 17;

         A9:

        now

          ( len p) <= ( len H) by A4, A6, FINSEQ_1: 17;

          then

           A10: ( Seg ( len p)) c= ( Seg ( len H)) by FINSEQ_1: 5;

          

           A11: ( dom p) = ( Seg n) by A4, A6, FINSEQ_1: 17;

          let k, v;

          assume that

           A12: k in ( Seg ( len p)) and

           A13: v = (q . k);

          ( dom q) = ( Seg n) by A3, A4, A6, FINSEQ_1: 17;

          then (I . k) = (q . k) by A8, A12, FUNCT_1: 47;

          then (H . k) = (a * v) by A5, A12, A13, A10;

          hence (p . k) = (a * v) by A8, A12, A11, FUNCT_1: 47;

        end;

        1 <= (n + 1) by NAT_1: 11;

        then (n + 1) in ( dom H) & (n + 1) in ( dom I) by A3, A4, FINSEQ_3: 25;

        then

        reconsider v1 = (H . (n + 1)), v2 = (I . (n + 1)) as Vector of V by FUNCT_1: 102;

        

         A14: v1 = (a * v2) by A4, A5, FINSEQ_1: 4;

        

         A15: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

        ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        

        hence ( Sum H) = (( Sum p) + v1) by A4, A8, RLVECT_1: 38

        .= ((a * ( Sum q)) + (a * v2)) by A2, A8, A7, A9, A14

        .= (a * (( Sum q) + v2)) by VECTSP_1:def 14

        .= (a * ( Sum I)) by A3, A4, A7, A15, RLVECT_1: 38;

      end;

      then

       A16: for n st P[n] holds P[(n + 1)];

      now

        let H, I;

        assume that

         A17: ( len H) = ( len I) and

         A18: ( len H) = 0 and for k, v st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (a * v);

        

         AA: ( Sum H) = ( 0. V) by A18, Lm2;

        ( Sum I) = ( 0. V) by A17, A18, Lm2;

        hence ( Sum H) = (a * ( Sum I)) by VECTSP_1: 14, AA;

      end;

      then

       A19: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A19, A16);

      hence thesis by A1;

    end;

    theorem :: ZMODUL01:13

    for V be Z_Module, a be Element of INT.Ring holds (a * ( Sum ( <*> the carrier of V))) = ( 0. V) by Lm1, Th1;

    theorem :: ZMODUL01:14

    for R be Ring, V be LeftMod of R, a be Element of R, v,u be Vector of V holds (a * ( Sum <*v, u*>)) = ((a * v) + (a * u))

    proof

      let R be Ring;

      let V be LeftMod of R, a be Element of R, v,u be Vector of V;

      

      thus (a * ( Sum <*v, u*>)) = (a * (v + u)) by RLVECT_1: 45

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

    end;

    theorem :: ZMODUL01:15

    for R be Ring holds for V be LeftMod of R, a be Element of R, v,u,w be Vector of V holds (a * ( Sum <*v, u, w*>)) = (((a * v) + (a * u)) + (a * w))

    proof

      let R be Ring;

      let V be LeftMod of R, a be Element of R, v,u,w be Vector of V;

      

      thus (a * ( Sum <*v, u, w*>)) = (a * ((v + u) + w)) by RLVECT_1: 46

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

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

    end;

    theorem :: ZMODUL01:16

    for V be LeftMod of INT.Ring , a be Element of INT.Ring , v be Vector of V holds (( - a) * v) = ( - (a * v))

    proof

      let V be LeftMod of INT.Ring , a be Element of INT.Ring , v be Vector of V;

      

      thus (( - a) * v) = (a * ( - v)) by Th5

      .= ( - (a * v)) by Th6;

    end;

    theorem :: ZMODUL01:17

    ( len F) = ( len G) & (for k st k in ( dom F) holds (G . k) = (a * (F /. k))) implies ( Sum G) = (a * ( Sum F))

    proof

      assume that

       A1: ( len F) = ( len G) and

       A2: for k st k in ( dom F) holds (G . k) = (a * (F /. k));

      

       A3: ( dom F) = ( Seg ( len F)) & ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

      now

        let k, v;

        assume that

         A4: k in ( dom G) and

         A5: v = (F . k);

        v = (F /. k) by A1, A3, A4, A5, PARTFUN1:def 6;

        hence (G . k) = (a * v) by A1, A2, A3, A4;

      end;

      hence thesis by A1, Th12;

    end;

    begin

    reserve R for Ring;

    reserve V,X,Y for LeftMod of R;

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

    reserve a for Element of R;

    reserve V1,V2,V3 for Subset of V;

    reserve x for set;

    theorem :: ZMODUL01:18

    V1 <> {} & V1 is linearly-closed implies ( 0. V) in V1 by VECTSP_4: 1;

    theorem :: ZMODUL01:19

    V1 is linearly-closed implies for v st v in V1 holds ( - v) in V1 by VECTSP_4: 2;

    theorem :: ZMODUL01:20

    V1 is linearly-closed implies for v, u st v in V1 & u in V1 holds (v - u) in V1 by VECTSP_4: 3;

    theorem :: ZMODUL01:21

    the carrier of V = V1 implies V1 is linearly-closed;

    theorem :: ZMODUL01:22

    V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) : v in V1 & u in V2 } implies V3 is linearly-closed

    proof

      assume that

       A1: V1 is linearly-closed & V2 is linearly-closed and

       A2: V3 = { (v + u) : v in V1 & u in V2 };

      thus for v, u st v in V3 & u in V3 holds (v + u) in V3

      proof

        let v, u;

        assume that

         A3: v in V3 and

         A4: u in V3;

        consider v2, v1 such that

         A5: v = (v1 + v2) and

         A6: v1 in V1 & v2 in V2 by A2, A3;

        consider u2, u1 such that

         A7: u = (u1 + u2) and

         A8: u1 in V1 & u2 in V2 by A2, A4;

        

         A9: (v + u) = (((v1 + v2) + u1) + u2) by A5, A7, RLVECT_1:def 3

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

        .= ((v1 + u1) + (v2 + u2)) by RLVECT_1:def 3;

        (v1 + u1) in V1 & (v2 + u2) in V2 by A1, A6, A8;

        hence thesis by A2, A9;

      end;

      let a, v;

      assume v in V3;

      then

      consider v2, v1 such that

       A10: v = (v1 + v2) and

       A11: v1 in V1 & v2 in V2 by A2;

      

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

      (a * v1) in V1 & (a * v2) in V2 by A1, A11;

      hence thesis by A2, A12;

    end;

    registration

      let R;

      let V;

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

      coherence by VECTSP_4: 4;

    end

    registration

      let R;

      let V;

      cluster linearly-closed for Subset of V;

      existence

      proof

        take {( 0. V)};

        thus thesis;

      end;

    end

    registration

      let R;

      let V;

      let V1,V2 be linearly-closed Subset of V;

      cluster (V1 /\ V2) -> linearly-closed;

      coherence by VECTSP_4: 7;

    end

    definition

      ::$Canceled

    end

    definition

      let R be Ring;

      let V be LeftMod of R;

      mode Submodule of V is Subspace of V;

    end

    reserve W,W1,W2 for Submodule of V;

    reserve w,w1,w2 for Vector of W;

    theorem :: ZMODUL01:23

    x in W1 & W1 is Submodule of W2 implies x in W2 by VECTSP_4: 8;

    theorem :: ZMODUL01:24

    

     Th24: for x be object holds x in W implies x in V by VECTSP_4: 9;

    theorem :: ZMODUL01:25

    

     Th25: w is Vector of V by VECTSP_4: 10;

    theorem :: ZMODUL01:26

    ( 0. W) = ( 0. V) by VECTSP_4:def 2;

    theorem :: ZMODUL01:27

    ( 0. W1) = ( 0. W2) by VECTSP_4: 12;

    theorem :: ZMODUL01:28

    w1 = v & w2 = u implies (w1 + w2) = (v + u) by VECTSP_4: 13;

    theorem :: ZMODUL01:29

    w = v implies (a * w) = (a * v) by VECTSP_4: 14;

    theorem :: ZMODUL01:30

    w = v implies ( - v) = ( - w) by VECTSP_4: 15;

    theorem :: ZMODUL01:31

    w1 = v & w2 = u implies (w1 - w2) = (v - u) by VECTSP_4: 16;

    theorem :: ZMODUL01:32

    

     Th32: V is Submodule of V by VECTSP_4: 24;

    theorem :: ZMODUL01:33

    

     Th33: ( 0. V) in W by VECTSP_4: 17;

    theorem :: ZMODUL01:34

    ( 0. W1) in W2 by VECTSP_4: 18;

    theorem :: ZMODUL01:35

    ( 0. W) in V by VECTSP_4: 19;

    theorem :: ZMODUL01:36

    

     Th36: u in W & v in W implies (u + v) in W by VECTSP_4: 20;

    theorem :: ZMODUL01:37

    v in W implies (a * v) in W by VECTSP_4: 21;

    theorem :: ZMODUL01:38

    v in W implies ( - v) in W by VECTSP_4: 22;

    theorem :: ZMODUL01:39

    

     Th39: u in W & v in W implies (u - v) in W by VECTSP_4: 23;

    reserve D for non empty set;

    reserve d1 for Element of D;

    reserve A for BinOp of D;

    reserve M for Function of [:the carrier of R, D:], D;

    theorem :: ZMODUL01:40

    

     Th40: V1 = D & d1 = ( 0. V) & A = (the addF of V || V1) & M = (the lmult of V | [:the carrier of R, V1:]) implies ModuleStr (# D, A, d1, M #) is Submodule of V

    proof

      assume that

       A1: V1 = D and

       A2: d1 = ( 0. V) and

       A3: A = (the addF of V || V1) and

       A4: M = (the lmult of V | [:the carrier of R, V1:]);

      reconsider W = ModuleStr (# D, A, d1, M #) as non empty ModuleStr over R;

      

       A5: for a be Element of R holds for x be Vector of W holds (a * x) = (the lmult of V . (a,x))

      proof

        let a be Element of R;

        let x be Vector of W;

        

        thus (a * x) = (the lmult of V . [a, x]) by A1, A4, FUNCT_1: 49

        .= (the lmult of V . (a,x));

      end;

      

       A6: for x,y be Vector of W holds (x + y) = (the addF of V . (x,y))

      proof

        let x,y be Vector of W;

        

        thus (x + y) = (the addF of V . [x, y]) by A1, A3, FUNCT_1: 49

        .= (the addF of V . (x,y));

      end;

      

       A7: W is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital

      proof

        set MV = the lmult of V;

        set AV = the addF of V;

        thus W is Abelian

        proof

          let x,y be Vector of W;

          reconsider x1 = x, y1 = y as Vector of V by A1, TARSKI:def 3;

          

          thus (x + y) = (x1 + y1) by A6

          .= (y1 + x1)

          .= (y + x) by A6;

        end;

        thus W is add-associative

        proof

          let x,y,z be Vector of W;

          reconsider x1 = x, y1 = y, z1 = z as Vector of V by A1, TARSKI:def 3;

          

          thus ((x + y) + z) = (AV . ((x + y),z1)) by A6

          .= ((x1 + y1) + z1) by A6

          .= (x1 + (y1 + z1)) by RLVECT_1:def 3

          .= (AV . (x1,(y + z))) by A6

          .= (x + (y + z)) by A6;

        end;

        thus W is right_zeroed

        proof

          let x be Vector of W;

          reconsider y = x as Vector of V by A1, TARSKI:def 3;

          

          thus (x + ( 0. W)) = (y + ( 0. V)) by A2, A6

          .= x by RLVECT_1: 4;

        end;

        thus W is right_complementable

        proof

          let x be Vector of W;

          reconsider x1 = x as Vector of V by A1, TARSKI:def 3;

          consider v such that

           A8: (x1 + v) = ( 0. V) by ALGSTR_0:def 11;

          v = ( - x1) by A8, RLVECT_1:def 10

          .= (( - ( 1. R)) * x1) by Th2

          .= (the lmult of V . (( - ( 1. R)),x1))

          .= (( - ( 1. R)) * x) by A5;

          then

          reconsider y = v as Vector of W;

          take y;

          thus thesis by A2, A6, A8;

        end;

        thus for a be Element of R holds for x,y be Vector of W holds (a * (x + y)) = ((a * x) + (a * y))

        proof

          let a be Element of R;

          let x,y be Vector of W;

          reconsider x1 = x, y1 = y as Vector of V by A1, TARSKI:def 3;

          (a * (x + y)) = (MV . (a,(x + y))) by A5

          .= (a * (x1 + y1)) by A6

          .= ((a * x1) + (a * y1)) by VECTSP_1:def 14

          .= (AV . ((MV . (a,x1)),(a * y))) by A5

          .= (AV . ((a * x),(a * y))) by A5

          .= ((a * x) + (a * y)) by A6;

          hence thesis;

        end;

        thus for a,b be Element of R holds for x be Vector of W holds ((a + b) * x) = ((a * x) + (b * x))

        proof

          let a,b be Element of R;

          let x be Vector of W;

          reconsider y = x as Vector of V by A1, TARSKI:def 3;

          ((a + b) * x) = ((a + b) * y) by A5

          .= ((a * y) + (b * y)) by VECTSP_1:def 15

          .= (AV . ((MV . (a,y)),(b * x))) by A5

          .= (AV . ((a * x),(b * x))) by A5

          .= ((a * x) + (b * x)) by A6;

          hence thesis;

        end;

        thus for a,b be Element of R holds for x be Vector of W holds ((a * b) * x) = (a * (b * x))

        proof

          let a,b be Element of R;

          let x be Vector of W;

          reconsider y = x as Vector of V by A1, TARSKI:def 3;

          reconsider a, b as Element of R;

          ((a * b) * x) = ((a * b) * y) by A5

          .= (a * (b * y)) by VECTSP_1:def 16

          .= (MV . (a,(b * x))) by A5

          .= (a * (b * x)) by A5;

          hence thesis;

        end;

        let x be Vector of W;

        reconsider y = x as Vector of V by A1, TARSKI:def 3;

        

        thus (( 1. R) * x) = (the lmult of V . (( 1. R),y)) by A5

        .= (( 1. R) * y)

        .= x by VECTSP_1:def 17;

      end;

      ( 0. W) = ( 0. V) by A2;

      hence thesis by A1, A3, A4, A7, VECTSP_4:def 2;

    end;

    theorem :: ZMODUL01:41

    for R be Ring holds for V,X be strict LeftMod of R st V is Submodule of X & X is Submodule of V holds V = X by VECTSP_4: 25;

    theorem :: ZMODUL01:42

    

     Th42: V is Submodule of X & X is Submodule of Y implies V is Submodule of Y by VECTSP_4: 26;

    theorem :: ZMODUL01:43

    

     Th43: the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2 by VECTSP_4: 27;

    theorem :: ZMODUL01:44

    (for v st v in W1 holds v in W2) implies W1 is Submodule of W2 by VECTSP_4: 28;

    registration

      let R be Ring;

      let V be LeftMod of R;

      cluster strict for Submodule of V;

      existence

      proof

        the carrier of V is Subset of V iff the carrier of V c= the carrier of V;

        then

        reconsider V1 = the carrier of V as Subset of V;

        the addF of V = (the addF of V || V1) & the lmult of V = (the lmult of V | [:the carrier of R, V1:]) by RELSET_1: 19;

        then ModuleStr (# the carrier of V, the addF of V, ( 0. V), the lmult of V #) is Submodule of V by Th40;

        hence thesis;

      end;

    end

    theorem :: ZMODUL01:45

    

     Th45: for W1,W2 be strict Submodule of V holds the carrier of W1 = the carrier of W2 implies W1 = W2 by VECTSP_4: 29;

    theorem :: ZMODUL01:46

    

     Th46: for W1,W2 be strict Submodule of V holds (for v holds v in W1 iff v in W2) implies W1 = W2 by VECTSP_4: 30;

    theorem :: ZMODUL01:47

    for V be strict LeftMod of R, W be strict Submodule of V holds the carrier of W = the carrier of V implies W = V by VECTSP_4: 31;

    theorem :: ZMODUL01:48

    for V be strict LeftMod of R, W be strict Submodule of V holds (for v be Vector of V holds v in W iff v in V) implies W = V

    proof

      let V be strict LeftMod of R, W be strict Submodule of V;

      assume

       A1: for v be Vector of V holds v in W iff v in V;

      V is Submodule of V by Th32;

      hence thesis by A1, Th46;

    end;

    theorem :: ZMODUL01:49

    the carrier of W = V1 implies V1 is linearly-closed by VECTSP_4: 33;

    theorem :: ZMODUL01:50

    V1 <> {} & V1 is linearly-closed implies ex W be strict Submodule of V st V1 = the carrier of W by VECTSP_4: 34;

    theorem :: ZMODUL01:51

    ( (0). W) = ( (0). V) by VECTSP_4: 36;

    theorem :: ZMODUL01:52

    ( (0). W1) = ( (0). W2) by VECTSP_4: 37;

    theorem :: ZMODUL01:53

    ( (0). W) is Submodule of V by Th42;

    theorem :: ZMODUL01:54

    

     Th54: ( (0). V) is Submodule of W by VECTSP_4: 39;

    theorem :: ZMODUL01:55

    ( (0). W1) is Submodule of W2 by VECTSP_4: 40;

    theorem :: ZMODUL01:56

    for V be LeftMod of R holds V is Submodule of ( (Omega). V) by VECTSP_4: 41;

    definition

      ::$Canceled

    end

    reserve B,C for Coset of W;

    theorem :: ZMODUL01:57

    ( 0. V) in (v + W) iff v in W by VECTSP_4: 43;

    theorem :: ZMODUL01:58

    

     Th58: v in (v + W) by VECTSP_4: 44;

    theorem :: ZMODUL01:59

    (( 0. V) + W) = the carrier of W by VECTSP_4: 45;

    theorem :: ZMODUL01:60

    (v + ( (0). V)) = {v} by VECTSP_4: 46;

    theorem :: ZMODUL01:61

    (v + ( (Omega). V)) = the carrier of V by VECTSP_4: 47;

    theorem :: ZMODUL01:62

    ( 0. V) in (v + W) iff (v + W) = the carrier of W by VECTSP_4: 48;

    theorem :: ZMODUL01:63

    v in W iff (v + W) = the carrier of W by VECTSP_4: 49;

    theorem :: ZMODUL01:64

    v in W implies ((a * v) + W) = the carrier of W by VECTSP_4: 50;

    theorem :: ZMODUL01:65

    u in W iff (v + W) = ((v + u) + W) by VECTSP_4: 53;

    theorem :: ZMODUL01:66

    u in W iff (v + W) = ((v - u) + W) by VECTSP_4: 54;

    theorem :: ZMODUL01:67

    v in (u + W) iff (u + W) = (v + W) by VECTSP_4: 55;

    theorem :: ZMODUL01:68

    u in (v1 + W) & u in (v2 + W) implies (v1 + W) = (v2 + W) by VECTSP_4: 56;

    theorem :: ZMODUL01:69

    v in W implies (a * v) in (v + W) by VECTSP_4: 58;

    theorem :: ZMODUL01:70

    (u + v) in (v + W) iff u in W by VECTSP_4: 60;

    theorem :: ZMODUL01:71

    (v - u) in (v + W) iff u in W by VECTSP_4: 61;

    theorem :: ZMODUL01:72

    u in (v + W) iff ex v1 st v1 in W & u = (v + v1)

    proof

      thus u in (v + W) implies ex v1 st v1 in W & u = (v + v1)

      proof

        assume u in (v + W);

        then ex v1 st u = (v + v1) & v1 in W;

        hence thesis;

      end;

      given v1 such that

       A1: v1 in W & u = (v + v1);

      thus thesis by A1;

    end;

    theorem :: ZMODUL01:73

    u in (v + W) iff ex v1 st v1 in W & u = (v - v1) by VECTSP_4: 62;

    theorem :: ZMODUL01:74

    (ex v st v1 in (v + W) & v2 in (v + W)) iff (v1 - v2) in W by VECTSP_4: 63;

    theorem :: ZMODUL01:75

    (v + W) = (u + W) implies ex v1 st v1 in W & (v + v1) = u by VECTSP_4: 64;

    theorem :: ZMODUL01:76

    (v + W) = (u + W) implies ex v1 st v1 in W & (v - v1) = u by VECTSP_4: 65;

    theorem :: ZMODUL01:77

    for W1,W2 be strict Submodule of V st (v + W1) = (v + W2) holds W1 = W2 by VECTSP_4: 66;

    theorem :: ZMODUL01:78

    for W1,W2 be strict Submodule of V st (v + W1) = (u + W2) holds W1 = W2 by VECTSP_4: 67;

    theorem :: ZMODUL01:79

    C is linearly-closed iff C = the carrier of W by VECTSP_4: 69;

    theorem :: ZMODUL01:80

    for W1,W2 be strict Submodule of V, C1 be Coset of W1, C2 be Coset of W2 st C1 = C2 holds W1 = W2 by VECTSP_4: 70;

    theorem :: ZMODUL01:81

     {v} is Coset of ( (0). V) by VECTSP_4: 71;

    theorem :: ZMODUL01:82

    V1 is Coset of ( (0). V) implies ex v st V1 = {v} by VECTSP_4: 72;

    theorem :: ZMODUL01:83

    the carrier of W is Coset of W by VECTSP_4: 73;

    theorem :: ZMODUL01:84

    the carrier of V is Coset of ( (Omega). V) by VECTSP_4: 74;

    theorem :: ZMODUL01:85

    V1 is Coset of ( (Omega). V) implies V1 = the carrier of V by VECTSP_4: 75;

    theorem :: ZMODUL01:86

    ( 0. V) in C iff C = the carrier of W by VECTSP_4: 76;

    theorem :: ZMODUL01:87

    u in C iff C = (u + W) by VECTSP_4: 77;

    theorem :: ZMODUL01:88

    u in C & v in C implies ex v1 st v1 in W & (u + v1) = v by VECTSP_4: 78;

    theorem :: ZMODUL01:89

    u in C & v in C implies ex v1 st v1 in W & (u - v1) = v by VECTSP_4: 79;

    theorem :: ZMODUL01:90

    (ex C st v1 in C & v2 in C) iff (v1 - v2) in W by VECTSP_4: 80;

    theorem :: ZMODUL01:91

    u in B & u in C implies B = C by VECTSP_4: 81;

    begin

    reserve V for LeftMod of R;

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

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

    reserve a,a1,a2 for Element of R;

    reserve X,Y,y,y1,y2 for set;

    definition

      let GF be Ring;

      let M be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF;

      let W1,W2 be Subspace of M;

      :: original: +

      redefine

      func W1 + W2;

      commutativity by VECTSP_5: 5;

    end

    theorem :: ZMODUL01:92

    

     Th92: x in (W1 + W2) iff ex v1, v2 st v1 in W1 & v2 in W2 & x = (v1 + v2) by VECTSP_5: 1;

    theorem :: ZMODUL01:93

    v in W1 or v in W2 implies v in (W1 + W2) by VECTSP_5: 2;

    theorem :: ZMODUL01:94

    

     Th94: for x be object holds x in (W1 /\ W2) iff x in W1 & x in W2 by VECTSP_5: 3;

    

     Lm6: the carrier of W1 c= the carrier of (W1 + W2)

    proof

      let x be object;

      set A = { (v + u) : v in W1 & u in W2 };

      assume x in the carrier of W1;

      then

      reconsider v = x as Element of W1;

      reconsider v as Vector of V by Th25;

      

       A1: v = (v + ( 0. V)) by RLVECT_1: 4;

      v in W1 & ( 0. V) in W2 by Th33;

      then x in A by A1;

      hence thesis by VECTSP_5:def 1;

    end;

    theorem :: ZMODUL01:95

    for W be strict Submodule of V holds (W + W) = W by VECTSP_5: 4;

    theorem :: ZMODUL01:96

    (W1 + (W2 + W3)) = ((W1 + W2) + W3) by VECTSP_5: 6;

    theorem :: ZMODUL01:97

    W1 is Submodule of (W1 + W2) by VECTSP_5: 7;

    theorem :: ZMODUL01:98

    

     Th98: for W2 be strict Submodule of V holds W1 is Submodule of W2 iff (W1 + W2) = W2 by VECTSP_5: 8;

    theorem :: ZMODUL01:99

    

     Th99: for W be strict Submodule of V holds (( (0). V) + W) = W by VECTSP_5: 9;

    theorem :: ZMODUL01:100

    (( (0). V) + ( (Omega). V)) = the ModuleStr of V by VECTSP_5: 10;

    theorem :: ZMODUL01:101

    

     Th101: (( (Omega). V) + W) = the ModuleStr of V by VECTSP_5: 11;

    theorem :: ZMODUL01:102

    for V be strict LeftMod of R holds (( (Omega). V) + ( (Omega). V)) = V by Th101;

    theorem :: ZMODUL01:103

    for W be strict Submodule of V holds (W /\ W) = W by VECTSP_5: 13;

    theorem :: ZMODUL01:104

    (W1 /\ (W2 /\ W3)) = ((W1 /\ W2) /\ W3) by VECTSP_5: 14;

    

     Lm8: the carrier of (W1 /\ W2) c= the carrier of W1

    proof

      the carrier of (W1 /\ W2) = (the carrier of W1 /\ the carrier of W2) by VECTSP_5:def 2;

      hence thesis by XBOOLE_1: 17;

    end;

    theorem :: ZMODUL01:105

    (W1 /\ W2) is Submodule of W1 by VECTSP_5: 15;

    theorem :: ZMODUL01:106

    

     Th106: for W1 be strict Submodule of V holds W1 is Submodule of W2 iff (W1 /\ W2) = W1 by VECTSP_5: 16;

    theorem :: ZMODUL01:107

    

     Th107: (( (0). V) /\ W) = ( (0). V) by VECTSP_5: 20;

    theorem :: ZMODUL01:108

    (( (0). V) /\ ( (Omega). V)) = ( (0). V) by Th107;

    theorem :: ZMODUL01:109

    

     Th109: for W be strict Submodule of V holds (( (Omega). V) /\ W) = W by VECTSP_5: 21;

    theorem :: ZMODUL01:110

    for V be strict LeftMod of R holds (( (Omega). V) /\ ( (Omega). V)) = V by Th109;

    

     Lm9: the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)

    proof

      the carrier of (W1 /\ W2) c= the carrier of W1 & the carrier of W1 c= the carrier of (W1 + W2) by Lm6, Lm8;

      hence thesis;

    end;

    theorem :: ZMODUL01:111

    (W1 /\ W2) is Submodule of (W1 + W2) by Lm9, Th43;

    

     Lm10: the carrier of ((W1 /\ W2) + W2) = the carrier of W2

    proof

      thus the carrier of ((W1 /\ W2) + W2) c= the carrier of W2

      proof

        let x be object;

        assume x in the carrier of ((W1 /\ W2) + W2);

        then x in { (u + v) where v, u : u in (W1 /\ W2) & v in W2 } by VECTSP_5:def 1;

        then

        consider v, u such that

         A1: x = (u + v) and

         A2: u in (W1 /\ W2) and

         A3: v in W2;

        u in W2 by A2, Th94;

        then (u + v) in W2 by A3, Th36;

        hence thesis by A1;

      end;

      let x be object;

      the carrier of W2 c= the carrier of ((W1 /\ W2) + W2) by Lm6;

      hence thesis;

    end;

    theorem :: ZMODUL01:112

    for W2 be strict Submodule of V holds ((W1 /\ W2) + W2) = W2 by Lm10, Th45;

    

     Lm11: the carrier of (W1 /\ (W1 + W2)) = the carrier of W1

    proof

      thus the carrier of (W1 /\ (W1 + W2)) c= the carrier of W1

      proof

        let x be object;

        assume

         A1: x in the carrier of (W1 /\ (W1 + W2));

        the carrier of (W1 /\ (W1 + W2)) = (the carrier of W1 /\ the carrier of (W1 + W2)) by VECTSP_5:def 2;

        hence thesis by A1, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A2: x in the carrier of W1;

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

      then

      reconsider x1 = x as Element of V by A2;

      

       A3: (x1 + ( 0. V)) = x1 & ( 0. V) in W2 by Th33, RLVECT_1: 4;

      x in W1 by A2;

      then x in { (u + v) where v, u : u in W1 & v in W2 } by A3;

      then x in the carrier of (W1 + W2) by VECTSP_5:def 1;

      then x in (the carrier of W1 /\ the carrier of (W1 + W2)) by A2, XBOOLE_0:def 4;

      hence thesis by VECTSP_5:def 2;

    end;

    theorem :: ZMODUL01:113

    for W1 be strict Submodule of V holds (W1 /\ (W1 + W2)) = W1 by Lm11, Th45;

    

     Lm12: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))

    proof

      let x be object;

      assume x in the carrier of ((W1 /\ W2) + (W2 /\ W3));

      then x in { (u + v) where v, u : u in (W1 /\ W2) & v in (W2 /\ W3) } by VECTSP_5:def 1;

      then

      consider v, u such that

       A1: x = (u + v) and

       A2: u in (W1 /\ W2) & v in (W2 /\ W3);

      u in W2 & v in W2 by A2, Th94;

      then

       A3: x in W2 by A1, Th36;

      u in W1 & v in W3 by A2, Th94;

      then x in (W1 + W3) by A1, Th92;

      then x in (W2 /\ (W1 + W3)) by A3, Th94;

      hence thesis;

    end;

    theorem :: ZMODUL01:114

    ((W1 /\ W2) + (W2 /\ W3)) is Submodule of (W2 /\ (W1 + W3)) by Lm12, Th43;

    

     Lm13: W1 is Submodule of W2 implies the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) by VECTSP_5: 27;

    theorem :: ZMODUL01:115

    W1 is Submodule of W2 implies (W2 /\ (W1 + W3)) = ((W1 /\ W2) + (W2 /\ W3)) by Lm13, Th45;

    

     Lm14: the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))

    proof

      let x be object;

      assume x in the carrier of (W2 + (W1 /\ W3));

      then x in { (u + v) where v, u : u in W2 & v in (W1 /\ W3) } by VECTSP_5:def 1;

      then

      consider v, u such that

       A1: x = (u + v) & u in W2 and

       A2: v in (W1 /\ W3);

      v in W3 by A2, Th94;

      then x in { (u1 + u2) where u2, u1 : u1 in W2 & u2 in W3 } by A1;

      then

       A3: x in the carrier of (W2 + W3) by VECTSP_5:def 1;

      v in W1 by A2, Th94;

      then x in { (v1 + v2) where v2, v1 : v1 in W1 & v2 in W2 } by A1;

      then x in the carrier of (W1 + W2) by VECTSP_5:def 1;

      then x in (the carrier of (W1 + W2) /\ the carrier of (W2 + W3)) by A3, XBOOLE_0:def 4;

      hence thesis by VECTSP_5:def 2;

    end;

    theorem :: ZMODUL01:116

    (W2 + (W1 /\ W3)) is Submodule of ((W1 + W2) /\ (W2 + W3)) by Lm14, Th43;

    

     Lm15: W1 is Submodule of W2 implies the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))

    proof

      reconsider V2 = the carrier of W2 as Subset of V by VECTSP_4:def 2;

      

       A1: V2 is linearly-closed by VECTSP_4: 33;

      assume W1 is Submodule of W2;

      then

       A2: the carrier of W1 c= the carrier of W2 by VECTSP_4:def 2;

      thus the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) by Lm14;

      let x be object;

      assume x in the carrier of ((W1 + W2) /\ (W2 + W3));

      then x in (the carrier of (W1 + W2) /\ the carrier of (W2 + W3)) by VECTSP_5:def 2;

      then x in the carrier of (W1 + W2) by XBOOLE_0:def 4;

      then x in { (u1 + u2) where u2, u1 : u1 in W1 & u2 in W2 } by VECTSP_5:def 1;

      then

      consider u2, u1 such that

       A3: x = (u1 + u2) and

       A4: u1 in W1 & u2 in W2;

      (u1 + u2) in V2 by A2, A1, A4;

      then

       A5: (u1 + u2) in W2;

      ( 0. V) in (W1 /\ W3) & ((u1 + u2) + ( 0. V)) = (u1 + u2) by Th33, RLVECT_1: 4;

      then x in { (u + v) where v, u : u in W2 & v in (W1 /\ W3) } by A3, A5;

      hence thesis by VECTSP_5:def 1;

    end;

    theorem :: ZMODUL01:117

    W1 is Submodule of W2 implies (W2 + (W1 /\ W3)) = ((W1 + W2) /\ (W2 + W3)) by Lm15, Th45;

    theorem :: ZMODUL01:118

    W1 is strict Submodule of W3 implies (W1 + (W2 /\ W3)) = ((W1 + W2) /\ W3) by VECTSP_5: 30;

    theorem :: ZMODUL01:119

    for W1,W2 be strict Submodule of V holds (W1 + W2) = W2 iff (W1 /\ W2) = W1

    proof

      let W1,W2 be strict Submodule of V;

      (W1 + W2) = W2 iff W1 is Submodule of W2 by Th98;

      hence thesis by Th106;

    end;

    theorem :: ZMODUL01:120

    for W2,W3 be strict Submodule of V holds W1 is Submodule of W2 implies (W1 + W3) is Submodule of (W2 + W3) by VECTSP_5: 32;

    theorem :: ZMODUL01:121

    (ex W st the carrier of W = (the carrier of W1 \/ the carrier of W2)) iff W1 is Submodule of W2 or W2 is Submodule of W1 by VECTSP_5: 35;

    notation

      let GF be Ring;

      let V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF;

      synonym Submodules V for Subspaces (V);

    end

    registration

      let R, V;

      cluster ( Submodules V) -> non empty;

      coherence ;

    end

    theorem :: ZMODUL01:122

    for V be strict LeftMod of R holds V in ( Submodules V)

    proof

      let V be strict LeftMod of R;

      ( (Omega). V) in ( Submodules V) by VECTSP_5:def 3;

      hence thesis;

    end;

    

     Lm16: for V be LeftMod of R, W be strict Submodule of V holds (for v be Vector of V holds v in W) implies W = the ModuleStr of V

    proof

      let V be LeftMod of R, W be strict Submodule of V;

      assume for v be Vector of V holds v in W;

      then for v be Vector of V holds (v in W iff v in ( (Omega). V));

      hence thesis by Th46;

    end;

    

     Lm17: for V be LeftMod of R, W1,W2 be Submodule of V holds (W1 + W2) = the ModuleStr of V iff for v be Vector of V holds ex v1,v2 be Vector of V st v1 in W1 & v2 in W2 & v = (v1 + v2)

    proof

      let V be LeftMod of R, W1,W2 be Submodule of V;

      thus (W1 + W2) = the ModuleStr of V implies for v be Vector of V holds ex v1,v2 be Vector of V st v1 in W1 & v2 in W2 & v = (v1 + v2) by RLVECT_1: 1, Th92;

      assume

       A1: for v be Vector of V holds ex v1,v2 be Vector of V st v1 in W1 & v2 in W2 & v = (v1 + v2);

      now

        let u be Vector of V;

        ex v1,v2 be Vector of V st v1 in W1 & v2 in W2 & u = (v1 + v2) by A1;

        hence u in (W1 + W2) by Th92;

      end;

      hence thesis by Lm16;

    end;

    definition

      ::$Canceled

      let R;

      let V be LeftMod of R;

      let W be Submodule of V;

      :: ZMODUL01:def17

      attr W is with_Linear_Compl means ex C be Submodule of V st V is_the_direct_sum_of (C,W);

    end

    registration

      let R;

      let V be LeftMod of R;

      cluster with_Linear_Compl for Submodule of V;

      correctness

      proof

        V is_the_direct_sum_of (( (0). V),( (Omega). V)) by Th99, Th107;

        then ( (Omega). V) is with_Linear_Compl;

        hence thesis;

      end;

    end

    definition

      let R;

      let V be LeftMod of R;

      let W be Submodule of V;

      assume

       A1: W is with_Linear_Compl;

      :: ZMODUL01:def18

      mode Linear_Compl of W -> Submodule of V means

      : Def19: V is_the_direct_sum_of (it ,W);

      existence by A1;

    end

    theorem :: ZMODUL01:123

    for W1,W2 be Submodule of V holds V is_the_direct_sum_of (W1,W2) implies W2 is Linear_Compl of W1

    proof

      let W1,W2 be Submodule of V;

      assume V is_the_direct_sum_of (W1,W2);

      then

       A1: V is_the_direct_sum_of (W2,W1) by VECTSP_5: 41;

      then W1 is with_Linear_Compl;

      hence thesis by Def19, A1;

    end;

    theorem :: ZMODUL01:124

    

     Th124: for W be with_Linear_Compl Submodule of V, L be Linear_Compl of W holds V is_the_direct_sum_of (L,W) & V is_the_direct_sum_of (W,L)

    proof

      let W be with_Linear_Compl Submodule of V, L be Linear_Compl of W;

      thus V is_the_direct_sum_of (L,W) by Def19;

      hence thesis by VECTSP_5: 41;

    end;

    theorem :: ZMODUL01:125

    for W be with_Linear_Compl Submodule of V, L be Linear_Compl of W holds (W + L) = the ModuleStr of V

    proof

      let W be with_Linear_Compl Submodule of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th124;

      hence (W + L) = the ModuleStr of V;

    end;

    theorem :: ZMODUL01:126

    for W be with_Linear_Compl Submodule of V, L be Linear_Compl of W holds (W /\ L) = ( (0). V)

    proof

      let W be with_Linear_Compl Submodule of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th124;

      hence (W /\ L) = ( (0). V);

    end;

    theorem :: ZMODUL01:127

    V is_the_direct_sum_of (W1,W2) implies V is_the_direct_sum_of (W2,W1) by VECTSP_5: 41;

    theorem :: ZMODUL01:128

    for V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W holds W is Linear_Compl of L

    proof

      let V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (L,W) by Def19;

      then

       A1: V is_the_direct_sum_of (W,L) by VECTSP_5: 41;

      then L is with_Linear_Compl;

      hence thesis by Def19, A1;

    end;

    theorem :: ZMODUL01:129

    

     Th129: for V be Z_Module holds V is_the_direct_sum_of (( (0). V),( (Omega). V)) & V is_the_direct_sum_of (( (Omega). V),( (0). V))

    proof

      let V be Z_Module;

      V is_the_direct_sum_of (( (0). V),( (Omega). V)) by Th99, Th107;

      hence thesis by VECTSP_5: 41;

    end;

    theorem :: ZMODUL01:130

    for V be Z_Module holds ( (0). V) is Linear_Compl of ( (Omega). V) & ( (Omega). V) is Linear_Compl of ( (0). V)

    proof

      let V be Z_Module;

      

       A1: V is_the_direct_sum_of (( (0). V),( (Omega). V)) & V is_the_direct_sum_of (( (Omega). V),( (0). V)) by Th129;

      then

       A2: ( (Omega). V) is with_Linear_Compl;

      ( (0). V) is with_Linear_Compl by A1;

      hence thesis by Def19, A1, A2;

    end;

    reserve C for Coset of W;

    reserve C1 for Coset of W1;

    reserve C2 for Coset of W2;

    theorem :: ZMODUL01:131

    C1 meets C2 implies (C1 /\ C2) is Coset of (W1 /\ W2) by VECTSP_5: 45;

    

     Lm18: ex C st v in C

    proof

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

      take C;

      thus thesis by Th58;

    end;

    theorem :: ZMODUL01:132

    for V be Z_Module, W1,W2 be Submodule of V holds V is_the_direct_sum_of (W1,W2) iff for C1 be Coset of W1, C2 be Coset of W2 holds ex v be Vector of V st (C1 /\ C2) = {v} by VECTSP_5: 46;

    theorem :: ZMODUL01:133

    for V be LeftMod of R, W1,W2 be Submodule of V holds (W1 + W2) = the ModuleStr of V iff for v be Vector of V holds ex v1,v2 be Vector of V st v1 in W1 & v2 in W2 & v = (v1 + v2) by Lm17;

    theorem :: ZMODUL01:134

    V is_the_direct_sum_of (W1,W2) & (v1 + v2) = (u1 + u2) & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies v1 = u1 & v2 = u2 by VECTSP_5: 48;

    theorem :: ZMODUL01:135

    V = (W1 + W2) & (ex v st for v1, v2, u1, u2 st (v1 + v2) = (u1 + u2) & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2) implies V is_the_direct_sum_of (W1,W2)

    proof

      assume

       A1: V = (W1 + W2);

      the carrier of ( (0). V) = {( 0. V)} & ( (0). V) is Submodule of (W1 /\ W2) by Th54, VECTSP_4:def 3;

      then

       A2: {( 0. V)} c= the carrier of (W1 /\ W2) by VECTSP_4:def 2;

      given v such that

       A3: for v1, v2, u1, u2 st (v1 + v2) = (u1 + u2) & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2;

      assume not thesis;

      then the carrier of (W1 /\ W2) <> {( 0. V)} by VECTSP_4:def 3, A1;

      then {( 0. V)} c< the carrier of (W1 /\ W2) by A2;

      then

      consider x be object such that

       A4: x in the carrier of (W1 /\ W2) and

       A5: not x in {( 0. V)} by XBOOLE_0: 6;

      

       A6: x <> ( 0. V) by A5, TARSKI:def 1;

      

       A7: x in (W1 /\ W2) by A4;

      then x in V by Th24;

      then

      reconsider u = x as Vector of V;

      consider v1, v2 such that

       A8: v1 in W1 and

       A9: v2 in W2 and

       A10: v = (v1 + v2) by A1, Lm17;

      

       A11: v = ((v1 + v2) + ( 0. V)) by A10, RLVECT_1: 4

      .= ((v1 + v2) + (u - u)) by RLVECT_1: 15

      .= (((v1 + v2) + u) - u) by RLVECT_1:def 3

      .= (((v1 + u) + v2) - u) by RLVECT_1:def 3

      .= ((v1 + u) + (v2 - u)) by RLVECT_1:def 3;

      x in W2 by A7, Th94;

      then

       A12: (v2 - u) in W2 by A9, Th39;

      x in W1 by A7, Th94;

      then (v1 + u) in W1 by A8, Th36;

      

      then (v2 - u) = v2 by A3, A8, A9, A10, A11, A12

      .= (v2 - ( 0. V)) by RLVECT_1: 13;

      hence thesis by A6, RLVECT_1: 23;

    end;

    definition

      ::$Canceled

    end

    theorem :: ZMODUL01:136

    

     Th136: V is_the_direct_sum_of (W1,W2) implies ((v |-- (W1,W2)) `1 ) = ((v |-- (W2,W1)) `2 ) by VECTSP_5: 50;

    theorem :: ZMODUL01:137

    

     Th137: V is_the_direct_sum_of (W1,W2) implies ((v |-- (W1,W2)) `2 ) = ((v |-- (W2,W1)) `1 ) by VECTSP_5: 51;

    theorem :: ZMODUL01:138

    for V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W, v be Vector of V, t be Element of [:the carrier of V, the carrier of V:] holds ((t `1 ) + (t `2 )) = v & (t `1 ) in W & (t `2 ) in L implies t = (v |-- (W,L))

    proof

      let V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th124;

      hence thesis by VECTSP_5:def 6;

    end;

    theorem :: ZMODUL01:139

    for V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W, v be Vector of V holds (((v |-- (W,L)) `1 ) + ((v |-- (W,L)) `2 )) = v

    proof

      let V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th124;

      hence thesis by VECTSP_5:def 6;

    end;

    theorem :: ZMODUL01:140

    for V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W, v be Vector of V holds ((v |-- (W,L)) `1 ) in W & ((v |-- (W,L)) `2 ) in L

    proof

      let V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th124;

      hence thesis by VECTSP_5:def 6;

    end;

    theorem :: ZMODUL01:141

    for V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W, v be Vector of V holds ((v |-- (W,L)) `1 ) = ((v |-- (L,W)) `2 ) by Th124, Th136;

    theorem :: ZMODUL01:142

    for V be Z_Module, W be with_Linear_Compl Submodule of V, L be Linear_Compl of W, v be Vector of V holds ((v |-- (W,L)) `2 ) = ((v |-- (L,W)) `1 ) by Th124, Th137;

    reserve A1,A2,B for Element of ( Submodules V);

    theorem :: ZMODUL01:143

    

     Th143: LattStr (# ( Submodules V), ( SubJoin V), ( SubMeet V) #) is Lattice by VECTSP_5: 57;

    registration

      let R;

      let V;

      cluster LattStr (# ( Submodules V), ( SubJoin V), ( SubMeet V) #) -> Lattice-like;

      coherence by Th143;

    end

    theorem :: ZMODUL01:144

    

     Th144: for V be Z_Module holds LattStr (# ( Submodules V), ( SubJoin V), ( SubMeet V) #) is lower-bounded by VECTSP_5: 58;

    theorem :: ZMODUL01:145

    

     Th145: for V be Z_Module holds LattStr (# ( Submodules V), ( SubJoin V), ( SubMeet V) #) is upper-bounded by VECTSP_5: 59;

    theorem :: ZMODUL01:146

    for V be Z_Module holds LattStr (# ( Submodules V), ( SubJoin V), ( SubMeet V) #) is 01_Lattice

    proof

      let V be Z_Module;

       LattStr (# ( Submodules V), ( SubJoin V), ( SubMeet V) #) is lower-bounded upper-bounded Lattice by Th144, Th145;

      hence thesis;

    end;

    theorem :: ZMODUL01:147

    for V be Z_Module holds LattStr (# ( Submodules V), ( SubJoin V), ( SubMeet V) #) is modular by VECTSP_5: 61;

    theorem :: ZMODUL01:148

    for V be Z_Module, W1,W2,W3 be strict Submodule of V holds W1 is Submodule of W2 implies (W1 /\ W3) is Submodule of (W2 /\ W3)

    proof

      let V be Z_Module, W1,W2,W3 be strict Submodule of V;

      set S = LattStr (# ( Submodules V), ( SubJoin V), ( SubMeet V) #);

      reconsider A = W1, B = W2, C = W3, AC = (W1 /\ W3), BC = (W2 /\ W3) as Element of S by VECTSP_5:def 3;

      assume

       A1: W1 is Submodule of W2;

      (A "\/" B) = (W1 + W2) by VECTSP_5:def 7

      .= B by A1, Th98;

      then A [= B;

      then (A "/\" C) [= (B "/\" C) by LATTICES: 9;

      then

       A2: ((A "/\" C) "\/" (B "/\" C)) = (B "/\" C);

      

       A3: (B "/\" C) = (W2 /\ W3) by VECTSP_5:def 8;

      ((A "/\" C) "\/" (B "/\" C)) = (( SubJoin V) . ((( SubMeet V) . (A,C)),BC)) by VECTSP_5:def 8

      .= (( SubJoin V) . (AC,BC)) by VECTSP_5:def 8

      .= ((W1 /\ W3) + (W2 /\ W3)) by VECTSP_5:def 7;

      hence thesis by A2, A3, Th98;

    end;

    theorem :: ZMODUL01:149

    for V be Z_Module, W be strict Submodule of V holds (for v be Vector of V holds v in W) implies W = the ModuleStr of V by Lm16;

    theorem :: ZMODUL01:150

    ex C st v in C by Lm18;

    begin

    definition

      let AG be non empty addLoopStr;

      :: ZMODUL01:def20

      func Int-mult-left (AG) -> Function of [:the carrier of INT.Ring , the carrier of AG:], the carrier of AG means

      : Def23: for i be Element of INT.Ring , a be Element of AG holds (i >= 0 implies (it . (i,a)) = (( Nat-mult-left AG) . (i,a))) & (i < 0 implies (it . (i,a)) = (( Nat-mult-left AG) . (( - i),( - a))));

      existence

      proof

        defpred P[ Element of the carrier of INT.Ring , Element of AG, Element of AG] means ($1 >= 0 implies $3 = (( Nat-mult-left AG) . ($1,$2))) & ($1 < 0 implies $3 = (( Nat-mult-left AG) . (( - $1),( - $2))));

        

         A1: for x be Element of the carrier of INT.Ring holds for y be Element of AG holds ex z be Element of AG st P[x, y, z]

        proof

          let x be Element of the carrier of INT.Ring , y be Element of AG;

          reconsider xx = x as Element of INT ;

          per cases ;

            suppose x >= 0 ;

            then

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

            reconsider z = (( Nat-mult-left AG) . (x0,y)) as Element of AG;

             P[x, y, z];

            hence thesis;

          end;

            suppose

             a2: x < 0 ;

            then

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

            reconsider z = (( Nat-mult-left AG) . (x0,( - y))) as Element of AG;

            

             T1: (x >= 0 implies z = (( Nat-mult-left AG) . (x,y))) by a2;

             P[x, y, z] by T1;

            hence thesis;

          end;

        end;

        consider f be Function of [:the carrier of INT.Ring , the carrier of AG:], the carrier of AG such that

         A3: for x be Element of the carrier of INT.Ring holds for y be Element of the carrier of AG holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

        take f;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let f1,f2 be Function of [:the carrier of INT.Ring , the carrier of AG:], the carrier of AG;

        assume

         A4: for i be Element of INT.Ring , a be Element of AG holds (i >= 0 implies (f1 . (i,a)) = (( Nat-mult-left AG) . (i,a))) & (i < 0 implies (f1 . (i,a)) = (( Nat-mult-left AG) . (( - i),( - a))));

        assume

         A5: for i be Element of INT.Ring , a be Element of AG holds (i >= 0 implies (f2 . (i,a)) = (( Nat-mult-left AG) . (i,a))) & (i < 0 implies (f2 . (i,a)) = (( Nat-mult-left AG) . (( - i),( - a))));

        for x,y be set st x in INT & y in the carrier of AG holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be set;

          assume

           A6: x in INT & y in the carrier of AG;

          then

          reconsider x0 = x as Element of INT ;

          reconsider x1 = x as Element of INT.Ring by A6;

          reconsider y0 = y as Element of AG by A6;

          per cases ;

            suppose

             A7: 0 <= x0;

            

            hence (f1 . (x,y)) = (( Nat-mult-left AG) . (x0,y0)) by A4

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

          end;

            suppose

             A8: 0 > x0;

            

            hence (f1 . (x,y)) = (( Nat-mult-left AG) . (( - x1),( - y0))) by A4

            .= (f2 . (x,y)) by A5, A8;

          end;

        end;

        hence f1 = f2;

      end;

    end

    theorem :: ZMODUL01:151

    for R be non empty addLoopStr, a be Element of R, i be Element of INT.Ring , i1 be Element of NAT st i = i1 holds (( Int-mult-left R) . (i,a)) = (i1 * a) by Def23;

    theorem :: ZMODUL01:152

    

     Th152: for R be non empty addLoopStr, a be Element of R, i be Integer st i = 0 holds (( Int-mult-left R) . (i,a)) = ( 0. R)

    proof

      let R be non empty addLoopStr, a be Element of R, i be Integer;

      assume i = 0 ;

      

      hence (( Int-mult-left R) . (i,a)) = ( 0 * a) by Def23

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

    end;

    theorem :: ZMODUL01:153

    

     Th153: for R be add-associative right_zeroed right_complementable non empty addLoopStr, i be Element of NAT holds (( Nat-mult-left R) . (i,( 0. R))) = ( 0. R)

    proof

      let R be add-associative right_zeroed right_complementable non empty addLoopStr, i be Element of NAT ;

      defpred P[ Nat] means (( Nat-mult-left R) . ($1,( 0. R))) = ( 0. R);

      

       A1: P[ 0 ] by BINOM:def 3;

      

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

      proof

        let n be Nat;

        assume

         A3: P[n];

        (( Nat-mult-left R) . ((n + 1),( 0. R))) = (( 0. R) + ( 0. R)) by A3, BINOM:def 3

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

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: ZMODUL01:154

    

     Th154: for R be add-associative right_zeroed right_complementable non empty addLoopStr, i be Element of INT.Ring holds (( Int-mult-left R) . (i,( 0. R))) = ( 0. R)

    proof

      let R be add-associative right_zeroed right_complementable non empty addLoopStr, i be Element of INT.Ring ;

      reconsider ii = i as Element of INT ;

      per cases ;

        suppose 0 <= i;

        then

        reconsider i1 = i as Element of NAT by INT_1: 3;

        

        thus (( Int-mult-left R) . (i,( 0. R))) = (( Nat-mult-left R) . (i1,( 0. R))) by Def23

        .= ( 0. R) by Th153;

      end;

        suppose

         A1: 0 > i;

        then

        reconsider i1 = ( - ii) as Element of NAT by INT_1: 3;

        

        thus (( Int-mult-left R) . (i,( 0. R))) = (( Nat-mult-left R) . (( - i),( - ( 0. R)))) by Def23, A1

        .= (( Nat-mult-left R) . (i1,( 0. R))) by RLVECT_1: 12

        .= ( 0. R) by Th153;

      end;

    end;

    theorem :: ZMODUL01:155

    

     Th155: for R be right_zeroed non empty addLoopStr, a be Element of R, i be Integer st i = 1 holds (( Int-mult-left R) . (i,a)) = a

    proof

      let R be right_zeroed non empty addLoopStr, a be Element of R, i be Integer;

      assume i = 1;

      

      hence (( Int-mult-left R) . (i,a)) = (1 * a) by Def23

      .= a by BINOM: 13;

    end;

    theorem :: ZMODUL01:156

    

     Th156: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j,k be Element of NAT st i <= j & k = (j - i) holds (( Nat-mult-left R) . (k,a)) = ((( Nat-mult-left R) . (j,a)) - (( Nat-mult-left R) . (i,a)))

    proof

      let R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j,k be Element of NAT ;

      assume

       A1: i <= j & k = (j - i);

      

       A2: (j * a) = ((k + i) * a) by A1

      .= ((k * a) + (i * a)) by BINOM: 15;

      

      thus ((( Nat-mult-left R) . (j,a)) - (( Nat-mult-left R) . (i,a))) = ((k * a) + ((i * a) - (i * a))) by A2, RLVECT_1: 28

      .= ((k * a) + ( 0. R)) by RLVECT_1: 15

      .= (( Nat-mult-left R) . (k,a)) by RLVECT_1: 4;

    end;

    theorem :: ZMODUL01:157

    

     Th157: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i be Element of NAT holds ( - (( Nat-mult-left R) . (i,a))) = (( Nat-mult-left R) . (i,( - a)))

    proof

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

      defpred P[ Nat] means ((( Nat-mult-left R) . ($1,a)) + (( Nat-mult-left R) . ($1,( - a)))) = ( 0. R);

      

       A1: P[ 0 ]

      proof

        ((( Nat-mult-left R) . ( 0 ,a)) + (( Nat-mult-left R) . ( 0 ,( - a)))) = (( 0. R) + (( Nat-mult-left R) . ( 0 ,( - a)))) by BINOM:def 3

        .= (( 0. R) + ( 0. R)) by BINOM:def 3

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

        hence thesis;

      end;

      

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

      proof

        let n be Nat;

        assume

         A3: P[n];

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

        .= ((a + (( Nat-mult-left R) . (n,a))) + (( - a) + (( Nat-mult-left R) . (n,( - a))))) by BINOM:def 3

        .= (((a + (( Nat-mult-left R) . (n,a))) + (( Nat-mult-left R) . (n,( - a)))) + ( - a)) by RLVECT_1:def 3

        .= ((a + ((( Nat-mult-left R) . (n,a)) + (( Nat-mult-left R) . (n,( - a))))) + ( - a)) by RLVECT_1:def 3

        .= (a + ( - a)) by A3, RLVECT_1: 4

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

        hence P[(n + 1)];

      end;

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

      then ((( Nat-mult-left R) . (i,a)) + (( Nat-mult-left R) . (i,( - a)))) = ( 0. R);

      hence thesis by RLVECT_1: 6;

    end;

    theorem :: ZMODUL01:158

    

     Th158: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring st i in NAT & not j in NAT holds (( Int-mult-left R) . ((i + j),a)) = ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (j,a)))

    proof

      let R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring ;

      reconsider jj = j, ii = i, ij = (i + j) as Element of INT ;

      assume

       A1: i in NAT & not j in NAT ;

      then

      reconsider i1 = i as Element of NAT ;

      

       A2: jj < 0 by A1, INT_1: 3;

      then

      reconsider j1 = ( - jj) as Element of NAT by INT_1: 3;

      per cases ;

        suppose

         A4: j1 <= i1;

        reconsider k1 = (i1 - j1) as Element of NAT by A4, INT_1: 5;

        set IT = ( Int-mult-left R);

        

         W1: (( Int-mult-left R) . (jj,a)) = (( Nat-mult-left R) . (( - j),( - a))) by A2, Def23;

        

        thus (( Int-mult-left R) . ((i + j),a)) = (( Nat-mult-left R) . (k1,a)) by Def23

        .= ((( Nat-mult-left R) . (i1,a)) - (( Nat-mult-left R) . (j1,a))) by Th156, A4

        .= ((( Nat-mult-left R) . (i1,a)) + (( Nat-mult-left R) . (j1,( - a)))) by Th157

        .= ((( Int-mult-left R) . (i,a)) + (( Nat-mult-left R) . (j1,( - a)))) by Def23

        .= ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (j,a))) by W1;

      end;

        suppose

         A5: j1 > i1;

        then

        reconsider k1 = (j1 - i1) as Element of NAT by INT_1: 5;

        

         A6: (i1 - j1) < 0 by A5, XREAL_1: 49;

        

         Z1: (( Int-mult-left R) . (j,a)) = (( Nat-mult-left R) . (( - j),( - a))) by Def23, A2;

        

        thus (( Int-mult-left R) . ((i + j),a)) = (( Nat-mult-left R) . (( - (i + j)),( - a))) by A6, Def23

        .= (( Nat-mult-left R) . (k1,( - a)))

        .= ((( Nat-mult-left R) . (j1,( - a))) - (( Nat-mult-left R) . (i1,( - a)))) by Th156, A5

        .= ((( Nat-mult-left R) . (j1,( - a))) + (( Nat-mult-left R) . (i1,( - ( - a))))) by Th157

        .= ((( Nat-mult-left R) . (j1,( - a))) + (( Nat-mult-left R) . (i1,a))) by RLVECT_1: 17

        .= ((( Int-mult-left R) . (j,a)) + (( Int-mult-left R) . (i,a))) by Def23, Z1

        .= ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (j,a)));

      end;

    end;

    theorem :: ZMODUL01:159

    

     Th159: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring holds (( Int-mult-left R) . ((i + j),a)) = ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (j,a)))

    proof

      let R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring ;

      reconsider ii = i, jj = j as Element of INT ;

      per cases ;

        suppose

         A1: i in NAT & j in NAT ;

        then

        reconsider i1 = i as Element of NAT ;

        reconsider j1 = j as Element of NAT by A1;

        

        thus (( Int-mult-left R) . ((i + j),a)) = (( Nat-mult-left R) . ((i1 + j1),a)) by Def23

        .= ((i1 + j1) * a)

        .= ((i1 * a) + (j1 * a)) by BINOM: 15

        .= ((( Int-mult-left R) . (i,a)) + (( Nat-mult-left R) . (j1,a))) by Def23

        .= ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (j,a))) by Def23;

      end;

        suppose i in NAT & not j in NAT ;

        hence (( Int-mult-left R) . ((i + j),a)) = ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (j,a))) by Th158;

      end;

        suppose not i in NAT & j in NAT ;

        hence (( Int-mult-left R) . ((i + j),a)) = ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (j,a))) by Th158;

      end;

        suppose not i in NAT & not j in NAT ;

        then

         A3: i < 0 & j < 0 by INT_1: 3;

        then

        reconsider i1 = ( - ii) as Element of NAT by INT_1: 3;

        reconsider j1 = ( - jj) as Element of NAT by A3, INT_1: 3;

        

         S1: (( Int-mult-left R) . (i,a)) = (( Nat-mult-left R) . (( - i),( - a))) by A3, Def23

        .= (i1 * ( - a));

        

         S2: (( Nat-mult-left R) . (( - j),( - a))) = (j1 * ( - a));

        

        thus (( Int-mult-left R) . ((i + j),a)) = (( Nat-mult-left R) . (( - (i + j)),( - a))) by Def23, A3

        .= ((i1 + j1) * ( - a))

        .= ((i1 * ( - a)) + (j1 * ( - a))) by BINOM: 15

        .= ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (j,a))) by A3, Def23, S1, S2;

      end;

    end;

    theorem :: ZMODUL01:160

    

     Th160: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a,b be Element of R, i be Element of NAT holds (( Nat-mult-left R) . (i,(a + b))) = ((( Nat-mult-left R) . (i,a)) + (( Nat-mult-left R) . (i,b)))

    proof

      let R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a,b be Element of R, i be Element of NAT ;

      defpred P[ Nat] means (( Nat-mult-left R) . ($1,(a + b))) = ((( Nat-mult-left R) . ($1,a)) + (( Nat-mult-left R) . ($1,b)));

      

       A1: P[ 0 ]

      proof

        (( Nat-mult-left R) . ( 0 ,(a + b))) = ( 0. R) by BINOM:def 3

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

        .= ((( Nat-mult-left R) . ( 0 ,a)) + ( 0. R)) by BINOM:def 3

        .= ((( Nat-mult-left R) . ( 0 ,a)) + (( Nat-mult-left R) . ( 0 ,b))) by BINOM:def 3;

        hence thesis;

      end;

      

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

      proof

        let n be Nat;

        assume

         A3: P[n];

        (( Nat-mult-left R) . ((n + 1),(a + b))) = ((a + b) + (( Nat-mult-left R) . (n,(a + b)))) by BINOM:def 3

        .= (((a + b) + (( Nat-mult-left R) . (n,a))) + (( Nat-mult-left R) . (n,b))) by A3, RLVECT_1:def 3

        .= (((a + (( Nat-mult-left R) . (n,a))) + b) + (( Nat-mult-left R) . (n,b))) by RLVECT_1:def 3

        .= (((( Nat-mult-left R) . ((n + 1),a)) + b) + (( Nat-mult-left R) . (n,b))) by BINOM:def 3

        .= ((( Nat-mult-left R) . ((n + 1),a)) + (b + (( Nat-mult-left R) . (n,b)))) by RLVECT_1:def 3

        .= ((( Nat-mult-left R) . ((n + 1),a)) + (( Nat-mult-left R) . ((n + 1),b))) by BINOM:def 3;

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: ZMODUL01:161

    

     Th161: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a,b be Element of R, i be Element of INT.Ring holds (( Int-mult-left R) . (i,(a + b))) = ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (i,b)))

    proof

      let R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a,b be Element of R, i be Element of INT.Ring ;

      reconsider ii = i as Element of INT ;

      per cases ;

        suppose 0 <= i;

        then

        reconsider i1 = i as Element of NAT by INT_1: 3;

        

        thus (( Int-mult-left R) . (i,(a + b))) = (( Nat-mult-left R) . (i1,(a + b))) by Def23

        .= ((i1 * a) + (i1 * b)) by Th160

        .= ((( Int-mult-left R) . (i,a)) + (( Nat-mult-left R) . (i1,b))) by Def23

        .= ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (i,b))) by Def23;

      end;

        suppose

         A1: 0 > i;

        then

        reconsider i1 = ( - ii) as Element of NAT by INT_1: 3;

        ((a + b) + (( - a) + ( - b))) = (((b + a) + ( - a)) + ( - b)) by RLVECT_1:def 3

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

        .= ((b + ( 0. R)) + ( - b)) by RLVECT_1: 5

        .= (b + ( - b)) by RLVECT_1: 4

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

        then

         A2: ( - (a + b)) = (( - a) + ( - b)) by RLVECT_1: 6;

        

         S1: (i1 * ( - a)) = (( Nat-mult-left R) . (( - i),( - a)))

        .= (( Int-mult-left R) . (i,a)) by A1, Def23;

        

         S2: (i1 * ( - b)) = (( Nat-mult-left R) . (( - i),( - b)));

        

        thus (( Int-mult-left R) . (i,(a + b))) = (( Nat-mult-left R) . (( - i),( - (a + b)))) by Def23, A1

        .= ((i1 * ( - a)) + (i1 * ( - b))) by A2, Th160

        .= ((( Int-mult-left R) . (i,a)) + (( Int-mult-left R) . (i,b))) by A1, Def23, S1, S2;

      end;

    end;

    theorem :: ZMODUL01:162

    

     Th162: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of NAT holds (( Nat-mult-left R) . ((i * j),a)) = (( Nat-mult-left R) . (i,(( Nat-mult-left R) . (j,a))))

    proof

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

      defpred P[ Nat] means (( Nat-mult-left R) . (($1 * j),a)) = (( Nat-mult-left R) . ($1,(( Nat-mult-left R) . (j,a))));

      

       A1: P[ 0 ]

      proof

        (( Nat-mult-left R) . (( 0 * j),a)) = ( 0. R) by BINOM:def 3

        .= (( Nat-mult-left R) . ( 0 ,(( Nat-mult-left R) . (j,a)))) by BINOM:def 3;

        hence thesis;

      end;

      

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

      proof

        let n be Nat;

        assume

         A3: P[n];

        (( Nat-mult-left R) . (((n + 1) * j),a)) = ((j + (n * j)) * a)

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

        .= (( Nat-mult-left R) . ((n + 1),(j * a))) by A3, BINOM:def 3;

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    

     Lm19: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring st i <> 0 & j <> 0 holds (( Int-mult-left R) . ((i * j),a)) = (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a))))

    proof

      let R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring ;

      reconsider ii = i, jj = j as Element of INT ;

      assume

       A1: i <> 0 & j <> 0 ;

      per cases ;

        suppose

         A2: i in NAT & j in NAT ;

        then

        reconsider i1 = i as Element of NAT ;

        reconsider j1 = j as Element of NAT by A2;

        

        thus (( Int-mult-left R) . ((i * j),a)) = (( Nat-mult-left R) . ((i1 * j1),a)) by Def23

        .= (( Nat-mult-left R) . (i1,(( Nat-mult-left R) . (j1,a)))) by Th162

        .= (( Nat-mult-left R) . (i1,(( Int-mult-left R) . (j,a)))) by Def23

        .= (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a)))) by Def23;

      end;

        suppose

         A4: i in NAT & not j in NAT ;

        then

         A5: 0 < i & jj < 0 by A1, INT_1: 3;

        reconsider i1 = i as Element of NAT by A4;

        reconsider j1 = ( - jj) as Element of NAT by A5, INT_1: 3;

        

         a7: (ii * jj) < 0 by XREAL_1: 132, A5;

        

        thus (( Int-mult-left R) . ((i * j),a)) = (( Nat-mult-left R) . (( - (i * j)),( - a))) by a7, Def23

        .= (( Nat-mult-left R) . ((i1 * j1),( - a)))

        .= (( Nat-mult-left R) . (i1,(( Nat-mult-left R) . (( - j),( - a))))) by Th162

        .= (( Nat-mult-left R) . (i1,(( Int-mult-left R) . (j,a)))) by Def23, A5

        .= (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a)))) by Def23;

      end;

        suppose

         A8: not i in NAT & j in NAT ;

        then

         A9: 0 < j & i < 0 by A1, INT_1: 3;

        then

        reconsider i1 = ( - ii) as Element of NAT by INT_1: 3;

        reconsider j1 = j as Element of NAT by A8;

        

         A11: (ii * jj) < 0 by A9, XREAL_1: 132;

        

        thus (( Int-mult-left R) . ((i * j),a)) = (( Nat-mult-left R) . (( - (i * j)),( - a))) by A11, Def23

        .= (( Nat-mult-left R) . ((i1 * j1),( - a)))

        .= (( Nat-mult-left R) . (( - i),(( Nat-mult-left R) . (j1,( - a))))) by Th162

        .= (( Nat-mult-left R) . (( - i),( - (( Nat-mult-left R) . (j1,a))))) by Th157

        .= (( Nat-mult-left R) . (( - i),( - (( Int-mult-left R) . (j,a))))) by Def23

        .= (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a)))) by A9, Def23;

      end;

        suppose not i in NAT & not j in NAT ;

        then

         A13: i < 0 & j < 0 by INT_1: 3;

        then

        reconsider i1 = ( - ii) as Element of NAT by INT_1: 3;

        reconsider j1 = ( - jj) as Element of NAT by A13, INT_1: 3;

        ( - (( Nat-mult-left R) . (j1,a))) = (( Nat-mult-left R) . (j1,( - a))) by Th157;

        then ((( Nat-mult-left R) . (j1,( - a))) + (( Nat-mult-left R) . (j1,a))) = ( 0. R) by RLVECT_1:def 10;

        then

         A15: (( Nat-mult-left R) . (j1,a)) = ( - (( Nat-mult-left R) . (j1,( - a)))) by RLVECT_1:def 10;

        

        thus (( Int-mult-left R) . ((i * j),a)) = (( Nat-mult-left R) . ((i1 * j1),a)) by Def23

        .= (( Nat-mult-left R) . (( - i),(( Nat-mult-left R) . (( - j),a)))) by Th162

        .= (( Nat-mult-left R) . (( - i),( - (( Int-mult-left R) . (j,a))))) by A13, A15, Def23

        .= (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a)))) by A13, Def23;

      end;

    end;

    

     Lm20: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring st i = 0 or j = 0 holds (( Int-mult-left R) . ((i * j),a)) = (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a))))

    proof

      let R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring ;

      assume

       A1: i = 0 or j = 0 ;

      per cases by A1;

        suppose

         A2: i = 0 ;

        

        hence (( Int-mult-left R) . ((i * j),a)) = ( 0. R) by Th152

        .= (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a)))) by A2, Th152;

      end;

        suppose

         A3: j = 0 ;

        

        hence (( Int-mult-left R) . ((i * j),a)) = ( 0. R) by Th152

        .= (( Int-mult-left R) . (i,( 0. R))) by Th154

        .= (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a)))) by Th152, A3;

      end;

    end;

    theorem :: ZMODUL01:163

    

     Th163: for R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring holds (( Int-mult-left R) . ((i * j),a)) = (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a))))

    proof

      let R be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, a be Element of R, i,j be Element of INT.Ring ;

      per cases ;

        suppose i = 0 or j = 0 ;

        hence (( Int-mult-left R) . ((i * j),a)) = (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a)))) by Lm20;

      end;

        suppose not (i = 0 or j = 0 );

        hence (( Int-mult-left R) . ((i * j),a)) = (( Int-mult-left R) . (i,(( Int-mult-left R) . (j,a)))) by Lm19;

      end;

    end;

    theorem :: ZMODUL01:164

    for AG be non empty Abelian add-associative right_zeroed right_complementable addLoopStr holds ModuleStr (# the carrier of AG, the addF of AG, the ZeroF of AG, ( Int-mult-left AG) #) is Z_Module

    proof

      let AG be non empty Abelian add-associative right_zeroed right_complementable addLoopStr;

      reconsider ZS = ModuleStr (# the carrier of AG, the addF of AG, the ZeroF of AG, ( Int-mult-left AG) #) as non empty ModuleStr over INT.Ring ;

      set ML = the lmult of ZS;

      set AD = the addF of ZS;

      set CA = the carrier of ZS;

      set Z0 = the ZeroF of ZS;

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

      

       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 AG;

        

        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 AG;

        

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

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

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

      end;

      

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

      proof

        let v be Vector of ZS;

        reconsider v1 = v as Element of AG;

        

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

        .= v by RLVECT_1:def 4;

      end;

       A4:

      now

        let v be Vector of ZS;

        reconsider v1 = v as Element of AG;

        consider w1 be Element of AG such that

         A5: (v1 + w1) = ( 0. AG) by ALGSTR_0:def 11;

        reconsider w = w1 as Element of ZS;

        (v + w) = ( 0. ZS) by A5;

        hence v is right_complementable;

      end;

      

       A6: 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 , v be Vector of ZS;

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

        reconsider v1 = v as Element of AG;

        

        thus ((a + b) * v) = ((MLI . (a,v1)) + (MLI . (b,v1))) by Th159

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

      end;

      

       A7: 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 , v,w be Vector of ZS;

        reconsider a1 = a as Element of INT.Ring ;

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

        

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

        .= ((MLI . (a1,v1)) + (MLI . (a1,w1))) by Th161

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

      end;

      

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

      for v be Vector of ZS holds (( 1. INT.Ring ) * v) = v by Th155;

      hence thesis by A1, A2, A3, A4, A6, A7, A8, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

    end;