:: Linear Combinations in Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002 Association of Mizar Users


begin

definition
let V be RealUnitarySpace;
let A be Subset of V;
func Lin A -> strict Subspace of V means :Def1: :: RUSUB_3:def 1
 the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;
existence
ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum }
proof end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b2 = { (Sum l) where l is Linear_Combination of A : verum } holds
b1 = b2 by RUSUB_1:24;
end;

:: deftheorem Def1 defines Lin RUSUB_3:def 1 :
for V being RealUnitarySpace
for A being Subset of V
for b3 being strict Subspace of V holds
( b3 = Lin A iff the carrier of b3 = { (Sum l) where l is Linear_Combination of A : verum } );

theorem Th1: :: RUSUB_3:1
for V being RealUnitarySpace
for A being Subset of V
for x being set holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
proof end;

theorem Th2: :: RUSUB_3:2
for V being RealUnitarySpace
for A being Subset of V
for x being set st x in A holds
x in Lin A
proof end;

Lm1: for V being RealUnitarySpace
for x being set holds
( x in (0). V iff x = 0. V )
proof end;

theorem :: RUSUB_3:3
for V being RealUnitarySpace holds Lin ({} the carrier of V) = (0). V
proof end;

theorem :: RUSUB_3:4
for V being RealUnitarySpace
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proof end;

theorem Th5: :: RUSUB_3:5
for V being RealUnitarySpace
for W being strict Subspace of V
for A being Subset of V st A = the carrier of W holds
Lin A = W
proof end;

theorem :: RUSUB_3:6
for V being strict RealUnitarySpace
for A being Subset of V st A = the carrier of V holds
Lin A = V
proof end;

Lm2: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
proof end;

Lm3: for V being RealUnitarySpace
for 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
proof end;

Lm4: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
proof end;

Lm5: for V being RealUnitarySpace
for 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
proof end;

theorem Th7: :: RUSUB_3:7
for V being RealUnitarySpace
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proof end;

theorem :: RUSUB_3:8
for V being strict RealUnitarySpace
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof end;

theorem :: RUSUB_3:9
for V being RealUnitarySpace
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof end;

theorem :: RUSUB_3:10
for V being RealUnitarySpace
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proof end;

theorem Th11: :: RUSUB_3:11
for V being RealUnitarySpace
for 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 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )
proof end;

theorem Th12: :: RUSUB_3:12
for V being RealUnitarySpace
for 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 )
proof end;

begin

definition
let V be RealUnitarySpace;
mode Basis of V -> Subset of V means :Def2: :: RUSUB_3:def 2
( it is linearly-independent & Lin it = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) );
existence
ex b1 being Subset of V st
( b1 is linearly-independent & Lin b1 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )
proof end;
end;

:: deftheorem Def2 defines Basis RUSUB_3:def 2 :
for V being RealUnitarySpace
for b2 being Subset of V holds
( b2 is Basis of V iff ( b2 is linearly-independent & Lin b2 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) );

theorem :: RUSUB_3:13
for V being strict RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof end;

theorem :: RUSUB_3:14
for V being RealUnitarySpace
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
proof end;

theorem Th15: :: RUSUB_3:15
for V being RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof end;

begin

theorem Th16: :: RUSUB_3:16
for V being RealUnitarySpace
for L being Linear_Combination of V
for A being Subset of V
for 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
proof end;

theorem :: RUSUB_3:17
for V being RealUnitarySpace
for L being Linear_Combination of V
for 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
proof end;

theorem Th18: :: RUSUB_3:18
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
proof end;

theorem Th19: :: RUSUB_3:19
for V being RealUnitarySpace
for W being Subspace of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
proof end;

theorem Th20: :: RUSUB_3:20
for V being RealUnitarySpace
for W being Subspace of V
for 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 )
proof end;

theorem Th21: :: RUSUB_3:21
for V being RealUnitarySpace
for I being Basis of V
for v being VECTOR of V holds v in Lin I
proof end;

theorem Th22: :: RUSUB_3:22
for V being RealUnitarySpace
for W being Subspace of V
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
proof end;

theorem :: RUSUB_3:23
for V being RealUnitarySpace
for W being Subspace of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
proof end;

theorem :: RUSUB_3:24
for V being RealUnitarySpace
for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
proof end;

theorem Th25: :: RUSUB_3:25
for V being RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
for v being VECTOR of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
proof end;

Lm6: for X, x being set st not x in X holds
X \ {x} = X
proof end;

theorem :: RUSUB_3:26
for V being RealUnitarySpace
for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
not B is linearly-independent
proof end;

theorem :: RUSUB_3:27
for V being RealUnitarySpace
for W being Subspace of V
for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
proof end;

theorem :: RUSUB_3:28
for V being RealUnitarySpace
for W being Subspace of V
for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
proof end;

begin

theorem Th29: :: RUSUB_3:29
for V being RealUnitarySpace
for v being VECTOR of V
for x being set holds
( x in Lin {v} iff ex a being Real st x = a * v )
proof end;

theorem :: RUSUB_3:30
for V being RealUnitarySpace
for v being VECTOR of V holds v in Lin {v}
proof end;

theorem :: RUSUB_3:31
for V being RealUnitarySpace
for v, w being VECTOR of V
for x being set holds
( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
proof end;

theorem Th32: :: RUSUB_3:32
for V being RealUnitarySpace
for w1, w2 being VECTOR of V
for x being set holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
proof end;

theorem :: RUSUB_3:33
for V being RealUnitarySpace
for w1, w2 being VECTOR of V holds
( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
proof end;

theorem :: RUSUB_3:34
for V being RealUnitarySpace
for v, w1, w2 being VECTOR of V
for x being set holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
proof end;

theorem Th35: :: RUSUB_3:35
for V being RealUnitarySpace
for v1, v2, v3 being VECTOR of V
for 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) )
proof end;

theorem :: RUSUB_3:36
for V being RealUnitarySpace
for 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} )
proof end;

theorem :: RUSUB_3:37
for V being RealUnitarySpace
for v, w1, w2, w3 being VECTOR of V
for 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) )
proof end;

theorem :: RUSUB_3:38
for V being RealUnitarySpace
for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds
Lin {v} = Lin {w}
proof end;

theorem :: RUSUB_3:39
for V being RealUnitarySpace
for 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 )
proof end;

begin

theorem :: RUSUB_3:40
for V being RealUnitarySpace
for x being set holds
( x in (0). V iff x = 0. V ) by Lm1;

theorem :: RUSUB_3:41
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3 by Lm2;

theorem :: RUSUB_3:42
for V being RealUnitarySpace
for 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 by Lm3;

theorem :: RUSUB_3:43
for V being RealUnitarySpace
for 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 by Lm5;

theorem :: RUSUB_3:44
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3 by Lm4;

theorem :: RUSUB_3:45
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for v being VECTOR of V st W1 is Subspace of W2 holds
v + W1 c= v + W2
proof end;