rmod_4.miz



    begin

    reserve R for Ring,

V for RightMod of R,

a,b for Scalar of R,

x,y for set,

p,q,r for FinSequence,

i,k for Nat,

u,v,v1,v2,v3,w for Vector of V,

F,G,H for FinSequence of V,

A,B for Subset of V,

f for Function of V, R,

S,T for finite Subset of V;

    

     Lm1: ( len F) = (( len G) + 1) & G = (F | ( Seg ( len G))) & v = (F . ( len F)) implies ( Sum F) = (( Sum G) + v)

    proof

      ( len F) = (( len G) + 1) & G = (F | ( dom G)) & v = (F . ( len F)) implies ( Sum F) = (( Sum G) + v) by RLVECT_1: 38;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: RMOD_4:1

    

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

    proof

      defpred P[ Nat] means for H,I be FinSequence of V st ( len H) = ( len I) & ( len H) = $1 & (for k, v st k in ( dom H) & v = (I . k) holds (H . k) = (v * a)) holds ( Sum H) = (( Sum I) * a);

      now

        let n be Nat;

        assume

         A1: for H,I be FinSequence of V st ( len H) = ( len I) & ( len H) = n & for k, v st k in ( dom H) & v = (I . k) holds (H . k) = (v * a) holds ( Sum H) = (( Sum I) * a);

        let H,I be FinSequence of V;

        assume that

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

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

         A4: for k, v st k in ( dom H) & v = (I . k) holds (H . k) = (v * a);

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

        

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

        then

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

        

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

         A8:

        now

          ( len p) <= ( len H) by A3, A5, FINSEQ_1: 17;

          then

           A9: ( dom p) c= ( dom H) by FINSEQ_3: 30;

          let k, v;

          assume that

           A10: k in ( dom p) and

           A11: v = (q . k);

          ( dom p) = ( dom q) by A6, A7, FINSEQ_3: 29;

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

          then (H . k) = (v * a) by A4, A10, A11, A9;

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

        end;

        

         A12: (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then (n + 1) in ( dom H) & (n + 1) in ( dom I) by A2, A3, FINSEQ_1:def 3;

        then

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

        (n + 1) in ( dom H) by A3, A12, FINSEQ_1:def 3;

        then

         A13: v1 = (v2 * a) by A4;

        

        thus ( Sum H) = (( Sum p) + v1) by A3, A6, Lm1

        .= ((( Sum q) * a) + (v2 * a)) by A1, A6, A7, A8, A13

        .= ((( Sum q) + v2) * a) by VECTSP_2:def 9

        .= (( Sum I) * a) by A2, A3, A7, Lm1;

      end;

      then

       A14: for i be Nat st P[i] holds P[(i + 1)];

      now

        let H,I be FinSequence of V;

        assume that

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

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

        H = ( <*> the carrier of V) by A16;

        then

         A17: ( Sum H) = ( 0. V) by RLVECT_1: 43;

        I = ( <*> the carrier of V) by A15, A16;

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

        hence ( Sum H) = (( Sum I) * a) by A17, VECTSP_2: 32;

      end;

      then

       A18: P[ 0 ];

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

      hence thesis;

    end;

    

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

    proof

      assume that

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

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

      now

        let k, v;

        assume that

         A3: k in ( dom G) and

         A4: v = (F . k);

        

         A5: k in ( dom F) by A1, A3, FINSEQ_3: 29;

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

        hence (G . k) = (v * a) by A2, A5;

      end;

      hence thesis by A1, Th1;

    end;

    theorem :: RMOD_4:2

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

    proof

      

      thus (( Sum ( <*> the carrier of V)) * a) = (( 0. V) * a) by RLVECT_1: 43

      .= ( 0. V) by VECTSP_2: 32;

    end;

    theorem :: RMOD_4:3

    (( Sum <*v, u*>) * a) = ((v * a) + (u * a))

    proof

      

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

      .= ((v * a) + (u * a)) by VECTSP_2:def 9;

    end;

    theorem :: RMOD_4:4

    (( Sum <*v, u, w*>) * a) = (((v * a) + (u * a)) + (w * a))

    proof

      

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

      .= (((v + u) * a) + (w * a)) by VECTSP_2:def 9

      .= (((v * a) + (u * a)) + (w * a)) by VECTSP_2:def 9;

    end;

    definition

      let R, V, T;

      :: RMOD_4:def1

      func Sum (T) -> Vector of V means

      : Def1: ex F st ( rng F) = T & F is one-to-one & it = ( Sum F);

      existence

      proof

        consider p such that

         A1: ( rng p) = T and

         A2: p is one-to-one by FINSEQ_4: 58;

        reconsider p as FinSequence of V by A1, FINSEQ_1:def 4;

        take ( Sum p);

        take p;

        thus thesis by A1, A2;

      end;

      uniqueness by RLVECT_1: 42;

    end

    theorem :: RMOD_4:5

    

     Th5: ( Sum ( {} V)) = ( 0. V)

    proof

      ( Sum ( <*> the carrier of V)) = ( 0. V) by RLVECT_1: 43;

      hence thesis by Def1, RELAT_1: 38;

    end;

    theorem :: RMOD_4:6

    ( Sum {v}) = v

    proof

      

       A1: ( Sum <*v*>) = v by RLVECT_1: 44;

      ( rng <*v*>) = {v} & <*v*> is one-to-one by FINSEQ_1: 39, FINSEQ_3: 93;

      hence thesis by A1, Def1;

    end;

    theorem :: RMOD_4:7

    v1 <> v2 implies ( Sum {v1, v2}) = (v1 + v2)

    proof

      assume v1 <> v2;

      then

       A1: <*v1, v2*> is one-to-one by FINSEQ_3: 94;

      ( rng <*v1, v2*>) = {v1, v2} & ( Sum <*v1, v2*>) = (v1 + v2) by FINSEQ_2: 127, RLVECT_1: 45;

      hence thesis by A1, Def1;

    end;

    theorem :: RMOD_4:8

    v1 <> v2 & v2 <> v3 & v1 <> v3 implies ( Sum {v1, v2, v3}) = ((v1 + v2) + v3)

    proof

      assume v1 <> v2 & v2 <> v3 & v1 <> v3;

      then

       A1: <*v1, v2, v3*> is one-to-one by FINSEQ_3: 95;

      ( rng <*v1, v2, v3*>) = {v1, v2, v3} & ( Sum <*v1, v2, v3*>) = ((v1 + v2) + v3) by FINSEQ_2: 128, RLVECT_1: 46;

      hence thesis by A1, Def1;

    end;

    theorem :: RMOD_4:9

    

     Th9: T misses S implies ( Sum (T \/ S)) = (( Sum T) + ( Sum S))

    proof

      consider F such that

       A1: ( rng F) = (T \/ S) and

       A2: F is one-to-one & ( Sum (T \/ S)) = ( Sum F) by Def1;

      consider G such that

       A3: ( rng G) = T and

       A4: G is one-to-one and

       A5: ( Sum T) = ( Sum G) by Def1;

      consider H such that

       A6: ( rng H) = S and

       A7: H is one-to-one and

       A8: ( Sum S) = ( Sum H) by Def1;

      set I = (G ^ H);

      assume T misses S;

      then

       A9: I is one-to-one by A3, A4, A6, A7, FINSEQ_3: 91;

      ( rng I) = ( rng F) by A1, A3, A6, FINSEQ_1: 31;

      

      hence ( Sum (T \/ S)) = ( Sum I) by A2, A9, RLVECT_1: 42

      .= (( Sum T) + ( Sum S)) by A5, A8, RLVECT_1: 41;

    end;

    theorem :: RMOD_4:10

    

     Th10: ( Sum (T \/ S)) = ((( Sum T) + ( Sum S)) - ( Sum (T /\ S)))

    proof

      set A = (S \ T);

      set B = (T \ S);

      set Z = (A \/ B);

      set I = (T /\ S);

      

       A1: (A \/ I) = S by XBOOLE_1: 51;

      

       A2: (B \/ I) = T by XBOOLE_1: 51;

      

       A3: Z = (T \+\ S);

      then (Z \/ I) = (T \/ S) by XBOOLE_1: 93;

      

      then (( Sum (T \/ S)) + ( Sum I)) = ((( Sum Z) + ( Sum I)) + ( Sum I)) by A3, Th9, XBOOLE_1: 103

      .= (((( Sum A) + ( Sum B)) + ( Sum I)) + ( Sum I)) by Th9, XBOOLE_1: 82

      .= ((( Sum A) + (( Sum I) + ( Sum B))) + ( Sum I)) by RLVECT_1:def 3

      .= ((( Sum A) + ( Sum I)) + (( Sum B) + ( Sum I))) by RLVECT_1:def 3

      .= (( Sum S) + (( Sum B) + ( Sum I))) by A1, Th9, XBOOLE_1: 89

      .= (( Sum T) + ( Sum S)) by A2, Th9, XBOOLE_1: 89;

      hence thesis by RLSUB_2: 61;

    end;

    theorem :: RMOD_4:11

    ( Sum (T /\ S)) = ((( Sum T) + ( Sum S)) - ( Sum (T \/ S)))

    proof

      ( Sum (T \/ S)) = ((( Sum T) + ( Sum S)) - ( Sum (T /\ S))) by Th10;

      then (( Sum T) + ( Sum S)) = (( Sum (T /\ S)) + ( Sum (T \/ S))) by RLSUB_2: 61;

      hence thesis by RLSUB_2: 61;

    end;

    theorem :: RMOD_4:12

    

     Th12: ( Sum (T \ S)) = (( Sum (T \/ S)) - ( Sum S))

    proof

      (T \ S) misses S by XBOOLE_1: 79;

      then

       A1: ((T \ S) /\ S) = ( {} V);

      ((T \ S) \/ S) = (T \/ S) by XBOOLE_1: 39;

      then ( Sum (T \/ S)) = ((( Sum (T \ S)) + ( Sum S)) - ( Sum ((T \ S) /\ S))) by Th10;

      

      then ( Sum (T \/ S)) = ((( Sum (T \ S)) + ( Sum S)) - ( 0. V)) by A1, Th5

      .= (( Sum (T \ S)) + ( Sum S)) by VECTSP_1: 18;

      hence thesis by RLSUB_2: 61;

    end;

    theorem :: RMOD_4:13

    

     Th13: ( Sum (T \ S)) = (( Sum T) - ( Sum (T /\ S)))

    proof

      (T \ (T /\ S)) = (T \ S) by XBOOLE_1: 47;

      then ( Sum (T \ S)) = (( Sum (T \/ (T /\ S))) - ( Sum (T /\ S))) by Th12;

      hence thesis by XBOOLE_1: 22;

    end;

    theorem :: RMOD_4:14

    ( Sum (T \+\ S)) = (( Sum (T \/ S)) - ( Sum (T /\ S)))

    proof

      (T \+\ S) = ((T \/ S) \ (T /\ S)) by XBOOLE_1: 101;

      

      hence ( Sum (T \+\ S)) = (( Sum (T \/ S)) - ( Sum ((T \/ S) /\ (T /\ S)))) by Th13

      .= (( Sum (T \/ S)) - ( Sum (((T \/ S) /\ T) /\ S))) by XBOOLE_1: 16

      .= (( Sum (T \/ S)) - ( Sum (T /\ S))) by XBOOLE_1: 21;

    end;

    theorem :: RMOD_4:15

    ( Sum (T \+\ S)) = (( Sum (T \ S)) + ( Sum (S \ T))) by Th9, XBOOLE_1: 82;

    definition

      let R, V;

      :: RMOD_4:def2

      mode Linear_Combination of V -> Element of ( Funcs (the carrier of V,the carrier of R)) means

      : Def2: ex T st for v st not v in T holds (it . v) = ( 0. R);

      existence

      proof

        ( {} V) = {} ;

        then

        reconsider P = {} as finite Subset of V;

        reconsider f = (the carrier of V --> ( 0. R)) as Function of V, R;

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

        take f;

        take P;

        thus thesis by FUNCOP_1: 7;

      end;

    end

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

    definition

      let R, V, L;

      :: RMOD_4:def3

      func Carrier (L) -> finite Subset of V equals { v : (L . v) <> ( 0. R) };

      coherence

      proof

        set A = { v : (L . v) <> ( 0. R) };

        consider T such that

         A1: for v st not v in T holds (L . v) = ( 0. R) by Def2;

        A c= T

        proof

          let x be object;

          assume x in A;

          then ex v st x = v & (L . v) <> ( 0. R);

          hence thesis by A1;

        end;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    theorem :: RMOD_4:16

    x in ( Carrier L) iff ex v st x = v & (L . v) <> ( 0. R);

    theorem :: RMOD_4:17

    (L . v) = ( 0. R) iff not v in ( Carrier L)

    proof

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

      proof

        assume

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

        assume not thesis;

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

        hence thesis by A1;

      end;

      assume not v in ( Carrier L);

      hence thesis;

    end;

    definition

      let R, V;

      :: RMOD_4:def4

      func ZeroLC (V) -> Linear_Combination of V means

      : Def4: ( Carrier it ) = {} ;

      existence

      proof

        reconsider f = (the carrier of V --> ( 0. R)) as Function of V, R;

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

        f is Linear_Combination of V

        proof

          reconsider T = ( {} V) as finite empty Subset of V;

          take T;

          thus thesis by FUNCOP_1: 7;

        end;

        then

        reconsider f as Linear_Combination of V;

        take f;

        set C = { v : (f . v) <> ( 0. R) };

        now

          set x = the Element of C;

          assume C <> {} ;

          then x in C;

          then ex v st x = v & (f . v) <> ( 0. R);

          hence contradiction by FUNCOP_1: 7;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let L,L9 be Linear_Combination of V;

        assume that

         A1: ( Carrier L) = {} and

         A2: ( Carrier L9) = {} ;

        now

          let x be object;

          assume x in the carrier of V;

          then

          reconsider v = x as Element of V;

           A3:

          now

            assume (L9 . v) <> ( 0. R);

            then v in { u : (L9 . u) <> ( 0. R) };

            hence contradiction by A2;

          end;

          now

            assume (L . v) <> ( 0. R);

            then v in { u : (L . u) <> ( 0. R) };

            hence contradiction by A1;

          end;

          hence (L . x) = (L9 . x) by A3;

        end;

        hence L = L9 by FUNCT_2: 12;

      end;

    end

    theorem :: RMOD_4:18

    

     Th18: (( ZeroLC V) . v) = ( 0. R)

    proof

      ( Carrier ( ZeroLC V)) = {} & not v in {} by Def4;

      hence thesis;

    end;

    definition

      let R, V, A;

      :: RMOD_4:def5

      mode Linear_Combination of A -> Linear_Combination of V means

      : Def5: ( Carrier it ) c= A;

      existence

      proof

        take L = ( ZeroLC V);

        ( Carrier L) = {} by Def4;

        hence thesis;

      end;

    end

    reserve l for Linear_Combination of A;

    theorem :: RMOD_4:19

    

     Th19: A c= B implies l is Linear_Combination of B

    proof

      assume

       A1: A c= B;

      ( Carrier l) c= A by Def5;

      then ( Carrier l) c= B by A1;

      hence thesis by Def5;

    end;

    theorem :: RMOD_4:20

    

     Th20: ( ZeroLC V) is Linear_Combination of A

    proof

      ( Carrier ( ZeroLC V)) = {} & {} c= A by Def4;

      hence thesis by Def5;

    end;

    theorem :: RMOD_4:21

    

     Th21: for l be Linear_Combination of ( {} the carrier of V) holds l = ( ZeroLC V)

    proof

      let l be Linear_Combination of ( {} the carrier of V);

      ( Carrier l) c= {} by Def5;

      then ( Carrier l) = {} ;

      hence thesis by Def4;

    end;

    theorem :: RMOD_4:22

    L is Linear_Combination of ( Carrier L) by Def5;

    definition

      let R, V, F, f;

      :: RMOD_4:def6

      func f (#) F -> FinSequence of V means

      : Def6: ( len it ) = ( len F) & for i be Nat st i in ( dom it ) holds (it . i) = ((F /. i) * (f . (F /. i)));

      existence

      proof

        deffunc Q( Nat) = ((F /. $1) * (f . (F /. $1)));

        consider G be FinSequence such that

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

         A2: for n be Nat st n in ( dom G) holds (G . n) = Q(n) from FINSEQ_1:sch 2;

        ( rng G) c= the carrier of V

        proof

          let x be object;

          assume x in ( rng G);

          then

          consider y be object such that

           A3: y in ( dom G) and

           A4: (G . y) = x by FUNCT_1:def 3;

          y in ( Seg ( len F)) by A1, A3, FINSEQ_1:def 3;

          then

          reconsider y as Element of NAT ;

          (G . y) = ((F /. y) * (f . (F /. y))) by A2, A3;

          hence thesis by A4;

        end;

        then

        reconsider G as FinSequence of V by FINSEQ_1:def 4;

        take G;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let H1,H2 be FinSequence of V;

        assume that

         A5: ( len H1) = ( len F) and

         A6: for i st i in ( dom H1) holds (H1 . i) = ((F /. i) * (f . (F /. i))) and

         A7: ( len H2) = ( len F) and

         A8: for i st i in ( dom H2) holds (H2 . i) = ((F /. i) * (f . (F /. i)));

        now

          let k be Nat;

          assume 1 <= k & k <= ( len H1);

          then

           A9: k in ( Seg ( len H1)) by FINSEQ_1: 1;

          then k in ( dom H1) by FINSEQ_1:def 3;

          then

           A10: (H1 . k) = ((F /. k) * (f . (F /. k))) by A6;

          k in ( dom H2) by A5, A7, A9, FINSEQ_1:def 3;

          hence (H1 . k) = (H2 . k) by A8, A10;

        end;

        hence thesis by A5, A7, FINSEQ_1: 14;

      end;

    end

    theorem :: RMOD_4:23

    

     Th23: i in ( dom F) & v = (F . i) implies ((f (#) F) . i) = (v * (f . v))

    proof

      assume that

       A1: i in ( dom F) and

       A2: v = (F . i);

      

       A3: (F /. i) = (F . i) by A1, PARTFUN1:def 6;

      ( len (f (#) F)) = ( len F) by Def6;

      then i in ( dom (f (#) F)) by A1, FINSEQ_3: 29;

      hence thesis by A2, A3, Def6;

    end;

    theorem :: RMOD_4:24

    (f (#) ( <*> the carrier of V)) = ( <*> the carrier of V)

    proof

      ( len (f (#) ( <*> the carrier of V))) = ( len ( <*> the carrier of V)) by Def6

      .= 0 ;

      hence thesis;

    end;

    theorem :: RMOD_4:25

    

     Th25: (f (#) <*v*>) = <*(v * (f . v))*>

    proof

      

       A1: 1 in {1} by TARSKI:def 1;

      

       A2: ( len (f (#) <*v*>)) = ( len <*v*>) by Def6

      .= 1 by FINSEQ_1: 40;

      then ( dom (f (#) <*v*>)) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      

      then ((f (#) <*v*>) . 1) = (( <*v*> /. 1) * (f . ( <*v*> /. 1))) by A1, Def6

      .= (v * (f . ( <*v*> /. 1))) by FINSEQ_4: 16

      .= (v * (f . v)) by FINSEQ_4: 16;

      hence thesis by A2, FINSEQ_1: 40;

    end;

    theorem :: RMOD_4:26

    

     Th26: (f (#) <*v1, v2*>) = <*(v1 * (f . v1)), (v2 * (f . v2))*>

    proof

      

       A1: ( len (f (#) <*v1, v2*>)) = ( len <*v1, v2*>) by Def6

      .= 2 by FINSEQ_1: 44;

      then

       A2: ( dom (f (#) <*v1, v2*>)) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      2 in {1, 2} by TARSKI:def 2;

      

      then

       A3: ((f (#) <*v1, v2*>) . 2) = (( <*v1, v2*> /. 2) * (f . ( <*v1, v2*> /. 2))) by A2, Def6

      .= (v2 * (f . ( <*v1, v2*> /. 2))) by FINSEQ_4: 17

      .= (v2 * (f . v2)) by FINSEQ_4: 17;

      1 in {1, 2} by TARSKI:def 2;

      

      then ((f (#) <*v1, v2*>) . 1) = (( <*v1, v2*> /. 1) * (f . ( <*v1, v2*> /. 1))) by A2, Def6

      .= (v1 * (f . ( <*v1, v2*> /. 1))) by FINSEQ_4: 17

      .= (v1 * (f . v1)) by FINSEQ_4: 17;

      hence thesis by A1, A3, FINSEQ_1: 44;

    end;

    theorem :: RMOD_4:27

    (f (#) <*v1, v2, v3*>) = <*(v1 * (f . v1)), (v2 * (f . v2)), (v3 * (f . v3))*>

    proof

      

       A1: ( len (f (#) <*v1, v2, v3*>)) = ( len <*v1, v2, v3*>) by Def6

      .= 3 by FINSEQ_1: 45;

      then

       A2: ( dom (f (#) <*v1, v2, v3*>)) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      3 in {1, 2, 3} by ENUMSET1:def 1;

      

      then

       A3: ((f (#) <*v1, v2, v3*>) . 3) = (( <*v1, v2, v3*> /. 3) * (f . ( <*v1, v2, v3*> /. 3))) by A2, Def6

      .= (v3 * (f . ( <*v1, v2, v3*> /. 3))) by FINSEQ_4: 18

      .= (v3 * (f . v3)) by FINSEQ_4: 18;

      2 in {1, 2, 3} by ENUMSET1:def 1;

      

      then

       A4: ((f (#) <*v1, v2, v3*>) . 2) = (( <*v1, v2, v3*> /. 2) * (f . ( <*v1, v2, v3*> /. 2))) by A2, Def6

      .= (v2 * (f . ( <*v1, v2, v3*> /. 2))) by FINSEQ_4: 18

      .= (v2 * (f . v2)) by FINSEQ_4: 18;

      1 in {1, 2, 3} by ENUMSET1:def 1;

      

      then ((f (#) <*v1, v2, v3*>) . 1) = (( <*v1, v2, v3*> /. 1) * (f . ( <*v1, v2, v3*> /. 1))) by A2, Def6

      .= (v1 * (f . ( <*v1, v2, v3*> /. 1))) by FINSEQ_4: 18

      .= (v1 * (f . v1)) by FINSEQ_4: 18;

      hence thesis by A1, A4, A3, FINSEQ_1: 45;

    end;

    theorem :: RMOD_4:28

    

     Th28: (f (#) (F ^ G)) = ((f (#) F) ^ (f (#) G))

    proof

      set H = ((f (#) F) ^ (f (#) G));

      set I = (F ^ G);

      

       A1: ( len F) = ( len (f (#) F)) by Def6;

      

       A2: ( len H) = (( len (f (#) F)) + ( len (f (#) G))) by FINSEQ_1: 22

      .= (( len F) + ( len (f (#) G))) by Def6

      .= (( len F) + ( len G)) by Def6

      .= ( len I) by FINSEQ_1: 22;

      

       A3: ( len G) = ( len (f (#) G)) by Def6;

      now

        let k be Nat;

        assume

         A4: k in ( dom H);

        now

          per cases by A4, FINSEQ_1: 25;

            suppose

             A5: k in ( dom (f (#) F));

            then

             A6: k in ( dom F) by A1, FINSEQ_3: 29;

            then

             A7: k in ( dom (F ^ G)) by FINSEQ_3: 22;

            

             A8: (F /. k) = (F . k) by A6, PARTFUN1:def 6

            .= ((F ^ G) . k) by A6, FINSEQ_1:def 7

            .= ((F ^ G) /. k) by A7, PARTFUN1:def 6;

            

            thus (H . k) = ((f (#) F) . k) by A5, FINSEQ_1:def 7

            .= ((I /. k) * (f . (I /. k))) by A5, A8, Def6;

          end;

            suppose

             A9: ex n be Nat st n in ( dom (f (#) G)) & k = (( len (f (#) F)) + n);

            

             A10: k in ( dom I) by A2, A4, FINSEQ_3: 29;

            consider n be Nat such that

             A11: n in ( dom (f (#) G)) and

             A12: k = (( len (f (#) F)) + n) by A9;

            

             A13: n in ( dom G) by A3, A11, FINSEQ_3: 29;

            

            then

             A14: (G /. n) = (G . n) by PARTFUN1:def 6

            .= ((F ^ G) . k) by A1, A12, A13, FINSEQ_1:def 7

            .= ((F ^ G) /. k) by A10, PARTFUN1:def 6;

            

            thus (H . k) = ((f (#) G) . n) by A11, A12, FINSEQ_1:def 7

            .= ((I /. k) * (f . (I /. k))) by A11, A14, Def6;

          end;

        end;

        hence (H . k) = ((I /. k) * (f . (I /. k)));

      end;

      hence thesis by A2, Def6;

    end;

    definition

      let R, V, L;

      :: RMOD_4:def7

      func Sum (L) -> Vector of V means

      : Def7: ex F st F is one-to-one & ( rng F) = ( Carrier L) & it = ( Sum (L (#) F));

      existence

      proof

        consider F be FinSequence such that

         A1: ( rng F) = ( Carrier L) and

         A2: F is one-to-one by FINSEQ_4: 58;

        reconsider F as FinSequence of V by A1, FINSEQ_1:def 4;

        take ( Sum (L (#) F));

        take F;

        thus F is one-to-one & ( rng F) = ( Carrier L) by A1, A2;

        thus thesis;

      end;

      uniqueness

      proof

        let v1, v2;

        given F1 be FinSequence of V such that

         A3: F1 is one-to-one and

         A4: ( rng F1) = ( Carrier L) and

         A5: v1 = ( Sum (L (#) F1));

        given F2 be FinSequence of V such that

         A6: F2 is one-to-one and

         A7: ( rng F2) = ( Carrier L) and

         A8: v2 = ( Sum (L (#) F2));

        defpred P[ object, object] means {$2} = (F1 " {(F2 . $1)});

        

         A9: ( len F1) = ( len F2) by A3, A4, A6, A7, FINSEQ_1: 48;

        

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

        

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

        

         A12: for x be object st x in ( dom F1) holds ex y be object st y in ( dom F1) & P[x, y]

        proof

          let x be object;

          assume x in ( dom F1);

          then (F2 . x) in ( rng F1) by A4, A7, A9, A10, A11, FUNCT_1:def 3;

          then

          consider y be object such that

           A13: (F1 " {(F2 . x)}) = {y} by A3, FUNCT_1: 74;

          take y;

          y in (F1 " {(F2 . x)}) by A13, TARSKI:def 1;

          hence y in ( dom F1) by FUNCT_1:def 7;

          thus thesis by A13;

        end;

        consider f be Function of ( dom F1), ( dom F1) such that

         A14: for x be object st x in ( dom F1) holds P[x, (f . x)] from FUNCT_2:sch 1( A12);

        

         A15: ( rng f) = ( dom F1)

        proof

          thus ( rng f) c= ( dom F1) by RELAT_1:def 19;

          let y be object;

          assume

           A16: y in ( dom F1);

          then (F1 . y) in ( rng F2) by A4, A7, FUNCT_1:def 3;

          then

          consider x be object such that

           A17: x in ( dom F2) and

           A18: (F2 . x) = (F1 . y) by FUNCT_1:def 3;

          (F1 " {(F2 . x)}) = (F1 " ( Im (F1,y))) by A16, A18, FUNCT_1: 59;

          then (F1 " {(F2 . x)}) c= {y} by A3, FUNCT_1: 82;

          then {(f . x)} c= {y} by A9, A10, A11, A14, A17;

          then

           A19: (f . x) = y by ZFMISC_1: 18;

          x in ( dom f) by A9, A10, A11, A17, FUNCT_2:def 1;

          hence thesis by A19, FUNCT_1:def 3;

        end;

        set G1 = (L (#) F1);

        

         A20: ( len G1) = ( len F1) by Def6;

        

         A21: ( dom F1) = {} implies ( dom F1) = {} ;

        

         A22: f is one-to-one

        proof

          let y1,y2 be object;

          assume that

           A23: y1 in ( dom f) and

           A24: y2 in ( dom f) and

           A25: (f . y1) = (f . y2);

          

           A26: y2 in ( dom F1) by A21, A24, FUNCT_2:def 1;

          then

           A27: (F1 " {(F2 . y2)}) = {(f . y2)} by A14;

          

           A28: y1 in ( dom F1) by A21, A23, FUNCT_2:def 1;

          then (F2 . y1) in ( rng F1) by A4, A7, A9, A10, A11, FUNCT_1:def 3;

          then

           A29: {(F2 . y1)} c= ( rng F1) by ZFMISC_1: 31;

          (F2 . y2) in ( rng F1) by A4, A7, A9, A10, A11, A26, FUNCT_1:def 3;

          then

           A30: {(F2 . y2)} c= ( rng F1) by ZFMISC_1: 31;

          (F1 " {(F2 . y1)}) = {(f . y1)} by A14, A28;

          then {(F2 . y1)} = {(F2 . y2)} by A25, A27, A29, A30, FUNCT_1: 91;

          then

           A31: (F2 . y1) = (F2 . y2) by ZFMISC_1: 3;

          y1 in ( dom F2) & y2 in ( dom F2) by A9, A10, A11, A21, A23, A24, FUNCT_2:def 1;

          hence thesis by A6, A31;

        end;

        set G2 = (L (#) F2);

        

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

        reconsider f as Permutation of ( dom F1) by A15, A22, FUNCT_2: 57;

        ( dom F1) = ( Seg ( len F1)) & ( dom G1) = ( Seg ( len G1)) by FINSEQ_1:def 3;

        then

        reconsider f as Permutation of ( dom G1) by A20;

        

         A33: ( len G2) = ( len F2) by Def6;

        

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

        now

          let i be Nat;

          assume

           A35: i in ( dom G2);

          then

           A36: (G2 . i) = ((F2 /. i) * (L . (F2 /. i))) & (F2 . i) = (F2 /. i) by A33, A11, A32, Def6, PARTFUN1:def 6;

          i in ( dom F2) by A33, A35, FINSEQ_3: 29;

          then

          reconsider u = (F2 . i) as Vector of V by FINSEQ_2: 11;

          i in ( dom f) by A9, A20, A33, A34, A32, A35, FUNCT_2:def 1;

          then

           A37: (f . i) in ( dom F1) by A15, FUNCT_1:def 3;

          then

          reconsider m = (f . i) as Element of NAT by A10;

          reconsider v = (F1 . m) as Vector of V by A37, FINSEQ_2: 11;

           {(F1 . (f . i))} = ( Im (F1,(f . i))) by A37, FUNCT_1: 59

          .= (F1 .: (F1 " {(F2 . i)})) by A9, A33, A10, A32, A14, A35;

          then

           A38: u = v by FUNCT_1: 75, ZFMISC_1: 18;

          (F1 . m) = (F1 /. m) by A37, PARTFUN1:def 6;

          hence (G2 . i) = (G1 . (f . i)) by A20, A10, A34, A37, A38, A36, Def6;

        end;

        hence thesis by A3, A4, A5, A6, A7, A8, A20, A33, FINSEQ_1: 48, RLVECT_2: 6;

      end;

    end

    

     Lm3: ( Sum ( ZeroLC V)) = ( 0. V)

    proof

      consider F such that F is one-to-one and

       A1: ( rng F) = ( Carrier ( ZeroLC V)) and

       A2: ( Sum ( ZeroLC V)) = ( Sum (( ZeroLC V) (#) F)) by Def7;

      ( Carrier ( ZeroLC V)) = {} by Def4;

      then F = {} by A1, RELAT_1: 41;

      then ( len F) = 0 ;

      then ( len (( ZeroLC V) (#) F)) = 0 by Def6;

      hence thesis by A2, RLVECT_1: 75;

    end;

    theorem :: RMOD_4:29

    

     Th29: ( 0. R) <> ( 1_ R) implies (A <> {} & A is linearly-closed iff for l holds ( Sum l) in A)

    proof

      assume

       A1: ( 0. R) <> ( 1_ R);

      thus A <> {} & A is linearly-closed implies for l holds ( Sum l) in A

      proof

        defpred P[ Nat] means for l st ( card ( Carrier l)) = $1 holds ( Sum l) in A;

        assume that

         A2: A <> {} and

         A3: A is linearly-closed;

        now

          let l;

          assume ( card ( Carrier l)) = 0 ;

          then ( Carrier l) = {} ;

          then l = ( ZeroLC V) by Def4;

          then ( Sum l) = ( 0. V) by Lm3;

          hence ( Sum l) in A by A2, A3, RMOD_2: 1;

        end;

        then

         A4: P[ 0 ];

        now

          let k be Nat;

          assume

           A5: for l st ( card ( Carrier l)) = k holds ( Sum l) in A;

          let l;

          deffunc Q( Element of V) = (l . $1);

          consider F such that

           A6: F is one-to-one and

           A7: ( rng F) = ( Carrier l) and

           A8: ( Sum l) = ( Sum (l (#) F)) by Def7;

          reconsider G = (F | ( Seg k)) as FinSequence of V by FINSEQ_1: 18;

          assume

           A9: ( card ( Carrier l)) = (k + 1);

          then

           A10: ( len F) = (k + 1) by A6, A7, FINSEQ_4: 62;

          then

           A11: ( len (l (#) F)) = (k + 1) by Def6;

          

           A12: (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

          then

           A13: (k + 1) in ( dom F) by A10, FINSEQ_1:def 3;

          (k + 1) in ( dom F) by A10, A12, FINSEQ_1:def 3;

          then

          reconsider v = (F . (k + 1)) as Vector of V by FINSEQ_2: 11;

          consider f be Function of V, R such that

           A14: (f . v) = ( 0. R) and

           A15: for u be Element of V st u <> v holds (f . u) = Q(u) from FUNCT_2:sch 6;

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

          

           A16: v in ( Carrier l) by A7, A13, FUNCT_1:def 3;

          now

            let u;

            assume

             A17: not u in ( Carrier l);

            

            hence (f . u) = (l . u) by A16, A15

            .= ( 0. R) by A17;

          end;

          then

          reconsider f as Linear_Combination of V by Def2;

          

           A18: (A \ {v}) c= A by XBOOLE_1: 36;

          

           A19: ( Carrier l) c= A by Def5;

          then

           A20: (v * (l . v)) in A by A3, A16;

          

           A21: ( Carrier f) = (( Carrier l) \ {v})

          proof

            thus ( Carrier f) c= (( Carrier l) \ {v})

            proof

              let x be object;

              assume x in ( Carrier f);

              then

              consider u such that

               A22: u = x and

               A23: (f . u) <> ( 0. R);

              (f . u) = (l . u) by A14, A15, A23;

              then

               A24: x in ( Carrier l) by A22, A23;

               not x in {v} by A14, A22, A23, TARSKI:def 1;

              hence thesis by A24, XBOOLE_0:def 5;

            end;

            let x be object;

            assume

             A25: x in (( Carrier l) \ {v});

            then x in ( Carrier l) by XBOOLE_0:def 5;

            then

            consider u such that

             A26: x = u and

             A27: (l . u) <> ( 0. R);

             not x in {v} by A25, XBOOLE_0:def 5;

            then x <> v by TARSKI:def 1;

            then (l . u) = (f . u) by A15, A26;

            hence thesis by A26, A27;

          end;

          then ( Carrier f) c= (A \ {v}) by A19, XBOOLE_1: 33;

          then ( Carrier f) c= A by A18;

          then

          reconsider f as Linear_Combination of A by Def5;

          

           A28: ( len G) = k by A10, FINSEQ_3: 53;

          then

           A29: ( len (f (#) G)) = k by Def6;

          

           A30: ( rng G) = ( Carrier f)

          proof

            thus ( rng G) c= ( Carrier f)

            proof

              let x be object;

              assume x in ( rng G);

              then

              consider y be object such that

               A31: y in ( dom G) and

               A32: (G . y) = x by FUNCT_1:def 3;

              reconsider y as Nat by A31, FINSEQ_3: 23;

              

               A33: ( dom G) c= ( dom F) & (G . y) = (F . y) by A31, FUNCT_1: 47, RELAT_1: 60;

              now

                assume x = v;

                then

                 A34: (k + 1) = y by A6, A13, A31, A32, A33;

                y <= k by A28, A31, FINSEQ_3: 25;

                hence contradiction by A34, XREAL_1: 29;

              end;

              then

               A35: not x in {v} by TARSKI:def 1;

              x in ( rng F) by A31, A32, A33, FUNCT_1:def 3;

              hence thesis by A7, A21, A35, XBOOLE_0:def 5;

            end;

            let x be object;

            assume

             A36: x in ( Carrier f);

            then x in ( rng F) by A7, A21, XBOOLE_0:def 5;

            then

            consider y be object such that

             A37: y in ( dom F) and

             A38: (F . y) = x by FUNCT_1:def 3;

            reconsider y as Element of NAT by A37, FINSEQ_3: 23;

            now

              assume not y in ( Seg k);

              then y in (( dom F) \ ( Seg k)) by A37, XBOOLE_0:def 5;

              then y in (( Seg (k + 1)) \ ( Seg k)) by A10, FINSEQ_1:def 3;

              then y in {(k + 1)} by FINSEQ_3: 15;

              then y = (k + 1) by TARSKI:def 1;

              then not v in {v} by A21, A36, A38, XBOOLE_0:def 5;

              hence contradiction by TARSKI:def 1;

            end;

            then y in (( dom F) /\ ( Seg k)) by A37, XBOOLE_0:def 4;

            then

             A39: y in ( dom G) by RELAT_1: 61;

            then (G . y) = (F . y) by FUNCT_1: 47;

            hence thesis by A38, A39, FUNCT_1:def 3;

          end;

          (( Seg (k + 1)) /\ ( Seg k)) = ( Seg k) by FINSEQ_1: 7, NAT_1: 12

          .= ( dom (f (#) G)) by A29, FINSEQ_1:def 3;

          then

           A40: ( dom (f (#) G)) = (( dom (l (#) F)) /\ ( Seg k)) by A11, FINSEQ_1:def 3;

          now

            let x be object;

            

             A41: ( rng F) c= the carrier of V by FINSEQ_1:def 4;

            assume

             A42: x in ( dom (f (#) G));

            then

            reconsider n = x as Nat by FINSEQ_3: 23;

            n in ( dom (l (#) F)) by A40, A42, XBOOLE_0:def 4;

            then

             A43: n in ( dom F) by A10, A11, FINSEQ_3: 29;

            then (F . n) in ( rng F) by FUNCT_1:def 3;

            then

            reconsider w = (F . n) as Vector of V by A41;

            

             A44: n in ( dom G) by A28, A29, A42, FINSEQ_3: 29;

            then

             A45: (G . n) in ( rng G) by FUNCT_1:def 3;

            ( rng G) c= the carrier of V by FINSEQ_1:def 4;

            then

            reconsider u = (G . n) as Vector of V by A45;

             not u in {v} by A21, A30, A45, XBOOLE_0:def 5;

            then

             A46: u <> v by TARSKI:def 1;

            

             A47: ((f (#) G) . n) = (u * (f . u)) by A44, Th23

            .= (u * (l . u)) by A15, A46;

            w = u by A44, FUNCT_1: 47;

            hence ((f (#) G) . x) = ((l (#) F) . x) by A47, A43, Th23;

          end;

          then (f (#) G) = ((l (#) F) | ( Seg k)) by A40, FUNCT_1: 46;

          then

           A48: (f (#) G) = ((l (#) F) | ( dom (f (#) G))) by A29, FINSEQ_1:def 3;

          v in ( rng F) by A13, FUNCT_1:def 3;

          then {v} c= ( Carrier l) by A7, ZFMISC_1: 31;

          

          then ( card ( Carrier f)) = ((k + 1) - ( card {v})) by A9, A21, CARD_2: 44

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

          .= k by XCMPLX_1: 26;

          then

           A49: ( Sum f) in A by A5;

          G is one-to-one by A6, FUNCT_1: 52;

          then

           A50: ( Sum (f (#) G)) = ( Sum f) by A30, Def7;

          ((l (#) F) . ( len F)) = (v * (l . v)) by A10, A13, Th23;

          then ( Sum (l (#) F)) = (( Sum (f (#) G)) + (v * (l . v))) by A10, A11, A29, A48, RLVECT_1: 38;

          hence ( Sum l) in A by A3, A8, A20, A50, A49;

        end;

        then

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

        let l;

        

         A52: ( card ( Carrier l)) = ( card ( Carrier l));

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

        hence thesis by A52;

      end;

      assume

       A53: for l holds ( Sum l) in A;

      hence A <> {} ;

      ( ZeroLC V) is Linear_Combination of A & ( Sum ( ZeroLC V)) = ( 0. V) by Lm3, Th20;

      then

       A54: ( 0. V) in A by A53;

      

       A55: for a, v st v in A holds (v * a) in A

      proof

        let a, v;

        assume

         A56: v in A;

        now

          per cases ;

            suppose a = ( 0. R);

            hence thesis by A54, VECTSP_2: 32;

          end;

            suppose

             A57: a <> ( 0. R);

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

            consider f such that

             A58: (f . v) = a and

             A59: for u be Element of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

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

            now

              let u;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (f . u) = ( 0. R) by A59;

            end;

            then

            reconsider f as Linear_Combination of V by Def2;

            

             A60: ( Carrier f) = {v}

            proof

              thus ( Carrier f) c= {v}

              proof

                let x be object;

                assume x in ( Carrier f);

                then

                consider u such that

                 A61: x = u and

                 A62: (f . u) <> ( 0. R);

                u = v by A59, A62;

                hence thesis by A61, TARSKI:def 1;

              end;

              let x be object;

              assume x in {v};

              then x = v by TARSKI:def 1;

              hence thesis by A57, A58;

            end;

             {v} c= A by A56, ZFMISC_1: 31;

            then

            reconsider f as Linear_Combination of A by A60, Def5;

            consider F such that

             A63: F is one-to-one & ( rng F) = ( Carrier f) and

             A64: ( Sum (f (#) F)) = ( Sum f) by Def7;

            F = <*v*> by A60, A63, FINSEQ_3: 97;

            then (f (#) F) = <*(v * (f . v))*> by Th25;

            then ( Sum f) = (v * a) by A58, A64, RLVECT_1: 44;

            hence thesis by A53;

          end;

        end;

        hence thesis;

      end;

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

      proof

        let v, u;

        assume that

         A65: v in A and

         A66: u in A;

        now

          per cases ;

            suppose u = v;

            

            then (v + u) = ((v * ( 1_ R)) + v) by VECTSP_2:def 9

            .= ((v * ( 1_ R)) + (v * ( 1_ R))) by VECTSP_2:def 9

            .= (v * (( 1_ R) + ( 1_ R))) by VECTSP_2:def 9;

            hence thesis by A55, A65;

          end;

            suppose

             A67: v <> u;

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

            consider f such that

             A68: (f . v) = ( 1_ R) & (f . u) = ( 1_ R) and

             A69: for w be Element of V st w <> v & w <> u holds (f . w) = F(w) from FUNCT_2:sch 7( A67);

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

            now

              let w;

              assume not w in {v, u};

              then w <> v & w <> u by TARSKI:def 2;

              hence (f . w) = ( 0. R) by A69;

            end;

            then

            reconsider f as Linear_Combination of V by Def2;

            

             A70: ( Carrier f) = {v, u}

            proof

              thus ( Carrier f) c= {v, u}

              proof

                let x be object;

                assume x in ( Carrier f);

                then ex w st x = w & (f . w) <> ( 0. R);

                then x = v or x = u by A69;

                hence thesis by TARSKI:def 2;

              end;

              let x be object;

              assume x in {v, u};

              then x = v or x = u by TARSKI:def 2;

              hence thesis by A1, A68;

            end;

            then

             A71: ( Carrier f) c= A by A65, A66, ZFMISC_1: 32;

            

             A72: (u * ( 1_ R)) = u & (v * ( 1_ R)) = v by VECTSP_2:def 9;

            reconsider f as Linear_Combination of A by A71, Def5;

            consider F such that

             A73: F is one-to-one & ( rng F) = ( Carrier f) and

             A74: ( Sum (f (#) F)) = ( Sum f) by Def7;

            F = <*v, u*> or F = <*u, v*> by A67, A70, A73, FINSEQ_3: 99;

            then (f (#) F) = <*(v * ( 1_ R)), (u * ( 1_ R))*> or (f (#) F) = <*(u * ( 1_ R)), (v * ( 1_ R))*> by A68, Th26;

            then ( Sum f) = (v + u) by A74, A72, RLVECT_1: 45;

            hence thesis by A53;

          end;

        end;

        hence thesis;

      end;

      thus thesis by A55;

    end;

    theorem :: RMOD_4:30

    ( Sum ( ZeroLC V)) = ( 0. V) by Lm3;

    theorem :: RMOD_4:31

    

     Th31: for l be Linear_Combination of ( {} the carrier of V) holds ( Sum l) = ( 0. V)

    proof

      let l be Linear_Combination of ( {} the carrier of V);

      l = ( ZeroLC V) by Th21;

      hence thesis by Lm3;

    end;

    theorem :: RMOD_4:32

    

     Th32: for l be Linear_Combination of {v} holds ( Sum l) = (v * (l . v))

    proof

      let l be Linear_Combination of {v};

      

       A1: ( Carrier l) c= {v} by Def5;

      now

        per cases by A1, ZFMISC_1: 33;

          suppose ( Carrier l) = {} ;

          then

           A2: l = ( ZeroLC V) by Def4;

          

          hence ( Sum l) = ( 0. V) by Lm3

          .= (v * ( 0. R)) by VECTSP_2: 32

          .= (v * (l . v)) by A2, Th18;

        end;

          suppose ( Carrier l) = {v};

          then

          consider F such that

           A3: F is one-to-one & ( rng F) = {v} and

           A4: ( Sum l) = ( Sum (l (#) F)) by Def7;

          F = <*v*> by A3, FINSEQ_3: 97;

          then (l (#) F) = <*(v * (l . v))*> by Th25;

          hence thesis by A4, RLVECT_1: 44;

        end;

      end;

      hence thesis;

    end;

    theorem :: RMOD_4:33

    

     Th33: v1 <> v2 implies for l be Linear_Combination of {v1, v2} holds ( Sum l) = ((v1 * (l . v1)) + (v2 * (l . v2)))

    proof

      assume

       A1: v1 <> v2;

      let l be Linear_Combination of {v1, v2};

      

       A2: ( Carrier l) c= {v1, v2} by Def5;

      now

        per cases by A2, ZFMISC_1: 36;

          suppose ( Carrier l) = {} ;

          then

           A3: l = ( ZeroLC V) by Def4;

          

          hence ( Sum l) = ( 0. V) by Lm3

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

          .= ((v1 * ( 0. R)) + ( 0. V)) by VECTSP_2: 32

          .= ((v1 * ( 0. R)) + (v2 * ( 0. R))) by VECTSP_2: 32

          .= ((v1 * (l . v1)) + (v2 * ( 0. R))) by A3, Th18

          .= ((v1 * (l . v1)) + (v2 * (l . v2))) by A3, Th18;

        end;

          suppose

           A4: ( Carrier l) = {v1};

          then

          reconsider L = l as Linear_Combination of {v1} by Def5;

          

           A5: not v2 in ( Carrier l) by A1, A4, TARSKI:def 1;

          

          thus ( Sum l) = ( Sum L)

          .= (v1 * (l . v1)) by Th32

          .= ((v1 * (l . v1)) + ( 0. V)) by RLVECT_1:def 4

          .= ((v1 * (l . v1)) + (v2 * ( 0. R))) by VECTSP_2: 32

          .= ((v1 * (l . v1)) + (v2 * (l . v2))) by A5;

        end;

          suppose

           A6: ( Carrier l) = {v2};

          then

          reconsider L = l as Linear_Combination of {v2} by Def5;

          

           A7: not v1 in ( Carrier l) by A1, A6, TARSKI:def 1;

          

          thus ( Sum l) = ( Sum L)

          .= (v2 * (l . v2)) by Th32

          .= (( 0. V) + (v2 * (l . v2))) by RLVECT_1:def 4

          .= ((v1 * ( 0. R)) + (v2 * (l . v2))) by VECTSP_2: 32

          .= ((v1 * (l . v1)) + (v2 * (l . v2))) by A7;

        end;

          suppose ( Carrier l) = {v1, v2};

          then

          consider F such that

           A8: F is one-to-one & ( rng F) = {v1, v2} and

           A9: ( Sum l) = ( Sum (l (#) F)) by Def7;

          F = <*v1, v2*> or F = <*v2, v1*> by A1, A8, FINSEQ_3: 99;

          then (l (#) F) = <*(v1 * (l . v1)), (v2 * (l . v2))*> or (l (#) F) = <*(v2 * (l . v2)), (v1 * (l . v1))*> by Th26;

          hence thesis by A9, RLVECT_1: 45;

        end;

      end;

      hence thesis;

    end;

    theorem :: RMOD_4:34

    ( Carrier L) = {} implies ( Sum L) = ( 0. V)

    proof

      assume ( Carrier L) = {} ;

      then L = ( ZeroLC V) by Def4;

      hence thesis by Lm3;

    end;

    theorem :: RMOD_4:35

    

     Th35: ( Carrier L) = {v} implies ( Sum L) = (v * (L . v))

    proof

      assume ( Carrier L) = {v};

      then L is Linear_Combination of {v} by Def5;

      hence thesis by Th32;

    end;

    theorem :: RMOD_4:36

    ( Carrier L) = {v1, v2} & v1 <> v2 implies ( Sum L) = ((v1 * (L . v1)) + (v2 * (L . v2)))

    proof

      assume that

       A1: ( Carrier L) = {v1, v2} and

       A2: v1 <> v2;

      L is Linear_Combination of {v1, v2} by A1, Def5;

      hence thesis by A2, Th33;

    end;

    definition

      let R, V, L1, L2;

      :: original: =

      redefine

      :: RMOD_4:def8

      pred L1 = L2 means for v holds (L1 . v) = (L2 . v);

      compatibility by FUNCT_2: 63;

    end

    definition

      let R, V, L1, L2;

      :: RMOD_4:def9

      func L1 + L2 -> Linear_Combination of V means

      : Def9: for v holds (it . v) = ((L1 . v) + (L2 . v));

      existence

      proof

        deffunc F( Element of V) = ((L1 . $1) + (L2 . $1));

        consider f be Function of V, R such that

         A1: for v be Element of V holds (f . v) = F(v) from FUNCT_2:sch 4;

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

        now

          let v;

          assume

           A2: not v in (( Carrier L1) \/ ( Carrier L2));

          then not v in ( Carrier L2) by XBOOLE_0:def 3;

          then

           A3: (L2 . v) = ( 0. R);

           not v in ( Carrier L1) by A2, XBOOLE_0:def 3;

          then (L1 . v) = ( 0. R);

          

          hence (f . v) = (( 0. R) + ( 0. R)) by A1, A3

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

        end;

        then

        reconsider f as Linear_Combination of V by Def2;

        take f;

        let v;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let M,N be Linear_Combination of V;

        assume

         A4: for v holds (M . v) = ((L1 . v) + (L2 . v));

        assume

         A5: for v holds (N . v) = ((L1 . v) + (L2 . v));

        let v;

        

        thus (M . v) = ((L1 . v) + (L2 . v)) by A4

        .= (N . v) by A5;

      end;

    end

    theorem :: RMOD_4:37

    

     Th37: ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2))

    proof

      let x be object;

      assume x in ( Carrier (L1 + L2));

      then

      consider u such that

       A1: x = u and

       A2: ((L1 + L2) . u) <> ( 0. R);

      ((L1 + L2) . u) = ((L1 . u) + (L2 . u)) by Def9;

      then (L1 . u) <> ( 0. R) or (L2 . u) <> ( 0. R) by A2, RLVECT_1: 4;

      then x in { v1 : (L1 . v1) <> ( 0. R) } or x in { v2 : (L2 . v2) <> ( 0. R) } by A1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: RMOD_4:38

    

     Th38: L1 is Linear_Combination of A & L2 is Linear_Combination of A implies (L1 + L2) is Linear_Combination of A

    proof

      assume L1 is Linear_Combination of A & L2 is Linear_Combination of A;

      then ( Carrier L1) c= A & ( Carrier L2) c= A by Def5;

      then

       A1: (( Carrier L1) \/ ( Carrier L2)) c= A by XBOOLE_1: 8;

      ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2)) by Th37;

      hence ( Carrier (L1 + L2)) c= A by A1;

    end;

    theorem :: RMOD_4:39

    

     Th39: for R be comRing holds for V be RightMod of R holds for L1,L2 be Linear_Combination of V holds (L1 + L2) = (L2 + L1)

    proof

      let R be comRing;

      let V be RightMod of R;

      let L1,L2 be Linear_Combination of V;

      let v be Vector of V;

      

      thus ((L1 + L2) . v) = ((L2 . v) + (L1 . v)) by Def9

      .= ((L2 + L1) . v) by Def9;

    end;

    theorem :: RMOD_4:40

    (L1 + (L2 + L3)) = ((L1 + L2) + L3)

    proof

      let v;

      

      thus ((L1 + (L2 + L3)) . v) = ((L1 . v) + ((L2 + L3) . v)) by Def9

      .= ((L1 . v) + ((L2 . v) + (L3 . v))) by Def9

      .= (((L1 . v) + (L2 . v)) + (L3 . v)) by RLVECT_1:def 3

      .= (((L1 + L2) . v) + (L3 . v)) by Def9

      .= (((L1 + L2) + L3) . v) by Def9;

    end;

    theorem :: RMOD_4:41

    for R be comRing holds for V be RightMod of R holds for L be Linear_Combination of V holds (L + ( ZeroLC V)) = L & (( ZeroLC V) + L) = L

    proof

      let R be comRing;

      let V be RightMod of R;

      let L be Linear_Combination of V;

      thus (L + ( ZeroLC V)) = L

      proof

        let v be Vector of V;

        

        thus ((L + ( ZeroLC V)) . v) = ((L . v) + (( ZeroLC V) . v)) by Def9

        .= ((L . v) + ( 0. R)) by Th18

        .= (L . v) by RLVECT_1: 4;

      end;

      hence thesis by Th39;

    end;

    definition

      let R, V, a, L;

      :: RMOD_4:def10

      func L * a -> Linear_Combination of V means

      : Def10: for v holds (it . v) = ((L . v) * a);

      existence

      proof

        deffunc F( Element of V) = ((L . $1) * a);

        consider f be Function of V, R such that

         A1: for v be Element of V holds (f . v) = F(v) from FUNCT_2:sch 4;

        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 ( Carrier L);

          then (L . v) = ( 0. R);

          

          hence (f . v) = (( 0. R) * a) by A1

          .= ( 0. R);

        end;

        then

        reconsider f as Linear_Combination of V by Def2;

        take f;

        let v;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let L1, L2;

        assume

         A2: for v holds (L1 . v) = ((L . v) * a);

        assume

         A3: for v holds (L2 . v) = ((L . v) * a);

        let v;

        

        thus (L1 . v) = ((L . v) * a) by A2

        .= (L2 . v) by A3;

      end;

    end

    theorem :: RMOD_4:42

    

     Th42: ( Carrier (L * a)) c= ( Carrier L)

    proof

      set T = { u : ((L * a) . u) <> ( 0. R) };

      set S = { v : (L . v) <> ( 0. R) };

      T c= S

      proof

        let x be object;

        assume x in T;

        then

        consider u such that

         A1: x = u and

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

        ((L * a) . u) = ((L . u) * a) by Def10;

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

        hence thesis by A1;

      end;

      hence thesis;

    end;

    reserve RR for domRing;

    reserve VV for RightMod of RR;

    reserve LL for Linear_Combination of VV;

    reserve aa for Scalar of RR;

    reserve uu,vv for Vector of VV;

    theorem :: RMOD_4:43

    

     Th43: aa <> ( 0. RR) implies ( Carrier (LL * aa)) = ( Carrier LL)

    proof

      set T = { uu : ((LL * aa) . uu) <> ( 0. RR) };

      set S = { vv : (LL . vv) <> ( 0. RR) };

      assume

       A1: aa <> ( 0. RR);

      T = S

      proof

        thus T c= S

        proof

          let x be object;

          assume x in T;

          then

          consider uu such that

           A2: x = uu and

           A3: ((LL * aa) . uu) <> ( 0. RR);

          ((LL * aa) . uu) = ((LL . uu) * aa) by Def10;

          then (LL . uu) <> ( 0. RR) by A3;

          hence thesis by A2;

        end;

        let x be object;

        assume x in S;

        then

        consider vv such that

         A4: x = vv and

         A5: (LL . vv) <> ( 0. RR);

        ((LL * aa) . vv) = ((LL . vv) * aa) by Def10;

        then ((LL * aa) . vv) <> ( 0. RR) by A1, A5, VECTSP_2:def 1;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    theorem :: RMOD_4:44

    

     Th44: (L * ( 0. R)) = ( ZeroLC V)

    proof

      let v;

      

      thus ((L * ( 0. R)) . v) = ((L . v) * ( 0. R)) by Def10

      .= ( 0. R)

      .= (( ZeroLC V) . v) by Th18;

    end;

    theorem :: RMOD_4:45

    

     Th45: L is Linear_Combination of A implies (L * a) is Linear_Combination of A

    proof

      assume L is Linear_Combination of A;

      then

       A1: ( Carrier L) c= A by Def5;

      ( Carrier (L * a)) c= ( Carrier L) by Th42;

      then ( Carrier (L * a)) c= A by A1;

      hence thesis by Def5;

    end;

    theorem :: RMOD_4:46

    (L * (a + b)) = ((L * a) + (L * b))

    proof

      let v;

      

      thus ((L * (a + b)) . v) = ((L . v) * (a + b)) by Def10

      .= (((L . v) * a) + ((L . v) * b)) by VECTSP_1:def 7

      .= (((L * a) . v) + ((L . v) * b)) by Def10

      .= (((L * a) . v) + ((L * b) . v)) by Def10

      .= (((L * a) + (L * b)) . v) by Def9;

    end;

    theorem :: RMOD_4:47

    ((L1 + L2) * a) = ((L1 * a) + (L2 * a))

    proof

      let v;

      

      thus (((L1 + L2) * a) . v) = (((L1 + L2) . v) * a) by Def10

      .= (((L1 . v) + (L2 . v)) * a) by Def9

      .= (((L1 . v) * a) + ((L2 . v) * a)) by VECTSP_1:def 7

      .= (((L1 * a) . v) + ((L2 . v) * a)) by Def10

      .= (((L1 * a) . v) + ((L2 * a) . v)) by Def10

      .= (((L1 * a) + (L2 * a)) . v) by Def9;

    end;

    theorem :: RMOD_4:48

    

     Th48: ((L * b) * a) = (L * (b * a))

    proof

      let v;

      

      thus (((L * b) * a) . v) = (((L * b) . v) * a) by Def10

      .= (((L . v) * b) * a) by Def10

      .= ((L . v) * (b * a)) by GROUP_1:def 3

      .= ((L * (b * a)) . v) by Def10;

    end;

    theorem :: RMOD_4:49

    (L * ( 1_ R)) = L

    proof

      let v;

      

      thus ((L * ( 1_ R)) . v) = ((L . v) * ( 1_ R)) by Def10

      .= (L . v);

    end;

    definition

      let R, V, L;

      :: RMOD_4:def11

      func - L -> Linear_Combination of V equals (L * ( - ( 1_ R)));

      correctness ;

      involutiveness

      proof

        let L,L9 be Linear_Combination of V;

        assume

         A1: L = (L9 * ( - ( 1_ R)));

        let v;

        

        thus (L9 . v) = ((L9 . v) * ( 1_ R))

        .= ((L9 . v) * (( 1_ R) * ( 1_ R)))

        .= ((L9 . v) * (( - ( 1_ R)) * ( - ( 1_ R)))) by VECTSP_1: 10

        .= ((L9 * (( - ( 1_ R)) * ( - ( 1_ R)))) . v) by Def10

        .= ((L * ( - ( 1_ R))) . v) by A1, Th48;

      end;

    end

    theorem :: RMOD_4:50

    

     Th50: (( - L) . v) = ( - (L . v))

    proof

      

      thus (( - L) . v) = ((L . v) * ( - ( 1_ R))) by Def10

      .= ( - (L . v)) by VECTSP_2: 28;

    end;

    theorem :: RMOD_4:51

    (L1 + L2) = ( ZeroLC V) implies L2 = ( - L1)

    proof

      assume

       A1: (L1 + L2) = ( ZeroLC V);

      let v;

      ((L1 . v) + (L2 . v)) = (( ZeroLC V) . v) by A1, Def9

      .= ( 0. R) by Th18;

      

      hence (L2 . v) = ( - (L1 . v)) by RLVECT_1: 6

      .= (( - L1) . v) by Th50;

    end;

    theorem :: RMOD_4:52

    

     Th52: ( Carrier ( - L)) = ( Carrier L)

    proof

      set a = ( - ( 1_ R));

      ( Carrier (L * a)) = ( Carrier L)

      proof

        set S = { v : (L . v) <> ( 0. R) };

        set T = { u : ((L * a) . u) <> ( 0. R) };

        T = S

        proof

          thus T c= S

          proof

            let x be object;

            assume x in T;

            then

            consider u such that

             A1: x = u and

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

            ((L * a) . u) = ((L . u) * a) by Def10;

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

            hence thesis by A1;

          end;

          let x be object;

          assume x in S;

          then

          consider v such that

           A3: x = v and

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

          ((L * a) . v) = ((L . v) * a) by Def10

          .= ( - (L . v)) by VECTSP_2: 28;

          then ((L * a) . v) <> ( 0. R) by A4, VECTSP_2: 3;

          hence thesis by A3;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: RMOD_4:53

    L is Linear_Combination of A implies ( - L) is Linear_Combination of A by Th45;

    definition

      let R, V, L1, L2;

      :: RMOD_4:def12

      func L1 - L2 -> Linear_Combination of V equals (L1 + ( - L2));

      correctness ;

    end

    theorem :: RMOD_4:54

    

     Th54: ((L1 - L2) . v) = ((L1 . v) - (L2 . v))

    proof

      

      thus ((L1 - L2) . v) = ((L1 . v) + (( - L2) . v)) by Def9

      .= ((L1 . v) + ( - (L2 . v))) by Th50

      .= ((L1 . v) - (L2 . v)) by RLVECT_1:def 11;

    end;

    theorem :: RMOD_4:55

    ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier L2))

    proof

      ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier ( - L2))) by Th37;

      hence thesis by Th52;

    end;

    theorem :: RMOD_4:56

    L1 is Linear_Combination of A & L2 is Linear_Combination of A implies (L1 - L2) is Linear_Combination of A

    proof

      assume that

       A1: L1 is Linear_Combination of A and

       A2: L2 is Linear_Combination of A;

      ( - L2) is Linear_Combination of A by A2, Th45;

      hence thesis by A1, Th38;

    end;

    theorem :: RMOD_4:57

    (L - L) = ( ZeroLC V)

    proof

      let v;

      

      thus ((L - L) . v) = ((L . v) - (L . v)) by Th54

      .= ( 0. R) by RLVECT_1: 15

      .= (( ZeroLC V) . v) by Th18;

    end;

    theorem :: RMOD_4:58

    

     Th58: ( Sum (L1 + L2)) = (( Sum L1) + ( Sum L2))

    proof

      set A = ((( Carrier (L1 + L2)) \/ ( Carrier L1)) \/ ( Carrier L2));

      set C1 = (A \ ( Carrier L1));

      consider p such that

       A1: ( rng p) = C1 and

       A2: p is one-to-one by FINSEQ_4: 58;

      reconsider p as FinSequence of V by A1, FINSEQ_1:def 4;

      

       A3: A = (( Carrier L1) \/ (( Carrier (L1 + L2)) \/ ( Carrier L2))) by XBOOLE_1: 4;

      set C3 = (A \ ( Carrier (L1 + L2)));

      consider r such that

       A4: ( rng r) = C3 and

       A5: r is one-to-one by FINSEQ_4: 58;

      reconsider r as FinSequence of V by A4, FINSEQ_1:def 4;

      

       A6: A = (( Carrier (L1 + L2)) \/ (( Carrier L1) \/ ( Carrier L2))) by XBOOLE_1: 4;

      set C2 = (A \ ( Carrier L2));

      consider q such that

       A7: ( rng q) = C2 and

       A8: q is one-to-one by FINSEQ_4: 58;

      reconsider q as FinSequence of V by A7, FINSEQ_1:def 4;

      consider F such that

       A9: F is one-to-one and

       A10: ( rng F) = ( Carrier (L1 + L2)) and

       A11: ( Sum ((L1 + L2) (#) F)) = ( Sum (L1 + L2)) by Def7;

      set FF = (F ^ r);

      consider G such that

       A12: G is one-to-one and

       A13: ( rng G) = ( Carrier L1) and

       A14: ( Sum (L1 (#) G)) = ( Sum L1) by Def7;

      ( rng FF) = (( rng F) \/ ( rng r)) by FINSEQ_1: 31;

      then ( rng FF) = (( Carrier (L1 + L2)) \/ A) by A10, A4, XBOOLE_1: 39;

      then

       A15: ( rng FF) = A by A6, XBOOLE_1: 7, XBOOLE_1: 12;

      set GG = (G ^ p);

      ( rng GG) = (( rng G) \/ ( rng p)) by FINSEQ_1: 31;

      then ( rng GG) = (( Carrier L1) \/ A) by A13, A1, XBOOLE_1: 39;

      then

       A16: ( rng GG) = A by A3, XBOOLE_1: 7, XBOOLE_1: 12;

      ( rng F) misses ( rng r)

      proof

        set x = the Element of (( rng F) /\ ( rng r));

        assume not thesis;

        then (( rng F) /\ ( rng r)) <> {} ;

        then x in ( Carrier (L1 + L2)) & x in C3 by A10, A4, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A17: FF is one-to-one by A9, A5, FINSEQ_3: 91;

      ( rng G) misses ( rng p)

      proof

        set x = the Element of (( rng G) /\ ( rng p));

        assume not thesis;

        then (( rng G) /\ ( rng p)) <> {} ;

        then x in ( Carrier L1) & x in C1 by A13, A1, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A18: GG is one-to-one by A12, A2, FINSEQ_3: 91;

      then

       A19: ( len GG) = ( len FF) by A17, A16, A15, FINSEQ_1: 48;

      deffunc Q( Nat) = (FF <- (GG . $1));

      consider P be FinSequence such that

       A20: ( len P) = ( len FF) and

       A21: for k be Nat st k in ( dom P) holds (P . k) = Q(k) from FINSEQ_1:sch 2;

      

       A22: ( dom P) = ( Seg ( len FF)) by A20, FINSEQ_1:def 3;

       A23:

      now

        let x be object;

        assume

         A24: x in ( dom GG);

        then

        reconsider n = x as Nat by FINSEQ_3: 23;

        (GG . n) in ( rng FF) by A16, A15, A24, FUNCT_1:def 3;

        then

         A25: FF just_once_values (GG . n) by A17, FINSEQ_4: 8;

        n in ( Seg ( len FF)) by A19, A24, FINSEQ_1:def 3;

        

        then (FF . (P . n)) = (FF . (FF <- (GG . n))) by A21, A22

        .= (GG . n) by A25, FINSEQ_4:def 3;

        hence (GG . x) = (FF . (P . x));

      end;

      

       A26: ( dom GG) = ( dom FF) by A19, FINSEQ_3: 29;

      

       A27: ( rng P) c= ( dom FF)

      proof

        let x be object;

        assume x in ( rng P);

        then

        consider y be object such that

         A28: y in ( dom P) and

         A29: (P . y) = x by FUNCT_1:def 3;

        reconsider y as Nat by A28, FINSEQ_3: 23;

        y in ( dom FF) by A20, A28, FINSEQ_3: 29;

        then (GG . y) in ( rng FF) by A16, A15, A26, FUNCT_1:def 3;

        then

         A30: FF just_once_values (GG . y) by A17, FINSEQ_4: 8;

        (P . y) = (FF <- (GG . y)) by A21, A28;

        hence thesis by A29, A30, FINSEQ_4:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom P) & (P . x) in ( dom FF)

        proof

          assume x in ( dom GG);

          hence x in ( dom P) by A19, A20, FINSEQ_3: 29;

          then (P . x) in ( rng P) by FUNCT_1:def 3;

          hence thesis by A27;

        end;

        assume that

         A31: x in ( dom P) and (P . x) in ( dom FF);

        x in ( Seg ( len P)) by A31, FINSEQ_1:def 3;

        hence x in ( dom GG) by A19, A20, FINSEQ_1:def 3;

      end;

      then

       A32: GG = (FF * P) by A23, FUNCT_1: 10;

      ( dom FF) c= ( rng P)

      proof

        set f = ((FF " ) * GG);

        let x be object;

        assume

         A33: x in ( dom FF);

        ( dom (FF " )) = ( rng GG) by A17, A16, A15, FUNCT_1: 33;

        

        then

         A34: ( rng f) = ( rng (FF " )) by RELAT_1: 28

        .= ( dom FF) by A17, FUNCT_1: 33;

        f = (((FF " ) * FF) * P) by A32, RELAT_1: 36

        .= (( id ( dom FF)) * P) by A17, FUNCT_1: 39

        .= P by A27, RELAT_1: 53;

        hence thesis by A33, A34;

      end;

      then

       A35: ( dom FF) = ( rng P) by A27;

      

       A36: ( len r) = ( len ((L1 + L2) (#) r)) by Def6;

      now

        let k;

        assume

         A37: k in ( dom r);

        then (r /. k) = (r . k) by PARTFUN1:def 6;

        then (r /. k) in C3 by A4, A37, FUNCT_1:def 3;

        then

         A38: not (r /. k) in ( Carrier (L1 + L2)) by XBOOLE_0:def 5;

        k in ( dom ((L1 + L2) (#) r)) by A36, A37, FINSEQ_3: 29;

        then (((L1 + L2) (#) r) . k) = ((r /. k) * ((L1 + L2) . (r /. k))) by Def6;

        hence (((L1 + L2) (#) r) . k) = ((r /. k) * ( 0. R)) by A38;

      end;

      

      then

       A39: ( Sum ((L1 + L2) (#) r)) = (( Sum r) * ( 0. R)) by A36, Lm2

      .= ( 0. V) by VECTSP_2: 32;

      

       A40: ( len p) = ( len (L1 (#) p)) by Def6;

      now

        let k;

        assume

         A41: k in ( dom p);

        then (p /. k) = (p . k) by PARTFUN1:def 6;

        then (p /. k) in C1 by A1, A41, FUNCT_1:def 3;

        then

         A42: not (p /. k) in ( Carrier L1) by XBOOLE_0:def 5;

        k in ( dom (L1 (#) p)) by A40, A41, FINSEQ_3: 29;

        then ((L1 (#) p) . k) = ((p /. k) * (L1 . (p /. k))) by Def6;

        hence ((L1 (#) p) . k) = ((p /. k) * ( 0. R)) by A42;

      end;

      

      then

       A43: ( Sum (L1 (#) p)) = (( Sum p) * ( 0. R)) by A40, Lm2

      .= ( 0. V) by VECTSP_2: 32;

      set f = ((L1 + L2) (#) FF);

      consider H such that

       A44: H is one-to-one and

       A45: ( rng H) = ( Carrier L2) and

       A46: ( Sum (L2 (#) H)) = ( Sum L2) by Def7;

      set HH = (H ^ q);

      ( rng H) misses ( rng q)

      proof

        set x = the Element of (( rng H) /\ ( rng q));

        assume not thesis;

        then (( rng H) /\ ( rng q)) <> {} ;

        then x in ( Carrier L2) & x in C2 by A45, A7, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A47: HH is one-to-one by A44, A8, FINSEQ_3: 91;

      

       A48: ( len q) = ( len (L2 (#) q)) by Def6;

      now

        let k;

        assume

         A49: k in ( dom q);

        then (q /. k) = (q . k) by PARTFUN1:def 6;

        then (q /. k) in C2 by A7, A49, FUNCT_1:def 3;

        then

         A50: not (q /. k) in ( Carrier L2) by XBOOLE_0:def 5;

        k in ( dom (L2 (#) q)) by A48, A49, FINSEQ_3: 29;

        then ((L2 (#) q) . k) = ((q /. k) * (L2 . (q /. k))) by Def6;

        hence ((L2 (#) q) . k) = ((q /. k) * ( 0. R)) by A50;

      end;

      

      then

       A51: ( Sum (L2 (#) q)) = (( Sum q) * ( 0. R)) by A48, Lm2

      .= ( 0. V) by VECTSP_2: 32;

      set g = (L1 (#) GG);

      

       A52: ( len g) = ( len GG) by Def6;

      then

       A53: ( Seg ( len GG)) = ( dom g) by FINSEQ_1:def 3;

      ( rng HH) = (( rng H) \/ ( rng q)) by FINSEQ_1: 31;

      then ( rng HH) = (( Carrier L2) \/ A) by A45, A7, XBOOLE_1: 39;

      then

       A54: ( rng HH) = A by XBOOLE_1: 7, XBOOLE_1: 12;

      then

       A55: ( len GG) = ( len HH) by A47, A18, A16, FINSEQ_1: 48;

      deffunc Q( Nat) = (HH <- (GG . $1));

      consider R be FinSequence such that

       A56: ( len R) = ( len HH) and

       A57: for k be Nat st k in ( dom R) holds (R . k) = Q(k) from FINSEQ_1:sch 2;

      

       A58: ( dom R) = ( Seg ( len HH)) by A56, FINSEQ_1:def 3;

       A59:

      now

        let x be object;

        assume

         A60: x in ( dom GG);

        then

        reconsider n = x as Nat by FINSEQ_3: 23;

        (GG . n) in ( rng HH) by A16, A54, A60, FUNCT_1:def 3;

        then

         A61: HH just_once_values (GG . n) by A47, FINSEQ_4: 8;

        n in ( Seg ( len HH)) by A55, A60, FINSEQ_1:def 3;

        

        then (HH . (R . n)) = (HH . (HH <- (GG . n))) by A57, A58

        .= (GG . n) by A61, FINSEQ_4:def 3;

        hence (GG . x) = (HH . (R . x));

      end;

      

       A62: ( dom GG) = ( dom HH) by A55, FINSEQ_3: 29;

      

       A63: ( rng R) c= ( dom HH)

      proof

        let x be object;

        assume x in ( rng R);

        then

        consider y be object such that

         A64: y in ( dom R) and

         A65: (R . y) = x by FUNCT_1:def 3;

        reconsider y as Nat by A64, FINSEQ_3: 23;

        y in ( dom HH) by A56, A64, FINSEQ_3: 29;

        then (GG . y) in ( rng HH) by A16, A54, A62, FUNCT_1:def 3;

        then

         A66: HH just_once_values (GG . y) by A47, FINSEQ_4: 8;

        (R . y) = (HH <- (GG . y)) by A57, A64;

        hence thesis by A65, A66, FINSEQ_4:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom R) & (R . x) in ( dom HH)

        proof

          assume x in ( dom GG);

          then x in ( Seg ( len R)) by A55, A56, FINSEQ_1:def 3;

          hence x in ( dom R) by FINSEQ_1:def 3;

          then (R . x) in ( rng R) by FUNCT_1:def 3;

          hence thesis by A63;

        end;

        assume that

         A67: x in ( dom R) and (R . x) in ( dom HH);

        x in ( Seg ( len R)) by A67, FINSEQ_1:def 3;

        hence x in ( dom GG) by A55, A56, FINSEQ_1:def 3;

      end;

      then

       A68: GG = (HH * R) by A59, FUNCT_1: 10;

      ( dom HH) c= ( rng R)

      proof

        set f = ((HH " ) * GG);

        let x be object;

        assume

         A69: x in ( dom HH);

        ( dom (HH " )) = ( rng GG) by A47, A16, A54, FUNCT_1: 33;

        

        then

         A70: ( rng f) = ( rng (HH " )) by RELAT_1: 28

        .= ( dom HH) by A47, FUNCT_1: 33;

        f = (((HH " ) * HH) * R) by A68, RELAT_1: 36

        .= (( id ( dom HH)) * R) by A47, FUNCT_1: 39

        .= R by A63, RELAT_1: 53;

        hence thesis by A69, A70;

      end;

      then

       A71: ( dom HH) = ( rng R) by A63;

      

       A72: ( Sum g) = ( Sum ((L1 (#) G) ^ (L1 (#) p))) by Th28

      .= (( Sum (L1 (#) G)) + ( 0. V)) by A43, RLVECT_1: 41

      .= ( Sum (L1 (#) G)) by RLVECT_1:def 4;

      set h = (L2 (#) HH);

      

       A73: ( Sum h) = ( Sum ((L2 (#) H) ^ (L2 (#) q))) by Th28

      .= (( Sum (L2 (#) H)) + ( 0. V)) by A51, RLVECT_1: 41

      .= ( Sum (L2 (#) H)) by RLVECT_1:def 4;

      

       A74: ( Sum f) = ( Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r))) by Th28

      .= (( Sum ((L1 + L2) (#) F)) + ( 0. V)) by A39, RLVECT_1: 41

      .= ( Sum ((L1 + L2) (#) F)) by RLVECT_1:def 4;

      

       A75: ( dom P) = ( dom FF) by A20, FINSEQ_3: 29;

      then

       A76: P is one-to-one by A35, FINSEQ_4: 60;

      

       A77: ( dom R) = ( dom HH) by A56, FINSEQ_3: 29;

      then

       A78: R is one-to-one by A71, FINSEQ_4: 60;

      reconsider R as Function of ( dom HH), ( dom HH) by A63, A77, FUNCT_2: 2;

      

       A79: ( len h) = ( len HH) by Def6;

      then

       A80: ( dom h) = ( dom HH) by FINSEQ_3: 29;

      then

      reconsider R as Function of ( dom h), ( dom h);

      reconsider Hp = (h * R) as FinSequence of V by FINSEQ_2: 47;

      reconsider R as Permutation of ( dom h) by A71, A78, A80, FUNCT_2: 57;

      

       A81: Hp = (h * R);

      then

       A82: ( len Hp) = ( len GG) by A55, A79, FINSEQ_2: 44;

      reconsider P as Function of ( dom FF), ( dom FF) by A27, A75, FUNCT_2: 2;

      

       A83: ( len f) = ( len FF) by Def6;

      then

       A84: ( dom f) = ( dom FF) by FINSEQ_3: 29;

      then

      reconsider P as Function of ( dom f), ( dom f);

      reconsider Fp = (f * P) as FinSequence of V by FINSEQ_2: 47;

      reconsider P as Permutation of ( dom f) by A35, A76, A84, FUNCT_2: 57;

      

       A85: Fp = (f * P);

      then

       A86: ( Sum Fp) = ( Sum f) by RLVECT_2: 7;

      deffunc Q( Nat) = ((g /. $1) + (Hp /. $1));

      consider I be FinSequence such that

       A87: ( len I) = ( len GG) and

       A88: for k be Nat st k in ( dom I) holds (I . k) = Q(k) from FINSEQ_1:sch 2;

      

       A89: ( dom I) = ( Seg ( len GG)) by A87, FINSEQ_1:def 3;

      then

       A90: for k be Nat st k in ( Seg ( len GG)) holds (I . k) = Q(k) by A88;

      ( rng I) c= the carrier of V

      proof

        let x be object;

        assume x in ( rng I);

        then

        consider y be object such that

         A91: y in ( dom I) and

         A92: (I . y) = x by FUNCT_1:def 3;

        reconsider y as Nat by A91, FINSEQ_3: 23;

        (I . y) = ((g /. y) + (Hp /. y)) by A88, A91;

        hence thesis by A92;

      end;

      then

      reconsider I as FinSequence of V by FINSEQ_1:def 4;

      

       A93: ( len Fp) = ( len I) by A19, A83, A85, A87, FINSEQ_2: 44;

       A94:

      now

        let x be object;

        assume

         A95: x in ( Seg ( len I));

        then

        reconsider k = x as Element of NAT ;

        

         A96: x in ( dom HH) by A55, A87, A95, FINSEQ_1:def 3;

        then (R . k) in ( dom R) by A71, A77, FUNCT_1:def 3;

        then

        reconsider j = (R . k) as Nat by FINSEQ_3: 23;

        

         A97: x in ( dom GG) by A87, A95, FINSEQ_1:def 3;

        

        then

         A98: (HH . j) = (GG . k) by A59

        .= (GG /. k) by A97, PARTFUN1:def 6;

        (P . k) in ( dom P) by A26, A62, A35, A75, A96, FUNCT_1:def 3;

        then

        reconsider l = (P . k) as Nat by FINSEQ_3: 23;

        set v = (GG /. k);

        

         A99: x in ( dom Fp) by A93, A95, FINSEQ_1:def 3;

        

         A100: (FF . l) = (GG . k) by A23, A97

        .= (GG /. k) by A97, PARTFUN1:def 6;

        (P . k) in ( dom FF) by A26, A62, A35, A75, A96, FUNCT_1:def 3;

        

        then

         A101: (f . l) = (v * ((L1 + L2) . v)) by A100, Th23

        .= (v * ((L1 . v) + (L2 . v))) by Def9

        .= ((v * (L1 . v)) + (v * (L2 . v))) by VECTSP_2:def 9;

        

         A102: x in ( dom Hp) by A87, A82, A95, FINSEQ_1:def 3;

        

        then

         A103: (Hp /. k) = ((h * R) . k) by PARTFUN1:def 6

        .= (h . (R . k)) by A102, FUNCT_1: 12;

        (R . k) in ( dom HH) by A71, A77, A96, FUNCT_1:def 3;

        then

         A104: (h . j) = (v * (L2 . v)) by A98, Th23;

        

         A105: x in ( dom g) by A87, A52, A95, FINSEQ_1:def 3;

        

        then (g /. k) = (g . k) by PARTFUN1:def 6

        .= (v * (L1 . v)) by A105, Def6;

        

        hence (I . x) = ((v * (L1 . v)) + (v * (L2 . v))) by A87, A88, A89, A95, A103, A104

        .= (Fp . x) by A99, A101, FUNCT_1: 12;

      end;

      ( dom I) = ( Seg ( len I)) & ( dom Fp) = ( Seg ( len I)) by A93, FINSEQ_1:def 3;

      then

       A106: I = Fp by A94;

      ( Sum Hp) = ( Sum h) by A81, RLVECT_2: 7;

      hence thesis by A11, A14, A46, A72, A73, A74, A86, A87, A90, A82, A52, A106, A53, RLVECT_2: 2;

    end;

    reserve R for domRing;

    reserve V for RightMod of R;

    reserve L,L1,L2 for Linear_Combination of V;

    reserve a for Scalar of R;

    theorem :: RMOD_4:59

    

     Th59: ( Sum (L * a)) = (( Sum L) * a)

    proof

      per cases ;

        suppose

         A1: a <> ( 0. R);

        set l = (L * a);

        

         A2: ( Carrier l) = ( Carrier L) by A1, Th43;

        consider G be FinSequence of V such that

         A3: G is one-to-one and

         A4: ( rng G) = ( Carrier L) and

         A5: ( Sum L) = ( Sum (L (#) G)) by Def7;

        set g = (L (#) G);

        consider F be FinSequence of V such that

         A6: F is one-to-one and

         A7: ( rng F) = ( Carrier (L * a)) and

         A8: ( Sum (L * a)) = ( Sum ((L * a) (#) F)) by Def7;

        

         A9: ( len G) = ( len F) by A1, A6, A7, A3, A4, Th43, FINSEQ_1: 48;

        set f = ((L * a) (#) F);

        deffunc Q( Nat) = (F <- (G . $1));

        consider P be FinSequence such that

         A10: ( len P) = ( len F) and

         A11: for k be Nat st k in ( dom P) holds (P . k) = Q(k) from FINSEQ_1:sch 2;

        

         A12: ( dom P) = ( Seg ( len F)) by A10, FINSEQ_1:def 3;

         A13:

        now

          let x be object;

          assume

           A14: x in ( dom G);

          then

          reconsider n = x as Nat by FINSEQ_3: 23;

          (G . n) in ( rng F) by A7, A4, A2, A14, FUNCT_1:def 3;

          then

           A15: F just_once_values (G . n) by A6, FINSEQ_4: 8;

          n in ( Seg ( len F)) by A9, A14, FINSEQ_1:def 3;

          

          then (F . (P . n)) = (F . (F <- (G . n))) by A11, A12

          .= (G . n) by A15, FINSEQ_4:def 3;

          hence (G . x) = (F . (P . x));

        end;

        

         A16: ( rng P) c= ( dom F)

        proof

          let x be object;

          assume x in ( rng P);

          then

          consider y be object such that

           A17: y in ( dom P) and

           A18: (P . y) = x by FUNCT_1:def 3;

          reconsider y as Nat by A17, FINSEQ_3: 23;

          y in ( dom G) by A10, A9, A17, FINSEQ_3: 29;

          then (G . y) in ( rng F) by A7, A4, A2, FUNCT_1:def 3;

          then

           A19: F just_once_values (G . y) by A6, FINSEQ_4: 8;

          (P . y) = (F <- (G . y)) by A11, A17;

          hence thesis by A18, A19, FINSEQ_4:def 3;

        end;

        now

          let x be object;

          thus x in ( dom G) implies x in ( dom P) & (P . x) in ( dom F)

          proof

            assume x in ( dom G);

            then x in ( Seg ( len P)) by A10, A9, FINSEQ_1:def 3;

            hence x in ( dom P) by FINSEQ_1:def 3;

            then (P . x) in ( rng P) by FUNCT_1:def 3;

            hence thesis by A16;

          end;

          assume that

           A20: x in ( dom P) and (P . x) in ( dom F);

          x in ( Seg ( len P)) by A20, FINSEQ_1:def 3;

          hence x in ( dom G) by A10, A9, FINSEQ_1:def 3;

        end;

        then

         A21: G = (F * P) by A13, FUNCT_1: 10;

        ( dom F) c= ( rng P)

        proof

          set f = ((F " ) * G);

          let x be object;

          assume

           A22: x in ( dom F);

          ( dom (F " )) = ( rng G) by A6, A7, A4, A2, FUNCT_1: 33;

          

          then

           A23: ( rng f) = ( rng (F " )) by RELAT_1: 28

          .= ( dom F) by A6, FUNCT_1: 33;

          f = (((F " ) * F) * P) by A21, RELAT_1: 36

          .= (( id ( dom F)) * P) by A6, FUNCT_1: 39

          .= P by A16, RELAT_1: 53;

          hence thesis by A22, A23;

        end;

        then

         A24: ( dom F) = ( rng P) by A16;

        

         A25: ( dom P) = ( dom F) by A10, FINSEQ_3: 29;

        then

         A26: P is one-to-one by A24, FINSEQ_4: 60;

        reconsider P as Function of ( dom F), ( dom F) by A16, A25, FUNCT_2: 2;

        

         A27: ( len f) = ( len F) by Def6;

        then

         A28: ( dom f) = ( dom F) by FINSEQ_3: 29;

        then

        reconsider P as Function of ( dom f), ( dom f);

        reconsider Fp = (f * P) as FinSequence of V by FINSEQ_2: 47;

        reconsider P as Permutation of ( dom f) by A24, A26, A28, FUNCT_2: 57;

        

         A29: Fp = (f * P);

        then

         A30: ( len Fp) = ( len f) by FINSEQ_2: 44;

        then

         A31: ( len Fp) = ( len g) by A9, A27, Def6;

         A32:

        now

          let k;

          let v be Vector of V;

          assume that

           A33: k in ( dom Fp) and

           A34: v = (g . k);

          

           A35: k in ( Seg ( len g)) by A31, A33, FINSEQ_1:def 3;

          then

           A36: k in ( dom P) by A10, A27, A30, A31, FINSEQ_1:def 3;

          

           A37: k in ( dom G) by A9, A27, A30, A31, A35, FINSEQ_1:def 3;

          then (G . k) in ( rng G) by FUNCT_1:def 3;

          then F just_once_values (G . k) by A6, A7, A4, A2, FINSEQ_4: 8;

          then

           A38: (F <- (G . k)) in ( dom F) by FINSEQ_4:def 3;

          then

          reconsider i = (F <- (G . k)) as Nat by FINSEQ_3: 23;

          

           A39: (G /. k) = (G . k) by A37, PARTFUN1:def 6

          .= (F . (P . k)) by A21, A36, FUNCT_1: 13

          .= (F . i) by A11, A12, A27, A30, A31, A35

          .= (F /. i) by A38, PARTFUN1:def 6;

          

           A40: k in ( dom g) by A35, FINSEQ_1:def 3;

          i in ( Seg ( len f)) by A27, A38, FINSEQ_1:def 3;

          then

           A41: i in ( dom f) by FINSEQ_1:def 3;

          

          thus (Fp . k) = (f . (P . k)) by A36, FUNCT_1: 13

          .= (f . (F <- (G . k))) by A11, A12, A27, A30, A31, A35

          .= ((F /. i) * (l . (F /. i))) by A41, Def6

          .= ((F /. i) * ((L . (F /. i)) * a)) by Def10

          .= (((F /. i) * (L . (F /. i))) * a) by VECTSP_2:def 9

          .= (v * a) by A34, A40, A39, Def6;

        end;

        ( Sum Fp) = ( Sum f) by A29, RLVECT_2: 7;

        hence thesis by A8, A5, A31, A32, Th1;

      end;

        suppose

         A42: a = ( 0. R);

        

        hence ( Sum (L * a)) = ( Sum ( ZeroLC V)) by Th44

        .= ( 0. V) by Lm3

        .= (( Sum L) * a) by A42, VECTSP_2: 32;

      end;

    end;

    theorem :: RMOD_4:60

    

     Th60: ( Sum ( - L)) = ( - ( Sum L))

    proof

      

      thus ( Sum ( - L)) = (( Sum L) * ( - ( 1_ R))) by Th59

      .= ( - ( Sum L)) by VECTSP_2: 32;

    end;

    theorem :: RMOD_4:61

    ( Sum (L1 - L2)) = (( Sum L1) - ( Sum L2))

    proof

      

      thus ( Sum (L1 - L2)) = (( Sum L1) + ( Sum ( - L2))) by Th58

      .= (( Sum L1) + ( - ( Sum L2))) by Th60

      .= (( Sum L1) - ( Sum L2)) by RLVECT_1:def 11;

    end;

    begin

    reserve x for set;

    reserve R for Ring;

    reserve V for RightMod of R;

    reserve v,v1,v2 for Vector of V;

    reserve A,B for Subset of V;

    definition

      let R, V;

      let IT be Subset of V;

      :: RMOD_4:def13

      attr IT is linearly-independent means for l be Linear_Combination of IT st ( Sum l) = ( 0. V) holds ( Carrier l) = {} ;

    end

    notation

      let R, V;

      let IT be Subset of V;

      antonym IT is linearly-dependent for IT is linearly-independent;

    end

    theorem :: RMOD_4:62

    A c= B & B is linearly-independent implies A is linearly-independent

    proof

      assume that

       A1: A c= B and

       A2: B is linearly-independent;

      let l be Linear_Combination of A;

      reconsider L = l as Linear_Combination of B by A1, Th19;

      assume ( Sum l) = ( 0. V);

      then ( Carrier L) = {} by A2;

      hence thesis;

    end;

    theorem :: RMOD_4:63

    

     Th63: ( 0. R) <> ( 1_ R) & A is linearly-independent implies not ( 0. V) in A

    proof

      assume that

       A1: ( 0. R) <> ( 1_ R) and

       A2: A is linearly-independent and

       A3: ( 0. V) in A;

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

      consider f be Function of the carrier of V, the carrier of R such that

       A4: (f . ( 0. V)) = ( 1_ R) and

       A5: for v be Element of V st v <> ( 0. V) holds (f . v) = F(v) from FUNCT_2:sch 6;

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

      ex T be finite Subset of V st for v st not v in T holds (f . v) = ( 0. R)

      proof

        take T = {( 0. V)};

        let v;

        assume not v in T;

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

        hence thesis by A5;

      end;

      then

      reconsider f as Linear_Combination of V by Def2;

      

       A6: ( Carrier f) = {( 0. V)}

      proof

        thus ( Carrier f) c= {( 0. V)}

        proof

          let x be object;

          assume x in ( Carrier f);

          then

          consider v such that

           A7: v = x and

           A8: (f . v) <> ( 0. R);

          v = ( 0. V) by A5, A8;

          hence thesis by A7, TARSKI:def 1;

        end;

        let x be object;

        assume x in {( 0. V)};

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

        hence thesis by A1, A4;

      end;

      then ( Carrier f) c= A by A3, ZFMISC_1: 31;

      then

      reconsider f as Linear_Combination of A by Def5;

      ( Sum f) = (( 0. V) * (f . ( 0. V))) by A6, Th35

      .= ( 0. V) by VECTSP_2: 32;

      hence contradiction by A2, A6;

    end;

    theorem :: RMOD_4:64

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

    proof

      let l be Linear_Combination of ( {} the carrier of V);

      ( Carrier l) c= {} by Def5;

      hence thesis;

    end;

    theorem :: RMOD_4:65

    

     Th65: ( 0. R) <> ( 1_ R) & {v1, v2} is linearly-independent implies v1 <> ( 0. V) & v2 <> ( 0. V)

    proof

      

       A1: v1 in {v1, v2} & v2 in {v1, v2} by TARSKI:def 2;

      assume ( 0. R) <> ( 1_ R) & {v1, v2} is linearly-independent;

      hence thesis by A1, Th63;

    end;

    theorem :: RMOD_4:66

    ( 0. R) <> ( 1_ R) implies {v, ( 0. V)} is linearly-dependent & {( 0. V), v} is linearly-dependent by Th65;

    reserve R for domRing;

    reserve V for RightMod of R;

    reserve v,u for Vector of V;

    reserve A,B for Subset of V;

    reserve l for Linear_Combination of A;

    reserve f,g for Function of the carrier of V, the carrier of R;

    definition

      let R, V, A;

      :: RMOD_4:def14

      func Lin (A) -> strict Submodule of V means

      : Def14: the carrier of it = the set of all ( Sum l);

      existence

      proof

        set A1 = the set of all ( Sum l);

        reconsider l = ( ZeroLC V) as Linear_Combination of A by Th20;

        A1 c= the carrier of V

        proof

          let x be object;

          assume x in A1;

          then ex l st x = ( Sum l);

          hence thesis;

        end;

        then

        reconsider A1 as Subset of V;

        

         A1: A1 is linearly-closed

        proof

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

          proof

            let v, u;

            assume that

             A2: v in A1 and

             A3: u in A1;

            consider l1 be Linear_Combination of A such that

             A4: v = ( Sum l1) by A2;

            consider l2 be Linear_Combination of A such that

             A5: u = ( Sum l2) by A3;

            reconsider f = (l1 + l2) as Linear_Combination of A by Th38;

            (v + u) = ( Sum f) by A4, A5, Th58;

            hence thesis;

          end;

          let a be Scalar of R, v;

          assume v in A1;

          then

          consider l such that

           A6: v = ( Sum l);

          reconsider f = (l * a) as Linear_Combination of A by Th45;

          (v * a) = ( Sum f) by A6, Th59;

          hence thesis;

        end;

        ( Sum l) = ( 0. V) by Lm3;

        then ( 0. V) in A1;

        hence thesis by A1, RMOD_2: 34;

      end;

      uniqueness by RMOD_2: 29;

    end

    theorem :: RMOD_4:67

    

     Th67: x in ( Lin A) iff ex l st x = ( Sum l)

    proof

      thus x in ( Lin A) implies ex l st x = ( Sum l)

      proof

        assume x in ( Lin A);

        then x in the carrier of ( Lin A) by STRUCT_0:def 5;

        then x in the set of all ( Sum l) by Def14;

        hence thesis;

      end;

      given k be Linear_Combination of A such that

       A1: x = ( Sum k);

      x in the set of all ( Sum l) by A1;

      then x in the carrier of ( Lin A) by Def14;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: RMOD_4:68

    

     Th68: x in A implies x in ( Lin A)

    proof

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

      assume

       A1: x in A;

      then

      reconsider v = x as Vector of V;

      consider f be Function of the carrier of V, the carrier of R such that

       A2: (f . v) = ( 1_ R) and

       A3: for u st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

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

      ex T be finite Subset of V st for u st not u in T holds (f . u) = ( 0. R)

      proof

        take T = {v};

        let u;

        assume not u in T;

        then u <> v by TARSKI:def 1;

        hence thesis by A3;

      end;

      then

      reconsider f as Linear_Combination of V by Def2;

      

       A4: ( Carrier f) c= {v}

      proof

        let x be object;

        assume x in ( Carrier f);

        then

        consider u such that

         A5: x = u and

         A6: (f . u) <> ( 0. R);

        u = v by A3, A6;

        hence thesis by A5, TARSKI:def 1;

      end;

      then

      reconsider f as Linear_Combination of {v} by Def5;

      

       A7: ( Sum f) = (v * ( 1_ R)) by A2, Th32

      .= v by VECTSP_2:def 9;

       {v} c= A by A1, ZFMISC_1: 31;

      then ( Carrier f) c= A by A4;

      then

      reconsider f as Linear_Combination of A by Def5;

      ( Sum f) = v by A7;

      hence thesis by Th67;

    end;

    theorem :: RMOD_4:69

    ( Lin ( {} the carrier of V)) = ( (0). V)

    proof

      set A = ( Lin ( {} the carrier of V));

      now

        let v;

        thus v in A implies v in ( (0). V)

        proof

          assume v in A;

          then

           A1: v in the carrier of A by STRUCT_0:def 5;

          the carrier of A = the set of all ( Sum l0) where l0 be Linear_Combination of ( {} the carrier of V) by Def14;

          then ex l0 be Linear_Combination of ( {} the carrier of V) st v = ( Sum l0) by A1;

          then v = ( 0. V) by Th31;

          hence thesis by RMOD_2: 35;

        end;

        assume v in ( (0). V);

        then v = ( 0. V) by RMOD_2: 35;

        hence v in A by RMOD_2: 17;

      end;

      hence thesis by RMOD_2: 30;

    end;

    theorem :: RMOD_4:70

    ( Lin A) = ( (0). V) implies A = {} or A = {( 0. V)}

    proof

      assume that

       A1: ( Lin A) = ( (0). V) and

       A2: A <> {} ;

      thus A c= {( 0. V)}

      proof

        let x be object;

        assume x in A;

        then x in ( Lin A) by Th68;

        then x = ( 0. V) by A1, RMOD_2: 35;

        hence thesis by TARSKI:def 1;

      end;

      set y = the Element of A;

      let x be object;

      assume x in {( 0. V)};

      then

       A3: x = ( 0. V) by TARSKI:def 1;

      y in A & y in ( Lin A) by A2, Th68;

      hence thesis by A1, A3, RMOD_2: 35;

    end;

    theorem :: RMOD_4:71

    

     Th71: for W be strict Submodule of V st ( 0. R) <> ( 1_ R) & A = the carrier of W holds ( Lin A) = W

    proof

      let W be strict Submodule of V;

      assume that

       A1: ( 0. R) <> ( 1_ R) and

       A2: A = the carrier of W;

      now

        let v;

        thus v in ( Lin A) implies v in W

        proof

          assume v in ( Lin A);

          then

           A3: ex l st v = ( Sum l) by Th67;

          A is linearly-closed by A2, RMOD_2: 33;

          then v in the carrier of W by A1, A2, A3, Th29;

          hence thesis by STRUCT_0:def 5;

        end;

        v in W iff v in the carrier of W by STRUCT_0:def 5;

        hence v in W implies v in ( Lin A) by A2, Th68;

      end;

      hence thesis by RMOD_2: 30;

    end;

    theorem :: RMOD_4:72

    for V be strict RightMod of R, A be Subset of V st ( 0. R) <> ( 1_ R) & A = the carrier of V holds ( Lin A) = V

    proof

      let V be strict RightMod of R, A be Subset of V such that

       A1: ( 0. R) <> ( 1_ R);

      assume

       A2: A = the carrier of V;

      ( (Omega). V) = V;

      hence thesis by A1, A2, Th71;

    end;

    theorem :: RMOD_4:73

    

     Th73: A c= B implies ( Lin A) is Submodule of ( Lin B)

    proof

      assume

       A1: A c= B;

      now

        let v;

        assume v in ( Lin A);

        then

        consider l such that

         A2: v = ( Sum l) by Th67;

        reconsider l as Linear_Combination of B by A1, Th19;

        ( Sum l) = v by A2;

        hence v in ( Lin B) by Th67;

      end;

      hence thesis by RMOD_2: 28;

    end;

    theorem :: RMOD_4:74

    for V be strict RightMod of R, A,B be Subset of V st ( Lin A) = V & A c= B holds ( Lin B) = V

    proof

      let V be strict RightMod of R, A,B be Subset of V;

      assume ( Lin A) = V & A c= B;

      then V is Submodule of ( Lin B) by Th73;

      hence thesis by RMOD_2: 25;

    end;

    theorem :: RMOD_4:75

    ( Lin (A \/ B)) = (( Lin A) + ( Lin B))

    proof

      now

        deffunc G( object) = ( 0. R);

        let v;

        assume v in ( Lin (A \/ B));

        then

        consider l be Linear_Combination of (A \/ B) such that

         A1: v = ( Sum l) by Th67;

        deffunc F( object) = (l . $1);

        set D = (( Carrier l) \ A);

        set C = (( Carrier l) /\ A);

        defpred P[ object] means $1 in C;

        defpred C[ object] means $1 in D;

        now

          let x;

          assume x in the carrier of V;

          then

          reconsider v = x as Vector of V;

          (f . v) in the carrier of R;

          hence x in C implies (l . x) in the carrier of R;

          assume not x in C;

          thus ( 0. R) in the carrier of R;

        end;

        then

         A2: for x be object st x in the carrier of V holds ( P[x] implies F(x) in the carrier of R) & ( not P[x] implies G(x) in the carrier of R);

        consider f be Function of the carrier of V, the carrier of R such that

         A3: for x be object st x in the carrier of V holds ( P[x] implies (f . x) = F(x)) & ( not P[x] implies (f . x) = G(x)) from FUNCT_2:sch 5( A2);

        reconsider C as finite Subset of V;

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

        for u holds not u in C implies (f . u) = ( 0. R) by A3;

        then

        reconsider f as Linear_Combination of V by Def2;

        

         A4: ( Carrier f) c= C

        proof

          let x be object;

          assume x in ( Carrier f);

          then

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

          assume not x in C;

          hence thesis by A3, A5;

        end;

        C c= A by XBOOLE_1: 17;

        then ( Carrier f) c= A by A4;

        then

        reconsider f as Linear_Combination of A by Def5;

        now

          let x;

          assume x in the carrier of V;

          then

          reconsider v = x as Vector of V;

          (g . v) in the carrier of R;

          hence x in D implies (l . x) in the carrier of R;

          assume not x in D;

          thus ( 0. R) in the carrier of R;

        end;

        then

         A6: for x be object st x in the carrier of V holds ( C[x] implies F(x) in the carrier of R) & ( not C[x] implies G(x) in the carrier of R);

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

         A7: for x be object st x in the carrier of V holds ( C[x] implies (g . x) = F(x)) & ( not C[x] implies (g . x) = G(x)) from FUNCT_2:sch 5( A6);

        reconsider D as finite Subset of V;

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

        for u holds not u in D implies (g . u) = ( 0. R) by A7;

        then

        reconsider g as Linear_Combination of V by Def2;

        

         A8: D c= B

        proof

          let x be object;

          assume x in D;

          then

           A9: x in ( Carrier l) & not x in A by XBOOLE_0:def 5;

          ( Carrier l) c= (A \/ B) by Def5;

          hence thesis by A9, XBOOLE_0:def 3;

        end;

        ( Carrier g) c= D

        proof

          let x be object;

          assume x in ( Carrier g);

          then

           A10: ex u st x = u & (g . u) <> ( 0. R);

          assume not x in D;

          hence thesis by A7, A10;

        end;

        then ( Carrier g) c= B by A8;

        then

        reconsider g as Linear_Combination of B by Def5;

        l = (f + g)

        proof

          let v;

          now

            per cases ;

              suppose

               A11: v in C;

               A12:

              now

                assume v in D;

                then not v in A by XBOOLE_0:def 5;

                hence contradiction by A11, XBOOLE_0:def 4;

              end;

              

              thus ((f + g) . v) = ((f . v) + (g . v)) by Def9

              .= ((l . v) + (g . v)) by A3, A11

              .= ((l . v) + ( 0. R)) by A7, A12

              .= (l . v) by RLVECT_1: 4;

            end;

              suppose

               A13: not v in C;

              now

                per cases ;

                  suppose

                   A14: v in ( Carrier l);

                   A15:

                  now

                    assume not v in D;

                    then not v in ( Carrier l) or v in A by XBOOLE_0:def 5;

                    hence contradiction by A13, A14, XBOOLE_0:def 4;

                  end;

                  

                  thus ((f + g) . v) = ((f . v) + (g . v)) by Def9

                  .= (( 0. R) + (g . v)) by A3, A13

                  .= (g . v) by RLVECT_1: 4

                  .= (l . v) by A7, A15;

                end;

                  suppose

                   A16: not v in ( Carrier l);

                  then

                   A17: not v in D by XBOOLE_0:def 5;

                  

                   A18: not v in C by A16, XBOOLE_0:def 4;

                  

                  thus ((f + g) . v) = ((f . v) + (g . v)) by Def9

                  .= (( 0. R) + (g . v)) by A3, A18

                  .= (( 0. R) + ( 0. R)) by A7, A17

                  .= ( 0. R) by RLVECT_1: 4

                  .= (l . v) by A16;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then

         A19: v = (( Sum f) + ( Sum g)) by A1, Th58;

        ( Sum f) in ( Lin A) & ( Sum g) in ( Lin B) by Th67;

        hence v in (( Lin A) + ( Lin B)) by A19, RMOD_3: 1;

      end;

      then

       A20: ( Lin (A \/ B)) is Submodule of (( Lin A) + ( Lin B)) by RMOD_2: 28;

      ( Lin A) is Submodule of ( Lin (A \/ B)) & ( Lin B) is Submodule of ( Lin (A \/ B)) by Th73, XBOOLE_1: 7;

      then (( Lin A) + ( Lin B)) is Submodule of ( Lin (A \/ B)) by RMOD_3: 35;

      hence thesis by A20, RMOD_2: 25;

    end;

    theorem :: RMOD_4:76

    ( Lin (A /\ B)) is Submodule of (( Lin A) /\ ( Lin B))

    proof

      ( Lin (A /\ B)) is Submodule of ( Lin A) & ( Lin (A /\ B)) is Submodule of ( Lin B) by Th73, XBOOLE_1: 17;

      hence thesis by RMOD_3: 20;

    end;