:: Linear Combinations in Real Unitary Space :: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama :: :: Received October 9, 2002 :: Copyright (c) 2002-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 BHSP_1, SUBSET_1, RLVECT_3, STRUCT_0, RLSUB_1, CARD_3, RLVECT_2, TARSKI, RLVECT_1, ARYTM_3, REAL_1, RELAT_1, SUPINF_2, CARD_1, FUNCT_1, NUMBERS, FUNCT_2, FINSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, ORDERS_1, ARYTM_1, FINSEQ_1, VALUED_1, NAT_1, ORDINAL4, CLASSES1, XXREAL_0, PARTFUN1, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, ORDERS_1, DOMAIN_1, STRUCT_0, RLVECT_1, FINSET_1, RLSUB_1, RLVECT_2, BHSP_1, RLVECT_3, RUSUB_1, RUSUB_2, CLASSES1, XXREAL_0; constructors PARTFUN1, XXREAL_0, REAL_1, NAT_1, ORDERS_1, REALSET1, RFINSEQ, RLVECT_2, RLVECT_3, CLASSES1, RUSUB_2, RELSET_1, NUMBERS; registrations SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, FINSEQ_1, STRUCT_0, RLVECT_3, BHSP_1, RUSUB_1, CARD_1, RLVECT_2, XREAL_0; 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 = the set of all Sum(l) where l is Linear_Combination of A; end; theorem :: RUSUB_3:1 for V being RealUnitarySpace, A being Subset of V, x be object 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 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 A is linearly-independent Subset of V; 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 A is linearly-independent Subset of W; 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;