:: The Steinitz Theorem and the Dimension of a Real Linear Space
:: by JingChao Chen
::
:: Received July 1, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users


theorem Th1: :: RLVECT_5:1
for V being RealLinearSpace
for KL1, KL2 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds
KL1 = KL2
proof end;

theorem Th2: :: RLVECT_5:2
for V being RealLinearSpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof end;

theorem Th3: :: RLVECT_5:3
for V being RealLinearSpace
for L being Linear_Combination of V
for x being VECTOR of V holds
( x in Carrier L iff ex v being VECTOR of V st
( x = v & L . v <> 0 ) )
proof end;

Lm1: for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
proof end;

:: More On Linear Combinations
theorem Th4: :: RLVECT_5:4
for V being RealLinearSpace
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 end;

theorem Th5: :: RLVECT_5:5
for V being RealLinearSpace
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 end;

theorem Th6: :: RLVECT_5:6
for V being RealLinearSpace
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 end;

theorem Th7: :: RLVECT_5:7
for V being RealLinearSpace
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 end;

theorem Th8: :: RLVECT_5:8
for V being RealLinearSpace
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 end;

theorem Th9: :: RLVECT_5:9
for V being RealLinearSpace
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 end;

theorem Th10: :: RLVECT_5:10
for V being RealLinearSpace
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 end;

theorem Th11: :: RLVECT_5:11
for V being RealLinearSpace
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 end;

theorem Th12: :: RLVECT_5:12
for V being RealLinearSpace
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 end;

:: More On Linear Independence & Basis
theorem Th13: :: RLVECT_5:13
for V being RealLinearSpace
for I being Basis of V
for v being VECTOR of V holds v in Lin I
proof end;

theorem Th14: :: RLVECT_5:14
for V being RealLinearSpace
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 end;

theorem Th15: :: RLVECT_5:15
for V being RealLinearSpace
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 end;

theorem Th16: :: RLVECT_5:16
for V being RealLinearSpace
for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
proof end;

theorem Th17: :: RLVECT_5:17
for V being RealLinearSpace
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 end;

theorem Th18: :: RLVECT_5:18
for V being RealLinearSpace
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 end;

theorem Th19: :: RLVECT_5:19
for V being RealLinearSpace
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 end;

theorem Th20: :: RLVECT_5:20
for V being RealLinearSpace
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 end;

:: Exchange Lemma
theorem Th21: :: RLVECT_5:21
for V being RealLinearSpace
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 end;

:: Steinitz Theorem
theorem Th22: :: RLVECT_5:22
for V being RealLinearSpace
for A, B being finite Subset of V st RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult 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) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )
proof end;

definition
let V be RealLinearSpace;
attr V is finite-dimensional means :Def1: :: RLVECT_5:def 1
 ex A being finite Subset of V st A is Basis of V;
end;

:: deftheorem Def1 defines finite-dimensional RLVECT_5:def 1 :
for V being RealLinearSpace holds
( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );

registration
cluster non empty V100() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional for RLSStruct ;
existence
ex b1 being RealLinearSpace st
( b1 is strict & b1 is finite-dimensional )
proof end;
end;

theorem Th23: :: RLVECT_5:23
for V being RealLinearSpace st V is finite-dimensional holds
for I being Basis of V holds I is finite
proof end;

theorem :: RLVECT_5:24
for V being RealLinearSpace st V is finite-dimensional holds
for A being Subset of V st A is linearly-independent holds
A is finite
proof end;

theorem Th25: :: RLVECT_5:25
for V being RealLinearSpace st V is finite-dimensional holds
for A, B being Basis of V holds card A = card B
proof end;

theorem Th26: :: RLVECT_5:26
for V being RealLinearSpace holds (0). V is finite-dimensional
proof end;

theorem Th27: :: RLVECT_5:27
for V being RealLinearSpace
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
proof end;

registration
let V be RealLinearSpace;
cluster non empty V100() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional for Subspace of V;
existence
ex b1 being Subspace of V st
( b1 is finite-dimensional & b1 is strict )
proof end;
end;

registration
let V be finite-dimensional RealLinearSpace;
cluster -> finite-dimensional for Subspace of V;
correctness
coherence
for b1 being Subspace of V holds b1 is finite-dimensional ;
by Th27;
end;

registration
let V be finite-dimensional RealLinearSpace;
cluster non empty V100() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional for Subspace of V;
existence
ex b1 being Subspace of V st b1 is strict
proof end;
end;

definition
let V be RealLinearSpace;
assume A1: V is finite-dimensional ;
func dim V -> Element of NAT means :Def2: :: RLVECT_5:def 2
 for I being Basis of V holds it = card I;
existence
ex b1 being Element of NAT st
for I being Basis of V holds b1 = card I
proof end;
uniqueness
for b1, b2 being Element of 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 end;
end;

:: deftheorem Def2 defines dim RLVECT_5:def 2 :
for V being RealLinearSpace st V is finite-dimensional holds
for b2 being Element of NAT holds
( b2 = dim V iff for I being Basis of V holds b2 = card I );

theorem Th28: :: RLVECT_5:28
for V being finite-dimensional RealLinearSpace
for W being Subspace of V holds dim W <= dim V
proof end;

theorem Th29: :: RLVECT_5:29
for V being finite-dimensional RealLinearSpace
for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)
proof end;

theorem Th30: :: RLVECT_5:30
for V being finite-dimensional RealLinearSpace holds dim V = dim ((Omega). V)
proof end;

theorem :: RLVECT_5:31
for V being finite-dimensional RealLinearSpace
for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
proof end;

theorem Th32: :: RLVECT_5:32
for V being finite-dimensional RealLinearSpace holds
( dim V = 0 iff (Omega). V = (0). V )
proof end;

theorem :: RLVECT_5:33
for V being finite-dimensional RealLinearSpace holds
( dim V = 1 iff ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
proof end;

theorem :: RLVECT_5:34
for V being finite-dimensional RealLinearSpace 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 end;

theorem Th35: :: RLVECT_5:35
for V being finite-dimensional RealLinearSpace
for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
proof end;

theorem :: RLVECT_5:36
for V being finite-dimensional RealLinearSpace
for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
proof end;

theorem :: RLVECT_5:37
for V being finite-dimensional RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
proof end;

Lm2: for n being Element of NAT
for V being finite-dimensional RealLinearSpace st n <= dim V holds
ex W being strict Subspace of V st dim W = n
proof end;

theorem :: RLVECT_5:38
for n being Element of NAT
for V being finite-dimensional RealLinearSpace holds
( n <= dim V iff ex W being strict Subspace of V st dim W = n ) by Lm2, Th28;

definition
let V be finite-dimensional RealLinearSpace;
let n be Element of NAT ;
func n Subspaces_of V -> set means :Def3: :: RLVECT_5:def 3
 for x being object 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 object holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) & ( for x being object holds
( x in b2 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Subspaces_of RLVECT_5:def 3 :
for V being finite-dimensional RealLinearSpace
for n being Element of NAT
for b3 being set holds
( b3 = n Subspaces_of V iff for x being object holds
( x in b3 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) );

theorem :: RLVECT_5:39
for n being Element of NAT
for V being finite-dimensional RealLinearSpace st n <= dim V holds
not n Subspaces_of V is empty
proof end;

theorem :: RLVECT_5:40
for n being Element of NAT
for V being finite-dimensional RealLinearSpace st dim V < n holds
n Subspaces_of V = {}
proof end;

theorem :: RLVECT_5:41
for n being Element of NAT
for V being finite-dimensional RealLinearSpace
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V
proof end;