vectsp_7.miz



    begin

    definition

      let GF be non empty doubleLoopStr, V be non empty ModuleStr over GF;

      let IT be Subset of V;

      :: VECTSP_7:def1

      attr IT is linearly-independent means for l be Linear_Combination of IT st ( Sum l) = ( 0. V) holds ( Carrier l) = {} ;

    end

    notation

      let GF be non empty doubleLoopStr, V be non empty ModuleStr over GF;

      let IT be Subset of V;

      antonym IT is linearly-dependent for IT is linearly-independent;

    end

    reserve x,y for object,

X,Y,Z for set;

    reserve GF for commutative Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

    reserve a,b for Element of GF;

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

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

    reserve A,B,C for Subset of V;

    reserve T for finite Subset of V;

    reserve l for Linear_Combination of A;

    reserve f,g for Function of V, GF;

    theorem :: VECTSP_7:1

    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, VECTSP_6: 4;

      assume ( Sum l) = ( 0. V);

      then ( Carrier L) = {} by A2;

      hence thesis;

    end;

    reserve GF for commutative non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

    reserve a,b for Element of GF;

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

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

    reserve A,B,C for Subset of V;

    reserve T for finite Subset of V;

    reserve l for Linear_Combination of A;

    reserve f,g for Function of V, GF;

    theorem :: VECTSP_7:2

    

     Th2: for R be non degenerated Ring, V be LeftMod of R, A be Subset of V st A is linearly-independent holds not ( 0. V) in A

    proof

      let R be non degenerated Ring, V be LeftMod of R, A be Subset of V;

      assume that

       A2: A is linearly-independent and

       A3: ( 0. V) in A;

      deffunc U( set) = ( 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) = U(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 be Vector of V st not v in T holds (f . v) = ( 0. R)

      proof

        take T = {( 0. V)};

        let v be Vector of 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 VECTSP_6:def 1;

      

       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 be Vector of 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 A4;

      end;

      then ( Carrier f) c= A by A3, ZFMISC_1: 31;

      then

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

      ( Sum f) = ((f . ( 0. V)) * ( 0. V)) by A6, VECTSP_6: 20

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

      hence contradiction by A2, A6;

    end;

    registration

      let GF, V;

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

      coherence

      proof

        let S be Subset of V such that

         A1: S is empty;

        let l be Linear_Combination of S;

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

        hence thesis;

      end;

    end

    registration

      let GF, V;

      cluster finite linearly-independent for Subset of V;

      existence

      proof

        take ( {} V);

        thus thesis;

      end;

    end

    theorem :: VECTSP_7:3

    for R be commutative non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of R, v be Vector of V holds {v} is linearly-independent iff v <> ( 0. V)

    proof

      let R be commutative non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

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

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

      proof

        assume {v} is linearly-independent;

        then not ( 0. V) in {v} by Th2;

        hence thesis by TARSKI:def 1;

      end;

      assume

       A1: v <> ( 0. V);

      let l be Linear_Combination of {v};

      

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

      assume

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

      now

        per cases by A2, ZFMISC_1: 33;

          suppose ( Carrier l) = {} ;

          hence thesis;

        end;

          suppose

           A4: ( Carrier l) = {v};

          

           A5: ( 0. V) = ((l . v) * v) by A3, VECTSP_6: 17;

          now

            assume v in ( Carrier l);

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

            hence contradiction by A1, A5, VECTSP_1: 15;

          end;

          hence thesis by A4, TARSKI:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_7:4

    

     Th4: for GF be commutative non degenerated Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian non empty ModuleStr over GF, v1,v2 be Vector of V st {v1, v2} is linearly-independent holds v1 <> ( 0. V)

    proof

      let GF be commutative non degenerated Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian non empty ModuleStr over GF, v1,v2 be Vector of V;

      

       A1: v1 in {v1, v2} by TARSKI:def 2;

      assume {v1, v2} is linearly-independent;

      hence thesis by A1, Th2;

    end;

    theorem :: VECTSP_7:5

    

     Th5: v1 <> v2 & {v1, v2} is linearly-independent iff v2 <> ( 0. V) & for a holds v1 <> (a * v2)

    proof

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

      proof

        deffunc F( set) = ( 0. GF);

        assume that

         A1: v1 <> v2 and

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

        thus v2 <> ( 0. V) by A2, Th4;

        let a;

        consider f such that

         A3: (f . v1) = ( - ( 1_ GF)) & (f . v2) = a and

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

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

        now

          let v;

          assume not v in {v1, v2};

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

          hence (f . v) = ( 0. GF) by A4;

        end;

        then

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

        ( Carrier f) c= {v1, v2}

        proof

          let x be object;

          assume x in ( Carrier f);

          then

           A5: ex u st x = u & (f . u) <> ( 0. GF);

          assume not x in {v1, v2};

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

          hence thesis by A4, A5;

        end;

        then

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

         A6:

        now

          assume not v1 in ( Carrier f);

          then ( 0. GF) = ( - ( 1_ GF)) by A3;

          hence contradiction by VECTSP_6: 49;

        end;

        set w = (a * v2);

        assume v1 = (a * v2);

        

        then ( Sum f) = ((( - ( 1_ GF)) * w) + w) by A1, A3, VECTSP_6: 18

        .= (( - w) + w) by VECTSP_1: 14

        .= ( - (w - w)) by VECTSP_1: 17

        .= ( - ( 0. V)) by VECTSP_1: 19

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

        hence thesis by A2, A6;

      end;

      assume

       A7: v2 <> ( 0. V);

      assume

       A8: for a holds v1 <> (a * v2);

      

       A9: (( 1_ GF) * v2) = v2 by VECTSP_1:def 17;

      hence v1 <> v2 by A8;

      let l be Linear_Combination of {v1, v2};

      assume that

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

       A11: ( Carrier l) <> {} ;

      

       A12: ( 0. V) = (((l . v1) * v1) + ((l . v2) * v2)) by A8, A9, A10, VECTSP_6: 18;

      set x = the Element of ( Carrier l);

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

      then

       A13: x in {v1, v2} by A11;

      x in ( Carrier l) by A11;

      then

       A14: ex u st x = u & (l . u) <> ( 0. GF);

      now

        per cases by A14, A13, TARSKI:def 2;

          suppose

           A15: (l . v1) <> ( 0. GF);

          ( 0. V) = (((l . v1) " ) * (((l . v1) * v1) + ((l . v2) * v2))) by A12, VECTSP_1: 15

          .= ((((l . v1) " ) * ((l . v1) * v1)) + (((l . v1) " ) * ((l . v2) * v2))) by VECTSP_1:def 14

          .= (((((l . v1) " ) * (l . v1)) * v1) + (((l . v1) " ) * ((l . v2) * v2))) by VECTSP_1:def 16

          .= (((((l . v1) " ) * (l . v1)) * v1) + ((((l . v1) " ) * (l . v2)) * v2)) by VECTSP_1:def 16

          .= ((( 1_ GF) * v1) + ((((l . v1) " ) * (l . v2)) * v2)) by A15, VECTSP_1:def 10

          .= (v1 + ((((l . v1) " ) * (l . v2)) * v2)) by VECTSP_1:def 17;

          

          then v1 = ( - ((((l . v1) " ) * (l . v2)) * v2)) by VECTSP_1: 16

          .= (( - ( 1_ GF)) * ((((l . v1) " ) * (l . v2)) * v2)) by VECTSP_1: 14

          .= ((( - ( 1_ GF)) * (((l . v1) " ) * (l . v2))) * v2) by VECTSP_1:def 16;

          hence thesis by A8;

        end;

          suppose

           A16: (l . v2) <> ( 0. GF) & (l . v1) = ( 0. GF);

          ( 0. V) = (((l . v2) " ) * (((l . v1) * v1) + ((l . v2) * v2))) by A12, VECTSP_1: 15

          .= ((((l . v2) " ) * ((l . v1) * v1)) + (((l . v2) " ) * ((l . v2) * v2))) by VECTSP_1:def 14

          .= (((((l . v2) " ) * (l . v1)) * v1) + (((l . v2) " ) * ((l . v2) * v2))) by VECTSP_1:def 16

          .= (((((l . v2) " ) * (l . v1)) * v1) + ((((l . v2) " ) * (l . v2)) * v2)) by VECTSP_1:def 16

          .= (((((l . v2) " ) * (l . v1)) * v1) + (( 1_ GF) * v2)) by A16, VECTSP_1:def 10

          .= (((((l . v2) " ) * (l . v1)) * v1) + v2) by VECTSP_1:def 17

          .= ((( 0. GF) * v1) + v2) by A16

          .= (( 0. V) + v2) by VECTSP_1: 15

          .= v2 by RLVECT_1: 4;

          hence thesis by A7;

        end;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_7:6

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

    proof

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

      proof

        assume

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

        let a, b;

        assume that

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

         A3: a <> ( 0. GF) or b <> ( 0. GF);

        now

          per cases by A3;

            suppose

             A4: a <> ( 0. GF);

            ( 0. V) = ((a " ) * ((a * v1) + (b * v2))) by A2, VECTSP_1: 15

            .= (((a " ) * (a * v1)) + ((a " ) * (b * v2))) by VECTSP_1:def 14

            .= ((((a " ) * a) * v1) + ((a " ) * (b * v2))) by VECTSP_1:def 16

            .= ((((a " ) * a) * v1) + (((a " ) * b) * v2)) by VECTSP_1:def 16

            .= ((( 1_ GF) * v1) + (((a " ) * b) * v2)) by A4, VECTSP_1:def 10

            .= (v1 + (((a " ) * b) * v2)) by VECTSP_1:def 17;

            

            then v1 = ( - (((a " ) * b) * v2)) by VECTSP_1: 16

            .= (( - ( 1_ GF)) * (((a " ) * b) * v2)) by VECTSP_1: 14

            .= ((( - ( 1_ GF)) * ((a " ) * b)) * v2) by VECTSP_1:def 16;

            hence thesis by A1, Th5;

          end;

            suppose

             A5: b <> ( 0. GF);

            ( 0. V) = ((b " ) * ((a * v1) + (b * v2))) by A2, VECTSP_1: 15

            .= (((b " ) * (a * v1)) + ((b " ) * (b * v2))) by VECTSP_1:def 14

            .= ((((b " ) * a) * v1) + ((b " ) * (b * v2))) by VECTSP_1:def 16

            .= ((((b " ) * a) * v1) + (((b " ) * b) * v2)) by VECTSP_1:def 16

            .= ((((b " ) * a) * v1) + (( 1_ GF) * v2)) by A5, VECTSP_1:def 10

            .= ((((b " ) * a) * v1) + v2) by VECTSP_1:def 17;

            

            then v2 = ( - (((b " ) * a) * v1)) by VECTSP_1: 16

            .= (( - ( 1_ GF)) * (((b " ) * a) * v1)) by VECTSP_1: 14

            .= ((( - ( 1_ GF)) * ((b " ) * a)) * v1) by VECTSP_1:def 16;

            hence thesis by A1, Th5;

          end;

        end;

        hence thesis;

      end;

      assume

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

       A7:

      now

        let a;

        assume v1 = (a * v2);

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

        

        then ( 0. V) = (v1 - (a * v2)) by VECTSP_2: 2

        .= (v1 + (( - a) * v2)) by VECTSP_1: 21

        .= ((( 1. GF) * v1) + (( - a) * v2)) by VECTSP_1:def 17;

        hence contradiction by A6;

      end;

      now

        assume

         A8: v2 = ( 0. V);

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

        .= ((( 0. GF) * v1) + ( 0. V)) by VECTSP_1: 15

        .= ((( 0. GF) * v1) + (( 1. GF) * v2)) by A8, VECTSP_1: 15;

        hence contradiction by A6;

      end;

      hence thesis by A7, Th5;

    end;

    

     TH2: for GF be Ring, V be LeftMod of GF, L be Linear_Combination of V, C be finite Subset of V holds ( Carrier L) c= C implies ex F be FinSequence of V st F is one-to-one & ( rng F) = C & ( Sum L) = ( Sum (L (#) F))

    proof

      let GF be Ring, V be LeftMod of GF, L be Linear_Combination of V, C be finite Subset of V;

      assume

       A1: ( Carrier L) c= C;

      set D = (C \ ( Carrier L));

      consider G be FinSequence of V such that

       A2: G is one-to-one and

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

       A4: ( Sum L) = ( Sum (L (#) G)) by VECTSP_6:def 6;

      consider p be FinSequence such that

       A5: ( rng p) = D and

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

      reconsider p as FinSequence of the carrier of V by A5, FINSEQ_1:def 4;

      

       A7: ( rng G) misses ( rng p)

      proof

        assume ( rng G) meets ( rng p);

        then ex x be object st x in ( Carrier L) & x in D by A3, A5, XBOOLE_0: 3;

        hence thesis by XBOOLE_0:def 5;

      end;

      

       A8: ( len p) = ( len (L (#) p)) by VECTSP_6:def 5;

      now

        let k be Nat;

        assume

         A9: k in ( dom p);

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

        then (p /. k) in D by A5, A9, FUNCT_1:def 3;

        then

         A10: not (p /. k) in ( Carrier L) by XBOOLE_0:def 5;

        k in ( dom (L (#) p)) by A8, A9, FINSEQ_3: 29;

        then ((L (#) p) . k) = ((L . (p /. k)) * (p /. k)) by VECTSP_6:def 5;

        hence ((L (#) p) . k) = (( 0. GF) * (p /. k)) by A10;

      end;

      

      then

       A11: ( Sum (L (#) p)) = (( 0. GF) * ( Sum p)) by A8, RLVECT_2: 67

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

      set F = (G ^ p);

      take F;

      

       A12: ( Sum (L (#) F)) = ( Sum ((L (#) G) ^ (L (#) p))) by VECTSP_6: 13

      .= (( Sum (L (#) G)) + ( 0. V)) by A11, RLVECT_1: 41

      .= ( Sum L) by A4, RLVECT_1:def 4;

      ( rng F) = (( Carrier L) \/ D) by A3, A5, FINSEQ_1: 31

      .= C by A1, XBOOLE_1: 45;

      hence thesis by A2, A6, A12, A7, FINSEQ_3: 91;

    end;

    

     TH3: for GF be Ring, V be LeftMod of GF, L be Linear_Combination of V, a be Scalar of V holds ( Sum (a * L)) = (a * ( Sum L))

    proof

      let GF be Ring, V be LeftMod of GF, L be Linear_Combination of V, a be Scalar of GF;

      set l = (a * L);

      ( Carrier l) c= ( Carrier L) by VECTSP_6: 28;

      then

      consider F be FinSequence of the carrier of V such that

       A1: F is one-to-one & ( rng F) = ( Carrier L) and

       A2: ( Sum l) = ( Sum (l (#) F)) by TH2;

      set f = (l (#) F), g = (L (#) F);

      

       A3: ( len f) = ( len F) by VECTSP_6:def 5

      .= ( len g) by VECTSP_6:def 5;

      ( len f) = ( len F) by VECTSP_6:def 5;

      then

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

       A5:

      now

        let k be Nat, v be Vector of V;

        assume that

         A6: k in ( dom f) and

         A7: v = (g . k);

        set v9 = (F /. k);

        

         A8: k in ( Seg ( len f)) by A6, FINSEQ_1:def 3;

        then

         A9: v9 = (F . k) by A4, PARTFUN1:def 6;

        

        hence (f . k) = ((l . v9) * v9) by A4, A8, VECTSP_6: 8

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

        .= (a * ((L . v9) * v9)) by VECTSP_1:def 16

        .= (a * v) by A4, A7, A8, A9, VECTSP_6: 8;

      end;

      ( Sum L) = ( Sum (L (#) F)) by A1, VECTSP_6:def 6;

      hence thesis by A2, A3, A5, RLVECT_2: 66;

    end;

    definition

      let GF be Ring;

      let V be LeftMod of GF, A be Subset of V;

      :: VECTSP_7:def2

      func Lin (A) -> strict Subspace of V means

      : Def2: the carrier of it = the set of all ( Sum l) where l be Linear_Combination of A;

      existence

      proof

        set A1 = the set of all ( Sum l) where l be Linear_Combination of A;

        A1 c= the carrier of V

        proof

          let x be object;

          assume x in A1;

          then ex l be Linear_Combination of A st x = ( Sum l);

          hence thesis;

        end;

        then

        reconsider A1 as Subset of V;

        reconsider l = ( ZeroLC V) as Linear_Combination of A by VECTSP_6: 5;

        

         A1: A1 is linearly-closed

        proof

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

          proof

            let v,u be Vector of V;

            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 VECTSP_6: 24;

            (v + u) = ( Sum f) by A4, A5, VECTSP_6: 44;

            hence thesis;

          end;

          let a be Scalar of V, v be Vector of V;

          assume v in A1;

          then

          consider l be Linear_Combination of A such that

           A6: v = ( Sum l);

          reconsider f = (a * l) as Linear_Combination of A by VECTSP_6: 31;

          (a * v) = ( Sum f) by A6, TH3;

          hence thesis;

        end;

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

        then ( 0. V) in A1;

        hence thesis by A1, VECTSP_4: 34;

      end;

      uniqueness by VECTSP_4: 29;

    end

    theorem :: VECTSP_7:7

    

     Th7: for GF be Ring, V be LeftMod of GF, A be Subset of V holds x in ( Lin A) iff ex l be Linear_Combination of A st x = ( Sum l)

    proof

      let GF be Ring, V be LeftMod of GF, A be Subset of V;

      thus x in ( Lin A) implies ex l be Linear_Combination of A 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) where l be Linear_Combination of A by Def2;

        hence thesis;

      end;

      given k be Linear_Combination of A such that

       A1: x = ( Sum k);

      x in the set of all ( Sum l) where l be Linear_Combination of A by A1;

      then x in the carrier of ( Lin A) by Def2;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: VECTSP_7:8

    

     Th8: for GF be Ring, V be LeftMod of GF, A be Subset of V holds x in A implies x in ( Lin A)

    proof

      let GF be Ring, V be LeftMod of GF, A be Subset of V;

      deffunc F( set) = ( 0. GF);

      assume

       A1: x in A;

      then

      reconsider v = x as Vector of V;

      consider f be Function of V, GF such that

       A2: (f . v) = ( 1_ GF) and

       A3: for u be Vector 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 GF)) by FUNCT_2: 8;

      ex T be finite Subset of V st for u be Vector of V st not u in T holds (f . u) = ( 0. GF)

      proof

        take T = {v};

        let u be Vector of V;

        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 VECTSP_6:def 1;

      

       A4: ( Carrier f) c= {v}

      proof

        let x be object;

        assume x in ( Carrier f);

        then

        consider u be Vector of V such that

         A5: x = u and

         A6: (f . u) <> ( 0. GF);

        u = v by A3, A6;

        hence thesis by A5, TARSKI:def 1;

      end;

      then

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

      

       A7: ( Sum f) = (( 1_ GF) * v) by A2, VECTSP_6: 17

      .= v by VECTSP_1:def 17;

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

      then ( Carrier f) c= A by A4;

      then

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

      ( Sum f) = v by A7;

      hence thesis by Th7;

    end;

    reserve l0 for Linear_Combination of ( {} the carrier of V);

    theorem :: VECTSP_7:9

    

     Th9: for GF be Ring, V be LeftMod of GF holds ( Lin ( {} the carrier of V)) = ( (0). V)

    proof

      let GF be Ring, V be LeftMod of GF;

      set A = ( Lin ( {} the carrier of V));

      now

        let v be Vector of 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 Def2;

          then ex l0 be Linear_Combination of ( {} the carrier of V) st v = ( Sum l0) by A1;

          then v = ( 0. V) by VECTSP_6: 16;

          hence thesis by VECTSP_4: 35;

        end;

        assume v in ( (0). V);

        then v = ( 0. V) by VECTSP_4: 35;

        hence v in A by VECTSP_4: 17;

      end;

      hence thesis by VECTSP_4: 30;

    end;

    theorem :: VECTSP_7:10

    for GF be Ring, V be LeftMod of GF, A be Subset of V holds ( Lin A) = ( (0). V) implies A = {} or A = {( 0. V)}

    proof

      let GF be Ring, V be LeftMod of GF, A be Subset of V;

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

        then x = ( 0. V) by A1, VECTSP_4: 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, Th8;

      hence thesis by A1, A3, VECTSP_4: 35;

    end;

    theorem :: VECTSP_7:11

    

     Th11: for GF be non degenerated Ring, V be LeftMod of GF, A be Subset of V holds for W be strict Subspace of V st A = the carrier of W holds ( Lin A) = W

    proof

      let GF be non degenerated Ring, V be LeftMod of GF, A be Subset of V;

      let W be strict Subspace of V;

      assume

       A1: A = the carrier of W;

      now

        let v be Vector of V;

        

         A2: ( 0. GF) <> ( 1. GF);

        thus v in ( Lin A) implies v in W

        proof

          assume v in ( Lin A);

          then

           A3: ex l be Linear_Combination of A st v = ( Sum l) by Th7;

          A is linearly-closed by A1, VECTSP_4: 33;

          then v in the carrier of W by A1, A2, A3, VECTSP_6: 14;

          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 A1, Th8;

      end;

      hence thesis by VECTSP_4: 30;

    end;

    theorem :: VECTSP_7:12

    for V be strict VectSp of GF, A be Subset of V st A = the carrier of V holds ( Lin A) = V

    proof

      let V be strict VectSp of GF, A be Subset of V such that

       A1: A = the carrier of V;

      ( (Omega). V) = V;

      hence thesis by A1, Th11;

    end;

    theorem :: VECTSP_7:13

    

     Th13: for GF be Ring, V be LeftMod of GF, A,B be Subset of V holds A c= B implies ( Lin A) is Subspace of ( Lin B)

    proof

      let GF be Ring, V be LeftMod of GF, A,B be Subset of V;

      assume

       A1: A c= B;

      now

        let v be Vector of V;

        assume v in ( Lin A);

        then

        consider l be Linear_Combination of A such that

         A2: v = ( Sum l) by Th7;

        reconsider l as Linear_Combination of B by A1, VECTSP_6: 4;

        ( Sum l) = v by A2;

        hence v in ( Lin B) by Th7;

      end;

      hence thesis by VECTSP_4: 28;

    end;

    theorem :: VECTSP_7:14

    ( Lin A) = V & A c= B implies ( Lin B) = V

    proof

      assume that

       A1: ( Lin A) = V and

       A2: A c= B;

      V is Subspace of ( Lin B) by A1, A2, Th13;

      hence thesis by A1, VECTSP_4: 25;

    end;

    theorem :: VECTSP_7:15

    for GF be Ring, V be LeftMod of GF, A,B be Subset of V holds ( Lin (A \/ B)) = (( Lin A) + ( Lin B))

    proof

      let GF be Ring, V be LeftMod of GF, A,B be Subset of V;

      now

        deffunc F( object) = ( 0. GF);

        let v be Vector of V;

        assume v in ( Lin (A \/ B));

        then

        consider l be Linear_Combination of (A \/ B) such that

         A1: v = ( Sum l) by Th7;

        deffunc G( object) = (l . $1);

        set D = (( Carrier l) \ A);

        set C = (( Carrier l) /\ A);

        defpred P[ object] means $1 in C;

         A2:

        now

          let x be object;

          assume x in the carrier of V;

          then

          reconsider v = x as Vector of V;

          for f be Function of V, GF holds (f . v) in the carrier of GF;

          hence P[x] implies G(x) in the carrier of GF;

          assume not P[x];

          thus F(x) in the carrier of GF;

        end;

        reconsider C as finite Subset of V;

        defpred C[ object] means $1 in D;

        reconsider D as finite Subset of V;

        

         A3: D c= B

        proof

          let x be object;

          assume x in D;

          then

           A4: x in ( Carrier l) & not x in A by XBOOLE_0:def 5;

          ( Carrier l) c= (A \/ B) by VECTSP_6:def 4;

          hence thesis by A4, XBOOLE_0:def 3;

        end;

        consider f be Function of V, GF such that

         A5: for x be object st x in the carrier of V holds ( P[x] implies (f . x) = G(x)) & ( not P[x] implies (f . x) = F(x)) from FUNCT_2:sch 5( A2);

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

        for u be Vector of V holds not u in C implies (f . u) = ( 0. GF) by A5;

        then

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

        

         A6: ( Carrier f) c= C

        proof

          let x be object;

          assume x in ( Carrier f);

          then

           A7: ex u be Vector of V st x = u & (f . u) <> ( 0. GF);

          assume not x in C;

          hence thesis by A5, A7;

        end;

        C c= A by XBOOLE_1: 17;

        then ( Carrier f) c= A by A6;

        then

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

        deffunc G( object) = (l . $1);

         A8:

        now

          let x be object;

          assume x in the carrier of V;

          then

          reconsider v = x as Vector of V;

          for g be Function of V, GF holds (g . v) in the carrier of GF;

          hence C[x] implies G(x) in the carrier of GF;

          assume not C[x];

          thus F(x) in the carrier of GF;

        end;

        consider g be Function of the carrier of V, the carrier of GF such that

         A9: for x be object st x in the carrier of V holds ( C[x] implies (g . x) = G(x)) & ( not C[x] implies (g . x) = F(x)) from FUNCT_2:sch 5( A8);

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

        for u be Vector of V holds not u in D implies (g . u) = ( 0. GF) by A9;

        then

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

        ( Carrier g) c= D

        proof

          let x be object;

          assume x in ( Carrier g);

          then

           A10: ex u be Vector of V st x = u & (g . u) <> ( 0. GF);

          assume not x in D;

          hence thesis by A9, A10;

        end;

        then ( Carrier g) c= B by A3;

        then

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

        l = (f + g)

        proof

          let v be Vector of 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 VECTSP_6: 22

              .= ((l . v) + (g . v)) by A5, A11

              .= ((l . v) + ( 0. GF)) by A9, 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 VECTSP_6: 22

                  .= ((g . v) + ( 0. GF)) by A5, A13

                  .= (g . v) by RLVECT_1: 4

                  .= (l . v) by A9, 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 VECTSP_6: 22

                  .= (( 0. GF) + (g . v)) by A5, A18

                  .= (( 0. GF) + ( 0. GF)) by A9, A17

                  .= ( 0. GF) 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, VECTSP_6: 44;

        ( Sum f) in ( Lin A) & ( Sum g) in ( Lin B) by Th7;

        hence v in (( Lin A) + ( Lin B)) by A19, VECTSP_5: 1;

      end;

      then

       A20: ( Lin (A \/ B)) is Subspace of (( Lin A) + ( Lin B)) by VECTSP_4: 28;

      ( Lin A) is Subspace of ( Lin (A \/ B)) & ( Lin B) is Subspace of ( Lin (A \/ B)) by Th13, XBOOLE_1: 7;

      then (( Lin A) + ( Lin B)) is Subspace of ( Lin (A \/ B)) by VECTSP_5: 34;

      hence thesis by A20, VECTSP_4: 25;

    end;

    theorem :: VECTSP_7:16

    for GF be Ring, V be LeftMod of GF, A,B be Subset of V holds ( Lin (A /\ B)) is Subspace of (( Lin A) /\ ( Lin B))

    proof

      let GF be Ring, V be LeftMod of GF, A,B be Subset of V;

      ( Lin (A /\ B)) is Subspace of ( Lin A) & ( Lin (A /\ B)) is Subspace of ( Lin B) by Th13, XBOOLE_1: 17;

      hence thesis by VECTSP_5: 19;

    end;

    definition

      let GF be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be LeftMod of GF;

      let A be Subset of V;

      :: VECTSP_7:def3

      attr A is base means

      : Def3: A is linearly-independent & ( Lin A) = the ModuleStr of V;

    end

    

     Lm1: for R be Ring, a be Scalar of R holds ( - a) = ( 0. R) implies a = ( 0. R)

    proof

      let R be Ring, a be Scalar of R;

      assume ( - a) = ( 0. R);

      then ( - ( - a)) = ( 0. R) by RLVECT_1: 12;

      hence thesis by RLVECT_1: 17;

    end;

    

     Lm2: for R be non degenerated almost_left_invertible Ring holds for V be LeftMod of R holds for a be Scalar of V, v be Vector of V holds a <> ( 0. R) implies ((a " ) * (a * v)) = (( 1. R) * v) & (((a " ) * a) * v) = (( 1. R) * v)

    proof

      let R be non degenerated almost_left_invertible Ring;

      let V be LeftMod of R, a be Scalar of V, v be Vector of V;

      assume

       A1: a <> ( 0. R);

      

      hence ((a " ) * (a * v)) = v by VECTSP_2: 31

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

      thus thesis by A1, VECTSP_2: 9;

    end;

    theorem :: VECTSP_7:17

    

     Th17: for R be non degenerated almost_left_invertible Ring holds for V be LeftMod of R holds for A be Subset of V st A is linearly-independent holds ex B be Subset of V st A c= B & B is base

    proof

      let R be non degenerated almost_left_invertible Ring;

      let V be LeftMod of R;

      let A be Subset of V;

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

      consider Q be set such that

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

       A2:

      now

        let Z;

        assume that

         A3: Z <> {} and

         A4: Z c= Q and

         A5: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A6: x in X and

           A7: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A1, A4, A7;

          hence thesis by A6;

        end;

        then

        reconsider W as Subset of V;

        

         A8: W is linearly-independent

        proof

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

          let l be Linear_Combination of W;

          assume that

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

           A10: ( Carrier l) <> {} ;

          consider f be Function such that

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

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

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

          set F = the Choice_Function of M;

          set S = ( rng F);

           A13:

          now

            assume {} in M;

            then

            consider x be object such that

             A14: x in ( dom f) and

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

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

            then

            consider X such that

             A16: x in X and

             A17: X in Z by A11, A14, TARSKI:def 4;

            reconsider X as Subset of V by A1, A4, A17;

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

            hence contradiction by A11, A12, A14, A15;

          end;

          then

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

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

          then

           A19: S is finite by FINSET_1: 8;

           A20:

          now

            let X;

            assume X in S;

            then

            consider x be object such that

             A21: x in ( dom F) and

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

            consider y be object such that

             A23: y in ( dom f) & (f . y) = x by A18, A21, FUNCT_1:def 3;

            

             A24: x = { C where C be Subset of V : y in C & C in Z } by A11, A12, A23;

            reconsider x as set by TARSKI: 1;

            X in x by A13, A18, A21, A22, ORDERS_1: 89;

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

            hence X in Z;

          end;

           A25:

          now

            let X, Y;

            assume X in S & Y in S;

            then X in Z & Y in Z by A20;

            then (X,Y) are_c=-comparable by A5, ORDINAL1:def 8;

            hence X c= Y or Y c= X;

          end;

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

          then ( union S) in S by A25, A19, CARD_2: 62;

          then ( union S) in Z by A20;

          then

          consider B be Subset of V such that

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

           A27: B is linearly-independent by A1, A4;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A28: x in ( Carrier l);

            then

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

            

             A30: (f . x) in M by A11, A28, FUNCT_1:def 3;

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

            then

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

            (F . X) in S by A18, A30, FUNCT_1:def 3;

            hence thesis by A31, TARSKI:def 4;

          end;

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

          hence thesis by A9, A10, A27;

        end;

        set x = the Element of Z;

        x in Q by A3, A4;

        then

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

        x c= W by A3, ZFMISC_1: 74;

        then A c= W by A32;

        hence ( union Z) in Q by A1, A8;

      end;

      assume A is linearly-independent;

      then Q <> {} by A1;

      then

      consider X such that

       A33: X in Q and

       A34: for Z st Z in Q & Z <> X holds not X c= Z by A2, ORDERS_1: 67;

      consider B be Subset of V such that

       A35: B = X and

       A36: A c= B and

       A37: B is linearly-independent by A1, A33;

      take B;

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

      assume ( Lin B) <> the ModuleStr of V;

      then

      consider v be Vector of V such that

       A38: not (v in ( Lin B) iff v in ( (Omega). V)) by VECTSP_4: 30;

      

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

      proof

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

        assume

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

        now

          per cases ;

            suppose v in ( Carrier l);

            then (l . v) <> ( 0. R) by VECTSP_6: 2;

            then ( - (l . v)) <> ( 0. R) by Lm1;

            

            then

             A41: ((( - (l . v)) " ) * (( - (l . v)) * v)) = (( 1. R) * v) by Lm2

            .= v by VECTSP_1:def 17;

            deffunc F( Vector of V) = (l . $1);

            consider f be Function of the carrier of V, the carrier of R such that

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

             A43: for u be Vector 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 be Vector of V;

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

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

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

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

            end;

            then

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

            ( Carrier f) c= B

            proof

              let x be object;

              

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

              assume x in ( Carrier f);

              then

              consider u be Vector of V such that

               A45: u = x and

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

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

              then u in ( Carrier l) by A46;

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

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

            end;

            then

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

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

            consider g be Function of the carrier of V, the carrier of R such that

             A47: (g . v) = ( - (l . v)) and

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

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

            now

              let u be Vector of V;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (g . u) = ( 0. R) by A48;

            end;

            then

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

            ( Carrier g) c= {v}

            proof

              let x be object;

              assume x in ( Carrier g);

              then ex u be Vector of V st x = u & (g . u) <> ( 0. R);

              then x = v by A48;

              hence thesis by TARSKI:def 1;

            end;

            then

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

            (f - g) = l

            proof

              let u be Vector of V;

              now

                per cases ;

                  suppose

                   A49: v = u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by VECTSP_6: 40

                  .= (( 0. R) + ( - ( - (l . v)))) by A42, A47, A49, RLVECT_1:def 11

                  .= ((l . v) + ( 0. R)) by RLVECT_1: 17

                  .= (l . u) by A49, RLVECT_1: 4;

                end;

                  suppose

                   A50: v <> u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by VECTSP_6: 40

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

                  .= ((l . u) - ( 0. R)) by A48, A50

                  .= (l . u) by RLVECT_1: 13;

                end;

              end;

              hence thesis;

            end;

            then

             A51: ( 0. V) = (( Sum f) - ( Sum g)) by A40, VECTSP_6: 47;

            ( Sum g) = (( - (l . v)) * v) by A47, VECTSP_6: 17;

            then ( Sum f) = (( - (l . v)) * v) by A51, VECTSP_1: 19;

            then (( - (l . v)) * v) in ( Lin B) by Th7;

            hence thesis by A38, A41, STRUCT_0:def 5, VECTSP_4: 21;

          end;

            suppose

             A52: not v in ( Carrier l);

            ( Carrier l) c= B

            proof

              let x be object;

              assume

               A53: x in ( Carrier l);

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

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

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

            end;

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

            hence thesis by A37, A40;

          end;

        end;

        hence thesis;

      end;

      v in {v} by TARSKI:def 1;

      then

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

      

       A55: not v in B by A38, Th8, STRUCT_0:def 5;

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

      then A c= (B \/ {v}) by A36;

      then (B \/ {v}) in Q by A1, A39;

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

    end;

    theorem :: VECTSP_7:18

    

     Th18: ( Lin A) = V implies ex B st B c= A & B is linearly-independent & ( Lin B) = V

    proof

      assume

       A1: ( Lin A) = V;

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

      consider Q be set such that

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

       A3:

      now

        let Z;

        assume that Z <> {} and

         A4: Z c= Q and

         A5: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A6: x in X and

           A7: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A2, A4, A7;

          hence thesis by A6;

        end;

        then

        reconsider W as Subset of V;

        

         A8: W is linearly-independent

        proof

          deffunc F( object) = { C : $1 in C & C in Z };

          let l be Linear_Combination of W;

          assume that

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

           A10: ( Carrier l) <> {} ;

          consider f be Function such that

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

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

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

          set F = the Choice_Function of M;

          set S = ( rng F);

           A13:

          now

            assume {} in M;

            then

            consider x be object such that

             A14: x in ( dom f) and

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

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

            then

            consider X such that

             A16: x in X and

             A17: X in Z by A11, A14, TARSKI:def 4;

            reconsider X as Subset of V by A2, A4, A17;

            X in { C : x in C & C in Z } by A16, A17;

            hence contradiction by A11, A12, A14, A15;

          end;

          then

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

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

          then

           A19: S is finite by FINSET_1: 8;

           A20:

          now

            let X;

            assume X in S;

            then

            consider x be object such that

             A21: x in ( dom F) and

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

            consider y be object such that

             A23: y in ( dom f) & (f . y) = x by A18, A21, FUNCT_1:def 3;

            

             A24: x = { C : y in C & C in Z } by A11, A12, A23;

            reconsider x as set by TARSKI: 1;

            X in x by A13, A18, A21, A22, ORDERS_1: 89;

            then ex C st C = X & y in C & C in Z by A24;

            hence X in Z;

          end;

           A25:

          now

            let X, Y;

            assume X in S & Y in S;

            then X in Z & Y in Z by A20;

            then (X,Y) are_c=-comparable by A5, ORDINAL1:def 8;

            hence X c= Y or Y c= X;

          end;

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

          then ( union S) in S by A25, A19, CARD_2: 62;

          then ( union S) in Z by A20;

          then

          consider B such that

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

           A27: B is linearly-independent by A2, A4;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A28: x in ( Carrier l);

            then

             A29: (f . x) = { C : x in C & C in Z } by A12;

            

             A30: (f . x) in M by A11, A28, FUNCT_1:def 3;

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

            then

             A31: ex C st (F . X) = C & x in C & C in Z by A29;

            (F . X) in S by A18, A30, FUNCT_1:def 3;

            hence thesis by A31, TARSKI:def 4;

          end;

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

          hence thesis by A9, A10, A27;

        end;

        W c= A

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A32: x in X and

           A33: X in Z by TARSKI:def 4;

          ex B st B = X & B c= A & B is linearly-independent by A2, A4, A33;

          hence thesis by A32;

        end;

        hence ( union Z) in Q by A2, A8;

      end;

      ( {} the carrier of V) c= A;

      then Q <> {} by A2;

      then

      consider X such that

       A34: X in Q and

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

      consider B such that

       A36: B = X and

       A37: B c= A and

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

      take B;

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

      assume

       A39: ( Lin B) <> V;

      now

        assume

         A40: for v st v in A holds v in ( Lin B);

        now

          reconsider F = the carrier of ( Lin B) as Subset of V by VECTSP_4:def 2;

          let v;

          assume v in ( Lin A);

          then

          consider l such that

           A41: v = ( Sum l) by Th7;

          ( Carrier l) c= the carrier of ( Lin B)

          proof

            let x be object;

            assume

             A42: x in ( Carrier l);

            then

            reconsider a = x as Vector of V;

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

            then a in ( Lin B) by A40, A42;

            hence thesis by STRUCT_0:def 5;

          end;

          then

          reconsider l as Linear_Combination of F by VECTSP_6:def 4;

          ( Sum l) = v by A41;

          then v in ( Lin F) by Th7;

          hence v in ( Lin B) by Th11;

        end;

        then ( Lin A) is Subspace of ( Lin B) by VECTSP_4: 28;

        hence contradiction by A1, A39, VECTSP_4: 25;

      end;

      then

      consider v such that

       A43: v in A and

       A44: not v in ( Lin B);

      

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

      proof

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

        assume

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

        now

          per cases ;

            suppose v in ( Carrier l);

            then (l . v) <> ( 0. GF) by VECTSP_6: 2;

            then

             A47: ( - (l . v)) <> ( 0. GF) by VECTSP_2: 3;

            deffunc G( Vector of V) = ( 0. GF);

            deffunc F( Vector of V) = (l . $1);

            consider f such that

             A48: (f . v) = ( 0. GF) and

             A49: 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 GF)) by FUNCT_2: 8;

            now

              let u;

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

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

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

              hence (f . u) = ( 0. GF) by A48, A49;

            end;

            then

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

            ( Carrier f) c= B

            proof

              let x be object;

              

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

              assume x in ( Carrier f);

              then

              consider u such that

               A51: u = x and

               A52: (f . u) <> ( 0. GF);

              (f . u) = (l . u) by A48, A49, A52;

              then u in ( Carrier l) by A52;

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

              hence thesis by A48, A51, A52, TARSKI:def 1;

            end;

            then

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

            consider g such that

             A53: (g . v) = ( - (l . v)) and

             A54: for u st u <> v holds (g . u) = G(u) from FUNCT_2:sch 6;

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

            now

              let u;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (g . u) = ( 0. GF) by A54;

            end;

            then

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

            ( Carrier g) c= {v}

            proof

              let x be object;

              assume x in ( Carrier g);

              then ex u st x = u & (g . u) <> ( 0. GF);

              then x = v by A54;

              hence thesis by TARSKI:def 1;

            end;

            then

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

            

             A55: ( Sum g) = (( - (l . v)) * v) by A53, VECTSP_6: 17;

            (f - g) = l

            proof

              let u;

              now

                per cases ;

                  suppose

                   A56: v = u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by VECTSP_6: 40

                  .= (( 0. GF) + ( - ( - (l . v)))) by A48, A53, A56, RLVECT_1:def 11

                  .= ((l . v) + ( 0. GF)) by RLVECT_1: 17

                  .= (l . u) by A56, RLVECT_1: 4;

                end;

                  suppose

                   A57: v <> u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by VECTSP_6: 40

                  .= ((l . u) - (g . u)) by A49, A57

                  .= ((l . u) - ( 0. GF)) by A54, A57

                  .= (l . u) by RLVECT_1: 13;

                end;

              end;

              hence thesis;

            end;

            then ( 0. V) = (( Sum f) - ( Sum g)) by A46, VECTSP_6: 47;

            

            then ( Sum f) = (( 0. V) + ( Sum g)) by VECTSP_2: 2

            .= (( - (l . v)) * v) by A55, RLVECT_1: 4;

            then

             A58: (( - (l . v)) * v) in ( Lin B) by Th7;

            ((( - (l . v)) " ) * (( - (l . v)) * v)) = (((( - (l . v)) " ) * ( - (l . v))) * v) by VECTSP_1:def 16

            .= (( 1_ GF) * v) by A47, VECTSP_1:def 10

            .= v by VECTSP_1:def 17;

            hence thesis by A44, A58, VECTSP_4: 21;

          end;

            suppose

             A59: not v in ( Carrier l);

            ( Carrier l) c= B

            proof

              let x be object;

              assume

               A60: x in ( Carrier l);

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

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

              hence thesis by A59, A60, TARSKI:def 1;

            end;

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

            hence thesis by A38, A46;

          end;

        end;

        hence thesis;

      end;

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

      then (B \/ {v}) c= A by A37, XBOOLE_1: 8;

      then

       A61: (B \/ {v}) in Q by A2, A45;

      v in {v} by TARSKI:def 1;

      then

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

       not v in B by A44, Th8;

      hence contradiction by A35, A36, A62, A61, XBOOLE_1: 7;

    end;

    

     Lem0A: for GF be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of GF holds ( {} the carrier of V) is linearly-independent

    proof

      let GF be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of GF;

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

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

      hence thesis;

    end;

    registration

      let GF be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of GF;

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

      coherence by Lem0A;

    end

    registration

      let GF be non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be LeftMod of GF;

      cluster base for Subset of V;

      existence

      proof

        consider B be Subset of V such that

         A1: ( {} the carrier of V) c= B & B is base by Th17;

        take B;

        thus thesis by A1;

      end;

    end

    definition

      let GF be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let IT be LeftMod of GF;

      :: VECTSP_7:def4

      attr IT is free means ex B be Subset of IT st B is base;

    end

    

     Lem1A: for GF be almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of GF holds ( (0). V) is free

    proof

      let GF be almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of GF;

      set W = ( (0). V);

      reconsider B9 = ( {} the carrier of V) as Subset of W by SUBSET_1: 1;

      reconsider V9 = V as Subspace of V by VECTSP_4: 24;

      

       A1: B9 = ( {} the carrier of W);

      then

       A2: B9 is linearly-independent;

      ( (0). V9) = ( (0). W) by VECTSP_4: 37;

      then ( Lin B9) = W by A1, Th9;

      then B9 is base by A2;

      hence thesis;

    end;

    registration

      let GF be almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of GF;

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

      coherence by Lem1A;

    end

    registration

      let GF be non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      cluster strict free for LeftMod of GF;

      existence

      proof

        set V = the LeftMod of GF;

        take ( (0). V);

        thus thesis;

      end;

    end

    definition

      let GF be non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be LeftMod of GF;

      mode Basis of V is base Subset of V;

    end

    theorem :: VECTSP_7:19

    for V be LeftMod of GF, A be Subset of V st A is linearly-independent holds ex I be Basis of V st A c= I

    proof

      let V be LeftMod of GF, A be Subset of V;

      assume A is linearly-independent;

      then

      consider B be Subset of V such that

       A1: A c= B and

       A2: B is base by Th17;

      reconsider B as Basis of V by A2;

      take B;

      thus thesis by A1;

    end;

    theorem :: VECTSP_7:20

    for V be LeftMod of GF, A be Subset of V st ( Lin A) = V holds ex I be Basis of V st I c= A

    proof

      let V be LeftMod of GF, A be Subset of V;

      assume ( Lin A) = V;

      then

      consider B be Subset of V such that

       A1: B c= A and

       A2: B is linearly-independent & ( Lin B) = V by Th18;

      reconsider B as Basis of V by A2, Def3;

      take B;

      thus thesis by A1;

    end;

    theorem :: VECTSP_7:21

    for R be Ring, V be LeftMod of R, L be Linear_Combination of V, C be finite Subset of V st ( Carrier L) c= C holds ex F be FinSequence of V st F is one-to-one & ( rng F) = C & ( Sum L) = ( Sum (L (#) F)) by TH2;

    theorem :: VECTSP_7:22

    for R be Ring, V be LeftMod of R, L be Linear_Combination of V, a be Scalar of V holds ( Sum (a * L)) = (a * ( Sum L)) by TH3;

    reserve x for set,

R for Ring,

V for LeftMod of R,

v,v1,v2 for Vector of V,

A,B for Subset of V;

    theorem :: VECTSP_7:23

    for R be non degenerated Ring, V be LeftMod of R, v1,v2 be Vector of V holds {v1, v2} is linearly-independent implies v1 <> ( 0. V) & v2 <> ( 0. V)

    proof

      let R be non degenerated Ring, V be LeftMod of R, v1,v2 be Vector of V;

      

       A1: v1 in {v1, v2} & v2 in {v1, v2} by TARSKI:def 2;

      assume {v1, v2} is linearly-independent;

      hence thesis by A1, Th2;

    end;

    theorem :: VECTSP_7:24

    for R be domRing, V be LeftMod of R, L be Linear_Combination of V, a be Scalar of R holds a <> ( 0. R) implies ( Carrier (a * L)) = ( Carrier L)

    proof

      let R be domRing, V be LeftMod of R, L be Linear_Combination of V, a be Scalar of R;

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

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

      assume

       A1: a <> ( 0. R);

      T = S

      proof

        thus T c= S

        proof

          let x be object;

          assume x in T;

          then

          consider u be Vector of V such that

           A2: x = u and

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

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

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

          hence thesis by A2;

        end;

        let x be object;

        assume x in S;

        then

        consider v be Vector of V such that

         A4: x = v and

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

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

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

        hence thesis by A4;

      end;

      hence thesis;

    end;

    reserve R for domRing,

V for LeftMod of R,

A,B for Subset of V,

l for Linear_Combination of A,

f,g for Function of the carrier of V, the carrier of R;

    theorem :: VECTSP_7:25

    

     Th12: for W be strict Subspace of V st R is non degenerated & A = the carrier of W holds ( Lin A) = W

    proof

      let W be strict Subspace of V;

      assume that R is non degenerated and

       A2: A = the carrier of W;

      

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

      now

        let v be Vector of 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 Th7;

          A is linearly-closed by A2, VECTSP_4: 33;

          then v in the carrier of W by A1, A2, A3, VECTSP_6: 14;

          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, Th8;

      end;

      hence thesis by VECTSP_4: 30;

    end;

    theorem :: VECTSP_7:26

    for V be strict LeftMod of R, A be Subset of V st R is non degenerated & A = the carrier of V holds ( Lin A) = V

    proof

      let V be strict LeftMod of R, A be Subset of V such that R is non degenerated;

      assume

       A2: A = the carrier of V;

      ( (Omega). V) = V;

      hence thesis by A2, Th12;

    end;

    theorem :: VECTSP_7:27

    for V be strict LeftMod of R, A,B be Subset of V st ( Lin A) = V & A c= B holds ( Lin B) = V

    proof

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

      assume ( Lin A) = V & A c= B;

      then V is Subspace of ( Lin B) by Th13;

      hence thesis by VECTSP_4: 25;

    end;

    theorem :: VECTSP_7:28

    for R be Ring, V be LeftMod of R, v1,v2 be Vector of V holds R is non degenerated & {v1, v2} is linearly-independent implies v1 <> ( 0. V) & v2 <> ( 0. V)

    proof

      let R be Ring, V be LeftMod of R, v1,v2 be Vector of V;

      

       A1: v1 in {v1, v2} & v2 in {v1, v2} by TARSKI:def 2;

      assume R is non degenerated & {v1, v2} is linearly-independent;

      hence thesis by A1, Th2;

    end;