:: RUSUB_3 semantic presentation

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

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

theorem Th1: :: RUSUB_3:1
for b1 being RealUnitarySpace
for b2 being Subset of b1
for b3 being set holds
( b3 in Lin b2 iff ex b4 being Linear_Combination of b2 st b3 = Sum b4 )
proof end;

theorem Th2: :: RUSUB_3:2
for b1 being RealUnitarySpace
for b2 being Subset of b1
for b3 being set st b3 in b2 holds
b3 in Lin b2
proof end;

Lemma4: for b1 being RealUnitarySpace
for b2 being set holds
( b2 in (0). b1 iff b2 = 0. b1 )
proof end;

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

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

theorem Th5: :: RUSUB_3:5
for b1 being RealUnitarySpace
for b2 being strict Subspace of b1
for b3 being Subset of b1 st b3 = the carrier of b2 holds
Lin b3 = b2
proof end;

theorem Th6: :: RUSUB_3:6
for b1 being strict RealUnitarySpace
for b2 being Subset of b1 st b2 = the carrier of b1 holds
Lin b2 = b1
proof end;

Lemma6: for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b4 holds
b2 /\ b3 is Subspace of b4
proof end;

Lemma7: for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b3 & b2 is Subspace of b4 holds
b2 is Subspace of b3 /\ b4
proof end;

Lemma8: for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b3 holds
b2 is Subspace of b3 + b4
proof end;

Lemma9: for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b4 & b3 is Subspace of b4 holds
b2 + b3 is Subspace of b4
proof end;

theorem Th7: :: RUSUB_3:7
for b1 being RealUnitarySpace
for b2, b3 being Subset of b1 st b2 c= b3 holds
Lin b2 is Subspace of Lin b3
proof end;

theorem Th8: :: RUSUB_3:8
for b1 being strict RealUnitarySpace
for b2, b3 being Subset of b1 st Lin b2 = b1 & b2 c= b3 holds
Lin b3 = b1
proof end;

theorem Th9: :: RUSUB_3:9
for b1 being RealUnitarySpace
for b2, b3 being Subset of b1 holds Lin (b2 \/ b3) = (Lin b2) + (Lin b3)
proof end;

theorem Th10: :: RUSUB_3:10
for b1 being RealUnitarySpace
for b2, b3 being Subset of b1 holds Lin (b2 /\ b3) is Subspace of (Lin b2) /\ (Lin b3)
proof end;

