Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Basis of Real Linear Space

**by****Wojciech A. Trybulec**- Received July 10, 1990
- MML identifier: RLVECT_3

- [ Mizar article, MML identifier index ]

environ vocabulary RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2, FINSEQ_1, FUNCT_1, ORDERS_1, SEQ_1, RELAT_1, FINSEQ_4, BOOLE, FUNCT_2, ARYTM_1, TARSKI, CARD_1, ZFMISC_1, RLVECT_3, HAHNBAN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, FINSEQ_1, RELAT_1, ORDINAL1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1, FINSEQ_4, FRAENKEL, FINSET_1, REAL_1, RLSUB_1, ORDERS_1, RLSUB_2, RLVECT_2, CARD_1, NAT_1; constructors NAT_1, REAL_1, ORDERS_1, RLSUB_2, RLVECT_2, FINSEQ_4, MEMBERED, PARTFUN1, XBOOLE_0; clusters SUBSET_1, FUNCT_1, RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2, RELSET_1, STRUCT_0, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x,y,X,Y,Z for set; reserve a,b for Real; reserve k,n for Nat; reserve V for RealLinearSpace; reserve W1,W2,W3 for Subspace of V; reserve v,v1,v2,u for VECTOR of V; reserve A,B,C for Subset of V; reserve T for finite Subset of V; reserve L,L1,L2 for Linear_Combination of V; reserve l for Linear_Combination of A; reserve F,G,H for FinSequence of the carrier of V; reserve f,g for Function of the carrier of V, REAL; reserve p,q,r for FinSequence; reserve M for non empty set; reserve CF for Choice_Function of M; theorem :: RLVECT_3:1 Sum(L1 + L2) = Sum(L1) + Sum(L2); theorem :: RLVECT_3:2 Sum(a * L) = a * Sum(L); theorem :: RLVECT_3:3 Sum(- L) = - Sum(L); theorem :: RLVECT_3:4 Sum(L1 - L2) = Sum(L1) - Sum(L2); definition let V; let A; attr A is linearly-independent means :: RLVECT_3:def 1 for l st Sum(l) = 0.V holds Carrier(l) = {}; antonym A is linearly-dependent; end; canceled; theorem :: RLVECT_3:6 A c= B & B is linearly-independent implies A is linearly-independent; theorem :: RLVECT_3:7 A is linearly-independent implies not 0.V in A; theorem :: RLVECT_3:8 {}(the carrier of V) is linearly-independent; theorem :: RLVECT_3:9 {v} is linearly-independent iff v <> 0.V; theorem :: RLVECT_3:10 {0.V} is linearly-dependent; theorem :: RLVECT_3:11 {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V; theorem :: RLVECT_3:12 {v,0.V} is linearly-dependent & {0.V,v} is linearly-dependent; theorem :: RLVECT_3:13 v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V & for a holds v1 <> a * v2; theorem :: RLVECT_3:14 v1 <> v2 & {v1,v2} is linearly-independent iff for a,b st a * v1 + b * v2 = 0.V holds a = 0 & b = 0; definition let V; let A; func Lin(A) -> strict Subspace of V means :: RLVECT_3:def 2 the carrier of it = {Sum(l) : not contradiction}; end; canceled 2; theorem :: RLVECT_3:17 x in Lin(A) iff ex l st x = Sum(l); theorem :: RLVECT_3:18 x in A implies x in Lin(A); reserve l0 for Linear_Combination of {}(the carrier of V); theorem :: RLVECT_3:19 Lin({}(the carrier of V)) = (0).V; theorem :: RLVECT_3:20 Lin(A) = (0).V implies A = {} or A = {0.V}; theorem :: RLVECT_3:21 for W being strict Subspace of V holds A = the carrier of W implies Lin(A) = W; theorem :: RLVECT_3:22 for V being strict RealLinearSpace,A being Subset of V holds A = the carrier of V implies Lin(A) = V; theorem :: RLVECT_3:23 A c= B implies Lin(A) is Subspace of Lin(B); theorem :: RLVECT_3:24 for V being strict RealLinearSpace,A,B being Subset of V holds Lin(A) = V & A c= B implies Lin(B) = V; theorem :: RLVECT_3:25 Lin(A \/ B) = Lin(A) + Lin(B); theorem :: RLVECT_3:26 Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B); theorem :: RLVECT_3:27 A is linearly-independent implies ex B st A c= B & B is linearly-independent & Lin(B) = the RLSStruct of V; theorem :: RLVECT_3:28 Lin(A) = V implies ex B st B c= A & B is linearly-independent & Lin(B) = V; definition let V be RealLinearSpace; mode Basis of V -> Subset of V means :: RLVECT_3:def 3 it is linearly-independent & Lin(it) = the RLSStruct of V; end; reserve I for Basis of V; canceled 3; theorem :: RLVECT_3:32 for V being strict RealLinearSpace,A being Subset of V holds A is linearly-independent implies ex I being Basis of V st A c= I; theorem :: RLVECT_3:33 Lin(A) = V implies ex I st I c= A; :: :: Auxiliary theorems. :: theorem :: RLVECT_3:34 Z <> {} & Z is finite & (for X,Y st X in Z & Y in Z holds X c= Y or Y c= X) implies union Z in Z; theorem :: RLVECT_3:35 not {} in M implies dom CF = M & rng CF c= union M; theorem :: RLVECT_3:36 x in (0).V iff x = 0.V; theorem :: RLVECT_3:37 W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3; theorem :: RLVECT_3:38 W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3; theorem :: RLVECT_3:39 W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3; theorem :: RLVECT_3:40 W1 is Subspace of W2 implies W1 is Subspace of W2 + W3; theorem :: RLVECT_3:41 f (#) (F ^ G) = (f (#) F) ^ (f (#) G);

Back to top