:: Linear Combinations in Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002-2011 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 b₁ being strict Subspace of V st the carrier of b₁ = { (Sum l) where l is Linear_Combination of A : verum }

proof end;

uniqueness
for b₁, b₂ being strict Subspace of V st the carrier of b₁ = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b₂ = { (Sum l) where l is Linear_Combination of A : verum } holds
b₁ = b₂ by RUSUB_1:24;

end;

:: deftheorem Def1 defines Lin RUSUB_3:def 1 :
for V being RealUnitarySpace
for A being Subset of V
for b₃ being strict Subspace of V holds
( b₃ = Lin A iff the carrier of b₃ = { (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 b₁ being Subset of V st
( 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;

end;

:: deftheorem Def2 defines Basis RUSUB_3:def 2 :
for V being RealUnitarySpace
for b₂ being Subset of V holds
( b₂ is Basis of V iff ( 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 #) ) );

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;