:: 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;