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 object ; :: 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 ModuleStr(# 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 object ; :: 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 object 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 by A12, TARSKI:def 4;
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 ModuleStr(# 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: ModuleStr(# 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 object st
( v in B & not v in C ) ;
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 , object ] 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 object st S1[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being object st S1[i,x] )
assume i in Seg (len p) ; :: thesis: ex x being object 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 object 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 object 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 object ; :: 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 ;
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