environ vocabulary VECTSP_1, RLSUB_1, FINSET_1, CARD_1, FINSEQ_1, RELAT_1, FUNCT_1, FINSEQ_4, RFINSEQ, BOOLE, RLVECT_2, FUNCT_2, RLVECT_1, SEQ_1, ARYTM_1, SUBSET_1, RLVECT_3, RLSUB_2, MATRLIN, TARSKI, VECTSP_9; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, CARD_1, FINSET_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, RFINSEQ, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_5, VECTSP_7, MATRLIN; constructors REAL_1, FINSEQ_3, RFINSEQ, VECTSP_6, VECTSP_5, VECTSP_7, MATRLIN, DOMAIN_1, RLVECT_2, PARTFUN1, XREAL_0, MEMBERED; clusters SUBSET_1, STRUCT_0, RELSET_1, FINSEQ_1, FINSET_1, MATRLIN, XREAL_0, FUNCT_2, VECTSP_1, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve GF for Field, V for VectSp of GF, W for Subspace of V, x, y, y1, y2 for set, i, n, m for Nat; :: :: Preliminaries :: definition let S be non empty 1-sorted; cluster non empty Subset of S; end; theorem :: VECTSP_9:1 for X being finite set st n <= Card X holds ex A being finite Subset of X st Card A = n; :: More On Functions reserve f, g for Function; theorem :: VECTSP_9:2 for f st f is one-to-one holds x in rng f implies Card(f"{x}) = 1; theorem :: VECTSP_9:3 for f holds not x in rng f implies Card(f"{x}) = 0; theorem :: VECTSP_9:4 for f, g st rng f = rng g & f is one-to-one & g is one-to-one holds f, g are_fiberwise_equipotent; :: More On Linear Combinations theorem :: VECTSP_9:5 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 :: VECTSP_9:6 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 :: VECTSP_9:7 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 :: VECTSP_9:8 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 :: VECTSP_9:9 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 :: VECTSP_9:10 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 :: VECTSP_9:11 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 :: VECTSP_9:12 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 :: VECTSP_9:13 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 Independance & Basis theorem :: VECTSP_9:14 for I being Basis of V, v being Vector of V holds v in Lin(I); theorem :: VECTSP_9:15 for A being Subset of W st A is linearly-independent holds ex B being Subset of V st B is linearly-independent & B = A; theorem :: VECTSP_9:16 for A being Subset of V st A is linearly-independent & A c= the carrier of W holds ex B being Subset of W st B is linearly-independent & B = A; theorem :: VECTSP_9:17 for A being Basis of W ex B being Basis of V st A c= B; theorem :: VECTSP_9:18 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 :: VECTSP_9:19 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 :: VECTSP_9:20 for A being Subset of V st A c= the carrier of W holds Lin(A) is Subspace of W; theorem :: VECTSP_9:21 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 :: VECTSP_9:22 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 :: VECTSP_9:23 for A, B being finite Subset of V st the VectSpStr 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 VectSpStr of V = Lin(B \/ C); begin :: :: Finite-Dimensional Vector Spaces :: definition let GF be Field, V be VectSp of GF; redefine attr V is finite-dimensional means :: VECTSP_9:def 1 ex I being finite Subset of V st I is Basis of V; end; theorem :: VECTSP_9:24 V is finite-dimensional implies for I being Basis of V holds I is finite; theorem :: VECTSP_9:25 V is finite-dimensional implies for A being Subset of V st A is linearly-independent holds A is finite; theorem :: VECTSP_9:26 V is finite-dimensional implies for A, B being Basis of V holds Card A = Card B; theorem :: VECTSP_9:27 (0).V is finite-dimensional; theorem :: VECTSP_9:28 V is finite-dimensional implies W is finite-dimensional; definition let GF be Field, V be VectSp of GF; cluster strict finite-dimensional Subspace of V; end; definition let GF be Field, V be finite-dimensional VectSp of GF; cluster -> finite-dimensional Subspace of V; end; definition let GF be Field, V be finite-dimensional VectSp of GF; cluster strict Subspace of V; end; begin :: :: Dimension of a Vector Space :: definition let GF be Field, V be VectSp of GF; assume V is finite-dimensional; func dim V -> Nat means :: VECTSP_9:def 2 for I being Basis of V holds it = Card I; end; reserve V for finite-dimensional VectSp of GF, W, W1, W2 for Subspace of V, u, v for Vector of V; theorem :: VECTSP_9:29 dim W <= dim V; theorem :: VECTSP_9:30 for A being Subset of V st A is linearly-independent holds Card A = dim Lin(A); theorem :: VECTSP_9:31 dim V = dim (Omega).V; theorem :: VECTSP_9:32 dim V = dim W iff (Omega).V = (Omega).W; theorem :: VECTSP_9:33 dim V = 0 iff (Omega).V = (0).V; theorem :: VECTSP_9:34 dim V = 1 iff ex v st v <> 0.V & (Omega).V = Lin{v}; theorem :: VECTSP_9:35 dim V = 2 iff ex u, v st u <> v & {u, v} is linearly-independent & (Omega).V = Lin{u, v}; theorem :: VECTSP_9:36 dim(W1 + W2) + dim(W1 /\ W2) = dim W1 + dim W2; theorem :: VECTSP_9:37 dim(W1 /\ W2) >= dim W1 + dim W2 - dim V; theorem :: VECTSP_9:38 V is_the_direct_sum_of W1, W2 implies dim V = dim W1 + dim W2; theorem :: VECTSP_9:39 n <= dim V iff ex W being strict Subspace of V st dim W = n; definition let GF be Field, V be finite-dimensional VectSp of GF, n be Nat; func n Subspaces_of V -> set means :: VECTSP_9:def 3 x in it iff ex W being strict Subspace of V st W = x & dim W = n; end; theorem :: VECTSP_9:40 n <= dim V implies n Subspaces_of V is non empty; theorem :: VECTSP_9:41 dim V < n implies n Subspaces_of V = {}; theorem :: VECTSP_9:42 n Subspaces_of W c= n Subspaces_of V;