:: Subspaces and Cosets of Subspace of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

definition
let V be RealUnitarySpace;
mode Subspace of V -> RealUnitarySpace means :Def1: :: RUSUB_1:def 1
( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V || the carrier of it & the Mult of it = the Mult of V | [:REAL, the carrier of it:] & the scalar of it = the scalar of V || the carrier of it );
existence
ex b1 being RealUnitarySpace st
( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:REAL, the carrier of b1:] & the scalar of b1 = the scalar of V || the carrier of b1 )
proof end;
end;

:: deftheorem Def1 defines Subspace RUSUB_1:def 1 :
for V, b2 being RealUnitarySpace holds
( b2 is Subspace of V iff ( the carrier of b2 c= the carrier of V & 0. b2 = 0. V & the addF of b2 = the addF of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:REAL, the carrier of b2:] & the scalar of b2 = the scalar of V || the carrier of b2 ) );

theorem :: RUSUB_1:1
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for x being set st x in W1 & W1 is Subspace of W2 holds
x in W2
proof end;

theorem Th2: :: RUSUB_1:2
for V being RealUnitarySpace
for W being Subspace of V
for x being set st x in W holds
x in V
proof end;

theorem Th3: :: RUSUB_1:3
for V being RealUnitarySpace
for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V
proof end;

theorem :: RUSUB_1:4
for V being RealUnitarySpace
for W being Subspace of V holds 0. W = 0. V by Def1;

theorem :: RUSUB_1:5
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds 0. W1 = 0. W2
proof end;

theorem Th6: :: RUSUB_1:6
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
proof end;

theorem Th7: :: RUSUB_1:7
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W
for a being Real st w = v holds
a * w = a * v
proof end;

theorem :: RUSUB_1:8
for V being RealUnitarySpace
for W being Subspace of V
for v1, v2 being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v1 & w2 = v2 holds
w1 .|. w2 = v1 .|. v2
proof end;

theorem Th9: :: RUSUB_1:9
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W st w = v holds
- v = - w
proof end;

theorem Th10: :: RUSUB_1:10
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
proof end;

theorem Th11: :: RUSUB_1:11
for V being RealUnitarySpace
for W being Subspace of V holds 0. V in W
proof end;

theorem :: RUSUB_1:12
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds 0. W1 in W2
proof end;

theorem :: RUSUB_1:13
for V being RealUnitarySpace
for W being Subspace of V holds 0. W in V by Th2, RLVECT_1:1;

Lm1: for V being RealUnitarySpace
for W being Subspace of V
for V1, V2 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
proof end;

theorem Th14: :: RUSUB_1:14
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st u in W & v in W holds
u + v in W
proof end;

theorem Th15: :: RUSUB_1:15
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
a * v in W
proof end;

theorem Th16: :: RUSUB_1:16
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V st v in W holds
- v in W
proof end;

theorem Th17: :: RUSUB_1:17
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st u in W & v in W holds
u - v in W
proof end;

theorem Th18: :: RUSUB_1:18
for V being RealUnitarySpace
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being Function of [:D,D:],REAL st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 holds
UNITSTR(# D,d1,A,M,S #) is Subspace of V
proof end;

theorem Th19: :: RUSUB_1:19
for V being RealUnitarySpace holds V is Subspace of V
proof end;

theorem Th20: :: RUSUB_1:20
for V, X being strict RealUnitarySpace st V is Subspace of X & X is Subspace of V holds
V = X
proof end;

theorem Th21: :: RUSUB_1:21
for V, X, Y being RealUnitarySpace st V is Subspace of X & X is Subspace of Y holds
V is Subspace of Y
proof end;

theorem Th22: :: RUSUB_1:22
for V being RealUnitarySpace
for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 is Subspace of W2
proof end;

theorem :: RUSUB_1:23
for V being RealUnitarySpace
for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds
v in W2 ) holds
W1 is Subspace of W2
proof end;

registration
let V be RealUnitarySpace;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like for Subspace of V;
existence
ex b1 being Subspace of V st b1 is strict
proof end;
end;

theorem Th24: :: RUSUB_1:24
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
proof end;

