Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Linear Combinations in Real Unitary Space

**by****Noboru Endou,****Takashi Mitsuishi, and****Yasunari Shidama**- Received October 9, 2002
- MML identifier: RUSUB_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, BHSP_1, RFINSEQ; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, NAT_1, FINSEQ_1, RELAT_1, ORDINAL1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1, FINSEQ_4, FRAENKEL, FINSET_1, RLSUB_1, ORDERS_1, RLVECT_2, BHSP_1, RLVECT_3, RUSUB_1, RUSUB_2, RFINSEQ; constructors NAT_1, REAL_1, ORDERS_1, RLVECT_2, FINSEQ_4, DOMAIN_1, PARTFUN1, RLVECT_3, RFINSEQ, RUSUB_2, XREAL_0, MEMBERED; clusters SUBSET_1, FINSET_1, RELSET_1, STRUCT_0, ARYTM_3, BHSP_1, RUSUB_1, FINSEQ_1, FUNCT_2, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Definition and fundamental properties of linear combination definition let V be RealUnitarySpace; let A be Subset of V; func Lin(A) -> strict Subspace of V means :: RUSUB_3:def 1 the carrier of it = {Sum(l) where l is Linear_Combination of A: not contradiction}; end; theorem :: RUSUB_3:1 for V being RealUnitarySpace, A being Subset of V, x be set holds x in Lin(A) iff ex l being Linear_Combination of A st x = Sum(l); theorem :: RUSUB_3:2 for V being RealUnitarySpace, A being Subset of V, x being set st x in A holds x in Lin(A); theorem :: RUSUB_3:3 for V being RealUnitarySpace holds Lin({}(the carrier of V)) = (0).V; theorem :: RUSUB_3:4 for V being RealUnitarySpace, A being Subset of V st Lin(A) = (0).V holds A = {} or A = {0.V}; theorem :: RUSUB_3:5 for V being RealUnitarySpace, W being strict Subspace of V, A being Subset of V st A = the carrier of W holds Lin(A) = W; theorem :: RUSUB_3:6 for V being strict RealUnitarySpace,A being Subset of V holds A = the carrier of V implies Lin(A) = V; theorem :: RUSUB_3:7 for V being RealUnitarySpace, A,B being Subset of V st A c= B holds Lin(A) is Subspace of Lin(B); theorem :: RUSUB_3:8 for V being strict RealUnitarySpace, A,B being Subset of V st Lin(A) = V & A c= B holds Lin(B) = V; theorem :: RUSUB_3:9 for V being RealUnitarySpace, A,B being Subset of V holds Lin(A \/ B) = Lin(A) + Lin(B); theorem :: RUSUB_3:10 for V being RealUnitarySpace, A,B being Subset of V holds Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B); theorem :: RUSUB_3:11 for V being RealUnitarySpace, A being Subset of V st A is linearly-independent holds ex B being Subset of V st A c= B & B is linearly-independent & Lin(B) = the UNITSTR of V; theorem :: RUSUB_3:12 for V being RealUnitarySpace, A being Subset of V st Lin(A) = V holds ex B being Subset of V st B c= A & B is linearly-independent & Lin(B) = V; begin :: Definition of the basis of real unitay space definition let V be RealUnitarySpace; mode Basis of V -> Subset of V means :: RUSUB_3:def 2 it is linearly-independent & Lin(it) = the UNITSTR of V; end; theorem :: RUSUB_3:13 for V being strict RealUnitarySpace, A being Subset of V st A is linearly-independent holds ex I being Basis of V st A c= I; theorem :: RUSUB_3:14 for V being RealUnitarySpace, A being Subset of V st Lin(A) = V holds ex I being Basis of V st I c= A; theorem :: RUSUB_3:15 for V being RealUnitarySpace, A being Subset of V st A is linearly-independent holds ex I being Basis of V st A c= I; begin :: Some theorems of Lin, Sum, Carrier theorem :: RUSUB_3:16 for V being RealUnitarySpace, L being Linear_Combination of V, A being Subset of V, 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 :: RUSUB_3:17 for V being RealUnitarySpace, L being Linear_Combination of V, 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 :: RUSUB_3:18 for V being RealUnitarySpace, W being Subspace of V, 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 :: RUSUB_3:19 for V being RealUnitarySpace, W being Subspace of V, K being Linear_Combination of W holds ex L being Linear_Combination of V st Carrier(K) = Carrier(L) & Sum(K) = Sum(L); theorem :: RUSUB_3:20 for V being RealUnitarySpace, W being Subspace of V, 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); theorem :: RUSUB_3:21 for V being RealUnitarySpace, I being Basis of V, v being VECTOR of V holds v in Lin(I); theorem :: RUSUB_3:22 for V being RealUnitarySpace, W being Subspace of V, 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 :: RUSUB_3:23 for V being RealUnitarySpace, W being Subspace of V, 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 :: RUSUB_3:24 for V being RealUnitarySpace, W being Subspace of V, A being Basis of W ex B being Basis of V st A c= B; theorem :: RUSUB_3:25 for V being RealUnitarySpace, 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 :: RUSUB_3:26 for V being RealUnitarySpace, I being Basis of V, 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 :: RUSUB_3:27 for V being RealUnitarySpace, W being Subspace of V, A being Subset of V st A c= the carrier of W holds Lin(A) is Subspace of W; theorem :: RUSUB_3:28 for V being RealUnitarySpace, W being Subspace of V, A being Subset of V, B being Subset of W st A = B holds Lin(A) = Lin(B); begin ::Subspaces of real unitary space generated by one, two, or three vectors theorem :: RUSUB_3:29 for V being RealUnitarySpace, v being VECTOR of V, x being set holds x in Lin{v} iff ex a being Real st x = a * v; theorem :: RUSUB_3:30 for V being RealUnitarySpace, v being VECTOR of V holds v in Lin{v}; theorem :: RUSUB_3:31 for V being RealUnitarySpace, v,w being VECTOR of V, x being set holds x in v + Lin{w} iff ex a being Real st x = v + a * w; theorem :: RUSUB_3:32 for V being RealUnitarySpace, w1,w2 being VECTOR of V, x being set holds x in Lin{w1,w2} iff ex a,b being Real st x = a * w1 + b * w2; theorem :: RUSUB_3:33 for V being RealUnitarySpace, w1,w2 being VECTOR of V holds w1 in Lin{w1,w2} & w2 in Lin{w1,w2}; theorem :: RUSUB_3:34 for V being RealUnitarySpace, v,w1,w2 being VECTOR of V, x being set holds x in v + Lin{w1,w2} iff ex a,b being Real st x = v + a * w1 + b * w2; theorem :: RUSUB_3:35 for V being RealUnitarySpace, v1,v2,v3 being VECTOR of V, x being set holds x in Lin{v1,v2,v3} iff ex a,b,c being Real st x = a * v1 + b * v2 + c * v3; theorem :: RUSUB_3:36 for V being RealUnitarySpace, w1,w2,w3 being VECTOR of V holds w1 in Lin{w1,w2,w3} & w2 in Lin{w1,w2,w3} & w3 in Lin{w1,w2,w3}; theorem :: RUSUB_3:37 for V being RealUnitarySpace, v,w1,w2,w3 being VECTOR of V, x being set holds x in v + Lin{w1,w2,w3} iff ex a,b,c being Real st x = v + a * w1 + b * w2 + c * w3; theorem :: RUSUB_3:38 for V being RealUnitarySpace, v,w being VECTOR of V st v in Lin{w} & v <> 0.V holds Lin{v} = Lin{w}; theorem :: RUSUB_3:39 for V being RealUnitarySpace, v1,v2,w1,w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin{w1,w2} & v2 in Lin{w1,w2} holds Lin{w1,w2} = Lin{v1,v2} & {w1,w2} is linearly-independent & w1 <> w2; begin :: Auxiliary theorems theorem :: RUSUB_3:40 for V being RealUnitarySpace, x being set holds x in (0).V iff x = 0.V; theorem :: RUSUB_3:41 for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is Subspace of W3 holds W1 /\ W2 is Subspace of W3; theorem :: RUSUB_3:42 for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds W1 is Subspace of W2 /\ W3; theorem :: RUSUB_3:43 for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds W1 + W2 is Subspace of W3; theorem :: RUSUB_3:44 for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is Subspace of W2 holds W1 is Subspace of W2 + W3; theorem :: RUSUB_3:45 for V being RealUnitarySpace, W1,W2 being Subspace of V, v being VECTOR of V st W1 is Subspace of W2 holds v + W1 c= v + W2;

Back to top