:: Steinitz Theorem and Dimension of a Vector Space
:: by Mariusz \.Zynel
::
:: Received October 6, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

::
:: Preliminaries
::
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
proofend;
end;

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

:: More On Linear Combinations
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)
proofend;

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

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

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 )
proofend;

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

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

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 )
proofend;

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 )
proofend;

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 )
proofend;

:: More On Linear Independence & Basis
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
proofend;

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

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

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

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

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

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

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

begin

::
:: Steinitz Theorem
::
:: Exchange Lemma
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}) )
proofend;

:: [WP: ] Steinitz_Theorem
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 &amp; ex C being finite Subset of V st
( C c= A &amp; card C = (card A) - (card B) &amp; VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )
proofend;

begin

::
:: Finite-Dimensional Vector Spaces
::
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
proofend;

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

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

theorem Th23: :: VECTSP_9:23
for GF being Field
for V being VectSp of GF holds (0). V is finite-dimensional
proofend;

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

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 &amp; b1 is finite-dimensional )
proofend;
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
proofend;
end;

begin

::
:: Dimension of a Vector Space
::
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
proofend;
uniqueness
 for b1, b2 being Nat st ( for I being Basis of V holds b1 = card I ) &amp; ( for I being Basis of V holds b2 = card I ) holds
b1 = b2
proofend;
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
proofend;

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)
proofend;

theorem Th27: :: VECTSP_9:27
for GF being Field
for V being finite-dimensional VectSp of GF holds dim V = dim ((Omega). V)
proofend;

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 )
proofend;

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 )
proofend;

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 &amp; (Omega). V = Lin {v} ) )
proofend;

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 &amp; {u,v} is linearly-independent &amp; (Omega). V = Lin {u,v} ) )
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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

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 &amp; 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 &amp; dim W = n ) )
proofend;
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 &amp; dim W = n ) ) ) &amp; ( for x being set holds
( x in b2 iff ex W being strict Subspace of V st
( W = x &amp; dim W = n ) ) ) holds
b1 = b2
proofend;
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 &amp; 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
proofend;

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 = {}
proofend;

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