theorem Th25: :: RUSUB_1:25
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2
proof end;

theorem :: RUSUB_1:26
for V being strict RealUnitarySpace
for W being strict Subspace of V st the carrier of W = the carrier of V holds
W = V
proof end;

theorem :: RUSUB_1:27
for V being strict RealUnitarySpace
for W being strict Subspace of V st ( for v being VECTOR of V holds
( v in W iff v in V ) ) holds
W = V
proof end;

theorem :: RUSUB_1:28
for V being RealUnitarySpace
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed by Lm1;

theorem Th29: :: RUSUB_1:29
for V being RealUnitarySpace
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
proof end;

begin

:: Definition of Zero Subspace and Improper Subspace of Real Unitary Space
definition
let V be RealUnitarySpace;
func (0). V -> strict Subspace of V means :Def2: :: RUSUB_1:def 2
 the carrier of it = {(0. V)};
correctness
existence
ex b1 being strict Subspace of V st the carrier of b1 = {(0. V)};
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = {(0. V)} & the carrier of b2 = {(0. V)} holds
b1 = b2;
by Th24, Th29, RLSUB_1:4;
end;

:: deftheorem Def2 defines (0). RUSUB_1:def 2 :
for V being RealUnitarySpace
for b2 being strict Subspace of V holds
( b2 = (0). V iff the carrier of b2 = {(0. V)} );

definition
let V be RealUnitarySpace;
func (Omega). V -> strict Subspace of V equals :: RUSUB_1:def 3
 UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #);
coherence
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict Subspace of V
proof end;
end;

:: deftheorem defines (Omega). RUSUB_1:def 3 :
for V being RealUnitarySpace holds (Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #);

begin

theorem Th30: :: RUSUB_1:30
for V being RealUnitarySpace
for W being Subspace of V holds (0). W = (0). V
proof end;

theorem Th31: :: RUSUB_1:31
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds (0). W1 = (0). W2
proof end;

theorem :: RUSUB_1:32
for V being RealUnitarySpace
for W being Subspace of V holds (0). W is Subspace of V by Th21;

theorem :: RUSUB_1:33
for V being RealUnitarySpace
for W being Subspace of V holds (0). V is Subspace of W
proof end;

theorem :: RUSUB_1:34
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2
proof end;

theorem :: RUSUB_1:35
for V being strict RealUnitarySpace holds V is Subspace of (Omega). V ;

begin

definition
let V be RealUnitarySpace;
let v be VECTOR of V;
let W be Subspace of V;
func v + W -> Subset of V equals :: RUSUB_1:def 4
 { (v + u) where u is VECTOR of V : u in W } ;
coherence
{ (v + u) where u is VECTOR of V : u in W } is Subset of V
proof end;
end;

:: deftheorem defines + RUSUB_1:def 4 :
for V being RealUnitarySpace
for v being VECTOR of V
for W being Subspace of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ;

Lm2: for V being RealUnitarySpace
for W being Subspace of V holds (0. V) + W = the carrier of W
proof end;

definition
let V be RealUnitarySpace;
let W be Subspace of V;
mode Coset of W -> Subset of V means :Def5: :: RUSUB_1:def 5
 ex v being VECTOR of V st it = v + W;
existence
ex b1 being Subset of V ex v being VECTOR of V st b1 = v + W
proof end;
end;

:: deftheorem Def5 defines Coset RUSUB_1:def 5 :
for V being RealUnitarySpace
for W being Subspace of V
for b3 being Subset of V holds
( b3 is Coset of W iff ex v being VECTOR of V st b3 = v + W );

begin

theorem Th36: :: RUSUB_1:36
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( 0. V in v + W iff v in W )
proof end;

theorem Th37: :: RUSUB_1:37
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds v in v + W
proof end;

theorem :: RUSUB_1:38
for V being RealUnitarySpace
for W being Subspace of V holds (0. V) + W = the carrier of W by Lm2;

theorem Th39: :: RUSUB_1:39
for V being RealUnitarySpace
for v being VECTOR of V holds v + ((0). V) = {v}
proof end;

Lm3: for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v in W iff v + W = the carrier of W )
proof end;

