rlvect_5.miz



    begin

    reserve V for RealLinearSpace,

W for Subspace of V,

x,y,y1,y2 for set,

i,n for Element of NAT ,

v for VECTOR of V,

KL1,KL2 for Linear_Combination of V,

X for Subset of V;

    theorem :: RLVECT_5:1

    

     Th1: X is linearly-independent & ( Carrier KL1) c= X & ( Carrier KL2) c= X & ( Sum KL1) = ( Sum KL2) implies KL1 = KL2

    proof

      assume

       A1: X is linearly-independent;

      assume

       A2: ( Carrier KL1) c= X;

      assume ( Carrier KL2) c= X;

      then

       A3: (( Carrier KL1) \/ ( Carrier KL2)) c= X by A2, XBOOLE_1: 8;

      assume ( Sum KL1) = ( Sum KL2);

      

      then (( Sum KL1) - ( Sum KL2)) = (( Sum KL1) + ( - ( Sum KL1))) by RLVECT_1:def 11

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

      then

       A4: (KL1 - KL2) is Linear_Combination of ( Carrier (KL1 - KL2)) & ( Sum (KL1 - KL2)) = ( 0. V) by RLVECT_2:def 6, RLVECT_3: 4;

      ( Carrier (KL1 - KL2)) c= (( Carrier KL1) \/ ( Carrier KL2)) by RLVECT_2: 55;

      then

       A5: ( Carrier (KL1 - KL2)) is linearly-independent by A1, A3, RLVECT_3: 5, XBOOLE_1: 1;

      now

        let v be VECTOR of V;

         not v in ( Carrier (KL1 - KL2)) by A5, A4, RLVECT_3:def 1;

        then ((KL1 - KL2) . v) = 0 by RLVECT_2: 19;

        then ((KL1 . v) - (KL2 . v)) = 0 by RLVECT_2: 54;

        hence (KL1 . v) = (KL2 . v);

      end;

      hence thesis by RLVECT_2:def 9;

    end;

    theorem :: RLVECT_5:2

    

     Th2: for V be RealLinearSpace, 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 RealLinearSpace, 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 linearly-independent & ( Lin B) = the RLSStruct of V by RLVECT_3: 24;

      reconsider B as Basis of V by A2, RLVECT_3:def 3;

      take B;

      thus thesis by A1;

    end;

    theorem :: RLVECT_5:3

    

     Th3: for L be Linear_Combination of V, x be VECTOR of V holds x in ( Carrier L) iff ex v st x = v & (L . v) <> 0

    proof

      let L be Linear_Combination of V, x be VECTOR of V;

      hereby

        assume x in ( Carrier L);

        then x in { w where w be VECTOR of V : (L . w) <> 0 } by RLVECT_2:def 4;

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

      end;

      given v such that

       A1: x = v & (L . v) <> 0 ;

      x in { w where w be VECTOR of V : (L . w) <> 0 } by A1;

      hence thesis by RLVECT_2:def 4;

    end;

    

     Lm1: for X,x be set st x in X holds ((X \ {x}) \/ {x}) = X

    proof

      let X,x be set;

      assume x in X;

      then

       A1: {x} is Subset of X by SUBSET_1: 41;

      ( {x} \/ (X \ {x})) = ( {x} \/ X) by XBOOLE_1: 39

      .= X by A1, XBOOLE_1: 12;

      hence thesis;

    end;

    theorem :: RLVECT_5:4

    

     Th4: for L be Linear_Combination of V holds for F,G be FinSequence of the carrier of V holds for P be Permutation of ( dom F) st G = (F * P) holds ( Sum (L (#) F)) = ( Sum (L (#) G))

    proof

      let L be Linear_Combination of V;

      let F,G be FinSequence of the carrier of V;

      set p = (L (#) F), q = (L (#) G);

      let P be Permutation of ( dom F) such that

       A1: G = (F * P);

      

       A2: ( len G) = ( len F) by A1, FINSEQ_2: 44;

      ( len F) = ( len (L (#) F)) by RLVECT_2:def 7;

      then

       A3: ( dom F) = ( dom (L (#) F)) by FINSEQ_3: 29;

      then

      reconsider r = ((L (#) F) * P) as FinSequence of the carrier of V by FINSEQ_2: 47;

      ( len r) = ( len (L (#) F)) by A3, FINSEQ_2: 44;

      then

       A4: ( dom r) = ( dom (L (#) F)) by FINSEQ_3: 29;

      

       A5: ( len p) = ( len F) by RLVECT_2:def 7;

      then

       A6: ( dom F) = ( dom p) by FINSEQ_3: 29;

      ( len q) = ( len G) by RLVECT_2:def 7;

      then

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

      

       A8: ( dom F) = ( dom G) by A2, FINSEQ_3: 29;

       A9:

      now

        let k be Nat;

        assume

         A10: k in ( dom q);

        set l = (P . k);

        ( dom P) = ( dom F) & ( rng P) = ( dom F) by FUNCT_2: 52, FUNCT_2:def 3;

        then

         A11: l in ( dom F) by A7, A6, A10, FUNCT_1:def 3;

        then

        reconsider l as Element of NAT ;

        (G /. k) = (G . k) by A7, A8, A6, A10, PARTFUN1:def 6

        .= (F . (P . k)) by A1, A7, A8, A6, A10, FUNCT_1: 12

        .= (F /. l) by A11, PARTFUN1:def 6;

        

        then (q . k) = ((L . (F /. l)) * (F /. l)) by A10, RLVECT_2:def 7

        .= ((L (#) F) . (P . k)) by A6, A11, RLVECT_2:def 7

        .= (r . k) by A7, A4, A10, FUNCT_1: 12;

        hence (q . k) = (r . k);

      end;

      

      thus ( Sum p) = ( Sum r) by A3, RLVECT_2: 7

      .= ( Sum q) by A7, A4, A9, FINSEQ_1: 13;

    end;

    theorem :: RLVECT_5:5

    

     Th5: for L be Linear_Combination of V holds for F be FinSequence of the carrier of V st ( Carrier L) misses ( rng F) holds ( Sum (L (#) F)) = ( 0. V)

    proof

      let L be Linear_Combination of V;

      defpred P[ FinSequence] means for G be FinSequence of the carrier of V st G = $1 holds ( Carrier L) misses ( rng G) implies ( Sum (L (#) G)) = ( 0. V);

      

       A1: for p be FinSequence, x be object st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence, x be object such that

         A2: P[p];

        let G be FinSequence of the carrier of V;

        assume

         A3: G = (p ^ <*x*>);

        then

        reconsider p, x9 = <*x*> as FinSequence of the carrier of V by FINSEQ_1: 36;

        x in {x} by TARSKI:def 1;

        then

         A4: x in ( rng x9) by FINSEQ_1: 38;

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

        then

        reconsider x as VECTOR of V by A4;

        assume ( Carrier L) misses ( rng G);

        

        then

         A5: {} = (( Carrier L) /\ ( rng G)) by XBOOLE_0:def 7

        .= (( Carrier L) /\ (( rng p) \/ ( rng <*x*>))) by A3, FINSEQ_1: 31

        .= (( Carrier L) /\ (( rng p) \/ {x})) by FINSEQ_1: 38

        .= ((( Carrier L) /\ ( rng p)) \/ (( Carrier L) /\ {x})) by XBOOLE_1: 23;

        then (( Carrier L) /\ ( rng p)) = {} ;

        then ( Carrier L) misses ( rng p) by XBOOLE_0:def 7;

        then

         A6: ( Sum (L (#) p)) = ( 0. V) by A2;

        

         A7: (( Carrier L) /\ {x}) = {} by A5;

        now

          

           A8: x in {x} by TARSKI:def 1;

          assume x in ( Carrier L);

          hence contradiction by A7, A8, XBOOLE_0:def 4;

        end;

        then

         A9: (L . x) = 0 by RLVECT_2: 19;

        ( Sum (L (#) G)) = ( Sum ((L (#) p) ^ (L (#) x9))) by A3, RLVECT_3: 34

        .= (( Sum (L (#) p)) + ( Sum (L (#) x9))) by RLVECT_1: 41

        .= (( 0. V) + ( Sum <*((L . x) * x)*>)) by A6, RLVECT_2: 26

        .= ( Sum <*((L . x) * x)*>) by RLVECT_1: 4

        .= ( 0 * x) by A9, RLVECT_1: 44

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

        hence thesis;

      end;

      

       A10: P[ {} ]

      proof

        let G be FinSequence of the carrier of V;

        assume G = {} ;

        then

         A11: (L (#) G) = ( <*> the carrier of V) by RLVECT_2: 25;

        assume ( Carrier L) misses ( rng G);

        thus thesis by A11, RLVECT_1: 43;

      end;

      

       A12: for p be FinSequence holds P[p] from FINSEQ_1:sch 3( A10, A1);

      let F be FinSequence of the carrier of V;

      assume ( Carrier L) misses ( rng F);

      hence thesis by A12;

    end;

    theorem :: RLVECT_5:6

    

     Th6: for F be FinSequence of the carrier of V st F is one-to-one holds for L be Linear_Combination of V st ( Carrier L) c= ( rng F) holds ( Sum (L (#) F)) = ( Sum L)

    proof

      let F be FinSequence of the carrier of V such that

       A1: F is one-to-one;

      ( rng F) c= ( rng F);

      then

      reconsider X = ( rng F) as Subset of ( rng F);

      let L be Linear_Combination of V such that

       A2: ( Carrier L) c= ( rng F);

      consider G be FinSequence of the carrier of V such that

       A3: G is one-to-one and

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

       A5: ( Sum L) = ( Sum (L (#) G)) by RLVECT_2:def 8;

      reconsider A = ( rng G) as Subset of ( rng F) by A2, A4;

      set F1 = (F - (A ` ));

      (X \ (A ` )) = (X /\ ((A ` ) ` )) by SUBSET_1: 13

      .= A by XBOOLE_1: 28;

      then

       A6: ( rng F1) = ( rng G) by FINSEQ_3: 65;

      F1 is one-to-one by A1, FINSEQ_3: 87;

      then (F1,G) are_fiberwise_equipotent by A3, A6, RFINSEQ: 26;

      then

       A7: ex Q be Permutation of ( dom G) st F1 = (G * Q) by RFINSEQ: 4;

      reconsider F1, F2 = (F - A) as FinSequence of the carrier of V by FINSEQ_3: 86;

      

       A8: (( rng F) \ ( rng G)) misses ( rng G) by XBOOLE_1: 79;

      (( rng F2) /\ ( rng G)) = ((( rng F) \ ( rng G)) /\ ( rng G)) by FINSEQ_3: 65

      .= {} by A8, XBOOLE_0:def 7;

      then

       A9: ( Carrier L) misses ( rng F2) by A4, XBOOLE_0:def 7;

      ex P be Permutation of ( dom F) st ((F - (A ` )) ^ (F - A)) = (F * P) by FINSEQ_3: 115;

      

      then ( Sum (L (#) F)) = ( Sum (L (#) (F1 ^ F2))) by Th4

      .= ( Sum ((L (#) F1) ^ (L (#) F2))) by RLVECT_3: 34

      .= (( Sum (L (#) F1)) + ( Sum (L (#) F2))) by RLVECT_1: 41

      .= (( Sum (L (#) F1)) + ( 0. V)) by A9, Th5

      .= (( Sum (L (#) G)) + ( 0. V)) by A7, Th4

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

      hence thesis;

    end;

    theorem :: RLVECT_5:7

    

     Th7: for L be Linear_Combination of V holds for F be FinSequence of the carrier of V holds ex K be Linear_Combination of V st ( Carrier K) = (( rng F) /\ ( Carrier L)) & (L (#) F) = (K (#) F)

    proof

      let L be Linear_Combination of V, F be FinSequence of the carrier of V;

      defpred P[ object, object] means $1 is VECTOR of V implies ($1 in ( rng F) & $2 = (L . $1)) or ( not $1 in ( rng F) & $2 = 0 );

      reconsider R = ( rng F) as finite Subset of V by FINSEQ_1:def 4;

      

       A1: for x be object st x in the carrier of V holds ex y be object st y in REAL & P[x, y]

      proof

        

         A2: 0 in REAL by XREAL_0:def 1;

        let x be object;

        assume x in the carrier of V;

        then

        reconsider x9 = x as VECTOR of V;

        per cases ;

          suppose x in ( rng F);

          then P[x, (L . x9)];

          hence thesis by A2;

        end;

          suppose not x in ( rng F);

          hence thesis by A2;

        end;

      end;

      ex K be Function of the carrier of V, REAL st for x be object st x in the carrier of V holds P[x, (K . x)] from FUNCT_2:sch 1( A1);

      then

      consider K be Function of the carrier of V, REAL such that

       A3: for x be object st x in the carrier of V holds P[x, (K . x)];

       A4:

      now

        let v be VECTOR of V;

        assume

         A5: not v in (R /\ ( Carrier L));

        per cases by A5, XBOOLE_0:def 4;

          suppose not v in R;

          hence (K . v) = 0 by A3;

        end;

          suppose not v in ( Carrier L);

          then (L . v) = 0 by RLVECT_2: 19;

          hence (K . v) = 0 by A3;

        end;

      end;

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

      reconsider K as Linear_Combination of V by A4, RLVECT_2:def 3;

      now

        let v be object;

        assume

         A6: v in (( rng F) /\ ( Carrier L));

        then

        reconsider v9 = v as VECTOR of V;

        v in ( Carrier L) by A6, XBOOLE_0:def 4;

        then

         A7: (L . v9) <> 0 by RLVECT_2: 19;

        v in R by A6, XBOOLE_0:def 4;

        then (K . v9) = (L . v9) by A3;

        then v in { w where w be VECTOR of V : (K . w) <> 0 } by A7;

        hence v in ( Carrier K) by RLVECT_2:def 4;

      end;

      then

       A8: (( rng F) /\ ( Carrier L)) c= ( Carrier K);

      take K;

      

       A9: (L (#) F) = (K (#) F)

      proof

        set p = (L (#) F), q = (K (#) F);

        

         A10: ( len p) = ( len F) by RLVECT_2:def 7;

        ( len q) = ( len F) by RLVECT_2:def 7;

        then

         A11: ( dom p) = ( dom q) by A10, FINSEQ_3: 29;

        

         A12: ( dom p) = ( dom F) by A10, FINSEQ_3: 29;

        now

          let k be Nat;

          set u = (F /. k);

          

           A13: P[u, (K . u)] by A3;

          assume

           A14: k in ( dom p);

          then (F /. k) = (F . k) & (p . k) = ((L . u) * u) by A12, PARTFUN1:def 6, RLVECT_2:def 7;

          hence (p . k) = (q . k) by A11, A12, A14, A13, FUNCT_1:def 3, RLVECT_2:def 7;

        end;

        hence thesis by A11, FINSEQ_1: 13;

      end;

      now

        let v be object;

        assume v in ( Carrier K);

        then v in { v9 where v9 be VECTOR of V : (K . v9) <> 0 } by RLVECT_2:def 4;

        then ex v9 be VECTOR of V st v9 = v & (K . v9) <> 0 ;

        hence v in (( rng F) /\ ( Carrier L)) by A4;

      end;

      then ( Carrier K) c= (( rng F) /\ ( Carrier L));

      hence thesis by A8, A9, XBOOLE_0:def 10;

    end;

    theorem :: RLVECT_5:8

    

     Th8: for L be Linear_Combination of V holds for A be Subset of V holds for F be FinSequence of the carrier of V st ( rng F) c= the carrier of ( Lin A) holds ex K be Linear_Combination of A st ( Sum (L (#) F)) = ( Sum K)

    proof

      let L be Linear_Combination of V;

      let A be Subset of V;

      defpred P[ Nat] means for F be FinSequence of the carrier of V st ( rng F) c= the carrier of ( Lin A) & ( len F) = $1 holds ex K be Linear_Combination of A st ( Sum (L (#) F)) = ( Sum K);

      

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

      proof

        let n be Nat;

        assume

         A2: P[n];

        let F be FinSequence of the carrier of V such that

         A3: ( rng F) c= the carrier of ( Lin A) and

         A4: ( len F) = (n + 1);

        consider G be FinSequence, x be object such that

         A5: F = (G ^ <*x*>) by A4, FINSEQ_2: 18;

        reconsider G, x9 = <*x*> as FinSequence of the carrier of V by A5, FINSEQ_1: 36;

        

         A6: ( rng (G ^ <*x*>)) = (( rng G) \/ ( rng <*x*>)) by FINSEQ_1: 31

        .= (( rng G) \/ {x}) by FINSEQ_1: 38;

        then

         A7: ( rng G) c= ( rng F) by A5, XBOOLE_1: 7;

         {x} c= ( rng F) by A5, A6, XBOOLE_1: 7;

        then {x} c= the carrier of ( Lin A) by A3;

        then x in {x} implies x in the carrier of ( Lin A);

        then

         A8: x in ( Lin A) by STRUCT_0:def 5, TARSKI:def 1;

        then

        consider LA1 be Linear_Combination of A such that

         A9: x = ( Sum LA1) by RLVECT_3: 14;

        x in V by A8, RLSUB_1: 9;

        then

        reconsider x as VECTOR of V by STRUCT_0:def 5;

        ( len (G ^ <*x*>)) = (( len G) + ( len <*x*>)) by FINSEQ_1: 22

        .= (( len G) + 1) by FINSEQ_1: 39;

        then

        consider LA2 be Linear_Combination of A such that

         A10: ( Sum (L (#) G)) = ( Sum LA2) by A2, A3, A4, A5, A7, XBOOLE_1: 1;

        ((L . x) * LA1) is Linear_Combination of A by RLVECT_2: 44;

        then

         A11: (LA2 + ((L . x) * LA1)) is Linear_Combination of A by RLVECT_2: 38;

        ( Sum (L (#) F)) = ( Sum ((L (#) G) ^ (L (#) x9))) by A5, RLVECT_3: 34

        .= (( Sum LA2) + ( Sum (L (#) x9))) by A10, RLVECT_1: 41

        .= (( Sum LA2) + ( Sum <*((L . x) * x)*>)) by RLVECT_2: 26

        .= (( Sum LA2) + ((L . x) * ( Sum LA1))) by A9, RLVECT_1: 44

        .= (( Sum LA2) + ( Sum ((L . x) * LA1))) by RLVECT_3: 2

        .= ( Sum (LA2 + ((L . x) * LA1))) by RLVECT_3: 1;

        hence thesis by A11;

      end;

      let F be FinSequence of the carrier of V;

      assume

       A12: ( rng F) c= the carrier of ( Lin A);

      

       A13: ( len F) is Element of NAT ;

      

       A14: P[ 0 ]

      proof

        let F be FinSequence of the carrier of V;

        assume that ( rng F) c= the carrier of ( Lin A) and

         A15: ( len F) = 0 ;

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

        then (L (#) F) = ( <*> the carrier of V) by RLVECT_2: 25;

        

        then

         A16: ( Sum (L (#) F)) = ( 0. V) by RLVECT_1: 43

        .= ( Sum ( ZeroLC V)) by RLVECT_2: 30;

        ( ZeroLC V) is Linear_Combination of A by RLVECT_2: 22;

        hence thesis by A16;

      end;

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

      hence thesis by A12, A13;

    end;

    theorem :: RLVECT_5:9

    

     Th9: for L be Linear_Combination of V holds for A be Subset of V st ( Carrier L) c= the carrier of ( Lin A) holds ex K be Linear_Combination of A st ( Sum L) = ( Sum K)

    proof

      let L be Linear_Combination of V, A be Subset of V;

      consider F be FinSequence of the carrier of V such that F is one-to-one and

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

       A2: ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

      assume ( Carrier L) c= the carrier of ( Lin A);

      then

      consider K be Linear_Combination of A such that

       A3: ( Sum (L (#) F)) = ( Sum K) by A1, Th8;

      take K;

      thus thesis by A2, A3;

    end;

    theorem :: RLVECT_5:10

    

     Th10: for L be Linear_Combination of V st ( Carrier L) c= the carrier of W holds for K be Linear_Combination of W st K = (L | the carrier of W) holds ( Carrier L) = ( Carrier K) & ( Sum L) = ( Sum K)

    proof

      let L be Linear_Combination of V such that

       A1: ( Carrier L) c= the carrier of W;

      let K be Linear_Combination of W such that

       A2: K = (L | the carrier of W);

      

       A3: ( dom K) = the carrier of W by FUNCT_2:def 1;

      now

        let x be object;

        assume x in ( Carrier K);

        then

        consider w be VECTOR of W such that

         A4: x = w and

         A5: (K . w) <> 0 by Th3;

        

         A6: w is VECTOR of V by RLSUB_1: 10;

        (L . w) <> 0 by A2, A3, A5, FUNCT_1: 47;

        hence x in ( Carrier L) by A4, A6, Th3;

      end;

      then

       A7: ( Carrier K) c= ( Carrier L);

      consider G be FinSequence of the carrier of W such that

       A8: G is one-to-one & ( rng G) = ( Carrier K) and

       A9: ( Sum K) = ( Sum (K (#) G)) by RLVECT_2:def 8;

      consider F be FinSequence of the carrier of V such that

       A10: F is one-to-one and

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

       A12: ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

      now

        let x be object;

        assume

         A13: x in ( Carrier L);

        then

        consider v be VECTOR of V such that

         A14: x = v and

         A15: (L . v) <> 0 by Th3;

        (K . v) <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1: 47;

        hence x in ( Carrier K) by A1, A13, A14, Th3;

      end;

      then

       A16: ( Carrier L) c= ( Carrier K);

      then

       A17: ( Carrier K) = ( Carrier L) by A7, XBOOLE_0:def 10;

      then (F,G) are_fiberwise_equipotent by A10, A11, A8, RFINSEQ: 26;

      then

      consider P be Permutation of ( dom G) such that

       A18: F = (G * P) by RFINSEQ: 4;

      ( len (K (#) G)) = ( len G) by RLVECT_2:def 7;

      then

       A19: ( dom (K (#) G)) = ( dom G) by FINSEQ_3: 29;

      then

      reconsider q = ((K (#) G) * P) as FinSequence of the carrier of W by FINSEQ_2: 47;

      

       A20: ( len q) = ( len (K (#) G)) by A19, FINSEQ_2: 44;

      then ( len q) = ( len G) by RLVECT_2:def 7;

      then

       A21: ( dom q) = ( dom G) by FINSEQ_3: 29;

      set p = (L (#) F);

      

       A22: the carrier of W c= the carrier of V by RLSUB_1:def 2;

      ( rng q) c= the carrier of W by FINSEQ_1:def 4;

      then ( rng q) c= the carrier of V by A22;

      then

      reconsider q9 = q as FinSequence of the carrier of V by FINSEQ_1:def 4;

      consider f be sequence of the carrier of W such that

       A23: ( Sum q) = (f . ( len q)) and

       A24: (f . 0 ) = ( 0. W) and

       A25: for i be Nat, w be VECTOR of W st i < ( len q) & w = (q . (i + 1)) holds (f . (i + 1)) = ((f . i) + w) by RLVECT_1:def 12;

      ( dom f) = NAT & ( rng f) c= the carrier of W by FUNCT_2:def 1, RELAT_1:def 19;

      then

      reconsider f9 = f as sequence of the carrier of V by A22, FUNCT_2: 2, XBOOLE_1: 1;

      

       A26: for i be Nat, v be VECTOR of V st i < ( len q9) & v = (q9 . (i + 1)) holds (f9 . (i + 1)) = ((f9 . i) + v)

      proof

        let i be Nat, v be VECTOR of V;

        assume that

         A27: i < ( len q9) and

         A28: v = (q9 . (i + 1));

        1 <= (i + 1) & (i + 1) <= ( len q) by A27, NAT_1: 11, NAT_1: 13;

        then (i + 1) in ( dom q) by FINSEQ_3: 25;

        then

        reconsider v9 = v as VECTOR of W by A28, FINSEQ_2: 11;

        (f . (i + 1)) = ((f . i) + v9) by A25, A27, A28;

        hence thesis by RLSUB_1: 13;

      end;

      

       A29: ( len G) = ( len F) by A18, FINSEQ_2: 44;

      then

       A30: ( dom G) = ( dom F) by FINSEQ_3: 29;

      ( len G) = ( len (L (#) F)) by A29, RLVECT_2:def 7;

      then

       A31: ( dom p) = ( dom G) by FINSEQ_3: 29;

      

       A32: ( dom q) = ( dom (K (#) G)) by A20, FINSEQ_3: 29;

      now

        let i be Nat;

        set v = (F /. i);

        set j = (P . i);

        assume

         A33: i in ( dom p);

        then

         A34: (F /. i) = (F . i) by A31, A30, PARTFUN1:def 6;

        then v in ( rng F) by A31, A30, A33, FUNCT_1:def 3;

        then

        reconsider w = v as VECTOR of W by A17, A11;

        ( dom P) = ( dom G) & ( rng P) = ( dom G) by FUNCT_2: 52, FUNCT_2:def 3;

        then

         A35: j in ( dom G) by A31, A33, FUNCT_1:def 3;

        then

        reconsider j as Element of NAT ;

        

         A36: (G /. j) = (G . (P . i)) by A35, PARTFUN1:def 6

        .= v by A18, A31, A30, A33, A34, FUNCT_1: 12;

        (q . i) = ((K (#) G) . j) by A31, A21, A33, FUNCT_1: 12

        .= ((K . w) * w) by A32, A21, A35, A36, RLVECT_2:def 7

        .= ((L . v) * w) by A2, A3, FUNCT_1: 47

        .= ((L . v) * v) by RLSUB_1: 14;

        hence (p . i) = (q . i) by A33, RLVECT_2:def 7;

      end;

      then

       A37: (L (#) F) = ((K (#) G) * P) by A31, A21, FINSEQ_1: 13;

      ( len G) = ( len (K (#) G)) by RLVECT_2:def 7;

      then ( dom G) = ( dom (K (#) G)) by FINSEQ_3: 29;

      then

      reconsider P as Permutation of ( dom (K (#) G));

      q = ((K (#) G) * P);

      then

       A38: ( Sum (K (#) G)) = ( Sum q) by RLVECT_2: 7;

      

       A39: (f9 . ( len q9)) is Element of V;

      (f9 . 0 ) = ( 0. V) by A24, RLSUB_1: 11;

      hence thesis by A7, A16, A12, A9, A37, A38, A23, A26, A39, RLVECT_1:def 12, XBOOLE_0:def 10;

    end;

    theorem :: RLVECT_5:11

    

     Th11: for K be Linear_Combination of W holds ex L be Linear_Combination of V st ( Carrier K) = ( Carrier L) & ( Sum K) = ( Sum L)

    proof

      let K be Linear_Combination of W;

      defpred P[ object, object] means ($1 in W & $2 = (K . $1)) or ( not $1 in W & $2 = 0 );

      reconsider K9 = K as Function of the carrier of W, REAL ;

      

       A1: the carrier of W c= the carrier of V by RLSUB_1:def 2;

      then

      reconsider C = ( Carrier K) as finite Subset of V by XBOOLE_1: 1;

      

       A2: for x be object st x in the carrier of V holds ex y be object st y in REAL & P[x, y]

      proof

        let x be object;

        assume x in the carrier of V;

        then

        reconsider x as VECTOR of V;

        

         A3: 0 in REAL by XREAL_0:def 1;

        per cases ;

          suppose

           A4: x in W;

          then

          reconsider x as VECTOR of W by STRUCT_0:def 5;

           P[x, (K . x)] by A4;

          hence thesis;

        end;

          suppose not x in W;

          hence thesis by A3;

        end;

      end;

      ex L be Function of the carrier of V, REAL st for x be object st x in the carrier of V holds P[x, (L . x)] from FUNCT_2:sch 1( A2);

      then

      consider L be Function of the carrier of V, REAL such that

       A5: for x be object st x in the carrier of V holds P[x, (L . x)];

       A6:

      now

        let v be VECTOR of V;

        assume not v in C;

        then P[v, (K . v)] & not v in C & v in the carrier of W or P[v, 0 ] by STRUCT_0:def 5;

        then P[v, (K . v)] & (K . v) = 0 or P[v, 0 ] by RLVECT_2: 19;

        hence (L . v) = 0 by A5;

      end;

      L is Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

      then

      reconsider L as Linear_Combination of V by A6, RLVECT_2:def 3;

      reconsider L9 = (L | the carrier of W) as Function of the carrier of W, REAL by A1, FUNCT_2: 32;

      take L;

      now

        let x be object;

        assume that

         A7: x in ( Carrier L) and

         A8: not x in the carrier of W;

        consider v be VECTOR of V such that

         A9: x = v and

         A10: (L . v) <> 0 by A7, Th3;

         P[v, 0 ] by A8, A9, STRUCT_0:def 5;

        hence contradiction by A5, A10;

      end;

      then

       A11: ( Carrier L) c= the carrier of W;

      now

        let x be object;

        assume

         A12: x in the carrier of W;

        then P[x, (L . x)] by A5, A1;

        hence (K9 . x) = (L9 . x) by A12, FUNCT_1: 49, STRUCT_0:def 5;

      end;

      then K9 = L9 by FUNCT_2: 12;

      hence thesis by A11, Th10;

    end;

    theorem :: RLVECT_5:12

    

     Th12: for L be Linear_Combination of V st ( Carrier L) c= the carrier of W holds ex K be Linear_Combination of W st ( Carrier K) = ( Carrier L) & ( Sum K) = ( Sum L)

    proof

      let L be Linear_Combination of V;

      assume

       A1: ( Carrier L) c= the carrier of W;

      then

      reconsider C = ( Carrier L) as finite Subset of W;

      the carrier of W c= the carrier of V by RLSUB_1:def 2;

      then

      reconsider K = (L | the carrier of W) as Function of the carrier of W, REAL by FUNCT_2: 32;

      

       A2: K is Element of ( Funcs (the carrier of W, REAL )) by FUNCT_2: 8;

      

       A3: ( dom K) = the carrier of W by FUNCT_2:def 1;

      now

        let w be VECTOR of W;

        

         A4: w is VECTOR of V by RLSUB_1: 10;

        assume not w in C;

        then (L . w) = 0 by A4, RLVECT_2: 19;

        hence (K . w) = 0 by A3, FUNCT_1: 47;

      end;

      then

      reconsider K as Linear_Combination of W by A2, RLVECT_2:def 3;

      take K;

      thus thesis by A1, Th10;

    end;

    theorem :: RLVECT_5:13

    

     Th13: for I be Basis of V, v be VECTOR of V holds v in ( Lin I)

    proof

      let I be Basis of V, v be VECTOR of V;

      v in the RLSStruct of V by STRUCT_0:def 5;

      hence thesis by RLVECT_3:def 3;

    end;

    theorem :: RLVECT_5:14

    

     Th14: for A be Subset of W st A is linearly-independent holds A is linearly-independent Subset of V

    proof

      let A be Subset of W;

      the carrier of W c= the carrier of V by RLSUB_1:def 2;

      then

      reconsider A9 = A as Subset of V by XBOOLE_1: 1;

      assume

       A1: A is linearly-independent;

      now

        assume A9 is linearly-dependent;

        then

        consider L be Linear_Combination of A9 such that

         A2: ( Sum L) = ( 0. V) and

         A3: ( Carrier L) <> {} by RLVECT_3:def 1;

        ( Carrier L) c= A by RLVECT_2:def 6;

        then

        consider LW be Linear_Combination of W such that

         A4: ( Carrier LW) = ( Carrier L) and

         A5: ( Sum LW) = ( Sum L) by Th12, XBOOLE_1: 1;

        reconsider LW as Linear_Combination of A by A4, RLVECT_2:def 6;

        ( Sum LW) = ( 0. W) by A2, A5, RLSUB_1: 11;

        hence contradiction by A1, A3, A4, RLVECT_3:def 1;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_5:15

    

     Th15: for A be Subset of V st A is linearly-independent & A c= the carrier of W holds A is linearly-independent Subset of W

    proof

      let A be Subset of V such that

       A1: A is linearly-independent and

       A2: A c= the carrier of W;

      reconsider A9 = A as Subset of W by A2;

      now

        assume A9 is linearly-dependent;

        then

        consider K be Linear_Combination of A9 such that

         A3: ( Sum K) = ( 0. W) and

         A4: ( Carrier K) <> {} by RLVECT_3:def 1;

        consider L be Linear_Combination of V such that

         A5: ( Carrier L) = ( Carrier K) and

         A6: ( Sum L) = ( Sum K) by Th11;

        reconsider L as Linear_Combination of A by A5, RLVECT_2:def 6;

        ( Sum L) = ( 0. V) by A3, A6, RLSUB_1: 11;

        hence contradiction by A1, A4, A5, RLVECT_3:def 1;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_5:16

    

     Th16: for A be Basis of W holds ex B be Basis of V st A c= B

    proof

      let A be Basis of W;

      A is linearly-independent by RLVECT_3:def 3;

      then A is linearly-independent Subset of V by Th14;

      then

      consider I be Basis of V such that

       A1: A c= I by Th2;

      take I;

      thus thesis by A1;

    end;

    theorem :: RLVECT_5:17

    

     Th17: for A be Subset of V st A is linearly-independent holds for v be VECTOR of V st v in A holds for B be Subset of V st B = (A \ {v}) holds not v in ( Lin B)

    proof

      let A be Subset of V such that

       A1: A is linearly-independent;

      let v be VECTOR of V;

      assume v in A;

      then

       A2: {v} is Subset of A by SUBSET_1: 41;

      v in {v} by TARSKI:def 1;

      then v in ( Lin {v}) by RLVECT_3: 15;

      then

      consider K be Linear_Combination of {v} such that

       A3: v = ( Sum K) by RLVECT_3: 14;

      let B be Subset of V such that

       A4: B = (A \ {v});

      B c= A by A4, XBOOLE_1: 36;

      then

       A5: (B \/ {v}) c= (A \/ A) by A2, XBOOLE_1: 13;

      assume v in ( Lin B);

      then

      consider L be Linear_Combination of B such that

       A6: v = ( Sum L) by RLVECT_3: 14;

      

       A7: ( Carrier L) c= B & ( Carrier K) c= {v} by RLVECT_2:def 6;

      then (( Carrier L) \/ ( Carrier K)) c= (B \/ {v}) by XBOOLE_1: 13;

      then ( Carrier (L - K)) c= (( Carrier L) \/ ( Carrier K)) & (( Carrier L) \/ ( Carrier K)) c= A by A5, RLVECT_2: 55;

      then ( Carrier (L - K)) c= A;

      then

       A8: (L - K) is Linear_Combination of A by RLVECT_2:def 6;

      

       A9: for x be VECTOR of V holds x in ( Carrier L) implies (K . x) = 0

      proof

        let x be VECTOR of V;

        assume x in ( Carrier L);

        then not x in ( Carrier K) by A4, A7, XBOOLE_0:def 5;

        hence thesis by RLVECT_2: 19;

      end;

       A10:

      now

        let x be set such that

         A11: x in ( Carrier L) and

         A12: not x in ( Carrier (L - K));

        reconsider x as VECTOR of V by A11;

        

         A13: (L . x) <> 0 by A11, RLVECT_2: 19;

        ((L - K) . x) = ((L . x) - (K . x)) by RLVECT_2: 54

        .= ((L . x) - 0 ) by A9, A11

        .= (L . x);

        hence contradiction by A12, A13, RLVECT_2: 19;

      end;

       {v} is linearly-independent by A1, A2, RLVECT_3: 5;

      then v <> ( 0. V) by RLVECT_3: 8;

      then ( Carrier L) is non empty by A6, RLVECT_2: 34;

      then ex w be object st w in ( Carrier L) by XBOOLE_0:def 1;

      then

       A14: ( Carrier (L - K)) is non empty by A10;

      ( 0. V) = (( Sum L) + ( - ( Sum K))) by A6, A3, RLVECT_1: 5

      .= (( Sum L) + ( Sum ( - K))) by RLVECT_3: 3

      .= ( Sum (L + ( - K))) by RLVECT_3: 1

      .= ( Sum (L - K)) by RLVECT_2:def 13;

      hence contradiction by A1, A8, A14, RLVECT_3:def 1;

    end;

    theorem :: RLVECT_5:18

    

     Th18: for I be Basis of V holds for A be non empty Subset of V st A misses I holds for B be Subset of V st B = (I \/ A) holds B is linearly-dependent

    proof

      let I be Basis of V;

      let A be non empty Subset of V such that

       A1: A misses I;

      consider v be object such that

       A2: v in A by XBOOLE_0:def 1;

      let B be Subset of V such that

       A3: B = (I \/ A);

      

       A4: A c= B by A3, XBOOLE_1: 7;

      reconsider v as VECTOR of V by A2;

      reconsider Bv = (B \ {v}) as Subset of V;

      

       A5: (I \ {v}) c= (B \ {v}) by A3, XBOOLE_1: 7, XBOOLE_1: 33;

       not v in I by A1, A2, XBOOLE_0: 3;

      then I c= Bv by A5, ZFMISC_1: 57;

      then

       A6: ( Lin I) is Subspace of ( Lin Bv) by RLVECT_3: 20;

      assume

       A7: B is linearly-independent;

      v in ( Lin I) by Th13;

      hence contradiction by A7, A2, A4, A6, Th17, RLSUB_1: 8;

    end;

    theorem :: RLVECT_5:19

    

     Th19: for A be Subset of V st A c= the carrier of W holds ( Lin A) is Subspace of W

    proof

      let A be Subset of V;

      assume

       A1: A c= the carrier of W;

      now

        let w be object;

        assume w in the carrier of ( Lin A);

        then w in ( Lin A) by STRUCT_0:def 5;

        then

        consider L be Linear_Combination of A such that

         A2: w = ( Sum L) by RLVECT_3: 14;

        ( Carrier L) c= A by RLVECT_2:def 6;

        then ex K be Linear_Combination of W st ( Carrier K) = ( Carrier L) & ( Sum L) = ( Sum K) by A1, Th12, XBOOLE_1: 1;

        hence w in the carrier of W by A2;

      end;

      then the carrier of ( Lin A) c= the carrier of W;

      hence thesis by RLSUB_1: 28;

    end;

    theorem :: RLVECT_5:20

    

     Th20: for A be Subset of V, B be Subset of W st A = B holds ( Lin A) = ( Lin B)

    proof

      let A be Subset of V, B be Subset of W;

      reconsider B9 = ( Lin B), V9 = V as RealLinearSpace;

      

       A1: B9 is Subspace of V9 by RLSUB_1: 27;

      assume

       A2: A = B;

      now

        let x be object;

        assume x in the carrier of ( Lin A);

        then x in ( Lin A) by STRUCT_0:def 5;

        then

        consider L be Linear_Combination of A such that

         A3: x = ( Sum L) by RLVECT_3: 14;

        ( Carrier L) c= A by RLVECT_2:def 6;

        then

        consider K be Linear_Combination of W such that

         A4: ( Carrier K) = ( Carrier L) and

         A5: ( Sum K) = ( Sum L) by A2, Th12, XBOOLE_1: 1;

        reconsider K as Linear_Combination of B by A2, A4, RLVECT_2:def 6;

        x = ( Sum K) by A3, A5;

        then x in ( Lin B) by RLVECT_3: 14;

        hence x in the carrier of ( Lin B) by STRUCT_0:def 5;

      end;

      then

       A6: the carrier of ( Lin A) c= the carrier of ( Lin B);

      now

        let x be object;

        assume x in the carrier of ( Lin B);

        then x in ( Lin B) by STRUCT_0:def 5;

        then

        consider K be Linear_Combination of B such that

         A7: x = ( Sum K) by RLVECT_3: 14;

        consider L be Linear_Combination of V such that

         A8: ( Carrier L) = ( Carrier K) and

         A9: ( Sum L) = ( Sum K) by Th11;

        reconsider L as Linear_Combination of A by A2, A8, RLVECT_2:def 6;

        x = ( Sum L) by A7, A9;

        then x in ( Lin A) by RLVECT_3: 14;

        hence x in the carrier of ( Lin A) by STRUCT_0:def 5;

      end;

      then the carrier of ( Lin B) c= the carrier of ( Lin A);

      then the carrier of ( Lin A) = the carrier of ( Lin B) by A6, XBOOLE_0:def 10;

      hence thesis by A1, RLSUB_1: 30;

    end;

    begin

    theorem :: RLVECT_5:21

    

     Th21: for A,B be finite Subset of V holds for v be VECTOR of V st v in ( Lin (A \/ B)) & not v in ( Lin B) holds ex w be VECTOR of V st w in A & w in ( Lin (((A \/ B) \ {w}) \/ {v}))

    proof

      let A,B be finite Subset of V;

      let v be VECTOR of V such that

       A1: v in ( Lin (A \/ B)) and

       A2: not v in ( Lin B);

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

       A3: v = ( Sum L) by A1, RLVECT_3: 14;

      

       A4: ( Carrier L) c= (A \/ B) by RLVECT_2:def 6;

      now

        assume

         A5: for w be VECTOR of V st w in A holds (L . w) = 0 ;

        now

          let x be object;

          assume that

           A6: x in ( Carrier L) and

           A7: x in A;

          ex u be VECTOR of V st x = u & (L . u) <> 0 by A6, Th3;

          hence contradiction by A5, A7;

        end;

        then ( Carrier L) misses A by XBOOLE_0: 3;

        then ( Carrier L) c= B by A4, XBOOLE_1: 73;

        then L is Linear_Combination of B by RLVECT_2:def 6;

        hence contradiction by A2, A3, RLVECT_3: 14;

      end;

      then

      consider w be VECTOR of V such that

       A8: w in A and

       A9: (L . w) <> 0 ;

      set a = (L . w);

      take w;

      consider F be FinSequence of the carrier of V such that

       A10: F is one-to-one and

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

       A12: ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

      

       A13: w in ( Carrier L) by A9, Th3;

      then

      reconsider Fw1 = (F -| w) as FinSequence of the carrier of V by A11, FINSEQ_4: 41;

      reconsider Fw2 = (F |-- w) as FinSequence of the carrier of V by A11, A13, FINSEQ_4: 50;

      

       A14: ( rng Fw1) misses ( rng Fw2) by A10, A11, A13, FINSEQ_4: 57;

      set Fw = (Fw1 ^ Fw2);

      F just_once_values w by A10, A11, A13, FINSEQ_4: 8;

      then

       A15: Fw = (F - {w}) by FINSEQ_4: 54;

      then

       A16: ( rng Fw) = (( Carrier L) \ {w}) by A11, FINSEQ_3: 65;

      F = (((F -| w) ^ <*w*>) ^ (F |-- w)) by A11, A13, FINSEQ_4: 51;

      then F = (Fw1 ^ ( <*w*> ^ Fw2)) by FINSEQ_1: 32;

      

      then (L (#) F) = ((L (#) Fw1) ^ (L (#) ( <*w*> ^ Fw2))) by RLVECT_3: 34

      .= ((L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2))) by RLVECT_3: 34

      .= (((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2)) by FINSEQ_1: 32

      .= (((L (#) Fw1) ^ <*(a * w)*>) ^ (L (#) Fw2)) by RLVECT_2: 26;

      

      then

       A17: ( Sum (L (#) F)) = ( Sum ((L (#) Fw1) ^ ( <*(a * w)*> ^ (L (#) Fw2)))) by FINSEQ_1: 32

      .= (( Sum (L (#) Fw1)) + ( Sum ( <*(a * w)*> ^ (L (#) Fw2)))) by RLVECT_1: 41

      .= (( Sum (L (#) Fw1)) + (( Sum <*(a * w)*>) + ( Sum (L (#) Fw2)))) by RLVECT_1: 41

      .= (( Sum (L (#) Fw1)) + (( Sum (L (#) Fw2)) + (a * w))) by RLVECT_1: 44

      .= ((( Sum (L (#) Fw1)) + ( Sum (L (#) Fw2))) + (a * w)) by RLVECT_1:def 3

      .= (( Sum ((L (#) Fw1) ^ (L (#) Fw2))) + (a * w)) by RLVECT_1: 41

      .= (( Sum (L (#) (Fw1 ^ Fw2))) + (a * w)) by RLVECT_3: 34;

      v in {v} by TARSKI:def 1;

      then v in ( Lin {v}) by RLVECT_3: 15;

      then

      consider Lv be Linear_Combination of {v} such that

       A18: v = ( Sum Lv) by RLVECT_3: 14;

      consider K be Linear_Combination of V such that

       A19: ( Carrier K) = (( rng Fw) /\ ( Carrier L)) and

       A20: (L (#) Fw) = (K (#) Fw) by Th7;

      ( rng Fw) = (( rng F) \ {w}) by A15, FINSEQ_3: 65;

      then

       A21: ( Carrier K) = ( rng Fw) by A11, A19, XBOOLE_1: 28;

      

       A22: (( Carrier L) \ {w}) c= ((A \/ B) \ {w}) by A4, XBOOLE_1: 33;

      then

      reconsider K as Linear_Combination of ((A \/ B) \ {w}) by A16, A21, RLVECT_2:def 6;

      (a " ) <> 0 by A9, XCMPLX_1: 202;

      then

       A23: ( Carrier ((a " ) * (( - K) + Lv))) = ( Carrier (( - K) + Lv)) by RLVECT_2: 42;

      set LC = ((a " ) * (( - K) + Lv));

      ( Carrier (( - K) + Lv)) c= (( Carrier ( - K)) \/ ( Carrier Lv)) by RLVECT_2: 37;

      then

       A24: ( Carrier (( - K) + Lv)) c= (( Carrier K) \/ ( Carrier Lv)) by RLVECT_2: 51;

      ( Carrier Lv) c= {v} by RLVECT_2:def 6;

      then (( Carrier K) \/ ( Carrier Lv)) c= (((A \/ B) \ {w}) \/ {v}) by A16, A21, A22, XBOOLE_1: 13;

      then ( Carrier (( - K) + Lv)) c= (((A \/ B) \ {w}) \/ {v}) by A24;

      then

       A25: LC is Linear_Combination of (((A \/ B) \ {w}) \/ {v}) by A23, RLVECT_2:def 6;

      Fw1 is one-to-one & Fw2 is one-to-one by A10, A11, A13, FINSEQ_4: 52, FINSEQ_4: 53;

      then Fw is one-to-one by A14, FINSEQ_3: 91;

      then ( Sum (K (#) Fw)) = ( Sum K) by A21, RLVECT_2:def 8;

      

      then ((a " ) * v) = (((a " ) * ( Sum K)) + ((a " ) * (a * w))) by A3, A12, A17, A20, RLVECT_1:def 5

      .= (((a " ) * ( Sum K)) + (((a " ) * a) * w)) by RLVECT_1:def 7

      .= (((a " ) * ( Sum K)) + (1 * w)) by A9, XCMPLX_0:def 7

      .= (((a " ) * ( Sum K)) + w) by RLVECT_1:def 8;

      

      then w = (((a " ) * v) - ((a " ) * ( Sum K))) by RLSUB_2: 61

      .= ((a " ) * (v - ( Sum K))) by RLVECT_1: 34

      .= ((a " ) * (( - ( Sum K)) + v)) by RLVECT_1:def 11;

      

      then w = ((a " ) * (( Sum ( - K)) + ( Sum Lv))) by A18, RLVECT_3: 3

      .= ((a " ) * ( Sum (( - K) + Lv))) by RLVECT_3: 1

      .= ( Sum ((a " ) * (( - K) + Lv))) by RLVECT_3: 2;

      hence thesis by A8, A25, RLVECT_3: 14;

    end;

    theorem :: RLVECT_5:22

    

     Th22: for A,B be finite Subset of V st the RLSStruct of V = ( Lin A) & B is linearly-independent holds ( card B) <= ( card A) & ex C be finite Subset of V st C c= A & ( card C) = (( card A) - ( card B)) & the RLSStruct of V = ( Lin (B \/ C))

    proof

      defpred P[ Nat] means for n be Element of NAT holds for A,B be finite Subset of V st ( card A) = n & ( card B) = $1 & the RLSStruct of V = ( Lin A) & B is linearly-independent holds $1 <= n & ex C be finite Subset of V st C c= A & ( card C) = (n - $1) & the RLSStruct of V = ( Lin (B \/ C));

      

       A1: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat such that

         A2: P[m];

        let n be Element of NAT ;

        let A,B be finite Subset of V such that

         A3: ( card A) = n and

         A4: ( card B) = (m + 1) and

         A5: the RLSStruct of V = ( Lin A) and

         A6: B is linearly-independent;

        consider v be object such that

         A7: v in B by A4, CARD_1: 27, XBOOLE_0:def 1;

        reconsider v as VECTOR of V by A7;

        set Bv = (B \ {v});

        

         A8: Bv is linearly-independent by A6, RLVECT_3: 5, XBOOLE_1: 36;

         {v} is Subset of B by A7, SUBSET_1: 41;

        

        then

         A9: ( card (B \ {v})) = (( card B) - ( card {v})) by CARD_2: 44

        .= ((m + 1) - 1) by A4, CARD_1: 30

        .= m;

        then

        consider C be finite Subset of V such that

         A10: C c= A and

         A11: ( card C) = (n - m) and

         A12: the RLSStruct of V = ( Lin (Bv \/ C)) by A2, A3, A5, A8;

        

         A13: not v in ( Lin Bv) by A6, A7, Th17;

         A14:

        now

          assume m = n;

          then

          consider C be finite Subset of V such that C c= A and

           A15: ( card C) = (m - m) and

           A16: the RLSStruct of V = ( Lin (Bv \/ C)) by A2, A3, A5, A9, A8;

          C = {} by A15;

          then Bv is Basis of V by A8, A16, RLVECT_3:def 3;

          hence contradiction by A13, Th13;

        end;

        v in ( Lin (Bv \/ C)) by A12, STRUCT_0:def 5;

        then

        consider w be VECTOR of V such that

         A17: w in C and

         A18: w in ( Lin (((C \/ Bv) \ {w}) \/ {v})) by A13, Th21;

        set Cw = (C \ {w});

        ((Bv \ {w}) \/ {v}) c= (Bv \/ {v}) by XBOOLE_1: 9, XBOOLE_1: 36;

        then (Cw \/ ((Bv \ {w}) \/ {v})) c= (Cw \/ (Bv \/ {v})) by XBOOLE_1: 9;

        then

         A19: (Cw \/ ((Bv \ {w}) \/ {v})) c= (B \/ Cw) by A7, Lm1;

         {w} is Subset of C by A17, SUBSET_1: 41;

        

        then

         A20: ( card Cw) = (( card C) - ( card {w})) by CARD_2: 44

        .= ((n - m) - 1) by A11, CARD_1: 30

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

        Cw c= C by XBOOLE_1: 36;

        then

         A21: Cw c= A by A10;

        (((C \/ Bv) \ {w}) \/ {v}) = ((Cw \/ (Bv \ {w})) \/ {v}) by XBOOLE_1: 42

        .= (Cw \/ ((Bv \ {w}) \/ {v})) by XBOOLE_1: 4;

        then ( Lin (((C \/ Bv) \ {w}) \/ {v})) is Subspace of ( Lin (B \/ Cw)) by A19, RLVECT_3: 20;

        then

         A22: w in ( Lin (B \/ Cw)) by A18, RLSUB_1: 8;

        

         A23: Bv c= B & C = (Cw \/ {w}) by A17, Lm1, XBOOLE_1: 36;

        now

          let x be object;

          assume x in (Bv \/ C);

          then x in Bv or x in C by XBOOLE_0:def 3;

          then x in B or x in Cw or x in {w} by A23, XBOOLE_0:def 3;

          then x in (B \/ Cw) or x in {w} by XBOOLE_0:def 3;

          then x in ( Lin (B \/ Cw)) or x = w by RLVECT_3: 15, TARSKI:def 1;

          hence x in the carrier of ( Lin (B \/ Cw)) by A22, STRUCT_0:def 5;

        end;

        then (Bv \/ C) c= the carrier of ( Lin (B \/ Cw));

        then ( Lin (Bv \/ C)) is Subspace of ( Lin (B \/ Cw)) by Th19;

        then

         A24: the carrier of ( Lin (Bv \/ C)) c= the carrier of ( Lin (B \/ Cw)) by RLSUB_1:def 2;

        the carrier of ( Lin (B \/ Cw)) c= the carrier of V by RLSUB_1:def 2;

        then the carrier of ( Lin (B \/ Cw)) = the carrier of V by A12, A24, XBOOLE_0:def 10;

        then

         A25: the RLSStruct of V = ( Lin (B \/ Cw)) by A12, RLSUB_1: 30;

        m <= n by A2, A3, A5, A9, A8;

        then m < n by A14, XXREAL_0: 1;

        hence thesis by A21, A20, A25, NAT_1: 13;

      end;

      

       A26: P[ 0 ]

      proof

        let n be Element of NAT ;

        let A,B be finite Subset of V such that

         A27: ( card A) = n and

         A28: ( card B) = 0 and

         A29: the RLSStruct of V = ( Lin A) and B is linearly-independent;

        B = {} by A28;

        then A = (B \/ A);

        hence thesis by A27, A29;

      end;

      

       A30: for m be Nat holds P[m] from NAT_1:sch 2( A26, A1);

      let A,B be finite Subset of V;

      assume the RLSStruct of V = ( Lin A) & B is linearly-independent;

      hence thesis by A30;

    end;

    begin

    definition

      let V be RealLinearSpace;

      :: RLVECT_5:def1

      attr V is finite-dimensional means

      : Def1: ex A be finite Subset of V st A is Basis of V;

    end

    registration

      cluster strict finite-dimensional for RealLinearSpace;

      existence

      proof

        set V = the RealLinearSpace;

        take ( (0). V);

        thus ( (0). V) is strict;

        take A = ( {} the carrier of ( (0). V));

        ( Lin A) = ( (0). ( (0). V)) by RLVECT_3: 16;

        then A is linearly-independent & ( Lin A) = the RLSStruct of ( (0). V) by RLSUB_1: 36, RLVECT_3: 7;

        hence thesis by RLVECT_3:def 3;

      end;

    end

    theorem :: RLVECT_5:23

    

     Th23: V is finite-dimensional implies for I be Basis of V holds I is finite

    proof

      assume V is finite-dimensional;

      then

      consider A be finite Subset of V such that

       A1: A is Basis of V;

      let B be Basis of V;

      consider p be FinSequence such that

       A2: ( rng p) = A by FINSEQ_1: 52;

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

      set Car = { ( Carrier L) where L be Linear_Combination of B : ex i st i in ( dom p) & ( Sum L) = (p . i) };

      set C = ( union Car);

      

       A3: C c= B

      proof

        let x be object;

        assume x in C;

        then

        consider R be set such that

         A4: x in R and

         A5: R in Car by TARSKI:def 4;

        ex L be Linear_Combination of B st R = ( Carrier L) & ex i st i in ( dom p) & ( Sum L) = (p . i) by A5;

        then R c= B by RLVECT_2:def 6;

        hence thesis by A4;

      end;

      then

      reconsider C as Subset of V by XBOOLE_1: 1;

      for v be VECTOR of V holds v in ( (Omega). V) iff v in ( Lin C)

      proof

        let v be VECTOR of V;

        hereby

          assume v in ( (Omega). V);

          then v in the RLSStruct of V by RLSUB_1:def 4;

          then v in ( Lin A) by A1, RLVECT_3:def 3;

          then

          consider LA be Linear_Combination of A such that

           A6: v = ( Sum LA) by RLVECT_3: 14;

          ( Carrier LA) c= the carrier of ( Lin C)

          proof

            let w be object;

            assume

             A7: w in ( Carrier LA);

            then

            reconsider w9 = w as VECTOR of V;

            w9 in ( Lin B) by Th13;

            then

            consider LB be Linear_Combination of B such that

             A8: w = ( Sum LB) by RLVECT_3: 14;

            ( Carrier LA) c= A by RLVECT_2:def 6;

            then ex i be object st i in ( dom p) & w = (p . i) by A2, A7, FUNCT_1:def 3;

            then

             A9: ( Carrier LB) in Car by A8;

            ( Carrier LB) c= C by A9, TARSKI:def 4;

            then LB is Linear_Combination of C by RLVECT_2:def 6;

            then w in ( Lin C) by A8, RLVECT_3: 14;

            hence thesis by STRUCT_0:def 5;

          end;

          then ex LC be Linear_Combination of C st ( Sum LA) = ( Sum LC) by Th9;

          hence v in ( Lin C) by A6, RLVECT_3: 14;

        end;

        assume v in ( Lin C);

        v in the carrier of the RLSStruct of V;

        then v in the carrier of ( (Omega). V) by RLSUB_1:def 4;

        hence thesis by STRUCT_0:def 5;

      end;

      then ( (Omega). V) = ( Lin C) by RLSUB_1: 31;

      then

       A10: the RLSStruct of V = ( Lin C) by RLSUB_1:def 4;

      

       A11: B is linearly-independent by RLVECT_3:def 3;

      then C is linearly-independent by A3, RLVECT_3: 5;

      then

       A12: C is Basis of V by A10, RLVECT_3:def 3;

      B c= C

      proof

        set D = (B \ C);

        assume not B c= C;

        then ex v be object st v in B & not v in C;

        then

        reconsider D as non empty Subset of V by XBOOLE_0:def 5;

        reconsider B as Subset of V;

        (C \/ (B \ C)) = (C \/ B) by XBOOLE_1: 39

        .= B by A3, XBOOLE_1: 12;

        then B = (C \/ D);

        hence contradiction by A11, A12, Th18, XBOOLE_1: 79;

      end;

      then

       A13: B = C by A3, XBOOLE_0:def 10;

      defpred P[ set, object] means ex L be Linear_Combination of B st $2 = ( Carrier L) & ( Sum L) = (p . $1);

      

       A14: for i be Nat st i in ( Seg ( len p)) holds ex x be object st P[i, x]

      proof

        let i be Nat;

        assume i in ( Seg ( len p));

        then i in ( dom p) by FINSEQ_1:def 3;

        then (p . i) in the carrier of V by FINSEQ_2: 11;

        then (p . i) in ( Lin B) by Th13;

        then

        consider L be Linear_Combination of B such that

         A15: (p . i) = ( Sum L) by RLVECT_3: 14;

         P[i, ( Carrier L)] by A15;

        hence thesis;

      end;

      ex q be FinSequence st ( dom q) = ( Seg ( len p)) & for i be Nat st i in ( Seg ( len p)) holds P[i, (q . i)] from FINSEQ_1:sch 1( A14);

      then

      consider q be FinSequence such that

       A16: ( dom q) = ( Seg ( len p)) and

       A17: for i be Nat st i in ( Seg ( len p)) holds P[i, (q . i)];

      

       A18: ( dom p) = ( dom q) by A16, FINSEQ_1:def 3;

      

       A19: for i be Nat, y1, y2 st i in ( Seg ( len p)) & P[i, y1] & P[i, y2] holds y1 = y2

      proof

        let i be Nat, y1, y2;

        assume that i in ( Seg ( len p)) and

         A20: P[i, y1] and

         A21: P[i, y2];

        consider L1 be Linear_Combination of B such that

         A22: y1 = ( Carrier L1) & ( Sum L1) = (p . i) by A20;

        consider L2 be Linear_Combination of B such that

         A23: y2 = ( Carrier L2) & ( Sum L2) = (p . i) by A21;

        ( Carrier L1) c= B & ( Carrier L2) c= B by RLVECT_2:def 6;

        hence thesis by A11, A22, A23, Th1;

      end;

      now

        let x be object;

        assume x in Car;

        then

        consider L be Linear_Combination of B such that

         A24: x = ( Carrier L) and

         A25: ex i st i in ( dom p) & ( Sum L) = (p . i);

        consider i such that

         A26: i in ( dom p) and

         A27: ( Sum L) = (p . i) by A25;

         P[i, (q . i)] by A16, A17, A18, A26;

        then x = (q . i) by A19, A16, A18, A24, A26, A27;

        hence x in ( rng q) by A18, A26, FUNCT_1:def 3;

      end;

      then

       A28: Car c= ( rng q);

      for R be set st R in Car holds R is finite

      proof

        let R be set;

        assume R in Car;

        then ex L be Linear_Combination of B st R = ( Carrier L) & ex i st i in ( dom p) & ( Sum L) = (p . i);

        hence thesis;

      end;

      hence thesis by A13, A28, FINSET_1: 7;

    end;

    theorem :: RLVECT_5:24

    V is finite-dimensional implies for A be Subset of V st A is linearly-independent holds A is finite

    proof

      assume

       A1: V is finite-dimensional;

      let A be Subset of V;

      assume A is linearly-independent;

      then

      consider B be Basis of V such that

       A2: A c= B by Th2;

      B is finite by A1, Th23;

      hence thesis by A2;

    end;

    theorem :: RLVECT_5:25

    

     Th25: V is finite-dimensional implies for A,B be Basis of V holds ( card A) = ( card B)

    proof

      assume

       A1: V is finite-dimensional;

      let A,B be Basis of V;

      reconsider A9 = A, B9 = B as finite Subset of V by A1, Th23;

       the RLSStruct of V = ( Lin B) & A9 is linearly-independent by RLVECT_3:def 3;

      then

       A2: ( card A9) <= ( card B9) by Th22;

       the RLSStruct of V = ( Lin A) & B9 is linearly-independent by RLVECT_3:def 3;

      then ( card B9) <= ( card A9) by Th22;

      hence thesis by A2, XXREAL_0: 1;

    end;

    theorem :: RLVECT_5:26

    

     Th26: ( (0). V) is finite-dimensional

    proof

      reconsider V9 = ( (0). V) as strict RealLinearSpace;

      reconsider I = ( {} the carrier of V9) as finite Subset of V9;

      the carrier of V9 = {( 0. V)} by RLSUB_1:def 3

      .= {( 0. V9)} by RLSUB_1: 11

      .= the carrier of ( (0). V9) by RLSUB_1:def 3;

      then

       A1: V9 = ( (0). V9) by RLSUB_1: 32;

      I is linearly-independent & ( Lin I) = ( (0). V9) by RLVECT_3: 7, RLVECT_3: 16;

      then I is Basis of V9 by A1, RLVECT_3:def 3;

      hence thesis;

    end;

    theorem :: RLVECT_5:27

    

     Th27: V is finite-dimensional implies W is finite-dimensional

    proof

      set A = the Basis of W;

      consider I be Basis of V such that

       A1: A c= I by Th16;

      assume V is finite-dimensional;

      then I is finite by Th23;

      hence thesis by A1;

    end;

    registration

      let V be RealLinearSpace;

      cluster finite-dimensional strict for Subspace of V;

      existence

      proof

        take ( (0). V);

        thus thesis by Th26;

      end;

    end

    registration

      let V be finite-dimensional RealLinearSpace;

      cluster -> finite-dimensional for Subspace of V;

      correctness by Th27;

    end

    registration

      let V be finite-dimensional RealLinearSpace;

      cluster strict for Subspace of V;

      existence

      proof

        ( (0). V) is strict finite-dimensional Subspace of V;

        hence thesis;

      end;

    end

    begin

    definition

      let V be RealLinearSpace;

      assume

       A1: V is finite-dimensional;

      :: RLVECT_5:def2

      func dim V -> Element of NAT means

      : Def2: for I be Basis of V holds it = ( card I);

      existence

      proof

        consider A be finite Subset of V such that

         A2: A is Basis of V by A1;

        consider n be Element of NAT such that

         A3: n = ( card A);

        for I be Basis of V holds ( card I) = n by A1, A2, A3, Th25;

        hence thesis;

      end;

      uniqueness

      proof

        let n,m be Element of NAT ;

        assume that

         A4: for I be Basis of V holds ( card I) = n and

         A5: for I be Basis of V holds ( card I) = m;

        consider A be finite Subset of V such that

         A6: A is Basis of V by A1;

        ( card A) = n by A4, A6;

        hence thesis by A5, A6;

      end;

    end

    reserve V for finite-dimensional RealLinearSpace,

W,W1,W2 for Subspace of V,

u,v for VECTOR of V;

    theorem :: RLVECT_5:28

    

     Th28: ( dim W) <= ( dim V)

    proof

      reconsider V9 = V as RealLinearSpace;

      set I = the Basis of V9;

      reconsider I as finite Subset of V by Th23;

      set A = the Basis of W;

      reconsider A as Subset of W;

      A is linearly-independent by RLVECT_3:def 3;

      then

      reconsider A9 = A as finite Subset of V by Th14, Th23;

      ( Lin I) = the RLSStruct of V9 & A is linearly-independent Subset of V by Th14, RLVECT_3:def 3;

      then

       A1: ( card A9) <= ( card I) by Th22;

      ( dim W) = ( card A) by Def2;

      hence thesis by A1, Def2;

    end;

    theorem :: RLVECT_5:29

    

     Th29: for A be Subset of V st A is linearly-independent holds ( card A) = ( dim ( Lin A))

    proof

      let A be Subset of V such that

       A1: A is linearly-independent;

      set W = ( Lin A);

      for x be object st x in A holds x in the carrier of W by STRUCT_0:def 5, RLVECT_3: 15;

      then

      reconsider B = A as linearly-independent Subset of W by A1, Th15, TARSKI:def 3;

      W = ( Lin B) by Th20;

      then

      reconsider B as Basis of W by RLVECT_3:def 3;

      ( card B) = ( dim W) by Def2;

      hence thesis;

    end;

    theorem :: RLVECT_5:30

    

     Th30: ( dim V) = ( dim ( (Omega). V))

    proof

      consider I be finite Subset of V such that

       A1: I is Basis of V by Def1;

      

       A2: ( (Omega). V) = the RLSStruct of V by RLSUB_1:def 4

      .= ( Lin I) by A1, RLVECT_3:def 3;

      ( card I) = ( dim V) & I is linearly-independent by A1, Def2, RLVECT_3:def 3;

      hence thesis by A2, Th29;

    end;

    theorem :: RLVECT_5:31

    ( dim V) = ( dim W) iff ( (Omega). V) = ( (Omega). W)

    proof

      consider A be finite Subset of V such that

       A1: A is Basis of V by Def1;

      hereby

        set A = the Basis of W;

        consider B be Basis of V such that

         A2: A c= B by Th16;

        the carrier of W c= the carrier of V by RLSUB_1:def 2;

        then

        reconsider A9 = A as finite Subset of V by Th23, XBOOLE_1: 1;

        reconsider B9 = B as finite Subset of V by Th23;

        assume ( dim V) = ( dim W);

        

        then

         A3: ( card A) = ( dim V) by Def2

        .= ( card B) by Def2;

         A4:

        now

          assume A <> B;

          then A c< B by A2, XBOOLE_0:def 8;

          then ( card A9) < ( card B9) by CARD_2: 48;

          hence contradiction by A3;

        end;

        reconsider B as Subset of V;

        reconsider A as Subset of W;

        ( (Omega). V) = the RLSStruct of V by RLSUB_1:def 4

        .= ( Lin B) by RLVECT_3:def 3

        .= ( Lin A) by A4, Th20

        .= the RLSStruct of W by RLVECT_3:def 3

        .= ( (Omega). W) by RLSUB_1:def 4;

        hence ( (Omega). V) = ( (Omega). W);

      end;

      consider B be finite Subset of W such that

       A5: B is Basis of W by Def1;

      

       A6: A is linearly-independent by A1, RLVECT_3:def 3;

      assume ( (Omega). V) = ( (Omega). W);

      

      then the RLSStruct of V = ( (Omega). W) by RLSUB_1:def 4

      .= the RLSStruct of W by RLSUB_1:def 4;

      

      then

       A7: ( Lin A) = the RLSStruct of W by A1, RLVECT_3:def 3

      .= ( Lin B) by A5, RLVECT_3:def 3;

      

       A8: B is linearly-independent by A5, RLVECT_3:def 3;

      reconsider B as Subset of W;

      reconsider A as Subset of V;

      ( dim V) = ( card A) by A1, Def2

      .= ( dim ( Lin B)) by A6, A7, Th29

      .= ( card B) by A8, Th29

      .= ( dim W) by A5, Def2;

      hence thesis;

    end;

    theorem :: RLVECT_5:32

    

     Th32: ( dim V) = 0 iff ( (Omega). V) = ( (0). V)

    proof

      consider I be finite Subset of V such that

       A1: I is Basis of V by Def1;

      hereby

        consider I be finite Subset of V such that

         A2: I is Basis of V by Def1;

        assume ( dim V) = 0 ;

        then ( card I) = 0 by A2, Def2;

        then

         A3: I = ( {} the carrier of V);

        ( (Omega). V) = the RLSStruct of V by RLSUB_1:def 4

        .= ( Lin I) by A2, RLVECT_3:def 3

        .= ( (0). V) by A3, RLVECT_3: 16;

        hence ( (Omega). V) = ( (0). V);

      end;

      

       A4: I <> {( 0. V)} by A1, RLVECT_3: 8, RLVECT_3:def 3;

      assume ( (Omega). V) = ( (0). V);

      then the RLSStruct of V = ( (0). V) by RLSUB_1:def 4;

      then ( Lin I) = ( (0). V) by A1, RLVECT_3:def 3;

      then I = {} or I = {( 0. V)} by RLVECT_3: 17;

      hence thesis by A1, A4, Def2, CARD_1: 27;

    end;

    theorem :: RLVECT_5:33

    ( dim V) = 1 iff ex v st v <> ( 0. V) & ( (Omega). V) = ( Lin {v})

    proof

      hereby

        consider I be finite Subset of V such that

         A1: I is Basis of V by Def1;

        assume ( dim V) = 1;

        then ( card I) = 1 by A1, Def2;

        then

        consider v be object such that

         A2: I = {v} by CARD_2: 42;

        v in I by A2, TARSKI:def 1;

        then

        reconsider v as VECTOR of V;

         {v} is linearly-independent by A1, A2, RLVECT_3:def 3;

        then

         A3: v <> ( 0. V) by RLVECT_3: 8;

        ( Lin {v}) = the RLSStruct of V by A1, A2, RLVECT_3:def 3;

        hence ex v st v <> ( 0. V) & ( (Omega). V) = ( Lin {v}) by A3, RLSUB_1:def 4;

      end;

      given v such that

       A4: v <> ( 0. V) & ( (Omega). V) = ( Lin {v});

       {v} is linearly-independent & ( Lin {v}) = the RLSStruct of V by A4, RLSUB_1:def 4, RLVECT_3: 8;

      then

       A5: {v} is Basis of V by RLVECT_3:def 3;

      ( card {v}) = 1 by CARD_1: 30;

      hence thesis by A5, Def2;

    end;

    theorem :: RLVECT_5:34

    ( dim V) = 2 iff ex u, v st u <> v & {u, v} is linearly-independent & ( (Omega). V) = ( Lin {u, v})

    proof

      hereby

        consider I be finite Subset of V such that

         A1: I is Basis of V by Def1;

        assume ( dim V) = 2;

        then

         A2: ( card I) = 2 by A1, Def2;

        then

        consider u be object such that

         A3: u in I by CARD_1: 27, XBOOLE_0:def 1;

        reconsider u as VECTOR of V by A3;

        now

          assume I c= {u};

          then ( card I) <= ( card {u}) by NAT_1: 43;

          then 2 <= 1 by A2, CARD_1: 30;

          hence contradiction;

        end;

        then

        consider v be object such that

         A4: v in I and

         A5: not v in {u};

        reconsider v as VECTOR of V by A4;

        

         A6: v <> u by A5, TARSKI:def 1;

         A7:

        now

          assume not I c= {u, v};

          then

          consider w be object such that

           A8: w in I and

           A9: not w in {u, v};

          for x be object st x in {u, v, w} holds x in I by A3, A4, A8, ENUMSET1:def 1;

          then {u, v, w} c= I;

          then

           A10: ( card {u, v, w}) <= ( card I) by NAT_1: 43;

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

          then 3 <= 2 by A2, A6, A10, CARD_2: 58;

          hence contradiction;

        end;

        for x be object st x in {u, v} holds x in I by A3, A4, TARSKI:def 2;

        then {u, v} c= I;

        then

         A11: I = {u, v} by A7, XBOOLE_0:def 10;

        then

         A12: {u, v} is linearly-independent by A1, RLVECT_3:def 3;

        ( Lin {u, v}) = the RLSStruct of V by A1, A11, RLVECT_3:def 3

        .= ( (Omega). V) by RLSUB_1:def 4;

        hence ex u, v st u <> v & {u, v} is linearly-independent & ( (Omega). V) = ( Lin {u, v}) by A6, A12;

      end;

      given u, v such that

       A13: u <> v and

       A14: {u, v} is linearly-independent and

       A15: ( (Omega). V) = ( Lin {u, v});

      ( Lin {u, v}) = the RLSStruct of V by A15, RLSUB_1:def 4;

      then

       A16: {u, v} is Basis of V by A14, RLVECT_3:def 3;

      ( card {u, v}) = 2 by A13, CARD_2: 57;

      hence thesis by A16, Def2;

    end;

    theorem :: RLVECT_5:35

    

     Th35: (( dim (W1 + W2)) + ( dim (W1 /\ W2))) = (( dim W1) + ( dim W2))

    proof

      reconsider V as RealLinearSpace;

      reconsider W1, W2 as Subspace of V;

      consider I be finite Subset of (W1 /\ W2) such that

       A1: I is Basis of (W1 /\ W2) by Def1;

      (W1 /\ W2) is Subspace of W2 by RLSUB_2: 16;

      then

      consider I2 be Basis of W2 such that

       A2: I c= I2 by A1, Th16;

      (W1 /\ W2) is Subspace of W1 by RLSUB_2: 16;

      then

      consider I1 be Basis of W1 such that

       A3: I c= I1 by A1, Th16;

      reconsider I2 as finite Subset of W2 by Th23;

      reconsider I1 as finite Subset of W1 by Th23;

       A4:

      now

        I1 is linearly-independent by RLVECT_3:def 3;

        then

        reconsider I19 = I1 as linearly-independent Subset of V by Th14;

        assume not (I1 /\ I2) c= I;

        then

        consider x be object such that

         A5: x in (I1 /\ I2) and

         A6: not x in I;

        x in I1 by A5, XBOOLE_0:def 4;

        then x in ( Lin I1) by RLVECT_3: 15;

        then x in the RLSStruct of W1 by RLVECT_3:def 3;

        then

         A7: x in the carrier of W1 by STRUCT_0:def 5;

        

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

        then

        reconsider x9 = x as VECTOR of V by A7;

        now

          let y be object;

          the carrier of (W1 /\ W2) c= the carrier of V by RLSUB_1:def 2;

          then

           A9: I c= the carrier of V;

          assume y in (I \/ {x});

          then y in I or y in {x} by XBOOLE_0:def 3;

          then y in the carrier of V or y = x by A9, TARSKI:def 1;

          hence y in the carrier of V by A7, A8;

        end;

        then

        reconsider Ix = (I \/ {x}) as Subset of V by TARSKI:def 3;

        now

          let y be object;

          assume y in (I \/ {x});

          then y in I or y in {x} by XBOOLE_0:def 3;

          then y in I1 or y = x by A3, TARSKI:def 1;

          hence y in I19 by A5, XBOOLE_0:def 4;

        end;

        then

         A10: Ix c= I19;

        x in {x} by TARSKI:def 1;

        then

         A11: x9 in Ix by XBOOLE_0:def 3;

        x in I2 by A5, XBOOLE_0:def 4;

        then x in ( Lin I2) by RLVECT_3: 15;

        then x in the RLSStruct of W2 by RLVECT_3:def 3;

        then x in the carrier of W2 by STRUCT_0:def 5;

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

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

        then

         A12: x in the RLSStruct of (W1 /\ W2) by STRUCT_0:def 5;

        the carrier of (W1 /\ W2) c= the carrier of V by RLSUB_1:def 2;

        then

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

        

         A13: ( Lin I) = ( Lin I9) by Th20;

        (Ix \ {x}) = (I \ {x}) by XBOOLE_1: 40

        .= I by A6, ZFMISC_1: 57;

        then not x9 in ( Lin I9) by A10, A11, Th17, RLVECT_3: 5;

        hence contradiction by A1, A12, A13, RLVECT_3:def 3;

      end;

      set A = (I1 \/ I2);

      now

        let v be object;

        

         A14: the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V by RLSUB_1:def 2;

        assume v in A;

        then

         A15: v in I1 or v in I2 by XBOOLE_0:def 3;

        then v in the carrier of W1 or v in the carrier of W2;

        then

        reconsider v9 = v as VECTOR of V by A14;

        v9 in W1 or v9 in W2 by A15, STRUCT_0:def 5;

        then v9 in (W1 + W2) by RLSUB_2: 2;

        hence v in the carrier of (W1 + W2) by STRUCT_0:def 5;

      end;

      then

      reconsider A as finite Subset of (W1 + W2) by TARSKI:def 3;

      I c= (I1 /\ I2) by A3, A2, XBOOLE_1: 19;

      then I = (I1 /\ I2) by A4, XBOOLE_0:def 10;

      then

       A16: ( card A) = ((( card I1) + ( card I2)) - ( card I)) by CARD_2: 45;

      for L be Linear_Combination of A st ( Sum L) = ( 0. (W1 + W2)) holds ( Carrier L) = {}

      proof

        W1 is Subspace of (W1 + W2) & I1 is linearly-independent by RLSUB_2: 7, RLVECT_3:def 3;

        then

        reconsider I19 = I1 as linearly-independent Subset of (W1 + W2) by Th14;

        reconsider W29 = W2 as Subspace of (W1 + W2) by RLSUB_2: 7;

        reconsider W19 = W1 as Subspace of (W1 + W2) by RLSUB_2: 7;

        let L be Linear_Combination of A;

        assume

         A17: ( Sum L) = ( 0. (W1 + W2));

        

         A18: I1 misses (( Carrier L) \ I1) by XBOOLE_1: 79;

        set B = (( Carrier L) /\ I1);

        consider F be FinSequence of the carrier of (W1 + W2) such that

         A19: F is one-to-one and

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

         A21: ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

        reconsider B as Subset of ( rng F) by A20, XBOOLE_1: 17;

        reconsider F1 = (F - (B ` )), F2 = (F - B) as FinSequence of the carrier of (W1 + W2) by FINSEQ_3: 86;

        consider L1 be Linear_Combination of (W1 + W2) such that

         A22: ( Carrier L1) = (( rng F1) /\ ( Carrier L)) and

         A23: (L1 (#) F1) = (L (#) F1) by Th7;

        F1 is one-to-one by A19, FINSEQ_3: 87;

        then

         A24: ( Sum (L (#) F1)) = ( Sum L1) by A22, A23, Th6, XBOOLE_1: 17;

        ( rng F) c= ( rng F);

        then

        reconsider X = ( rng F) as Subset of ( rng F);

        consider L2 be Linear_Combination of (W1 + W2) such that

         A25: ( Carrier L2) = (( rng F2) /\ ( Carrier L)) and

         A26: (L2 (#) F2) = (L (#) F2) by Th7;

        F2 is one-to-one by A19, FINSEQ_3: 87;

        then

         A27: ( Sum (L (#) F2)) = ( Sum L2) by A25, A26, Th6, XBOOLE_1: 17;

        (X \ (B ` )) = (X /\ ((B ` ) ` )) by SUBSET_1: 13

        .= B by XBOOLE_1: 28;

        then ( rng F1) = B by FINSEQ_3: 65;

        

        then

         A28: ( Carrier L1) = (I1 /\ (( Carrier L) /\ ( Carrier L))) by A22, XBOOLE_1: 16

        .= (( Carrier L) /\ I1);

        then

        consider K1 be Linear_Combination of W19 such that ( Carrier K1) = ( Carrier L1) and

         A29: ( Sum K1) = ( Sum L1) by Th12;

        ( rng F2) = (( Carrier L) \ (( Carrier L) /\ I1)) by A20, FINSEQ_3: 65

        .= (( Carrier L) \ I1) by XBOOLE_1: 47;

        then

         A30: ( Carrier L2) = (( Carrier L) \ I1) by A25, XBOOLE_1: 28, XBOOLE_1: 36;

        

        then (( Carrier L1) /\ ( Carrier L2)) = (( Carrier L) /\ (I1 /\ (( Carrier L) \ I1))) by A28, XBOOLE_1: 16

        .= (( Carrier L) /\ {} ) by A18, XBOOLE_0:def 7

        .= {} ;

        then

         A31: ( Carrier L1) misses ( Carrier L2) by XBOOLE_0:def 7;

        

         A32: ( Carrier L) c= (I1 \/ I2) by RLVECT_2:def 6;

        then

         A33: ( Carrier L2) c= I2 by A30, XBOOLE_1: 43;

        ( Carrier L2) c= I2 by A32, A30, XBOOLE_1: 43;

        then

        consider K2 be Linear_Combination of W29 such that ( Carrier K2) = ( Carrier L2) and

         A34: ( Sum K2) = ( Sum L2) by Th12, XBOOLE_1: 1;

        

         A35: ( Sum K1) in W1 by STRUCT_0:def 5;

        ex P be Permutation of ( dom F) st ((F - (B ` )) ^ (F - B)) = (F * P) by FINSEQ_3: 115;

        

        then

         A36: ( 0. (W1 + W2)) = ( Sum (L (#) (F1 ^ F2))) by A17, A21, Th4

        .= ( Sum ((L (#) F1) ^ (L (#) F2))) by RLVECT_3: 34

        .= (( Sum L1) + ( Sum L2)) by A24, A27, RLVECT_1: 41;

        

        then ( Sum L1) = ( - ( Sum L2)) by RLVECT_1:def 10

        .= ( - ( Sum K2)) by A34, RLSUB_1: 15;

        then ( Sum K1) in W2 by A29, STRUCT_0:def 5;

        then ( Sum K1) in (W1 /\ W2) by A35, RLSUB_2: 3;

        then ( Sum K1) in ( Lin I) by A1, RLVECT_3:def 3;

        then

        consider KI be Linear_Combination of I such that

         A37: ( Sum K1) = ( Sum KI) by RLVECT_3: 14;

        

         A38: ( Carrier L) = (( Carrier L1) \/ ( Carrier L2)) by A28, A30, XBOOLE_1: 51;

         A39:

        now

          assume not ( Carrier L) c= ( Carrier (L1 + L2));

          then

          consider x be object such that

           A40: x in ( Carrier L) and

           A41: not x in ( Carrier (L1 + L2));

          reconsider x as VECTOR of (W1 + W2) by A40;

          

           A42: 0 = ((L1 + L2) . x) by A41, RLVECT_2: 19

          .= ((L1 . x) + (L2 . x)) by RLVECT_2:def 10;

          per cases by A38, A40, XBOOLE_0:def 3;

            suppose

             A43: x in ( Carrier L1);

            then not x in ( Carrier L2) by A31, XBOOLE_0: 3;

            then

             A44: (L2 . x) = 0 by RLVECT_2: 19;

            ex v be VECTOR of (W1 + W2) st x = v & (L1 . v) <> 0 by A43, Th3;

            hence contradiction by A42, A44;

          end;

            suppose

             A45: x in ( Carrier L2);

            then not x in ( Carrier L1) by A31, XBOOLE_0: 3;

            then

             A46: (L1 . x) = 0 by RLVECT_2: 19;

            ex v be VECTOR of (W1 + W2) st x = v & (L2 . v) <> 0 by A45, Th3;

            hence contradiction by A42, A46;

          end;

        end;

        

         A47: (I \/ I2) = I2 by A2, XBOOLE_1: 12;

        

         A48: I2 is linearly-independent by RLVECT_3:def 3;

        

         A49: ( Carrier L1) c= I1 by A28, XBOOLE_1: 17;

        (W1 /\ W2) is Subspace of (W1 + W2) by RLSUB_2: 22;

        then

        consider LI be Linear_Combination of (W1 + W2) such that

         A50: ( Carrier LI) = ( Carrier KI) and

         A51: ( Sum LI) = ( Sum KI) by Th11;

        ( Carrier LI) c= I by A50, RLVECT_2:def 6;

        then ( Carrier LI) c= I19 by A3;

        then

         A52: LI = L1 by A49, A29, A37, A51, Th1;

        ( Carrier LI) c= I by A50, RLVECT_2:def 6;

        then ( Carrier (LI + L2)) c= (( Carrier LI) \/ ( Carrier L2)) & (( Carrier LI) \/ ( Carrier L2)) c= I2 by A47, A33, RLVECT_2: 37, XBOOLE_1: 13;

        then

         A53: ( Carrier (LI + L2)) c= I2;

        W2 is Subspace of (W1 + W2) by RLSUB_2: 7;

        then

        consider K be Linear_Combination of W2 such that

         A54: ( Carrier K) = ( Carrier (LI + L2)) and

         A55: ( Sum K) = ( Sum (LI + L2)) by A53, Th12, XBOOLE_1: 1;

        reconsider K as Linear_Combination of I2 by A53, A54, RLVECT_2:def 6;

        ( 0. W2) = (( Sum LI) + ( Sum L2)) by A29, A36, A37, A51, RLSUB_1: 12

        .= ( Sum K) by A55, RLVECT_3: 1;

        then {} = ( Carrier (L1 + L2)) by A54, A52, A48, RLVECT_3:def 1;

        hence thesis by A39;

      end;

      then

       A56: A is linearly-independent by RLVECT_3:def 1;

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

      then

      reconsider A9 = A as Subset of V by XBOOLE_1: 1;

      

       A57: ( card I2) = ( dim W2) by Def2;

      now

        let x be object;

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

        then x in (W1 + W2) by STRUCT_0:def 5;

        then

        consider w1,w2 be VECTOR of V such that

         A58: w1 in W1 and

         A59: w2 in W2 and

         A60: x = (w1 + w2) by RLSUB_2: 1;

        reconsider w1 as VECTOR of W1 by A58, STRUCT_0:def 5;

        w1 in ( Lin I1) by Th13;

        then

        consider K1 be Linear_Combination of I1 such that

         A61: w1 = ( Sum K1) by RLVECT_3: 14;

        reconsider w2 as VECTOR of W2 by A59, STRUCT_0:def 5;

        w2 in ( Lin I2) by Th13;

        then

        consider K2 be Linear_Combination of I2 such that

         A62: w2 = ( Sum K2) by RLVECT_3: 14;

        consider L2 be Linear_Combination of V such that

         A63: ( Carrier L2) = ( Carrier K2) and

         A64: ( Sum L2) = ( Sum K2) by Th11;

        

         A65: ( Carrier L2) c= I2 by A63, RLVECT_2:def 6;

        consider L1 be Linear_Combination of V such that

         A66: ( Carrier L1) = ( Carrier K1) and

         A67: ( Sum L1) = ( Sum K1) by Th11;

        set L = (L1 + L2);

        ( Carrier L1) c= I1 by A66, RLVECT_2:def 6;

        then ( Carrier L) c= (( Carrier L1) \/ ( Carrier L2)) & (( Carrier L1) \/ ( Carrier L2)) c= (I1 \/ I2) by A65, RLVECT_2: 37, XBOOLE_1: 13;

        then ( Carrier L) c= (I1 \/ I2);

        then

        reconsider L as Linear_Combination of A9 by RLVECT_2:def 6;

        x = ( Sum L) by A60, A61, A67, A62, A64, RLVECT_3: 1;

        then x in ( Lin A9) by RLVECT_3: 14;

        hence x in the carrier of ( Lin A9) by STRUCT_0:def 5;

      end;

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

      then

       A68: (W1 + W2) is Subspace of ( Lin A9) by RLSUB_1: 28;

      ( Lin A9) = ( Lin A) by Th20;

      then ( Lin A) = (W1 + W2) by A68, RLSUB_1: 26;

      then A is Basis of (W1 + W2) by A56, RLVECT_3:def 3;

      then

       A69: ( card A) = ( dim (W1 + W2)) by Def2;

      ( card I) = ( dim (W1 /\ W2)) by A1, Def2;

      hence thesis by A57, A16, A69, Def2;

    end;

    theorem :: RLVECT_5:36

    ( dim (W1 /\ W2)) >= ((( dim W1) + ( dim W2)) - ( dim V))

    proof

      

       A1: ( dim (W1 + W2)) <= ( dim V) & (( dim V) + (( dim (W1 /\ W2)) - ( dim V))) = ( dim (W1 /\ W2)) by Th28;

      ((( dim W1) + ( dim W2)) - ( dim V)) = ((( dim (W1 + W2)) + ( dim (W1 /\ W2))) - ( dim V)) by Th35

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

      hence thesis by A1, XREAL_1: 6;

    end;

    theorem :: RLVECT_5:37

    V is_the_direct_sum_of (W1,W2) implies ( dim V) = (( dim W1) + ( dim W2))

    proof

      assume

       A1: V is_the_direct_sum_of (W1,W2);

      then

       A2: the RLSStruct of V = (W1 + W2) by RLSUB_2:def 4;

      (W1 /\ W2) = ( (0). V) by A1, RLSUB_2:def 4;

      

      then ( (Omega). (W1 /\ W2)) = ( (0). V) by RLSUB_1:def 4

      .= ( (0). (W1 /\ W2)) by RLSUB_1: 36;

      then ( dim (W1 /\ W2)) = 0 by Th32;

      

      then (( dim W1) + ( dim W2)) = (( dim (W1 + W2)) + 0 ) by Th35

      .= ( dim ( (Omega). V)) by A2, RLSUB_1:def 4

      .= ( dim V) by Th30;

      hence thesis;

    end;

    

     Lm2: n <= ( dim V) implies ex W be strict Subspace of V st ( dim W) = n

    proof

      consider I be finite Subset of V such that

       A1: I is Basis of V by Def1;

      assume n <= ( dim V);

      then n <= ( card I) by A1, Def2;

      then

      consider A be finite Subset of I such that

       A2: ( card A) = n by FINSEQ_4: 72;

      reconsider A as Subset of V by XBOOLE_1: 1;

      reconsider W = ( Lin A) as strict finite-dimensional Subspace of V;

      I is linearly-independent by A1, RLVECT_3:def 3;

      then ( dim W) = n by A2, Th29, RLVECT_3: 5;

      hence thesis;

    end;

    theorem :: RLVECT_5:38

    n <= ( dim V) iff ex W be strict Subspace of V st ( dim W) = n by Lm2, Th28;

    definition

      let V be finite-dimensional RealLinearSpace, n be Element of NAT ;

      :: RLVECT_5:def3

      func n Subspaces_of V -> set means

      : Def3: for x be object holds x in it iff ex W be strict Subspace of V st W = x & ( dim W) = n;

      existence

      proof

        set S = { ( Lin A) where A be Subset of V : A is linearly-independent & ( card A) = n };

        take S;

        for x be object holds x in S iff ex W be strict Subspace of V st W = x & ( dim W) = n

        proof

          let x be object;

          hereby

            assume x in S;

            then

             A1: ex A be Subset of V st x = ( Lin A) & A is linearly-independent & ( card A) = n;

            then

            reconsider W = x as strict Subspace of V;

            ( dim W) = n by A1, Th29;

            hence ex W be strict Subspace of V st W = x & ( dim W) = n;

          end;

          given W be strict Subspace of V such that

           A2: W = x and

           A3: ( dim W) = n;

          consider A be finite Subset of W such that

           A4: A is Basis of W by Def1;

          reconsider A as Subset of W;

          A is linearly-independent by A4, RLVECT_3:def 3;

          then

          reconsider B = A as linearly-independent Subset of V by Th14;

          

           A5: x = ( Lin A) by A2, A4, RLVECT_3:def 3

          .= ( Lin B) by Th20;

          then ( card B) = n by A2, A3, Th29;

          hence thesis by A5;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be set;

        assume that

         A6: for x be object holds x in S1 iff ex W be strict Subspace of V st W = x & ( dim W) = n and

         A7: for x be object holds x in S2 iff ex W be strict Subspace of V st W = x & ( dim W) = n;

        for x be object holds x in S1 iff x in S2

        proof

          let x be object;

          hereby

            assume x in S1;

            then ex W be strict Subspace of V st W = x & ( dim W) = n by A6;

            hence x in S2 by A7;

          end;

          assume x in S2;

          then ex W be strict Subspace of V st W = x & ( dim W) = n by A7;

          hence thesis by A6;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: RLVECT_5:39

    n <= ( dim V) implies (n Subspaces_of V) is non empty

    proof

      assume n <= ( dim V);

      then ex W be strict Subspace of V st ( dim W) = n by Lm2;

      hence thesis by Def3;

    end;

    theorem :: RLVECT_5:40

    ( dim V) < n implies (n Subspaces_of V) = {}

    proof

      assume that

       A1: ( dim V) < n and

       A2: (n Subspaces_of V) <> {} ;

      consider x be object such that

       A3: x in (n Subspaces_of V) by A2, XBOOLE_0:def 1;

      ex W be strict Subspace of V st W = x & ( dim W) = n by A3, Def3;

      hence contradiction by A1, Th28;

    end;

    theorem :: RLVECT_5:41

    (n Subspaces_of W) c= (n Subspaces_of V)

    proof

      let x be object;

      assume x in (n Subspaces_of W);

      then

      consider W1 be strict Subspace of W such that

       A1: W1 = x and

       A2: ( dim W1) = n by Def3;

      reconsider W1 as strict Subspace of V by RLSUB_1: 27;

      W1 in (n Subspaces_of V) by A2, Def3;

      hence thesis by A1;

    end;