:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RLVECT_1, RLSUB_1, SUBSET_1, RLVECT_2, RLVECT_3, TARSKI,
CARD_3, XBOOLE_0, ARYTM_1, ARYTM_3, SUPINF_2, FUNCT_1, CARD_1, FINSEQ_1,
STRUCT_0, FUNCT_2, RELAT_1, VALUED_1, NAT_1, PARTFUN1, ORDINAL4,
CLASSES1, FINSET_1, XXREAL_0, FINSEQ_4, RLSUB_2, RLVECT_5;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, FINSET_1,
FINSEQ_1, FINSEQ_3, FINSEQ_4, DOMAIN_1, STRUCT_0, CLASSES1, RLVECT_1,
RLVECT_2, RLSUB_1, RLSUB_2, RLVECT_3, XXREAL_0;
constructors PARTFUN1, XXREAL_0, REAL_1, NAT_1, FINSEQ_3, FINSEQ_4, REALSET1,
RFINSEQ, RLSUB_2, RLVECT_2, CLASSES1, RLVECT_3, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FINSET_1, NUMBERS, NAT_1, FINSEQ_1, STRUCT_0, RLVECT_3, CARD_1, RELSET_1,
RLVECT_2, XREAL_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve V for RealLinearSpace,
W for Subspace of V,
x, y, y1, y2 for set,
i, n for Element of NAT,
v for VECTOR of V,
KL1, KL2 for Linear_Combination of V,
X for Subset of V;
theorem :: RLVECT_5:1
X is linearly-independent & Carrier(KL1) c= X & Carrier(KL2) c= X
& Sum(KL1) = Sum(KL2) implies KL1 = KL2;
theorem :: RLVECT_5:2
for V being RealLinearSpace, A being Subset of V st A is
linearly-independent holds ex I being Basis of V st A c= I;
theorem :: RLVECT_5:3
for L being Linear_Combination of V, x being VECTOR of V holds x
in Carrier L iff ex v st x = v & L.v <> 0;
:: More On Linear Combinations
theorem :: RLVECT_5:4
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);
theorem :: RLVECT_5:5
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;
theorem :: RLVECT_5:6
for F being FinSequence of the carrier of V st F is one-to-one
for L being Linear_Combination of V st Carrier(L) c= rng F holds Sum(L (#) F) =
Sum(L);
theorem :: RLVECT_5:7
for L being Linear_Combination of V for F being FinSequence of
the carrier of V holds ex K being Linear_Combination of V st Carrier(K) = rng F
/\ Carrier(L) & L (#) F = K (#) F;
theorem :: RLVECT_5:8
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);
theorem :: RLVECT_5:9
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);
theorem :: RLVECT_5:10
for L being Linear_Combination of V st Carrier(L) c= the carrier
of W for K being Linear_Combination of W st K = L|the carrier of W holds
Carrier(L) = Carrier(K) & Sum(L) = Sum(K);
theorem :: RLVECT_5:11
for K being Linear_Combination of W holds ex L being
Linear_Combination of V st Carrier(K) = Carrier(L) & Sum(K) = Sum(L);
theorem :: RLVECT_5:12
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);
:: More On Linear Independence & Basis
theorem :: RLVECT_5:13
for I being Basis of V, v being VECTOR of V holds v in Lin(I);
theorem :: RLVECT_5:14
for A being Subset of W st A is linearly-independent holds A is
linearly-independent Subset of V;
theorem :: RLVECT_5:15
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;
theorem :: RLVECT_5:16
for A being Basis of W ex B being Basis of V st A c= B;
theorem :: RLVECT_5:17
for A being Subset of V st A is linearly-independent for v being
VECTOR of V st v in A for B being Subset of V st B = A \ {v} holds not v in Lin
(B);
theorem :: RLVECT_5:18
for I being Basis of V for A being non empty Subset of V st A
misses I for B being Subset of V st B = I \/ A holds B is linearly-dependent;
theorem :: RLVECT_5:19
for A being Subset of V st A c= the carrier of W holds Lin(A) is
Subspace of W;
theorem :: RLVECT_5:20
for A being Subset of V, B being Subset of W st A = B holds Lin( A) = Lin(B);
begin :: Steinitz Theorem
:: Exchange Lemma
theorem :: RLVECT_5:21
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});
:: Steinitz Theorem
theorem :: RLVECT_5:22
for A, B being finite Subset of V st the RLSStruct 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 & the RLSStruct of V = Lin(B \/ C);
begin :: Finite-Dimensional Vector Spaces
definition
let V be RealLinearSpace;
attr V is finite-dimensional means
:: RLVECT_5:def 1
ex A being finite Subset of V st A is Basis of V;
end;
registration
cluster strict finite-dimensional for RealLinearSpace;
end;
theorem :: RLVECT_5:23
V is finite-dimensional implies for I being Basis of V holds I is finite;
theorem :: RLVECT_5:24
V is finite-dimensional implies for A being Subset of V st A is
linearly-independent holds A is finite;
theorem :: RLVECT_5:25
V is finite-dimensional implies for A, B being Basis of V holds
card A = card B;
theorem :: RLVECT_5:26
(0).V is finite-dimensional;
theorem :: RLVECT_5:27
V is finite-dimensional implies W is finite-dimensional;
registration
let V be RealLinearSpace;
cluster finite-dimensional strict for Subspace of V;
end;
registration
let V be finite-dimensional RealLinearSpace;
cluster -> finite-dimensional for Subspace of V;
end;
registration
let V be finite-dimensional RealLinearSpace;
cluster strict for Subspace of V;
end;
begin :: Dimension of a Vector Space
definition
let V be RealLinearSpace;
assume
V is finite-dimensional;
func dim V -> Element of NAT means
:: RLVECT_5:def 2
for I being Basis of V holds it = card I;
end;
reserve V for finite-dimensional RealLinearSpace,
W, W1, W2 for Subspace of V,
u, v for VECTOR of V;
theorem :: RLVECT_5:28
dim W <= dim V;
theorem :: RLVECT_5:29
for A being Subset of V st A is linearly-independent holds card
A = dim Lin(A);
theorem :: RLVECT_5:30
dim V = dim (Omega).V;
theorem :: RLVECT_5:31
dim V = dim W iff (Omega).V = (Omega).W;
theorem :: RLVECT_5:32
dim V = 0 iff (Omega).V = (0).V;
theorem :: RLVECT_5:33
dim V = 1 iff ex v st v <> 0.V & (Omega).V = Lin{v};
theorem :: RLVECT_5:34
dim V = 2 iff ex u, v st u <> v & {u, v} is linearly-independent &
(Omega).V = Lin{u, v};
theorem :: RLVECT_5:35
dim(W1 + W2) + dim(W1 /\ W2) = dim W1 + dim W2;
theorem :: RLVECT_5:36
dim(W1 /\ W2) >= dim W1 + dim W2 - dim V;
theorem :: RLVECT_5:37
V is_the_direct_sum_of W1, W2 implies dim V = dim W1 + dim W2;
theorem :: RLVECT_5:38
n <= dim V iff ex W being strict Subspace of V st dim W = n;
definition
let V be finite-dimensional RealLinearSpace, n be Element of NAT;
func n Subspaces_of V -> set means
:: 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;
end;
theorem :: RLVECT_5:39
n <= dim V implies n Subspaces_of V is non empty;
theorem :: RLVECT_5:40
dim V < n implies n Subspaces_of V = {};
theorem :: RLVECT_5:41
n Subspaces_of W c= n Subspaces_of V;