Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Linear Combinations in Real Unitary Space

by
Noboru Endou,
Takashi Mitsuishi, and
Yasunari Shidama

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;

```