:: VECTSP_9 semantic presentation
begin
registration
let S be non empty 1-sorted ;
cluster non empty for Element of K27( the carrier of S);
existence
not for b1 being Subset of S holds b1 is empty
proof
set A = the non empty Subset of S;
the non empty Subset of S is Subset of S ;
hence not for b1 being Subset of S holds b1 is empty ; ::_thesis: verum
end;
end;
Lm1: for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
proof
let X, x be set ; ::_thesis: ( x in X implies (X \ {x}) \/ {x} = X )
assume x in X ; ::_thesis: (X \ {x}) \/ {x} = 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 (X \ {x}) \/ {x} = X ; ::_thesis: verum
end;
theorem Th1: :: VECTSP_9:1
for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for L being Linear_Combination of V
for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let V be VectSp of GF; ::_thesis: for L being Linear_Combination of V
for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let L be Linear_Combination of V; ::_thesis: for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let F, G be FinSequence of the carrier of V; ::_thesis: for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
set p = L (#) F;
set q = L (#) G;
let P be Permutation of (dom F); ::_thesis: ( G = F * P implies Sum (L (#) F) = Sum (L (#) G) )
assume A1: G = F * P ; ::_thesis: Sum (L (#) F) = Sum (L (#) G)
A2: len G = len F by A1, FINSEQ_2:44;
len F = len (L (#) F) by VECTSP_6:def_5;
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 (L (#) F) = len F by VECTSP_6:def_5;
then A6: dom F = dom (L (#) F) by FINSEQ_3:29;
len (L (#) G) = len G by VECTSP_6:def_5;
then A7: dom (L (#) F) = dom (L (#) G) by A5, A2, FINSEQ_3:29;
A8: dom F = dom G by A2, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_(L_(#)_G)_holds_
(L_(#)_G)_._k_=_r_._k
let k be Nat; ::_thesis: ( k in dom (L (#) G) implies (L (#) G) . k = r . k )
assume A9: k in dom (L (#) G) ; ::_thesis: (L (#) G) . k = r . k
set l = P . k;
( dom P = dom F & rng P = dom F ) by FUNCT_2:52, FUNCT_2:def_3;
then A10: P . k in dom F by A7, A6, A9, FUNCT_1:def_3;
then reconsider l = P . k as Element of NAT ;
G /. k = G . k by A7, A8, A6, A9, PARTFUN1:def_6
.= F . (P . k) by A1, A7, A8, A6, A9, FUNCT_1:12
.= F /. l by A10, PARTFUN1:def_6 ;
then (L (#) G) . k = (L . (F /. l)) * (F /. l) by A9, VECTSP_6:def_5
.= (L (#) F) . (P . k) by A6, A10, VECTSP_6:def_5
.= r . k by A7, A4, A9, FUNCT_1:12 ;
hence (L (#) G) . k = r . k ; ::_thesis: verum
end;
hence Sum (L (#) F) = Sum (L (#) G) by A3, A7, A4, FINSEQ_1:13, RLVECT_2:7; ::_thesis: verum
end;
theorem Th2: :: VECTSP_9:2
for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for F being FinSequence of the carrier of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for L being Linear_Combination of V
for F being FinSequence of the carrier of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V
let V be VectSp of GF; ::_thesis: for L being Linear_Combination of V
for F being FinSequence of the carrier of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V
let L be Linear_Combination of V; ::_thesis: for F being FinSequence of the carrier of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V
defpred S1[ FinSequence] means for G being FinSequence of the carrier of V st G = $1 & Carrier L misses rng G holds
Sum (L (#) G) = 0. V;
A1: for p being FinSequence
for x being set st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence; ::_thesis: for x being set st S1[p] holds
S1[p ^ <*x*>]
let x be set ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: S1[p] ; ::_thesis: S1[p ^ <*x*>]
let G be FinSequence of the carrier of V; ::_thesis: ( G = p ^ <*x*> & Carrier L misses rng G implies Sum (L (#) G) = 0. V )
assume A3: G = p ^ <*x*> ; ::_thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )
then reconsider p = 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 = x as Vector of V by A4;
assume Carrier L misses rng G ; ::_thesis: Sum (L (#) G) = 0. V
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;
now__::_thesis:_not_x_in_Carrier_L
A7: x in {x} by TARSKI:def_1;
assume x in Carrier L ; ::_thesis: contradiction
then x in (Carrier L) /\ {x} by A7, XBOOLE_0:def_4;
hence contradiction by A5; ::_thesis: verum
end;
then A8: L . x = 0. GF by VECTSP_6:2;
Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by A3, VECTSP_6:13
.= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41
.= (0. V) + (Sum <*((L . x) * x)*>) by A6, VECTSP_6:10
.= Sum <*((L . x) * x)*> by RLVECT_1:4
.= (0. GF) * x by A8, RLVECT_1:44
.= 0. V by VECTSP_1:15 ;
hence Sum (L (#) G) = 0. V ; ::_thesis: verum
end;
A9: S1[ {} ]
proof
let G be FinSequence of the carrier of V; ::_thesis: ( G = {} & Carrier L misses rng G implies Sum (L (#) G) = 0. V )
assume G = {} ; ::_thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )
then A10: L (#) G = <*> the carrier of V by VECTSP_6:9;
assume Carrier L misses rng G ; ::_thesis: Sum (L (#) G) = 0. V
thus Sum (L (#) G) = 0. V by A10, RLVECT_1:43; ::_thesis: verum
end;
A11: for p being FinSequence holds S1[p] from FINSEQ_1:sch_3(A9, A1);
let F be FinSequence of the carrier of V; ::_thesis: ( Carrier L misses rng F implies Sum (L (#) F) = 0. V )
assume Carrier L misses rng F ; ::_thesis: Sum (L (#) F) = 0. V
hence Sum (L (#) F) = 0. V by A11; ::_thesis: verum
end;
theorem Th3: :: VECTSP_9:3
for GF being Field
for V being VectSp of GF
for F being FinSequence of the carrier of V st F is one-to-one holds
for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for F being FinSequence of the carrier of V st F is one-to-one holds
for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L
let V be VectSp of GF; ::_thesis: for F being FinSequence of the carrier of V st F is one-to-one holds
for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L
let F be FinSequence of the carrier of V; ::_thesis: ( F is one-to-one implies for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L )
assume A1: F is one-to-one ; ::_thesis: for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L
rng F c= rng F ;
then reconsider X = rng F as Subset of (rng F) ;
let L be Linear_Combination of V; ::_thesis: ( Carrier L c= rng F implies Sum (L (#) F) = Sum L )
assume A2: Carrier L c= rng F ; ::_thesis: Sum (L (#) F) = Sum L
consider G being 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 VECTSP_6:def_6;
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 (F - (A `)) = rng G by FINSEQ_3:65;
F - (A `) is one-to-one by A1, FINSEQ_3:87;
then F - (A `),G are_fiberwise_equipotent by A3, A6, RFINSEQ:26;
then A7: ex Q being Permutation of (dom G) st F - (A `) = G * Q by RFINSEQ:4;
reconsider F1 = F - (A `), F2 = F - A as FinSequence of the carrier of V by FINSEQ_3:86;
rng F2 = (rng F) \ (rng G) by FINSEQ_3:65;
then A8: rng F2 misses rng G by XBOOLE_1:79;
ex P being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * P by FINSEQ_3:115;
then Sum (L (#) F) = Sum (L (#) (F1 ^ F2)) by Th1
.= Sum ((L (#) F1) ^ (L (#) F2)) by VECTSP_6:13
.= (Sum (L (#) F1)) + (Sum (L (#) F2)) by RLVECT_1:41
.= (Sum (L (#) F1)) + (0. V) by A4, A8, Th2
.= (Sum (L (#) G)) + (0. V) by A7, Th1
.= Sum L by A5, RLVECT_1:4 ;
hence Sum (L (#) F) = Sum L ; ::_thesis: verum
end;
theorem Th4: :: VECTSP_9:4
for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for F being FinSequence of the carrier of V ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for L being Linear_Combination of V
for F being FinSequence of the carrier of V ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )
let V be VectSp of GF; ::_thesis: for L being Linear_Combination of V
for F being FinSequence of the carrier of V ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )
let L be Linear_Combination of V; ::_thesis: for F being FinSequence of the carrier of V ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )
let F be FinSequence of the carrier of V; ::_thesis: ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )
defpred S1[ set , set ] means ( not $1 is Vector of V or ( $1 in rng F & $2 = L . $1 ) or ( not $1 in rng F & $2 = 0. GF ) );
reconsider R = rng F as finite Subset of V by FINSEQ_1:def_4;
A1: for x being set st x in the carrier of V holds
ex y being set st
( y in the carrier of GF & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st
( y in the carrier of GF & S1[x,y] ) )
assume x in the carrier of V ; ::_thesis: ex y being set st
( y in the carrier of GF & S1[x,y] )
then reconsider x9 = x as Vector of V ;
percases ( x in rng F or not x in rng F ) ;
suppose x in rng F ; ::_thesis: ex y being set st
( y in the carrier of GF & S1[x,y] )
then S1[x,L . x9] ;
hence ex y being set st
( y in the carrier of GF & S1[x,y] ) ; ::_thesis: verum
end;
suppose not x in rng F ; ::_thesis: ex y being set st
( y in the carrier of GF & S1[x,y] )
hence ex y being set st
( y in the carrier of GF & S1[x,y] ) ; ::_thesis: verum
end;
end;
end;
ex K being Function of the carrier of V, the carrier of GF st
for x being set st x in the carrier of V holds
S1[x,K . x] from FUNCT_2:sch_1(A1);
then consider K being Function of the carrier of V, the carrier of GF such that
A2: for x being set st x in the carrier of V holds
S1[x,K . x] ;
A3: now__::_thesis:_for_v_being_Vector_of_V_st_not_v_in_R_/\_(Carrier_L)_holds_
K_._v_=_0._GF
let v be Vector of V; ::_thesis: ( not v in R /\ (Carrier L) implies K . b1 = 0. GF )
assume A4: not v in R /\ (Carrier L) ; ::_thesis: K . b1 = 0. GF
percases ( not v in R or not v in Carrier L ) by A4, XBOOLE_0:def_4;
suppose not v in R ; ::_thesis: K . b1 = 0. GF
hence K . v = 0. GF by A2; ::_thesis: verum
end;
supposeA5: not v in Carrier L ; ::_thesis: K . b1 = 0. GF
( ( S1[v,K . v] & S1[v,L . v] ) or ( S1[v,K . v] & S1[v, 0. GF] ) ) by A2;
hence K . v = 0. GF by A5, VECTSP_6:2; ::_thesis: verum
end;
end;
end;
reconsider K = K as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
reconsider K = K as Linear_Combination of V by A3, VECTSP_6:def_1;
now__::_thesis:_for_v_being_set_st_v_in_(rng_F)_/\_(Carrier_L)_holds_
v_in_Carrier_K
let v be set ; ::_thesis: ( v in (rng F) /\ (Carrier L) implies v in Carrier K )
assume A6: v in (rng F) /\ (Carrier L) ; ::_thesis: v in Carrier K
then reconsider v9 = v as Vector of V ;
v in Carrier L by A6, XBOOLE_0:def_4;
then A7: L . v9 <> 0. GF by VECTSP_6:2;
v in R by A6, XBOOLE_0:def_4;
then K . v9 = L . v9 by A2;
hence v in Carrier K by A7, VECTSP_6:1; ::_thesis: verum
end;
then A8: (rng F) /\ (Carrier L) c= Carrier K by TARSKI:def_3;
take K ; ::_thesis: ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )
A9: L (#) F = K (#) F
proof
set p = L (#) F;
set q = K (#) F;
A10: len (L (#) F) = len F by VECTSP_6:def_5;
len (K (#) F) = len F by VECTSP_6:def_5;
then A11: dom (L (#) F) = dom (K (#) F) by A10, FINSEQ_3:29;
A12: dom (L (#) F) = dom F by A10, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_(L_(#)_F)_holds_
(L_(#)_F)_._k_=_(K_(#)_F)_._k
let k be Nat; ::_thesis: ( k in dom (L (#) F) implies (L (#) F) . k = (K (#) F) . k )
set u = F /. k;
A13: S1[F /. k,K . (F /. k)] by A2;
assume A14: k in dom (L (#) F) ; ::_thesis: (L (#) F) . k = (K (#) F) . k
then ( F /. k = F . k & (L (#) F) . k = (L . (F /. k)) * (F /. k) ) by A12, PARTFUN1:def_6, VECTSP_6:def_5;
hence (L (#) F) . k = (K (#) F) . k by A11, A12, A14, A13, FUNCT_1:def_3, VECTSP_6:def_5; ::_thesis: verum
end;
hence L (#) F = K (#) F by A11, FINSEQ_1:13; ::_thesis: verum
end;
now__::_thesis:_for_v_being_set_st_v_in_Carrier_K_holds_
v_in_(rng_F)_/\_(Carrier_L)
let v be set ; ::_thesis: ( v in Carrier K implies v in (rng F) /\ (Carrier L) )
assume v in Carrier K ; ::_thesis: v in (rng F) /\ (Carrier L)
then ex v9 being Vector of V st
( v9 = v & K . v9 <> 0. GF ) by VECTSP_6:1;
hence v in (rng F) /\ (Carrier L) by A3; ::_thesis: verum
end;
then Carrier K c= (rng F) /\ (Carrier L) by TARSKI:def_3;
hence ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) by A8, A9, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th5: :: VECTSP_9:5
for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for A being Subset of V
for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for L being Linear_Combination of V
for A being Subset of V
for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
let V be VectSp of GF; ::_thesis: for L being Linear_Combination of V
for A being Subset of V
for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
let L be Linear_Combination of V; ::_thesis: for A being Subset of V
for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
let A be Subset of V; ::_thesis: for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
defpred S1[ Nat] means for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) & len F = $1 holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let F be FinSequence of the carrier of V; ::_thesis: ( rng F c= the carrier of (Lin A) & len F = n + 1 implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume that
A3: rng F c= the carrier of (Lin A) and
A4: len F = n + 1 ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
consider G being FinSequence, x being set such that
A5: F = G ^ <*x*> by A4, FINSEQ_2:18;
reconsider G = 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, XBOOLE_1:1;
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 being Linear_Combination of A such that
A9: x = Sum LA1 by VECTSP_7:7;
x in V by A8, VECTSP_4:9;
then reconsider x = 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 being 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 VECTSP_6:31;
then A11: LA2 + ((L . x) * LA1) is Linear_Combination of A by VECTSP_6:24;
Sum (L (#) F) = Sum ((L (#) G) ^ (L (#) x9)) by A5, VECTSP_6:13
.= (Sum LA2) + (Sum (L (#) x9)) by A10, RLVECT_1:41
.= (Sum LA2) + (Sum <*((L . x) * x)*>) by VECTSP_6:10
.= (Sum LA2) + ((L . x) * (Sum LA1)) by A9, RLVECT_1:44
.= (Sum LA2) + (Sum ((L . x) * LA1)) by VECTSP_6:45
.= Sum (LA2 + ((L . x) * LA1)) by VECTSP_6:44 ;
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A11; ::_thesis: verum
end;
let F be FinSequence of the carrier of V; ::_thesis: ( rng F c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume A12: rng F c= the carrier of (Lin A) ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
A13: len F is Nat ;
A14: S1[ 0 ]
proof
let F be FinSequence of the carrier of V; ::_thesis: ( rng F c= the carrier of (Lin A) & len F = 0 implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume that
rng F c= the carrier of (Lin A) and
A15: len F = 0 ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
F = <*> the carrier of V by A15;
then L (#) F = <*> the carrier of V by VECTSP_6:9;
then A16: Sum (L (#) F) = 0. V by RLVECT_1:43
.= Sum (ZeroLC V) by VECTSP_6:15 ;
ZeroLC V is Linear_Combination of A by VECTSP_6:5;
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A16; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A14, A1);
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A12, A13; ::_thesis: verum
end;
theorem Th6: :: VECTSP_9:6
for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for L being Linear_Combination of V
for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K
let V be VectSp of GF; ::_thesis: for L being Linear_Combination of V
for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K
let L be Linear_Combination of V; ::_thesis: for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K
let A be Subset of V; ::_thesis: ( Carrier L c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum L = Sum K )
consider F being 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 VECTSP_6:def_6;
assume Carrier L c= the carrier of (Lin A) ; ::_thesis: ex K being Linear_Combination of A st Sum L = Sum K
then consider K being Linear_Combination of A such that
A3: Sum (L (#) F) = Sum K by A1, Th5;
take K ; ::_thesis: Sum L = Sum K
thus Sum L = Sum K by A2, A3; ::_thesis: verum
end;
theorem Th7: :: VECTSP_9:7
for GF being Field
for V being VectSp of GF
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let V be VectSp of GF; ::_thesis: for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let W be Subspace of V; ::_thesis: for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let L be Linear_Combination of V; ::_thesis: ( Carrier L c= the carrier of W implies for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K ) )
assume A1: Carrier L c= the carrier of W ; ::_thesis: for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let K be Linear_Combination of W; ::_thesis: ( K = L | the carrier of W implies ( Carrier L = Carrier K & Sum L = Sum K ) )
assume A2: K = L | the carrier of W ; ::_thesis: ( Carrier L = Carrier K & Sum L = Sum K )
A3: dom K = the carrier of W by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_Carrier_K_holds_
x_in_Carrier_L
let x be set ; ::_thesis: ( x in Carrier K implies x in Carrier L )
assume x in Carrier K ; ::_thesis: x in Carrier L
then consider w being Vector of W such that
A4: x = w and
A5: K . w <> 0. GF by VECTSP_6:1;
A6: w is Vector of V by VECTSP_4:10;
L . w <> 0. GF by A2, A3, A5, FUNCT_1:47;
hence x in Carrier L by A4, A6, VECTSP_6:1; ::_thesis: verum
end;
then A7: Carrier K c= Carrier L by TARSKI:def_3;
consider G being 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 VECTSP_6:def_6;
consider F being 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 VECTSP_6:def_6;
now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
x_in_Carrier_K
let x be set ; ::_thesis: ( x in Carrier L implies x in Carrier K )
assume A13: x in Carrier L ; ::_thesis: x in Carrier K
then consider v being Vector of V such that
A14: x = v and
A15: L . v <> 0. GF by VECTSP_6:1;
K . v <> 0. GF by A1, A2, A3, A13, A14, A15, FUNCT_1:47;
hence x in Carrier K by A1, A13, A14, VECTSP_6:1; ::_thesis: verum
end;
then A16: Carrier L c= Carrier K by TARSKI:def_3;
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 being Permutation of (dom G) such that
A18: F = G * P by RFINSEQ:4;
len (K (#) G) = len G by VECTSP_6:def_5;
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 VECTSP_6:def_5;
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 VECTSP_4:def_2;
rng q c= the carrier of W by FINSEQ_1:def_4;
then rng q c= the carrier of V by A22, XBOOLE_1:1;
then reconsider q9 = q as FinSequence of the carrier of V by FINSEQ_1:def_4;
consider f being Function of NAT, the carrier of W such that
A23: Sum q = f . (len q) and
A24: f . 0 = 0. W and
A25: for i being Element of NAT
for w being 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 Function of NAT, the carrier of V by A22, FUNCT_2:2, XBOOLE_1:1;
A26: for i being Element of NAT
for v being Vector of V st i < len q9 & v = q9 . (i + 1) holds
f9 . (i + 1) = (f9 . i) + v
proof
let i be Element of NAT ; ::_thesis: for v being Vector of V st i < len q9 & v = q9 . (i + 1) holds
f9 . (i + 1) = (f9 . i) + v
let v be Vector of V; ::_thesis: ( i < len q9 & v = q9 . (i + 1) implies f9 . (i + 1) = (f9 . i) + v )
assume that
A27: i < len q9 and
A28: v = q9 . (i + 1) ; ::_thesis: f9 . (i + 1) = (f9 . i) + v
( 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 f9 . (i + 1) = (f9 . i) + v by VECTSP_4:13; ::_thesis: verum
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, VECTSP_6:def_5;
then A31: dom (L (#) F) = dom G by FINSEQ_3:29;
A32: dom q = dom (K (#) G) by A20, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(L_(#)_F)_holds_
(L_(#)_F)_._i_=_q_._i
let i be Nat; ::_thesis: ( i in dom (L (#) F) implies (L (#) F) . i = q . i )
set v = F /. i;
set j = P . i;
assume A33: i in dom (L (#) F) ; ::_thesis: (L (#) F) . i = q . i
then A34: F /. i = F . i by A31, A30, PARTFUN1:def_6;
then F /. i in rng F by A31, A30, A33, FUNCT_1:def_3;
then reconsider w = F /. i 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: P . i in dom G by A31, A33, FUNCT_1:def_3;
then reconsider j = P . i as Element of NAT ;
A36: G /. j = G . (P . i) by A35, PARTFUN1:def_6
.= F /. i 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, VECTSP_6:def_5
.= (L . (F /. i)) * w by A2, A3, FUNCT_1:47
.= (L . (F /. i)) * (F /. i) by VECTSP_4:14 ;
hence (L (#) F) . i = q . i by A33, VECTSP_6:def_5; ::_thesis: verum
end;
then A37: L (#) F = (K (#) G) * P by A31, A21, FINSEQ_1:13;
len G = len (K (#) G) by VECTSP_6:def_5;
then dom G = dom (K (#) G) by FINSEQ_3:29;
then reconsider P = 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, VECTSP_4:11;
hence ( Carrier L = Carrier K & Sum L = Sum K ) by A7, A16, A12, A9, A37, A38, A23, A26, A39, RLVECT_1:def_12, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th8: :: VECTSP_9:8
for GF being Field
for V being VectSp of GF
for W being Subspace of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
let V be VectSp of GF; ::_thesis: for W being Subspace of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
let W be Subspace of V; ::_thesis: for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
let K be Linear_Combination of W; ::_thesis: ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
defpred S1[ set , set ] means ( ( $1 in W & $2 = K . $1 ) or ( not $1 in W & $2 = 0. GF ) );
reconsider K9 = K as Function of the carrier of W, the carrier of GF ;
A1: the carrier of W c= the carrier of V by VECTSP_4:def_2;
then reconsider C = Carrier K as finite Subset of V by XBOOLE_1:1;
A2: for x being set st x in the carrier of V holds
ex y being set st
( y in the carrier of GF & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st
( y in the carrier of GF & S1[x,y] ) )
assume x in the carrier of V ; ::_thesis: ex y being set st
( y in the carrier of GF & S1[x,y] )
then reconsider x = x as Vector of V ;
percases ( x in W or not x in W ) ;
supposeA3: x in W ; ::_thesis: ex y being set st
( y in the carrier of GF & S1[x,y] )
then reconsider x = x as Vector of W by STRUCT_0:def_5;
S1[x,K . x] by A3;
hence ex y being set st
( y in the carrier of GF & S1[x,y] ) ; ::_thesis: verum
end;
suppose not x in W ; ::_thesis: ex y being set st
( y in the carrier of GF & S1[x,y] )
hence ex y being set st
( y in the carrier of GF & S1[x,y] ) ; ::_thesis: verum
end;
end;
end;
ex L being Function of the carrier of V, the carrier of GF st
for x being set st x in the carrier of V holds
S1[x,L . x] from FUNCT_2:sch_1(A2);
then consider L being Function of the carrier of V, the carrier of GF such that
A4: for x being set st x in the carrier of V holds
S1[x,L . x] ;
A5: now__::_thesis:_for_v_being_Vector_of_V_st_not_v_in_C_holds_
L_._v_=_0._GF
let v be Vector of V; ::_thesis: ( not v in C implies L . v = 0. GF )
assume not v in C ; ::_thesis: L . v = 0. GF
then ( ( S1[v,K . v] & not v in C & v in the carrier of W ) or S1[v, 0. GF] ) by STRUCT_0:def_5;
then ( ( S1[v,K . v] & K . v = 0. GF ) or S1[v, 0. GF] ) by VECTSP_6:2;
hence L . v = 0. GF by A4; ::_thesis: verum
end;
L is Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
then reconsider L = L as Linear_Combination of V by A5, VECTSP_6:def_1;
reconsider L9 = L | the carrier of W as Function of the carrier of W, the carrier of GF by A1, FUNCT_2:32;
take L ; ::_thesis: ( Carrier K = Carrier L & Sum K = Sum L )
now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
x_in_the_carrier_of_W
let x be set ; ::_thesis: ( x in Carrier L implies x in the carrier of W )
assume that
A6: x in Carrier L and
A7: not x in the carrier of W ; ::_thesis: contradiction
consider v being Vector of V such that
A8: x = v and
A9: L . v <> 0. GF by A6, VECTSP_6:1;
S1[v, 0. GF] by A7, A8, STRUCT_0:def_5;
hence contradiction by A4, A9; ::_thesis: verum
end;
then A10: Carrier L c= the carrier of W by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_W_holds_
K9_._x_=_L9_._x
let x be set ; ::_thesis: ( x in the carrier of W implies K9 . x = L9 . x )
assume A11: x in the carrier of W ; ::_thesis: K9 . x = L9 . x
then S1[x,L . x] by A4, A1;
hence K9 . x = L9 . x by A11, FUNCT_1:49, STRUCT_0:def_5; ::_thesis: verum
end;
then K9 = L9 by FUNCT_2:12;
hence ( Carrier K = Carrier L & Sum K = Sum L ) by A10, Th7; ::_thesis: verum
end;
theorem Th9: :: VECTSP_9:9
for GF being Field
for V being VectSp of GF
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
let V be VectSp of GF; ::_thesis: for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
let W be Subspace of V; ::_thesis: for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
let L be Linear_Combination of V; ::_thesis: ( Carrier L c= the carrier of W implies ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L ) )
assume A1: Carrier L c= the carrier of W ; ::_thesis: ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
then reconsider C = Carrier L as finite Subset of W ;
the carrier of W c= the carrier of V by VECTSP_4:def_2;
then reconsider K = L | the carrier of W as Function of the carrier of W, the carrier of GF by FUNCT_2:32;
A2: K is Element of Funcs ( the carrier of W, the carrier of GF) by FUNCT_2:8;
A3: dom K = the carrier of W by FUNCT_2:def_1;
now__::_thesis:_for_w_being_Vector_of_W_st_not_w_in_C_holds_
K_._w_=_0._GF
let w be Vector of W; ::_thesis: ( not w in C implies K . w = 0. GF )
A4: w is Vector of V by VECTSP_4:10;
assume not w in C ; ::_thesis: K . w = 0. GF
then L . w = 0. GF by A4, VECTSP_6:2;
hence K . w = 0. GF by A3, FUNCT_1:47; ::_thesis: verum
end;
then reconsider K = K as Linear_Combination of W by A2, VECTSP_6:def_1;
take K ; ::_thesis: ( Carrier K = Carrier L & Sum K = Sum L )
thus ( Carrier K = Carrier L & Sum K = Sum L ) by A1, Th7; ::_thesis: verum
end;
theorem Th10: :: VECTSP_9:10
for GF being Field
for V being VectSp of GF
for I being Basis of V
for v being Vector of V holds v in Lin I
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for I being Basis of V
for v being Vector of V holds v in Lin I
let V be VectSp of GF; ::_thesis: for I being Basis of V
for v being Vector of V holds v in Lin I
let I be Basis of V; ::_thesis: for v being Vector of V holds v in Lin I
let v be Vector of V; ::_thesis: v in Lin I
v in VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by STRUCT_0:def_5;
hence v in Lin I by VECTSP_7:def_3; ::_thesis: verum
end;
registration
let GF be Field;
let V be VectSp of GF;
cluster linearly-independent for Element of K27( the carrier of V);
existence
ex b1 being Subset of V st b1 is linearly-independent
proof
take {} V ; ::_thesis: {} V is linearly-independent
thus {} V is linearly-independent ; ::_thesis: verum
end;
end;
theorem Th11: :: VECTSP_9:11
for GF being Field
for V being VectSp of GF
for W being Subspace of V
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
let V be VectSp of GF; ::_thesis: for W being Subspace of V
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
let W be Subspace of V; ::_thesis: for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
let A be Subset of W; ::_thesis: ( A is linearly-independent implies A is linearly-independent Subset of V )
the carrier of W c= the carrier of V by VECTSP_4:def_2;
then reconsider A9 = A as Subset of V by XBOOLE_1:1;
assume A1: A is linearly-independent ; ::_thesis: A is linearly-independent Subset of V
now__::_thesis:_not_A9_is_linearly-dependent
assume A9 is linearly-dependent ; ::_thesis: contradiction
then consider L being Linear_Combination of A9 such that
A2: Sum L = 0. V and
A3: Carrier L <> {} by VECTSP_7:def_1;
Carrier L c= A9 by VECTSP_6:def_4;
then consider LW being Linear_Combination of W such that
A4: Carrier LW = Carrier L and
A5: Sum LW = Sum L by Th9, XBOOLE_1:1;
reconsider LW = LW as Linear_Combination of A by A4, VECTSP_6:def_4;
Sum LW = 0. W by A2, A5, VECTSP_4:11;
hence contradiction by A1, A3, A4, VECTSP_7:def_1; ::_thesis: verum
end;
hence A is linearly-independent Subset of V ; ::_thesis: verum
end;
theorem Th12: :: VECTSP_9:12
for GF being Field
for V being VectSp of GF
for W being Subspace of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let V be VectSp of GF; ::_thesis: for W being Subspace of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let W be Subspace of V; ::_thesis: for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let A be Subset of V; ::_thesis: ( A is linearly-independent & A c= the carrier of W implies A is linearly-independent Subset of W )
assume that
A1: A is linearly-independent and
A2: A c= the carrier of W ; ::_thesis: A is linearly-independent Subset of W
reconsider A9 = A as Subset of W by A2;
now__::_thesis:_not_A9_is_linearly-dependent
assume A9 is linearly-dependent ; ::_thesis: contradiction
then consider K being Linear_Combination of A9 such that
A3: Sum K = 0. W and
A4: Carrier K <> {} by VECTSP_7:def_1;
consider L being Linear_Combination of V such that
A5: Carrier L = Carrier K and
A6: Sum L = Sum K by Th8;
reconsider L = L as Linear_Combination of A by A5, VECTSP_6:def_4;
Sum L = 0. V by A3, A6, VECTSP_4:11;
hence contradiction by A1, A4, A5, VECTSP_7:def_1; ::_thesis: verum
end;
hence A is linearly-independent Subset of W ; ::_thesis: verum
end;
theorem Th13: :: VECTSP_9:13
for GF being Field
for V being VectSp of GF
for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
let V be VectSp of GF; ::_thesis: for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
let W be Subspace of V; ::_thesis: for A being Basis of W ex B being Basis of V st A c= B
let A be Basis of W; ::_thesis: ex B being Basis of V st A c= B
A is linearly-independent by VECTSP_7:def_3;
then reconsider B = A as linearly-independent Subset of V by Th11;
consider I being Basis of V such that
A1: B c= I by VECTSP_7:19;
take I ; ::_thesis: A c= I
thus A c= I by A1; ::_thesis: verum
end;
theorem Th14: :: VECTSP_9:14
for GF being Field
for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
let V be VectSp of GF; ::_thesis: for A being Subset of V st A is linearly-independent holds
for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
let A be Subset of V; ::_thesis: ( A is linearly-independent implies for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B )
assume A1: A is linearly-independent ; ::_thesis: for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
let v be Vector of V; ::_thesis: ( v in A implies for B being Subset of V st B = A \ {v} holds
not v in Lin B )
assume v in A ; ::_thesis: for B being Subset of V st B = A \ {v} holds
not v in Lin B
then A2: {v} is Subset of A by SUBSET_1:41;
v in {v} by TARSKI:def_1;
then v in Lin {v} by VECTSP_7:8;
then consider K being Linear_Combination of {v} such that
A3: v = Sum K by VECTSP_7:7;
let B be Subset of V; ::_thesis: ( B = A \ {v} implies not v in Lin B )
assume A4: B = A \ {v} ; ::_thesis: not v in Lin B
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 ; ::_thesis: contradiction
then consider L being Linear_Combination of B such that
A6: v = Sum L by VECTSP_7:7;
A7: ( Carrier L c= B & Carrier K c= {v} ) by VECTSP_6:def_4;
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, VECTSP_6:41, XBOOLE_1:1;
then Carrier (L - K) c= A by XBOOLE_1:1;
then A8: L - K is Linear_Combination of A by VECTSP_6:def_4;
A9: for x being Vector of V st x in Carrier L holds
K . x = 0. GF
proof
let x be Vector of V; ::_thesis: ( x in Carrier L implies K . x = 0. GF )
assume x in Carrier L ; ::_thesis: K . x = 0. GF
then not x in Carrier K by A4, A7, XBOOLE_0:def_5;
hence K . x = 0. GF by VECTSP_6:2; ::_thesis: verum
end;
A10: now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
x_in_Carrier_(L_-_K)
let x be set ; ::_thesis: ( x in Carrier L implies x in Carrier (L - K) )
assume that
A11: x in Carrier L and
A12: not x in Carrier (L - K) ; ::_thesis: contradiction
reconsider x = x as Vector of V by A11;
A13: L . x <> 0. GF by A11, VECTSP_6:2;
(L - K) . x = (L . x) - (K . x) by VECTSP_6:40
.= (L . x) - (0. GF) by A9, A11
.= (L . x) + (- (0. GF)) by RLVECT_1:def_11
.= (L . x) + (0. GF) by RLVECT_1:12
.= L . x by RLVECT_1:4 ;
hence contradiction by A12, A13, VECTSP_6:2; ::_thesis: verum
end;
{v} is linearly-independent by A1, A2, VECTSP_7:1;
then v <> 0. V by VECTSP_7:3;
then Carrier L <> {} by A6, VECTSP_6:19;
then ex w being set st w in Carrier L by XBOOLE_0:def_1;
then A14: not Carrier (L - K) is empty by A10;
0. V = (Sum L) + (- (Sum K)) by A6, A3, RLVECT_1:def_10
.= (Sum L) + (Sum (- K)) by VECTSP_6:46
.= Sum (L + (- K)) by VECTSP_6:44
.= Sum (L - K) by VECTSP_6:def_11 ;
hence contradiction by A1, A8, A14, VECTSP_7:def_1; ::_thesis: verum
end;
theorem Th15: :: VECTSP_9:15
for GF being Field
for V being VectSp of GF
for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
let V be VectSp of GF; ::_thesis: for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
let I be Basis of V; ::_thesis: for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
let A be non empty Subset of V; ::_thesis: ( A misses I implies for B being Subset of V st B = I \/ A holds
B is linearly-dependent )
assume A1: A misses I ; ::_thesis: for B being Subset of V st B = I \/ A holds
B is linearly-dependent
consider v being set such that
A2: v in A by XBOOLE_0:def_1;
let B be Subset of V; ::_thesis: ( B = I \/ A implies B is linearly-dependent )
assume A3: B = I \/ A ; ::_thesis: B is linearly-dependent
A4: A c= B by A3, XBOOLE_1:7;
reconsider v = 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 VECTSP_7:13;
assume A7: B is linearly-independent ; ::_thesis: contradiction
v in Lin I by Th10;
hence contradiction by A7, A2, A4, A6, Th14, VECTSP_4:8; ::_thesis: verum
end;
theorem Th16: :: VECTSP_9:16
for GF being Field
for V being VectSp of GF
for W being Subspace of V
for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V
for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
let V be VectSp of GF; ::_thesis: for W being Subspace of V
for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
let W be Subspace of V; ::_thesis: for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
let A be Subset of V; ::_thesis: ( A c= the carrier of W implies Lin A is Subspace of W )
assume A1: A c= the carrier of W ; ::_thesis: Lin A is Subspace of W
now__::_thesis:_for_w_being_set_st_w_in_the_carrier_of_(Lin_A)_holds_
w_in_the_carrier_of_W
let w be set ; ::_thesis: ( w in the carrier of (Lin A) implies w in the carrier of W )
assume w in the carrier of (Lin A) ; ::_thesis: w in the carrier of W
then w in Lin A by STRUCT_0:def_5;
then consider L being Linear_Combination of A such that
A2: w = Sum L by VECTSP_7:7;
Carrier L c= A by VECTSP_6:def_4;
then ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum L = Sum K ) by A1, Th9, XBOOLE_1:1;
hence w in the carrier of W by A2; ::_thesis: verum
end;
then the carrier of (Lin A) c= the carrier of W by TARSKI:def_3;
hence Lin A is Subspace of W by VECTSP_4:27; ::_thesis: verum
end;
theorem Th17: :: VECTSP_9:17
for GF being Field
for V being VectSp of GF
for W being Subspace of V
for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V
for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
let V be VectSp of GF; ::_thesis: for W being Subspace of V
for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
let W be Subspace of V; ::_thesis: for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
let A be Subset of V; ::_thesis: for B being Subset of W st A = B holds
Lin A = Lin B
let B be Subset of W; ::_thesis: ( A = B implies Lin A = Lin B )
reconsider B9 = Lin B, V9 = V as VectSp of GF ;
A1: B9 is Subspace of V9 by VECTSP_4:26;
assume A2: A = B ; ::_thesis: Lin A = Lin B
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Lin_A)_holds_
x_in_the_carrier_of_(Lin_B)
let x be set ; ::_thesis: ( x in the carrier of (Lin A) implies x in the carrier of (Lin B) )
assume x in the carrier of (Lin A) ; ::_thesis: x in the carrier of (Lin B)
then x in Lin A by STRUCT_0:def_5;
then consider L being Linear_Combination of A such that
A3: x = Sum L by VECTSP_7:7;
Carrier L c= A by VECTSP_6:def_4;
then consider K being Linear_Combination of W such that
A4: Carrier K = Carrier L and
A5: Sum K = Sum L by A2, Th9, XBOOLE_1:1;
reconsider K = K as Linear_Combination of B by A2, A4, VECTSP_6:def_4;
x = Sum K by A3, A5;
then x in Lin B by VECTSP_7:7;
hence x in the carrier of (Lin B) by STRUCT_0:def_5; ::_thesis: verum
end;
then A6: the carrier of (Lin A) c= the carrier of (Lin B) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Lin_B)_holds_
x_in_the_carrier_of_(Lin_A)
let x be set ; ::_thesis: ( x in the carrier of (Lin B) implies x in the carrier of (Lin A) )
assume x in the carrier of (Lin B) ; ::_thesis: x in the carrier of (Lin A)
then x in Lin B by STRUCT_0:def_5;
then consider K being Linear_Combination of B such that
A7: x = Sum K by VECTSP_7:7;
consider L being Linear_Combination of V such that
A8: Carrier L = Carrier K and
A9: Sum L = Sum K by Th8;
reconsider L = L as Linear_Combination of A by A2, A8, VECTSP_6:def_4;
x = Sum L by A7, A9;
then x in Lin A by VECTSP_7:7;
hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;
then the carrier of (Lin B) c= the carrier of (Lin A) by TARSKI:def_3;
then the carrier of (Lin A) = the carrier of (Lin B) by A6, XBOOLE_0:def_10;
hence Lin A = Lin B by A1, VECTSP_4:29; ::_thesis: verum
end;
begin
theorem Th18: :: VECTSP_9:18
for GF being Field
for V being VectSp of GF
for A, B being finite Subset of V
for v being Vector of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being Vector of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A, B being finite Subset of V
for v being Vector of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being Vector of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
let V be VectSp of GF; ::_thesis: for A, B being finite Subset of V
for v being Vector of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being Vector of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
let A, B be finite Subset of V; ::_thesis: for v being Vector of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being Vector of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
let v be Vector of V; ::_thesis: ( v in Lin (A \/ B) & not v in Lin B implies ex w being Vector of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) )
assume that
A1: v in Lin (A \/ B) and
A2: not v in Lin B ; ::_thesis: ex w being Vector of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
consider L being Linear_Combination of A \/ B such that
A3: v = Sum L by A1, VECTSP_7:7;
v in {v} by TARSKI:def_1;
then v in Lin {v} by VECTSP_7:8;
then consider Lv being Linear_Combination of {v} such that
A4: v = Sum Lv by VECTSP_7:7;
A5: Carrier L c= A \/ B by VECTSP_6:def_4;
now__::_thesis:_ex_w_being_Vector_of_V_st_
(_w_in_A_&_not_L_._w_=_0._GF_)
assume A6: for w being Vector of V st w in A holds
L . w = 0. GF ; ::_thesis: contradiction
now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
not_x_in_A
let x be set ; ::_thesis: ( x in Carrier L implies not x in A )
assume that
A7: x in Carrier L and
A8: x in A ; ::_thesis: contradiction
ex u being Vector of V st
( x = u & L . u <> 0. GF ) by A7, VECTSP_6:1;
hence contradiction by A6, A8; ::_thesis: verum
end;
then Carrier L misses A by XBOOLE_0:3;
then Carrier L c= B by A5, XBOOLE_1:73;
then L is Linear_Combination of B by VECTSP_6:def_4;
hence contradiction by A2, A3, VECTSP_7:7; ::_thesis: verum
end;
then consider w being Vector of V such that
A9: w in A and
A10: L . w <> 0. GF ;
set a = L . w;
take w ; ::_thesis: ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
consider F being FinSequence of the carrier of V such that
A11: F is one-to-one and
A12: rng F = Carrier L and
A13: Sum L = Sum (L (#) F) by VECTSP_6:def_6;
A14: w in Carrier L by A10, VECTSP_6:1;
then reconsider Fw1 = F -| w as FinSequence of the carrier of V by A12, FINSEQ_4:41;
reconsider Fw2 = F |-- w as FinSequence of the carrier of V by A12, A14, FINSEQ_4:50;
A15: rng Fw1 misses rng Fw2 by A11, A12, A14, FINSEQ_4:57;
set Fw = Fw1 ^ Fw2;
F just_once_values w by A11, A12, A14, FINSEQ_4:8;
then A16: Fw1 ^ Fw2 = F - {w} by FINSEQ_4:54;
then A17: rng (Fw1 ^ Fw2) = (Carrier L) \ {w} by A12, FINSEQ_3:65;
F = ((F -| w) ^ <*w*>) ^ (F |-- w) by A12, A14, FINSEQ_4:51;
then F = Fw1 ^ (<*w*> ^ Fw2) by FINSEQ_1:32;
then L (#) F = (L (#) Fw1) ^ (L (#) (<*w*> ^ Fw2)) by VECTSP_6:13
.= (L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2)) by VECTSP_6:13
.= ((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2) by FINSEQ_1:32
.= ((L (#) Fw1) ^ <*((L . w) * w)*>) ^ (L (#) Fw2) by VECTSP_6:10 ;
then A18: Sum (L (#) F) = Sum ((L (#) Fw1) ^ (<*((L . w) * w)*> ^ (L (#) Fw2))) by FINSEQ_1:32
.= (Sum (L (#) Fw1)) + (Sum (<*((L . w) * w)*> ^ (L (#) Fw2))) by RLVECT_1:41
.= (Sum (L (#) Fw1)) + ((Sum <*((L . w) * w)*>) + (Sum (L (#) Fw2))) by RLVECT_1:41
.= (Sum (L (#) Fw1)) + ((Sum (L (#) Fw2)) + ((L . w) * w)) by RLVECT_1:44
.= ((Sum (L (#) Fw1)) + (Sum (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:def_3
.= (Sum ((L (#) Fw1) ^ (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:41
.= (Sum (L (#) (Fw1 ^ Fw2))) + ((L . w) * w) by VECTSP_6:13 ;
consider K being Linear_Combination of V such that
A19: Carrier K = (rng (Fw1 ^ Fw2)) /\ (Carrier L) and
A20: L (#) (Fw1 ^ Fw2) = K (#) (Fw1 ^ Fw2) by Th4;
rng (Fw1 ^ Fw2) = (rng F) \ {w} by A16, FINSEQ_3:65;
then A21: Carrier K = rng (Fw1 ^ Fw2) by A12, A19, XBOOLE_1:28;
A22: (Carrier L) \ {w} c= (A \/ B) \ {w} by A5, XBOOLE_1:33;
then reconsider K = K as Linear_Combination of (A \/ B) \ {w} by A17, A21, VECTSP_6:def_4;
set LC = ((L . w) ") * ((- K) + Lv);
Carrier ((- K) + Lv) c= (Carrier (- K)) \/ (Carrier Lv) by VECTSP_6:23;
then A23: Carrier ((- K) + Lv) c= (Carrier K) \/ (Carrier Lv) by VECTSP_6:38;
Carrier Lv c= {v} by VECTSP_6:def_4;
then (Carrier K) \/ (Carrier Lv) c= ((A \/ B) \ {w}) \/ {v} by A17, A21, A22, XBOOLE_1:13;
then ( Carrier (((L . w) ") * ((- K) + Lv)) c= Carrier ((- K) + Lv) & Carrier ((- K) + Lv) c= ((A \/ B) \ {w}) \/ {v} ) by A23, VECTSP_6:28, XBOOLE_1:1;
then Carrier (((L . w) ") * ((- K) + Lv)) c= ((A \/ B) \ {w}) \/ {v} by XBOOLE_1:1;
then A24: ((L . w) ") * ((- K) + Lv) is Linear_Combination of ((A \/ B) \ {w}) \/ {v} by VECTSP_6:def_4;
( Fw1 is one-to-one & Fw2 is one-to-one ) by A11, A12, A14, FINSEQ_4:52, FINSEQ_4:53;
then Fw1 ^ Fw2 is one-to-one by A15, FINSEQ_3:91;
then Sum (K (#) (Fw1 ^ Fw2)) = Sum K by A21, VECTSP_6:def_6;
then ((L . w) ") * v = (((L . w) ") * (Sum K)) + (((L . w) ") * ((L . w) * w)) by A3, A13, A18, A20, VECTSP_1:def_14
.= (((L . w) ") * (Sum K)) + w by A10, VECTSP_1:20 ;
then w = (((L . w) ") * v) - (((L . w) ") * (Sum K)) by VECTSP_2:2
.= ((L . w) ") * (v - (Sum K)) by VECTSP_1:23
.= ((L . w) ") * ((- (Sum K)) + v) by RLVECT_1:def_11 ;
then w = ((L . w) ") * ((Sum (- K)) + (Sum Lv)) by A4, VECTSP_6:46
.= ((L . w) ") * (Sum ((- K) + Lv)) by VECTSP_6:44
.= Sum (((L . w) ") * ((- K) + Lv)) by VECTSP_6:45 ;
hence ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) by A9, A24, VECTSP_7:7; ::_thesis: verum
end;
theorem Th19: :: VECTSP_9:19
for GF being Field
for V being VectSp of GF
for A, B being finite Subset of V st VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A, B being finite Subset of V st VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
let V be VectSp of GF; ::_thesis: for A, B being finite Subset of V st VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
defpred S1[ Nat] means for n being Nat
for A, B being finite Subset of V st card A = n & card B = $1 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds
( $1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - $1 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) );
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; ::_thesis: S1[m + 1]
let n be Nat; ::_thesis: for A, B being finite Subset of V st card A = n & card B = m + 1 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds
( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
let A, B be finite Subset of V; ::_thesis: ( card A = n & card B = m + 1 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent implies ( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) ) )
assume that
A3: card A = n and
A4: card B = m + 1 and
A5: VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A and
A6: B is linearly-independent ; ::_thesis: ( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
consider v being set such that
A7: v in B by A4, CARD_1:27, XBOOLE_0:def_1;
reconsider v = v as Vector of V by A7;
set Bv = B \ {v};
A8: B \ {v} is linearly-independent by A6, VECTSP_7:1, 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 being finite Subset of V such that
A10: C c= A and
A11: card C = n - m and
A12: VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A8;
A13: not v in Lin (B \ {v}) by A6, A7, Th14;
A14: now__::_thesis:_not_m_=_n
assume m = n ; ::_thesis: contradiction
then consider C being finite Subset of V such that
C c= A and
A15: card C = m - m and
A16: VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A9, A8;
C = {} by A15;
then B \ {v} is Basis of V by A8, A16, VECTSP_7:def_3;
hence contradiction by A13, Th10; ::_thesis: verum
end;
v in Lin ((B \ {v}) \/ C) by A12, STRUCT_0:def_5;
then consider w being Vector of V such that
A17: w in C and
A18: w in Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) by A13, Th18;
set Cw = C \ {w};
((B \ {v}) \ {w}) \/ {v} c= (B \ {v}) \/ {v} by XBOOLE_1:9, XBOOLE_1:36;
then (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= (C \ {w}) \/ ((B \ {v}) \/ {v}) by XBOOLE_1:9;
then A19: (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= B \/ (C \ {w}) by A7, Lm1;
{w} is Subset of C by A17, SUBSET_1:41;
then A20: card (C \ {w}) = (card C) - (card {w}) by CARD_2:44
.= (n - m) - 1 by A11, CARD_1:30
.= n - (m + 1) ;
C \ {w} c= C by XBOOLE_1:36;
then A21: C \ {w} c= A by A10, XBOOLE_1:1;
((C \/ (B \ {v})) \ {w}) \/ {v} = ((C \ {w}) \/ ((B \ {v}) \ {w})) \/ {v} by XBOOLE_1:42
.= (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) by XBOOLE_1:4 ;
then Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) is Subspace of Lin (B \/ (C \ {w})) by A19, VECTSP_7:13;
then A22: w in Lin (B \/ (C \ {w})) by A18, VECTSP_4:8;
A23: ( B \ {v} c= B & C = (C \ {w}) \/ {w} ) by A17, Lm1, XBOOLE_1:36;
now__::_thesis:_for_x_being_set_st_x_in_(B_\_{v})_\/_C_holds_
x_in_the_carrier_of_(Lin_(B_\/_(C_\_{w})))
let x be set ; ::_thesis: ( x in (B \ {v}) \/ C implies x in the carrier of (Lin (B \/ (C \ {w}))) )
assume x in (B \ {v}) \/ C ; ::_thesis: x in the carrier of (Lin (B \/ (C \ {w})))
then ( x in B \ {v} or x in C ) by XBOOLE_0:def_3;
then ( x in B or x in C \ {w} or x in {w} ) by A23, XBOOLE_0:def_3;
then ( x in B \/ (C \ {w}) or x in {w} ) by XBOOLE_0:def_3;
then ( x in Lin (B \/ (C \ {w})) or x = w ) by TARSKI:def_1, VECTSP_7:8;
hence x in the carrier of (Lin (B \/ (C \ {w}))) by A22, STRUCT_0:def_5; ::_thesis: verum
end;
then (B \ {v}) \/ C c= the carrier of (Lin (B \/ (C \ {w}))) by TARSKI:def_3;
then Lin ((B \ {v}) \/ C) is Subspace of Lin (B \/ (C \ {w})) by Th16;
then A24: the carrier of (Lin ((B \ {v}) \/ C)) c= the carrier of (Lin (B \/ (C \ {w}))) by VECTSP_4:def_2;
the carrier of (Lin (B \/ (C \ {w}))) c= the carrier of V by VECTSP_4:def_2;
then the carrier of (Lin (B \/ (C \ {w}))) = the carrier of V by A12, A24, XBOOLE_0:def_10;
then A25: VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ (C \ {w})) by A12, VECTSP_4:29;
m <= n by A2, A3, A5, A9, A8;
then m < n by A14, XXREAL_0:1;
hence ( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) ) by A21, A20, A25, NAT_1:13; ::_thesis: verum
end;
A26: S1[ 0 ]
proof
let n be Nat; ::_thesis: for A, B being finite Subset of V st card A = n & card B = 0 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds
( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
let A, B be finite Subset of V; ::_thesis: ( card A = n & card B = 0 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent implies ( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) ) )
assume that
A27: card A = n and
A28: card B = 0 and
A29: VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A and
B is linearly-independent ; ::_thesis: ( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
B = {} by A28;
then A = B \/ A ;
hence ( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) ) by A27, A29; ::_thesis: verum
end;
A30: for m being Nat holds S1[m] from NAT_1:sch_2(A26, A1);
let A, B be finite Subset of V; ::_thesis: ( VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent implies ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) ) )
assume ( VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent ) ; ::_thesis: ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
hence ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) ) by A30; ::_thesis: verum
end;
begin
theorem Th20: :: VECTSP_9:20
for GF being Field
for V being VectSp of GF st V is finite-dimensional holds
for I being Basis of V holds I is finite
proof
let GF be Field; ::_thesis: for V being VectSp of GF st V is finite-dimensional holds
for I being Basis of V holds I is finite
let V be VectSp of GF; ::_thesis: ( V is finite-dimensional implies for I being Basis of V holds I is finite )
assume V is finite-dimensional ; ::_thesis: for I being Basis of V holds I is finite
then consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def_1;
let B be Basis of V; ::_thesis: B is finite
consider p being FinSequence such that
A2: rng p = A by FINSEQ_1:52;
reconsider p = p as FinSequence of the carrier of V by A2, FINSEQ_1:def_4;
set Car = { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ;
set C = union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ;
A3: union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } or x in B )
assume x in union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ; ::_thesis: x in B
then consider R being set such that
A4: x in R and
A5: R in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } by TARSKI:def_4;
ex L being Linear_Combination of B st
( R = Carrier L & ex i being Nat st
( i in dom p & Sum L = p . i ) ) by A5;
then R c= B by VECTSP_6:def_4;
hence x in B by A4; ::_thesis: verum
end;
then reconsider C = union { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } as Subset of V by XBOOLE_1:1;
for v being Vector of V holds
( v in (Omega). V iff v in Lin C )
proof
let v be Vector of V; ::_thesis: ( v in (Omega). V iff v in Lin C )
hereby ::_thesis: ( v in Lin C implies v in (Omega). V )
assume v in (Omega). V ; ::_thesis: v in Lin C
then v in VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def_4;
then v in Lin A by A1, VECTSP_7:def_3;
then consider LA being Linear_Combination of A such that
A6: v = Sum LA by VECTSP_7:7;
Carrier LA c= the carrier of (Lin C)
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in Carrier LA or w in the carrier of (Lin C) )
assume A7: w in Carrier LA ; ::_thesis: w in the carrier of (Lin C)
then reconsider w9 = w as Vector of V ;
w9 in Lin B by Th10;
then consider LB being Linear_Combination of B such that
A8: w = Sum LB by VECTSP_7:7;
A9: Carrier LA c= A by VECTSP_6:def_4;
ex i being Nat st
( i in dom p & w = p . i )
proof
consider i being set such that
A10: i in dom p and
A11: w = p . i by A2, A7, A9, FUNCT_1:def_3;
reconsider i = i as Element of NAT by A10;
take i ; ::_thesis: ( i in dom p & w = p . i )
thus ( i in dom p & w = p . i ) by A10, A11; ::_thesis: verum
end;
then A12: Carrier LB in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } by A8;
Carrier LB c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier LB or x in C )
assume x in Carrier LB ; ::_thesis: x in C
hence x in C by A12, TARSKI:def_4; ::_thesis: verum
end;
then LB is Linear_Combination of C by VECTSP_6:def_4;
then w in Lin C by A8, VECTSP_7:7;
hence w in the carrier of (Lin C) by STRUCT_0:def_5; ::_thesis: verum
end;
then ex LC being Linear_Combination of C st Sum LA = Sum LC by Th6;
hence v in Lin C by A6, VECTSP_7:7; ::_thesis: verum
end;
assume v in Lin C ; ::_thesis: v in (Omega). V
v in the carrier of VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ;
then v in the carrier of ((Omega). V) by VECTSP_4:def_4;
hence v in (Omega). V by STRUCT_0:def_5; ::_thesis: verum
end;
then (Omega). V = Lin C by VECTSP_4:30;
then A13: VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin C by VECTSP_4:def_4;
A14: B is linearly-independent by VECTSP_7:def_3;
then C is linearly-independent by A3, VECTSP_7:1;
then A15: C is Basis of V by A13, VECTSP_7:def_3;
B c= C
proof
set D = B \ C;
assume not B c= C ; ::_thesis: contradiction
then ex v being set st
( v in B & not v in C ) by TARSKI:def_3;
then reconsider D = B \ C as non empty Subset of V by XBOOLE_0:def_5;
reconsider B = 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 A14, A15, Th15, XBOOLE_1:79; ::_thesis: verum
end;
then A16: B = C by A3, XBOOLE_0:def_10;
defpred S1[ set , set ] means ex L being Linear_Combination of B st
( $2 = Carrier L & Sum L = p . $1 );
A17: for i being Nat st i in Seg (len p) holds
ex x being set st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len p) implies ex x being set st S1[i,x] )
assume i in Seg (len p) ; ::_thesis: ex x being set st S1[i,x]
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 Th10;
then consider L being Linear_Combination of B such that
A18: p . i = Sum L by VECTSP_7:7;
S1[i, Carrier L] by A18;
hence ex x being set st S1[i,x] ; ::_thesis: verum
end;
ex q being FinSequence st
( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S1[i,q . i] ) ) from FINSEQ_1:sch_1(A17);
then consider q being FinSequence such that
A19: dom q = Seg (len p) and
A20: for i being Nat st i in Seg (len p) holds
S1[i,q . i] ;
A21: dom p = dom q by A19, FINSEQ_1:def_3;
A22: for i being Nat
for y1, y2 being set st i in Seg (len p) & S1[i,y1] & S1[i,y2] holds
y1 = y2
proof
let i be Nat; ::_thesis: for y1, y2 being set st i in Seg (len p) & S1[i,y1] & S1[i,y2] holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( i in Seg (len p) & S1[i,y1] & S1[i,y2] implies y1 = y2 )
assume that
i in Seg (len p) and
A23: S1[i,y1] and
A24: S1[i,y2] ; ::_thesis: y1 = y2
consider L1 being Linear_Combination of B such that
A25: ( y1 = Carrier L1 & Sum L1 = p . i ) by A23;
consider L2 being Linear_Combination of B such that
A26: ( y2 = Carrier L2 & Sum L2 = p . i ) by A24;
( Carrier L1 c= B & Carrier L2 c= B ) by VECTSP_6:def_4;
hence y1 = y2 by A14, A25, A26, MATRLIN:5; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in__{__(Carrier_L)_where_L_is_Linear_Combination_of_B_:_ex_i_being_Nat_st_
(_i_in_dom_p_&_Sum_L_=_p_._i_)__}__holds_
x_in_rng_q
let x be set ; ::_thesis: ( x in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } implies x in rng q )
assume x in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ; ::_thesis: x in rng q
then consider L being Linear_Combination of B such that
A27: x = Carrier L and
A28: ex i being Nat st
( i in dom p & Sum L = p . i ) ;
consider i being Nat such that
A29: i in dom p and
A30: Sum L = p . i by A28;
S1[i,q . i] by A19, A20, A21, A29;
then x = q . i by A22, A19, A21, A27, A29, A30;
hence x in rng q by A21, A29, FUNCT_1:def_3; ::_thesis: verum
end;
then A31: { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } c= rng q by TARSKI:def_3;
for R being set st R in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } holds
R is finite
proof
let R be set ; ::_thesis: ( R in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } implies R is finite )
assume R in { (Carrier L) where L is Linear_Combination of B : ex i being Nat st
( i in dom p & Sum L = p . i ) } ; ::_thesis: R is finite
then ex L being Linear_Combination of B st
( R = Carrier L & ex i being Nat st
( i in dom p & Sum L = p . i ) ) ;
hence R is finite ; ::_thesis: verum
end;
hence B is finite by A16, A31, FINSET_1:7; ::_thesis: verum
end;
theorem :: VECTSP_9:21
for GF being Field
for V being VectSp of GF st V is finite-dimensional holds
for A being Subset of V st A is linearly-independent holds
A is finite
proof
let GF be Field; ::_thesis: for V being VectSp of GF st V is finite-dimensional holds
for A being Subset of V st A is linearly-independent holds
A is finite
let V be VectSp of GF; ::_thesis: ( V is finite-dimensional implies for A being Subset of V st A is linearly-independent holds
A is finite )
assume A1: V is finite-dimensional ; ::_thesis: for A being Subset of V st A is linearly-independent holds
A is finite
let A be Subset of V; ::_thesis: ( A is linearly-independent implies A is finite )
assume A is linearly-independent ; ::_thesis: A is finite
then consider B being Basis of V such that
A2: A c= B by VECTSP_7:19;
B is finite by A1, Th20;
hence A is finite by A2; ::_thesis: verum
end;
theorem Th22: :: VECTSP_9:22
for GF being Field
for V being VectSp of GF st V is finite-dimensional holds
for A, B being Basis of V holds card A = card B
proof
let GF be Field; ::_thesis: for V being VectSp of GF st V is finite-dimensional holds
for A, B being Basis of V holds card A = card B
let V be VectSp of GF; ::_thesis: ( V is finite-dimensional implies for A, B being Basis of V holds card A = card B )
assume A1: V is finite-dimensional ; ::_thesis: for A, B being Basis of V holds card A = card B
let A, B be Basis of V; ::_thesis: card A = card B
reconsider A9 = A, B9 = B as finite Subset of V by A1, Th20;
( VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin B & A9 is linearly-independent ) by VECTSP_7:def_3;
then A2: card A9 <= card B9 by Th19;
( VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B9 is linearly-independent ) by VECTSP_7:def_3;
then card B9 <= card A9 by Th19;
hence card A = card B by A2, XXREAL_0:1; ::_thesis: verum
end;
theorem Th23: :: VECTSP_9:23
for GF being Field
for V being VectSp of GF holds (0). V is finite-dimensional
proof
let GF be Field; ::_thesis: for V being VectSp of GF holds (0). V is finite-dimensional
let V be VectSp of GF; ::_thesis: (0). V is finite-dimensional
reconsider V9 = (0). V as strict VectSp of GF ;
reconsider I = {} the carrier of V9 as finite Subset of V9 ;
the carrier of V9 = {(0. V)} by VECTSP_4:def_3
.= {(0. V9)} by VECTSP_4:11
.= the carrier of ((0). V9) by VECTSP_4:def_3 ;
then A1: V9 = (0). V9 by VECTSP_4:31;
Lin I = (0). V9 by VECTSP_7:9;
then I is Basis of V9 by A1, VECTSP_7:def_3;
hence (0). V is finite-dimensional by MATRLIN:def_1; ::_thesis: verum
end;
theorem Th24: :: VECTSP_9:24
for GF being Field
for V being VectSp of GF
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
let V be VectSp of GF; ::_thesis: for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
let W be Subspace of V; ::_thesis: ( V is finite-dimensional implies W is finite-dimensional )
set A = the Basis of W;
consider I being Basis of V such that
A1: the Basis of W c= I by Th13;
assume V is finite-dimensional ; ::_thesis: W is finite-dimensional
then I is finite by Th20;
hence W is finite-dimensional by A1, MATRLIN:def_1; ::_thesis: verum
end;
registration
let GF be Field;
let V be VectSp of GF;
cluster non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() finite-dimensional for Subspace of V;
existence
ex b1 being Subspace of V st
( b1 is strict & b1 is finite-dimensional )
proof
take (0). V ; ::_thesis: ( (0). V is strict & (0). V is finite-dimensional )
thus ( (0). V is strict & (0). V is finite-dimensional ) by Th23; ::_thesis: verum
end;
end;
registration
let GF be Field;
let V be finite-dimensional VectSp of GF;
cluster -> finite-dimensional for Subspace of V;
correctness
coherence
for b1 being Subspace of V holds b1 is finite-dimensional ;
by Th24;
end;
registration
let GF be Field;
let V be finite-dimensional VectSp of GF;
cluster non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() finite-dimensional for Subspace of V;
existence
ex b1 being Subspace of V st b1 is strict
proof
(0). V is strict finite-dimensional Subspace of V ;
hence ex b1 being Subspace of V st b1 is strict ; ::_thesis: verum
end;
end;
begin
definition
let GF be Field;
let V be VectSp of GF;
assume A1: V is finite-dimensional ;
func dim V -> Nat means :Def1: :: VECTSP_9:def 1
for I being Basis of V holds it = card I;
existence
ex b1 being Nat st
for I being Basis of V holds b1 = card I
proof
consider A being finite Subset of V such that
A2: A is Basis of V by A1, MATRLIN:def_1;
consider n being Nat such that
A3: n = card A ;
for I being Basis of V holds card I = n by A1, A2, A3, Th22;
hence ex b1 being Nat st
for I being Basis of V holds b1 = card I ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Nat st ( for I being Basis of V holds b1 = card I ) & ( for I being Basis of V holds b2 = card I ) holds
b1 = b2
proof
let n, m be Nat; ::_thesis: ( ( for I being Basis of V holds n = card I ) & ( for I being Basis of V holds m = card I ) implies n = m )
assume that
A4: for I being Basis of V holds card I = n and
A5: for I being Basis of V holds card I = m ; ::_thesis: n = m
consider A being finite Subset of V such that
A6: A is Basis of V by A1, MATRLIN:def_1;
card A = n by A4, A6;
hence n = m by A5, A6; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines dim VECTSP_9:def_1_:_
for GF being Field
for V being VectSp of GF st V is finite-dimensional holds
for b3 being Nat holds
( b3 = dim V iff for I being Basis of V holds b3 = card I );
theorem Th25: :: VECTSP_9:25
for GF being Field
for V being finite-dimensional VectSp of GF
for W being Subspace of V holds dim W <= dim V
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF
for W being Subspace of V holds dim W <= dim V
let V be finite-dimensional VectSp of GF; ::_thesis: for W being Subspace of V holds dim W <= dim V
let W be Subspace of V; ::_thesis: dim W <= dim V
set A = the Basis of W;
reconsider A = the Basis of W as Subset of W ;
A1: dim W = card A by Def1;
A is linearly-independent by VECTSP_7:def_3;
then reconsider B = A as linearly-independent Subset of V by Th11;
reconsider A9 = B as finite Subset of V by Th20;
reconsider V9 = V as VectSp of GF ;
set I = the Basis of V9;
A2: Lin the Basis of V9 = VectSpStr(# the carrier of V9, the U5 of V9, the ZeroF of V9, the lmult of V9 #) by VECTSP_7:def_3;
reconsider I = the Basis of V9 as finite Subset of V by Th20;
card A9 <= card I by A2, Th19;
hence dim W <= dim V by A1, Def1; ::_thesis: verum
end;
theorem Th26: :: VECTSP_9:26
for GF being Field
for V being finite-dimensional VectSp of GF
for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF
for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)
let V be finite-dimensional VectSp of GF; ::_thesis: for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)
let A be Subset of V; ::_thesis: ( A is linearly-independent implies card A = dim (Lin A) )
assume A1: A is linearly-independent ; ::_thesis: card A = dim (Lin A)
set W = Lin A;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_in_the_carrier_of_(Lin_A)
let x be set ; ::_thesis: ( x in A implies x in the carrier of (Lin A) )
assume x in A ; ::_thesis: x in the carrier of (Lin A)
then x in Lin A by VECTSP_7:8;
hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider B = A as linearly-independent Subset of (Lin A) by A1, Th12, TARSKI:def_3;
Lin A = Lin B by Th17;
then reconsider B = B as Basis of Lin A by VECTSP_7:def_3;
card B = dim (Lin A) by Def1;
hence card A = dim (Lin A) ; ::_thesis: verum
end;
theorem Th27: :: VECTSP_9:27
for GF being Field
for V being finite-dimensional VectSp of GF holds dim V = dim ((Omega). V)
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF holds dim V = dim ((Omega). V)
let V be finite-dimensional VectSp of GF; ::_thesis: dim V = dim ((Omega). V)
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def_1;
A2: (Omega). V = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def_4
.= Lin I by A1, VECTSP_7:def_3 ;
( card I = dim V & I is linearly-independent ) by A1, Def1, VECTSP_7:def_3;
hence dim V = dim ((Omega). V) by A2, Th26; ::_thesis: verum
end;
theorem :: VECTSP_9:28
for GF being Field
for V being finite-dimensional VectSp of GF
for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF
for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
let V be finite-dimensional VectSp of GF; ::_thesis: for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
let W be Subspace of V; ::_thesis: ( dim V = dim W iff (Omega). V = (Omega). W )
consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def_1;
hereby ::_thesis: ( (Omega). V = (Omega). W implies dim V = dim W )
set A = the Basis of W;
consider B being Basis of V such that
A2: the Basis of W c= B by Th13;
the carrier of W c= the carrier of V by VECTSP_4:def_2;
then reconsider A9 = the Basis of W as finite Subset of V by Th20, XBOOLE_1:1;
reconsider B9 = B as finite Subset of V by Th20;
assume dim V = dim W ; ::_thesis: (Omega). V = (Omega). W
then A3: card the Basis of W = dim V by Def1
.= card B by Def1 ;
A4: now__::_thesis:_not_the_Basis_of_W_<>_B
assume the Basis of W <> B ; ::_thesis: contradiction
then the Basis of W c< B by A2, XBOOLE_0:def_8;
then card A9 < card B9 by CARD_2:48;
hence contradiction by A3; ::_thesis: verum
end;
reconsider B = B as Subset of V ;
reconsider A = the Basis of W as Subset of W ;
(Omega). V = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def_4
.= Lin B by VECTSP_7:def_3
.= Lin A by A4, Th17
.= VectSpStr(# the carrier of W, the U5 of W, the ZeroF of W, the lmult of W #) by VECTSP_7:def_3
.= (Omega). W by VECTSP_4:def_4 ;
hence (Omega). V = (Omega). W ; ::_thesis: verum
end;
consider B being finite Subset of W such that
A5: B is Basis of W by MATRLIN:def_1;
A6: A is linearly-independent by A1, VECTSP_7:def_3;
assume (Omega). V = (Omega). W ; ::_thesis: dim V = dim W
then VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = (Omega). W by VECTSP_4:def_4
.= VectSpStr(# the carrier of W, the U5 of W, the ZeroF of W, the lmult of W #) by VECTSP_4:def_4 ;
then A7: Lin A = VectSpStr(# the carrier of W, the U5 of W, the ZeroF of W, the lmult of W #) by A1, VECTSP_7:def_3
.= Lin B by A5, VECTSP_7:def_3 ;
A8: B is linearly-independent by A5, VECTSP_7:def_3;
reconsider B = B as Subset of W ;
reconsider A = A as Subset of V ;
dim V = card A by A1, Def1
.= dim (Lin B) by A6, A7, Th26
.= card B by A8, Th26
.= dim W by A5, Def1 ;
hence dim V = dim W ; ::_thesis: verum
end;
theorem Th29: :: VECTSP_9:29
for GF being Field
for V being finite-dimensional VectSp of GF holds
( dim V = 0 iff (Omega). V = (0). V )
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF holds
( dim V = 0 iff (Omega). V = (0). V )
let V be finite-dimensional VectSp of GF; ::_thesis: ( dim V = 0 iff (Omega). V = (0). V )
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def_1;
hereby ::_thesis: ( (Omega). V = (0). V implies dim V = 0 )
consider I being finite Subset of V such that
A2: I is Basis of V by MATRLIN:def_1;
assume dim V = 0 ; ::_thesis: (Omega). V = (0). V
then card I = 0 by A2, Def1;
then A3: I = {} the carrier of V ;
(Omega). V = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def_4
.= Lin I by A2, VECTSP_7:def_3
.= (0). V by A3, VECTSP_7:9 ;
hence (Omega). V = (0). V ; ::_thesis: verum
end;
A4: now__::_thesis:_not_I_=_{(0._V)}
assume I = {(0. V)} ; ::_thesis: contradiction
then I is linearly-dependent by VECTSP_7:3;
hence contradiction by A1, VECTSP_7:def_3; ::_thesis: verum
end;
assume (Omega). V = (0). V ; ::_thesis: dim V = 0
then VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = (0). V by VECTSP_4:def_4;
then Lin I = (0). V by A1, VECTSP_7:def_3;
then ( I = {} or I = {(0. V)} ) by VECTSP_7:10;
hence dim V = 0 by A1, A4, Def1, CARD_1:27; ::_thesis: verum
end;
theorem :: VECTSP_9:30
for GF being Field
for V being finite-dimensional VectSp of GF holds
( dim V = 1 iff ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF holds
( dim V = 1 iff ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
let V be finite-dimensional VectSp of GF; ::_thesis: ( dim V = 1 iff ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
hereby ::_thesis: ( ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) implies dim V = 1 )
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def_1;
assume dim V = 1 ; ::_thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )
then card I = 1 by A1, Def1;
then consider v being set such that
A2: I = {v} by CARD_2:42;
v in I by A2, TARSKI:def_1;
then reconsider v = v as Vector of V ;
{v} is linearly-independent by A1, A2, VECTSP_7:def_3;
then A3: v <> 0. V by VECTSP_7:3;
Lin {v} = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by A1, A2, VECTSP_7:def_3;
hence ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) by A3, VECTSP_4:def_4; ::_thesis: verum
end;
given v being Vector of V such that A4: ( v <> 0. V & (Omega). V = Lin {v} ) ; ::_thesis: dim V = 1
( {v} is linearly-independent & Lin {v} = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) by A4, VECTSP_4:def_4, VECTSP_7:3;
then A5: {v} is Basis of V by VECTSP_7:def_3;
card {v} = 1 by CARD_1:30;
hence dim V = 1 by A5, Def1; ::_thesis: verum
end;
theorem :: VECTSP_9:31
for GF being Field
for V being finite-dimensional VectSp of GF holds
( dim V = 2 iff ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF holds
( dim V = 2 iff ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )
let V be finite-dimensional VectSp of GF; ::_thesis: ( dim V = 2 iff ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )
hereby ::_thesis: ( ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) implies dim V = 2 )
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def_1;
assume dim V = 2 ; ::_thesis: ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} )
then A2: card I = 2 by A1, Def1;
then consider u being set such that
A3: u in I by CARD_1:27, XBOOLE_0:def_1;
reconsider u = u as Vector of V by A3;
now__::_thesis:_not_I_c=_{u}
assume I c= {u} ; ::_thesis: contradiction
then card I <= card {u} by NAT_1:43;
then 2 <= 1 by A2, CARD_1:30;
hence contradiction ; ::_thesis: verum
end;
then consider v being set such that
A4: v in I and
A5: not v in {u} by TARSKI:def_3;
reconsider v = v as Vector of V by A4;
A6: v <> u by A5, TARSKI:def_1;
A7: now__::_thesis:_I_c=_{u,v}
assume not I c= {u,v} ; ::_thesis: contradiction
then consider w being set such that
A8: w in I and
A9: not w in {u,v} by TARSKI:def_3;
for x being set st x in {u,v,w} holds
x in I by A3, A4, A8, ENUMSET1:def_1;
then {u,v,w} c= I by TARSKI:def_3;
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 ; ::_thesis: verum
end;
for x being set st x in {u,v} holds
x in I by A3, A4, TARSKI:def_2;
then {u,v} c= I by TARSKI:def_3;
then A11: I = {u,v} by A7, XBOOLE_0:def_10;
then A12: {u,v} is linearly-independent by A1, VECTSP_7:def_3;
Lin {u,v} = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by A1, A11, VECTSP_7:def_3
.= (Omega). V by VECTSP_4:def_4 ;
hence ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) by A6, A12; ::_thesis: verum
end;
given u, v being Vector of V such that A13: u <> v and
A14: {u,v} is linearly-independent and
A15: (Omega). V = Lin {u,v} ; ::_thesis: dim V = 2
Lin {u,v} = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by A15, VECTSP_4:def_4;
then A16: {u,v} is Basis of V by A14, VECTSP_7:def_3;
card {u,v} = 2 by A13, CARD_2:57;
hence dim V = 2 by A16, Def1; ::_thesis: verum
end;
theorem Th32: :: VECTSP_9:32
for GF being Field
for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
let V be finite-dimensional VectSp of GF; ::_thesis: for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
let W1, W2 be Subspace of V; ::_thesis: (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
reconsider V = V as VectSp of GF ;
reconsider W1 = W1, W2 = W2 as Subspace of V ;
consider I being finite Subset of (W1 /\ W2) such that
A1: I is Basis of W1 /\ W2 by MATRLIN:def_1;
W1 /\ W2 is Subspace of W2 by VECTSP_5:15;
then consider I2 being Basis of W2 such that
A2: I c= I2 by A1, Th13;
W1 /\ W2 is Subspace of W1 by VECTSP_5:15;
then consider I1 being Basis of W1 such that
A3: I c= I1 by A1, Th13;
reconsider I2 = I2 as finite Subset of W2 by Th20;
reconsider I1 = I1 as finite Subset of W1 by Th20;
A4: now__::_thesis:_I1_/\_I2_c=_I
I1 is linearly-independent by VECTSP_7:def_3;
then reconsider I19 = I1 as linearly-independent Subset of V by Th11;
assume not I1 /\ I2 c= I ; ::_thesis: contradiction
then consider x being set such that
A5: x in I1 /\ I2 and
A6: not x in I by TARSKI:def_3;
x in I1 by A5, XBOOLE_0:def_4;
then x in Lin I1 by VECTSP_7:8;
then x in VectSpStr(# the carrier of W1, the U5 of W1, the ZeroF of W1, the lmult of W1 #) by VECTSP_7: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 VECTSP_4:def_2;
then reconsider x9 = x as Vector of V by A7;
now__::_thesis:_for_y_being_set_st_y_in_I_\/_{x}_holds_
y_in_the_carrier_of_V
let y be set ; ::_thesis: ( y in I \/ {x} implies y in the carrier of V )
the carrier of (W1 /\ W2) c= the carrier of V by VECTSP_4:def_2;
then A9: I c= the carrier of V by XBOOLE_1:1;
assume y in I \/ {x} ; ::_thesis: y in the carrier of V
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; ::_thesis: verum
end;
then reconsider Ix = I \/ {x} as Subset of V by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_I_\/_{x}_holds_
y_in_I19
let y be set ; ::_thesis: ( y in I \/ {x} implies y in I19 )
assume y in I \/ {x} ; ::_thesis: y in I19
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; ::_thesis: verum
end;
then A10: Ix c= I19 by TARSKI:def_3;
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 VECTSP_7:8;
then x in VectSpStr(# the carrier of W2, the U5 of W2, the ZeroF of W2, the lmult of W2 #) by VECTSP_7: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 VECTSP_5:def_2;
then A12: x in VectSpStr(# the carrier of (W1 /\ W2), the U5 of (W1 /\ W2), the ZeroF of (W1 /\ W2), the lmult of (W1 /\ W2) #) by STRUCT_0:def_5;
the carrier of (W1 /\ W2) c= the carrier of V by VECTSP_4:def_2;
then reconsider I9 = I as Subset of V by XBOOLE_1:1;
A13: Lin I = Lin I9 by Th17;
Ix \ {x} = I \ {x} by XBOOLE_1:40
.= I by A6, ZFMISC_1:57 ;
then not x9 in Lin I9 by A10, A11, Th14, VECTSP_7:1;
hence contradiction by A1, A12, A13, VECTSP_7:def_3; ::_thesis: verum
end;
set A = I1 \/ I2;
now__::_thesis:_for_v_being_set_st_v_in_I1_\/_I2_holds_
v_in_the_carrier_of_(W1_+_W2)
let v be set ; ::_thesis: ( v in I1 \/ I2 implies v in the carrier of (W1 + W2) )
A14: ( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by VECTSP_4:def_2;
assume v in I1 \/ I2 ; ::_thesis: v in the carrier of (W1 + W2)
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 VECTSP_5:2;
hence v in the carrier of (W1 + W2) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider A = I1 \/ I2 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 being 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 VECTSP_5:7, VECTSP_7:def_3;
then reconsider I19 = I1 as linearly-independent Subset of (W1 + W2) by Th11;
reconsider W29 = W2 as Subspace of W1 + W2 by VECTSP_5:7;
reconsider W19 = W1 as Subspace of W1 + W2 by VECTSP_5:7;
let L be Linear_Combination of A; ::_thesis: ( Sum L = 0. (W1 + W2) implies Carrier L = {} )
assume A17: Sum L = 0. (W1 + W2) ; ::_thesis: Carrier L = {}
A18: I1 misses (Carrier L) \ I1 by XBOOLE_1:79;
set B = (Carrier L) /\ I1;
consider F being 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 VECTSP_6:def_6;
reconsider B = (Carrier L) /\ I1 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 being Linear_Combination of W1 + W2 such that
A22: Carrier L1 = (rng F1) /\ (Carrier L) and
A23: L1 (#) F1 = L (#) F1 by Th4;
F1 is one-to-one by A19, FINSEQ_3:87;
then A24: Sum (L (#) F1) = Sum L1 by A22, A23, Th3, XBOOLE_1:17;
rng F c= rng F ;
then reconsider X = rng F as Subset of (rng F) ;
consider L2 being Linear_Combination of W1 + W2 such that
A25: Carrier L2 = (rng F2) /\ (Carrier L) and
A26: L2 (#) F2 = L (#) F2 by Th4;
F2 is one-to-one by A19, FINSEQ_3:87;
then A27: Sum (L (#) F2) = Sum L2 by A25, A26, Th3, 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 being Linear_Combination of W19 such that
Carrier K1 = Carrier L1 and
A29: Sum K1 = Sum L1 by Th9;
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 VECTSP_6:def_4;
then A33: Carrier L2 c= I2 by A30, XBOOLE_1:43;
Carrier L2 c= I2 by A32, A30, XBOOLE_1:43;
then consider K2 being Linear_Combination of W29 such that
Carrier K2 = Carrier L2 and
A34: Sum K2 = Sum L2 by Th9, XBOOLE_1:1;
A35: Sum K1 in W1 by STRUCT_0:def_5;
ex P being 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, Th1
.= Sum ((L (#) F1) ^ (L (#) F2)) by VECTSP_6:13
.= (Sum L1) + (Sum L2) by A24, A27, RLVECT_1:41 ;
then Sum L1 = - (Sum L2) by VECTSP_1:16
.= - (Sum K2) by A34, VECTSP_4:15 ;
then Sum K1 in W2 by A29, STRUCT_0:def_5;
then Sum K1 in W1 /\ W2 by A35, VECTSP_5:3;
then Sum K1 in Lin I by A1, VECTSP_7:def_3;
then consider KI being Linear_Combination of I such that
A37: Sum K1 = Sum KI by VECTSP_7:7;
A38: Carrier L = (Carrier L1) \/ (Carrier L2) by A28, A30, XBOOLE_1:51;
A39: now__::_thesis:_Carrier_L_c=_Carrier_(L1_+_L2)
assume not Carrier L c= Carrier (L1 + L2) ; ::_thesis: contradiction
then consider x being set such that
A40: x in Carrier L and
A41: not x in Carrier (L1 + L2) by TARSKI:def_3;
reconsider x = x as Vector of (W1 + W2) by A40;
A42: 0. GF = (L1 + L2) . x by A41, VECTSP_6:2
.= (L1 . x) + (L2 . x) by VECTSP_6:22 ;
percases ( x in Carrier L1 or x in Carrier L2 ) by A38, A40, XBOOLE_0:def_3;
supposeA43: x in Carrier L1 ; ::_thesis: contradiction
then not x in Carrier L2 by A31, XBOOLE_0:3;
then A44: L2 . x = 0. GF by VECTSP_6:2;
ex v being Vector of (W1 + W2) st
( x = v & L1 . v <> 0. GF ) by A43, VECTSP_6:1;
hence contradiction by A42, A44, RLVECT_1:4; ::_thesis: verum
end;
supposeA45: x in Carrier L2 ; ::_thesis: contradiction
then not x in Carrier L1 by A31, XBOOLE_0:3;
then A46: L1 . x = 0. GF by VECTSP_6:2;
ex v being Vector of (W1 + W2) st
( x = v & L2 . v <> 0. GF ) by A45, VECTSP_6:1;
hence contradiction by A42, A46, RLVECT_1:4; ::_thesis: verum
end;
end;
end;
A47: I \/ I2 = I2 by A2, XBOOLE_1:12;
A48: I2 is linearly-independent by VECTSP_7:def_3;
A49: Carrier L1 c= I1 by A28, XBOOLE_1:17;
W1 /\ W2 is Subspace of W1 + W2 by VECTSP_5:23;
then consider LI being Linear_Combination of W1 + W2 such that
A50: Carrier LI = Carrier KI and
A51: Sum LI = Sum KI by Th8;
Carrier LI c= I by A50, VECTSP_6:def_4;
then Carrier LI c= I19 by A3, XBOOLE_1:1;
then A52: LI = L1 by A49, A29, A37, A51, MATRLIN:5;
Carrier LI c= I by A50, VECTSP_6:def_4;
then ( Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2) & (Carrier LI) \/ (Carrier L2) c= I2 ) by A47, A33, VECTSP_6:23, XBOOLE_1:13;
then A53: Carrier (LI + L2) c= I2 by XBOOLE_1:1;
W2 is Subspace of W1 + W2 by VECTSP_5:7;
then consider K being Linear_Combination of W2 such that
A54: Carrier K = Carrier (LI + L2) and
A55: Sum K = Sum (LI + L2) by A53, Th9, XBOOLE_1:1;
reconsider K = K as Linear_Combination of I2 by A53, A54, VECTSP_6:def_4;
0. W2 = (Sum LI) + (Sum L2) by A29, A36, A37, A51, VECTSP_4:12
.= Sum K by A55, VECTSP_6:44 ;
then {} = Carrier (L1 + L2) by A54, A52, A48, VECTSP_7:def_1;
hence Carrier L = {} by A39; ::_thesis: verum
end;
then A56: A is linearly-independent by VECTSP_7:def_1;
the carrier of (W1 + W2) c= the carrier of V by VECTSP_4:def_2;
then reconsider A9 = A as Subset of V by XBOOLE_1:1;
A57: card I2 = dim W2 by Def1;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(W1_+_W2)_holds_
x_in_the_carrier_of_(Lin_A9)
let x be set ; ::_thesis: ( x in the carrier of (W1 + W2) implies x in the carrier of (Lin A9) )
assume x in the carrier of (W1 + W2) ; ::_thesis: x in the carrier of (Lin A9)
then x in W1 + W2 by STRUCT_0:def_5;
then consider w1, w2 being Vector of V such that
A58: w1 in W1 and
A59: w2 in W2 and
A60: x = w1 + w2 by VECTSP_5:1;
reconsider w1 = w1 as Vector of W1 by A58, STRUCT_0:def_5;
w1 in Lin I1 by Th10;
then consider K1 being Linear_Combination of I1 such that
A61: w1 = Sum K1 by VECTSP_7:7;
reconsider w2 = w2 as Vector of W2 by A59, STRUCT_0:def_5;
w2 in Lin I2 by Th10;
then consider K2 being Linear_Combination of I2 such that
A62: w2 = Sum K2 by VECTSP_7:7;
consider L2 being Linear_Combination of V such that
A63: Carrier L2 = Carrier K2 and
A64: Sum L2 = Sum K2 by Th8;
A65: Carrier L2 c= I2 by A63, VECTSP_6:def_4;
consider L1 being Linear_Combination of V such that
A66: Carrier L1 = Carrier K1 and
A67: Sum L1 = Sum K1 by Th8;
set L = L1 + L2;
Carrier L1 c= I1 by A66, VECTSP_6:def_4;
then ( Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) & (Carrier L1) \/ (Carrier L2) c= I1 \/ I2 ) by A65, VECTSP_6:23, XBOOLE_1:13;
then Carrier (L1 + L2) c= I1 \/ I2 by XBOOLE_1:1;
then reconsider L = L1 + L2 as Linear_Combination of A9 by VECTSP_6:def_4;
x = Sum L by A60, A61, A67, A62, A64, VECTSP_6:44;
then x in Lin A9 by VECTSP_7:7;
hence x in the carrier of (Lin A9) by STRUCT_0:def_5; ::_thesis: verum
end;
then the carrier of (W1 + W2) c= the carrier of (Lin A9) by TARSKI:def_3;
then A68: W1 + W2 is Subspace of Lin A9 by VECTSP_4:27;
Lin A9 = Lin A by Th17;
then Lin A = W1 + W2 by A68, VECTSP_4:25;
then A69: A is Basis of W1 + W2 by A56, VECTSP_7:def_3;
card I = dim (W1 /\ W2) by A1, Def1;
then (dim (W1 + W2)) + (dim (W1 /\ W2)) = (((card I1) + (card I2)) + (- (card I))) + (card I) by A16, A69, Def1
.= (dim W1) + (dim W2) by A57, Def1 ;
hence (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) ; ::_thesis: verum
end;
theorem :: VECTSP_9:33
for GF being Field
for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
let V be finite-dimensional VectSp of GF; ::_thesis: for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
let W1, W2 be Subspace of V; ::_thesis: dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
A1: ( dim (W1 + W2) <= dim V & (dim V) + ((dim (W1 /\ W2)) - (dim V)) = dim (W1 /\ W2) ) by Th25;
((dim W1) + (dim W2)) - (dim V) = ((dim (W1 + W2)) + (dim (W1 /\ W2))) - (dim V) by Th32
.= (dim (W1 + W2)) + ((dim (W1 /\ W2)) - (dim V)) ;
hence dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V) by A1, XREAL_1:6; ::_thesis: verum
end;
theorem :: VECTSP_9:34
for GF being Field
for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
proof
let GF be Field; ::_thesis: for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
let V be finite-dimensional VectSp of GF; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies dim V = (dim W1) + (dim W2) )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: dim V = (dim W1) + (dim W2)
then A2: VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = W1 + W2 by VECTSP_5:def_4;
W1 /\ W2 = (0). V by A1, VECTSP_5:def_4;
then (Omega). (W1 /\ W2) = (0). V by VECTSP_4:def_4
.= (0). (W1 /\ W2) by VECTSP_4:36 ;
then dim (W1 /\ W2) = 0 by Th29;
then (dim W1) + (dim W2) = (dim (W1 + W2)) + 0 by Th32
.= dim ((Omega). V) by A2, VECTSP_4:def_4
.= dim V by Th27 ;
hence dim V = (dim W1) + (dim W2) ; ::_thesis: verum
end;
Lm2: for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
ex W being strict Subspace of V st dim W = n
proof
let GF be Field; ::_thesis: for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
ex W being strict Subspace of V st dim W = n
let n be Nat; ::_thesis: for V being finite-dimensional VectSp of GF st n <= dim V holds
ex W being strict Subspace of V st dim W = n
let V be finite-dimensional VectSp of GF; ::_thesis: ( n <= dim V implies ex W being strict Subspace of V st dim W = n )
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def_1;
assume n <= dim V ; ::_thesis: ex W being strict Subspace of V st dim W = n
then n <= card I by A1, Def1;
then consider A being finite Subset of I such that
A2: card A = n by FINSEQ_4:72;
reconsider A = 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, VECTSP_7:def_3;
then dim W = n by A2, Th26, VECTSP_7:1;
hence ex W being strict Subspace of V st dim W = n ; ::_thesis: verum
end;
theorem :: VECTSP_9:35
for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF holds
( n <= dim V iff ex W being strict Subspace of V st dim W = n ) by Lm2, Th25;
definition
let GF be Field;
let V be finite-dimensional VectSp of GF;
let n be Nat;
funcn Subspaces_of V -> set means :Def2: :: VECTSP_9:def 2
for x being set holds
( x in it iff ex W being strict Subspace of V st
( W = x & dim W = n ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
proof
set S = { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ;
take { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; ::_thesis: for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
proof
let x be set ; ::_thesis: ( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
hereby ::_thesis: ( ex W being strict Subspace of V st
( W = x & dim W = n ) implies x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } )
assume x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; ::_thesis: ex W being strict Subspace of V st
( W = x & dim W = n )
then A1: ex A being 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, Th26;
hence ex W being strict Subspace of V st
( W = x & dim W = n ) ; ::_thesis: verum
end;
given W being strict Subspace of V such that A2: W = x and
A3: dim W = n ; ::_thesis: x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) }
consider A being finite Subset of W such that
A4: A is Basis of W by MATRLIN:def_1;
reconsider A = A as Subset of W ;
A is linearly-independent by A4, VECTSP_7:def_3;
then reconsider B = A as linearly-independent Subset of V by Th11;
A5: x = Lin A by A2, A4, VECTSP_7:def_3
.= Lin B by Th17 ;
then card B = n by A2, A3, Th26;
hence x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } by A5; ::_thesis: verum
end;
hence for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) & ( for x being set holds
( x in b2 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex W being strict Subspace of V st
( W = $1 & dim W = n );
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Subspaces_of VECTSP_9:def_2_:_
for GF being Field
for V being finite-dimensional VectSp of GF
for n being Nat
for b4 being set holds
( b4 = n Subspaces_of V iff for x being set holds
( x in b4 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) );
theorem :: VECTSP_9:36
for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
not n Subspaces_of V is empty
proof
let GF be Field; ::_thesis: for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
not n Subspaces_of V is empty
let n be Nat; ::_thesis: for V being finite-dimensional VectSp of GF st n <= dim V holds
not n Subspaces_of V is empty
let V be finite-dimensional VectSp of GF; ::_thesis: ( n <= dim V implies not n Subspaces_of V is empty )
assume n <= dim V ; ::_thesis: not n Subspaces_of V is empty
then ex W being strict Subspace of V st dim W = n by Lm2;
hence not n Subspaces_of V is empty by Def2; ::_thesis: verum
end;
theorem :: VECTSP_9:37
for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF st dim V < n holds
n Subspaces_of V = {}
proof
let GF be Field; ::_thesis: for n being Nat
for V being finite-dimensional VectSp of GF st dim V < n holds
n Subspaces_of V = {}
let n be Nat; ::_thesis: for V being finite-dimensional VectSp of GF st dim V < n holds
n Subspaces_of V = {}
let V be finite-dimensional VectSp of GF; ::_thesis: ( dim V < n implies n Subspaces_of V = {} )
assume that
A1: dim V < n and
A2: n Subspaces_of V <> {} ; ::_thesis: contradiction
consider x being set such that
A3: x in n Subspaces_of V by A2, XBOOLE_0:def_1;
ex W being strict Subspace of V st
( W = x & dim W = n ) by A3, Def2;
hence contradiction by A1, Th25; ::_thesis: verum
end;
theorem :: VECTSP_9:38
for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
proof
let GF be Field; ::_thesis: for n being Nat
for V being finite-dimensional VectSp of GF
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
let n be Nat; ::_thesis: for V being finite-dimensional VectSp of GF
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
let V be finite-dimensional VectSp of GF; ::_thesis: for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
let W be Subspace of V; ::_thesis: n Subspaces_of W c= n Subspaces_of V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n Subspaces_of W or x in n Subspaces_of V )
assume x in n Subspaces_of W ; ::_thesis: x in n Subspaces_of V
then consider W1 being strict Subspace of W such that
A1: W1 = x and
A2: dim W1 = n by Def2;
reconsider W1 = W1 as strict Subspace of V by VECTSP_4:26;
W1 in n Subspaces_of V by A2, Def2;
hence x in n Subspaces_of V by A1; ::_thesis: verum
end;