theorem Th11: :: RUSUB_3:11
for b1 being RealUnitarySpace
for b2 being Subset of b1 st b2 is linearly-independent holds
ex b3 being Subset of b1 st
( b2 c= b3 & b3 is linearly-independent & Lin b3 = UNITSTR(# the carrier of b1,the Zero of b1,the add of b1,the Mult of b1,the scalar of b1 #) )
proof end;

theorem Th12: :: RUSUB_3:12
for b1 being RealUnitarySpace
for b2 being Subset of b1 st Lin b2 = b1 holds
ex b3 being Subset of b1 st
( b3 c= b2 & b3 is linearly-independent & Lin b3 = b1 )
proof end;

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

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

theorem Th13: :: RUSUB_3:13
for b1 being strict RealUnitarySpace
for b2 being Subset of b1 st b2 is linearly-independent holds
ex b3 being Basis of b1 st b2 c= b3
proof end;

theorem Th14: :: RUSUB_3:14
for b1 being RealUnitarySpace
for b2 being Subset of b1 st Lin b2 = b1 holds
ex b3 being Basis of b1 st b3 c= b2
proof end;

theorem Th15: :: RUSUB_3:15
for b1 being RealUnitarySpace
for b2 being Subset of b1 st b2 is linearly-independent holds
ex b3 being Basis of b1 st b2 c= b3
proof end;

theorem Th16: :: RUSUB_3:16
for b1 being RealUnitarySpace
for b2 being Linear_Combination of b1
for b3 being Subset of b1
for b4 being FinSequence of the carrier of b1 st rng b4 c= the carrier of (Lin b3) holds
ex b5 being Linear_Combination of b3 st Sum (b2 (#) b4) = Sum b5
proof end;

theorem Th17: :: RUSUB_3:17
for b1 being RealUnitarySpace
for b2 being Linear_Combination of b1
for b3 being Subset of b1 st Carrier b2 c= the carrier of (Lin b3) holds
ex b4 being Linear_Combination of b3 st Sum b2 = Sum b4
proof end;

theorem Th18: :: RUSUB_3:18
for b1 being RealUnitarySpace
for b2 being Subspace of b1
for b3 being Linear_Combination of b1 st Carrier b3 c= the carrier of b2 holds
for b4 being Linear_Combination of b2 st b4 = b3 | the carrier of b2 holds
( Carrier b3 = Carrier b4 & Sum b3 = Sum b4 )
proof end;

theorem Th19: :: RUSUB_3:19
for b1 being RealUnitarySpace
for b2 being Subspace of b1
for b3 being Linear_Combination of b2 ex b4 being Linear_Combination of b1 st
( Carrier b3 = Carrier b4 & Sum b3 = Sum b4 )
proof end;

theorem Th20: :: RUSUB_3:20
for b1 being RealUnitarySpace
for b2 being Subspace of b1
for b3 being Linear_Combination of b1 st Carrier b3 c= the carrier of b2 holds
ex b4 being Linear_Combination of b2 st
( Carrier b4 = Carrier b3 & Sum b4 = Sum b3 )
proof end;

theorem Th21: :: RUSUB_3:21
for b1 being RealUnitarySpace
for b2 being Basis of b1
for b3 being VECTOR of b1 holds b3 in Lin b2
proof end;

theorem Th22: :: RUSUB_3:22
for b1 being RealUnitarySpace
for b2 being Subspace of b1
for b3 being Subset of b2 st b3 is linearly-independent holds
b3 is linearly-independent Subset of b1
proof end;

theorem Th23: :: RUSUB_3:23
for b1 being RealUnitarySpace
for b2 being Subspace of b1
for b3 being Subset of b1 st b3 is linearly-independent & b3 c= the carrier of b2 holds
b3 is linearly-independent Subset of b2
proof end;

theorem Th24: :: RUSUB_3:24
for b1 being RealUnitarySpace
for b2 being Subspace of b1
for b3 being Basis of b2 ex b4 being Basis of b1 st b3 c= b4
proof end;

theorem Th25: :: RUSUB_3:25
for b1 being RealUnitarySpace
for b2 being Subset of b1 st b2 is linearly-independent holds
for b3 being VECTOR of b1 st b3 in b2 holds
for b4 being Subset of b1 st b4 = b2 \ {b3} holds
not b3 in Lin b4
proof end;

Lemma22: for b1, b2 being set st not b2 in b1 holds
b1 \ {b2} = b1
proof end;

theorem Th26: :: RUSUB_3:26
for b1 being RealUnitarySpace
for b2 being Basis of b1
for b3 being non empty Subset of b1 st b3 misses b2 holds
for b4 being Subset of b1 st b4 = b2 \/ b3 holds
not b4 is linearly-independent
proof end;

theorem Th27: :: RUSUB_3:27
for b1 being RealUnitarySpace
for b2 being Subspace of b1
for b3 being Subset of b1 st b3 c= the carrier of b2 holds
Lin b3 is Subspace of b2
proof end;

theorem Th28: :: RUSUB_3:28
for b1 being RealUnitarySpace
for b2 being Subspace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
Lin b3 = Lin b4
proof end;

theorem Th29: :: RUSUB_3:29
for b1 being RealUnitarySpace
for b2 being VECTOR of b1
for b3 being set holds
( b3 in Lin {b2} iff ex b4 being Real st b3 = b4 * b2 )
proof end;

theorem Th30: :: RUSUB_3:30
for b1 being RealUnitarySpace
for b2 being VECTOR of b1 holds b2 in Lin {b2}
proof end;

theorem Th31: :: RUSUB_3:31
for b1 being RealUnitarySpace
for b2, b3 being VECTOR of b1
for b4 being set holds
( b4 in b2 + (Lin {b3}) iff ex b5 being Real st b4 = b2 + (b5 * b3) )
proof end;

theorem Th32: :: RUSUB_3:32
for b1 being RealUnitarySpace
for b2, b3 being VECTOR of b1
for b4 being set holds
( b4 in Lin {b2,b3} iff ex b5, b6 being Real st b4 = (b5 * b2) + (b6 * b3) )
proof end;

theorem Th33: :: RUSUB_3:33
for b1 being RealUnitarySpace
for b2, b3 being VECTOR of b1 holds
( b2 in Lin {b2,b3} & b3 in Lin {b2,b3} )
proof end;

theorem Th34: :: RUSUB_3:34
for b1 being RealUnitarySpace
for b2, b3, b4 being VECTOR of b1
for b5 being set holds
( b5 in b2 + (Lin {b3,b4}) iff ex b6, b7 being Real st b5 = (b2 + (b6 * b3)) + (b7 * b4) )
proof end;

theorem Th35: :: RUSUB_3:35
for b1 being RealUnitarySpace
for b2, b3, b4 being VECTOR of b1
for b5 being set holds
( b5 in Lin {b2,b3,b4} iff ex b6, b7, b8 being Real st b5 = ((b6 * b2) + (b7 * b3)) + (b8 * b4) )
proof end;

theorem Th36: :: RUSUB_3:36
for b1 being RealUnitarySpace
for b2, b3, b4 being VECTOR of b1 holds
( b2 in Lin {b2,b3,b4} & b3 in Lin {b2,b3,b4} & b4 in Lin {b2,b3,b4} )
proof end;

theorem Th37: :: RUSUB_3:37
for b1 being RealUnitarySpace
for b2, b3, b4, b5 being VECTOR of b1
for b6 being set holds
( b6 in b2 + (Lin {b3,b4,b5}) iff ex b7, b8, b9 being Real st b6 = ((b2 + (b7 * b3)) + (b8 * b4)) + (b9 * b5) )
proof end;

theorem Th38: :: RUSUB_3:38
for b1 being RealUnitarySpace
for b2, b3 being VECTOR of b1 st b2 in Lin {b3} & b2 <> 0. b1 holds
Lin {b2} = Lin {b3}
proof end;

theorem Th39: :: RUSUB_3:39
for b1 being RealUnitarySpace
for b2, b3, b4, b5 being VECTOR of b1 st b2 <> b3 & {b2,b3} is linearly-independent & b2 in Lin {b4,b5} & b3 in Lin {b4,b5} holds
( Lin {b4,b5} = Lin {b2,b3} & {b4,b5} is linearly-independent & b4 <> b5 )
proof end;

theorem Th40: :: RUSUB_3:40
for b1 being RealUnitarySpace
for b2 being set holds
( b2 in (0). b1 iff b2 = 0. b1 ) by Lemma4;

theorem Th41: :: RUSUB_3:41
for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b4 holds
b2 /\ b3 is Subspace of b4 by Lemma6;

theorem Th42: :: RUSUB_3:42
for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b3 & b2 is Subspace of b4 holds
b2 is Subspace of b3 /\ b4 by Lemma7;

theorem Th43: :: RUSUB_3:43
for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b4 & b3 is Subspace of b4 holds
b2 + b3 is Subspace of b4 by Lemma9;

theorem Th44: :: RUSUB_3:44
for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b3 holds
b2 is Subspace of b3 + b4 by Lemma8;

theorem Th45: :: RUSUB_3:45
for b1 being RealUnitarySpace
for b2, b3 being Subspace of b1
for b4 being VECTOR of b1 st b2 is Subspace of b3 holds
b4 + b2 c= b4 + b3
proof end;