theorem Th40: :: RUSUB_1:40
for V being RealUnitarySpace
for v being VECTOR of V holds v + ((Omega). V) = the carrier of V
proof end;

theorem Th41: :: RUSUB_1:41
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( 0. V in v + W iff v + W = the carrier of W )
proof end;

theorem :: RUSUB_1:42
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v in W iff v + W = the carrier of W ) by Lm3;

theorem Th43: :: RUSUB_1:43
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
(a * v) + W = the carrier of W
proof end;

theorem Th44: :: RUSUB_1:44
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st a <> 0 & (a * v) + W = the carrier of W holds
v in W
proof end;

theorem Th45: :: RUSUB_1:45
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v in W iff (- v) + W = the carrier of W )
proof end;

theorem Th46: :: RUSUB_1:46
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in W iff v + W = (v + u) + W )
proof end;

theorem :: RUSUB_1:47
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in W iff v + W = (v - u) + W )
proof end;

theorem Th48: :: RUSUB_1:48
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( v in u + W iff u + W = v + W )
proof end;

theorem Th49: :: RUSUB_1:49
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v + W = (- v) + W iff v in W )
proof end;

theorem Th50: :: RUSUB_1:50
for V being RealUnitarySpace
for W being Subspace of V
for u, v1, v2 being VECTOR of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
proof end;

theorem :: RUSUB_1:51
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st u in v + W & u in (- v) + W holds
v in W
proof end;

theorem Th52: :: RUSUB_1:52
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st a <> 1 & a * v in v + W holds
v in W
proof end;

theorem Th53: :: RUSUB_1:53
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
a * v in v + W
proof end;

theorem :: RUSUB_1:54
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( - v in v + W iff v in W )
proof end;

theorem Th55: :: RUSUB_1:55
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u + v in v + W iff u in W )
proof end;

theorem :: RUSUB_1:56
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( v - u in v + W iff u in W )
proof end;

theorem Th57: :: RUSUB_1:57
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
proof end;

theorem :: RUSUB_1:58
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
proof end;

theorem Th59: :: RUSUB_1:59
for V being RealUnitarySpace
for W being Subspace of V
for v1, v2 being VECTOR of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
proof end;

theorem Th60: :: RUSUB_1:60
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
proof end;

theorem Th61: :: RUSUB_1:61
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
proof end;

theorem Th62: :: RUSUB_1:62
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V
for v being VECTOR of V holds
( v + W1 = v + W2 iff W1 = W2 )
proof end;

theorem Th63: :: RUSUB_1:63
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V
for u, v being VECTOR of V st v + W1 = u + W2 holds
W1 = W2
proof end;

theorem :: RUSUB_1:64
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
proof end;

theorem :: RUSUB_1:65
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
proof end;

theorem :: RUSUB_1:66
for V being RealUnitarySpace
for v being VECTOR of V holds {v} is Coset of (0). V
proof end;

theorem :: RUSUB_1:67
for V being RealUnitarySpace
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}
proof end;

theorem :: RUSUB_1:68
for V being RealUnitarySpace
for W being Subspace of V holds the carrier of W is Coset of W
proof end;

theorem :: RUSUB_1:69
for V being RealUnitarySpace holds the carrier of V is Coset of (Omega). V
proof end;

theorem :: RUSUB_1:70
for V being RealUnitarySpace
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
proof end;

theorem :: RUSUB_1:71
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
proof end;

theorem Th72: :: RUSUB_1:72
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W
for u being VECTOR of V holds
( u in C iff C = u + W )
proof end;

theorem :: RUSUB_1:73
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W
for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
proof end;

theorem :: RUSUB_1:74
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W
for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
proof end;

theorem :: RUSUB_1:75
for V being RealUnitarySpace
for W being Subspace of V
for v1, v2 being VECTOR of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
proof end;

theorem :: RUSUB_1:76
for V being RealUnitarySpace
for W being Subspace of V
for u being VECTOR of V
for B, C being Coset of W st u in B & u in C holds
B = C
proof end;