:: Subspaces and Cosets of Subspaces in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1:  for GF being non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a, b being Element of GF
for v being Element of V holds (a - b) * v = (a * v) - (b * v)
proofend;

definition
let GF be non empty multMagma ;
let V be non empty VectSpStr over GF;
let V1 be Subset of V;
attrV1 is linearly-closed  means :Def1: :: VECTSP_4:def 1
( ( for v, u being Element of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Element of GF
for v being Element of V st v in V1 holds
a * v in V1 ) );
end;

:: deftheorem Def1 defines linearly-closed VECTSP_4:def_1_:_
 for GF being non empty multMagma
for V being non empty VectSpStr over GF
for V1 being Subset of V holds
( V1 is linearly-closed iff ( ( for v, u being Element of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Element of GF
for v being Element of V st v in V1 holds
a * v in V1 ) ) );

theorem Th1: :: VECTSP_4:1
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1 being Subset of V st V1 <> {} &amp; V1 is linearly-closed holds
0. V in V1
proofend;

theorem Th2: :: VECTSP_4:2
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1 being Subset of V st V1 is linearly-closed holds
for v being Element of V st v in V1 holds
- v in V1
proofend;

theorem :: VECTSP_4:3
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1 being Subset of V st V1 is linearly-closed holds
for v, u being Element of V st v in V1 &amp; u in V1 holds
v - u in V1
proofend;

theorem Th4: :: VECTSP_4:4
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds {(0. V)} is linearly-closed
proofend;

theorem :: VECTSP_4:5
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1 being Subset of V st the carrier of V = V1 holds
V1 is linearly-closed
proofend;

theorem :: VECTSP_4:6
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1, V2, V3 being Subset of V st V1 is linearly-closed &amp; V2 is linearly-closed &amp; V3 =  {  (v + u) where v, u is Element of V : ( v in V1 &amp; u in V2 )  }  holds
V3 is linearly-closed
proofend;

theorem :: VECTSP_4:7
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1, V2 being Subset of V st V1 is linearly-closed &amp; V2 is linearly-closed holds
V1 /\ V2 is linearly-closed
proofend;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
mode Subspace of V ->  non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF means :Def2: :: VECTSP_4:def 2
( the carrier of it c= the carrier of V &amp; 0. it = 0. V &amp; the addF of it = the addF of V || the carrier of it &amp; the lmult of it = the lmult of V | [: the carrier of GF, the carrier of it:] );
existence
 ex b1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF st
( the carrier of b1 c= the carrier of V &amp; 0. b1 = 0. V &amp; the addF of b1 = the addF of V || the carrier of b1 &amp; the lmult of b1 = the lmult of V | [: the carrier of GF, the carrier of b1:] )
proofend;
end;

:: deftheorem Def2 defines Subspace VECTSP_4:def_2_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V, b3 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds
( b3 is Subspace of V iff ( the carrier of b3 c= the carrier of V &amp; 0. b3 = 0. V &amp; the addF of b3 = the addF of V || the carrier of b3 &amp; the lmult of b3 = the lmult of V | [: the carrier of GF, the carrier of b3:] ) );

theorem :: VECTSP_4:8
for x being set
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of V st x in W1 &amp; W1 is Subspace of W2 holds
x in W2
proofend;

theorem Th9: :: VECTSP_4:9
for x being set
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V st x in W holds
x in V
proofend;

theorem Th10: :: VECTSP_4:10
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V
for w being Element of W holds w is Element of V
proofend;

theorem :: VECTSP_4:11
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds 0. W = 0. V by Def2;

theorem :: VECTSP_4:12
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of V holds 0. W1 = 0. W2
proofend;

theorem Th13: :: VECTSP_4:13
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v, u being Element of V
for W being Subspace of V
for w1, w2 being Element of W st w1 = v &amp; w2 = u holds
w1 + w2 = v + u
proofend;

theorem Th14: :: VECTSP_4:14
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for v being Element of V
for W being Subspace of V
for w being Element of W st w = v holds
a * w = a * v
proofend;

theorem Th15: :: VECTSP_4:15
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V
for w being Element of W st w = v holds
- v = - w
proofend;

theorem Th16: :: VECTSP_4:16
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v, u being Element of V
for W being Subspace of V
for w1, w2 being Element of W st w1 = v &amp; w2 = u holds
w1 - w2 = v - u
proofend;

Lm2:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
proofend;

theorem Th17: :: VECTSP_4:17
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds 0. V in W
proofend;

theorem :: VECTSP_4:18
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of V holds 0. W1 in W2
proofend;

theorem :: VECTSP_4:19
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds 0. W in V by Th9, RLVECT_1:1;

theorem Th20: :: VECTSP_4:20
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v being Element of V
for W being Subspace of V st u in W &amp; v in W holds
u + v in W
proofend;

theorem Th21: :: VECTSP_4:21
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for v being Element of V
for W being Subspace of V st v in W holds
a * v in W
proofend;

theorem Th22: :: VECTSP_4:22
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V st v in W holds
- v in W
proofend;

theorem Th23: :: VECTSP_4:23
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v being Element of V
for W being Subspace of V st u in W &amp; v in W holds
u - v in W
proofend;

theorem Th24: :: VECTSP_4:24
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds V is Subspace of V
proofend;

theorem Th25: :: VECTSP_4:25
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for X, V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF st V is Subspace of X &amp; X is Subspace of V holds
V = X
proofend;

theorem Th26: :: VECTSP_4:26
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V, X, Y being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF st V is Subspace of X &amp; X is Subspace of Y holds
V is Subspace of Y
proofend;

theorem Th27: :: VECTSP_4:27
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 is Subspace of W2
proofend;

theorem :: VECTSP_4:28
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of V st ( for v being Element of V st v in W1 holds
v in W2 ) holds
W1 is Subspace of W2
proofend;

registration
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed for Subspace of V;
existence
 ex b1 being Subspace of V st b1 is strict
proofend;
end;

theorem Th29: :: VECTSP_4:29
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
proofend;

theorem Th30: :: VECTSP_4:30
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being strict Subspace of V st ( for v being Element of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2
proofend;

theorem :: VECTSP_4:31
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of V st the carrier of W = the carrier of V holds
W = V
proofend;

theorem :: VECTSP_4:32
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of V st ( for v being Element of V holds v in W ) holds
W = V
proofend;

theorem :: VECTSP_4:33
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed by Lm2;

theorem Th34: :: VECTSP_4:34
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1 being Subset of V st V1 <> {} &amp; V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
proofend;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
func (0). V ->  strict Subspace of V means :Def3: :: VECTSP_4:def 3
 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)} &amp; the carrier of b2 = {(0. V)} holds
b1 = b2;
by Th4, Th29, Th34;
end;

:: deftheorem Def3 defines (0). VECTSP_4:def_3_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for b3 being strict Subspace of V holds
( b3 = (0). V iff the carrier of b3 = {(0. V)} );

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
func (Omega). V ->  strict Subspace of V equals :: VECTSP_4:def 4
 VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);
coherence
 VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V
proofend;
end;

:: deftheorem  defines (Omega). VECTSP_4:def_4_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds (Omega). V = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);

theorem :: VECTSP_4:35
for x being set
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds
( x in (0). V iff x = 0. V )
proofend;

theorem Th36: :: VECTSP_4:36
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds (0). W = (0). V
proofend;

theorem Th37: :: VECTSP_4:37
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of V holds (0). W1 = (0). W2
proofend;

theorem :: VECTSP_4:38
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds (0). W is Subspace of V by Th26;

theorem :: VECTSP_4:39
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds (0). V is Subspace of W
proofend;

theorem :: VECTSP_4:40
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2
proofend;

theorem :: VECTSP_4:41
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds V is Subspace of (Omega). V ;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let v be Element of V;
let W be Subspace of V;
funcv + W ->  Subset of V equals :: VECTSP_4:def 5
 {  (v + u) where u is Element of V : u in W  }  ;
coherence
  {  (v + u) where u is Element of V : u in W  }  is Subset of V
proofend;
end;

:: deftheorem  defines + VECTSP_4:def_5_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V holds v + W =  {  (v + u) where u is Element of V : u in W  }  ;

Lm3:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds (0. V) + W = the carrier of W
proofend;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let W be Subspace of V;
mode Coset of W ->  Subset of V means :Def6: :: VECTSP_4:def 6
 ex v being Element of V st it = v + W;
existence
 ex b1 being Subset of V ex v being Element of V st b1 = v + W
proofend;
end;

:: deftheorem Def6 defines Coset VECTSP_4:def_6_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V
for b4 being Subset of V holds
( b4 is Coset of W iff ex v being Element of V st b4 = v + W );

theorem Th42: :: VECTSP_4:42
for x being set
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V holds
( x in v + W iff ex u being Element of V st
( u in W &amp; x = v + u ) )
proofend;

theorem Th43: :: VECTSP_4:43
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V holds
( 0. V in v + W iff v in W )
proofend;

theorem Th44: :: VECTSP_4:44
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V holds v in v + W
proofend;

theorem :: VECTSP_4:45
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds (0. V) + W = the carrier of W by Lm3;

theorem Th46: :: VECTSP_4:46
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V holds v + ((0). V) = {v}
proofend;

Lm4:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
proofend;

theorem Th47: :: VECTSP_4:47
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V holds v + ((Omega). V) = the carrier of V
proofend;

theorem Th48: :: VECTSP_4:48
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V holds
( 0. V in v + W iff v + W = the carrier of W )
proofend;

theorem :: VECTSP_4:49
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W ) by Lm4;

theorem Th50: :: VECTSP_4:50
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for v being Element of V
for W being Subspace of V st v in W holds
(a * v) + W = the carrier of W
proofend;

theorem Th51: :: VECTSP_4:51
for GF being Field
for V being VectSp of GF
for a being Element of GF
for v being Element of V
for W being Subspace of V st a <> 0. GF &amp; (a * v) + W = the carrier of W holds
v in W
proofend;

theorem :: VECTSP_4:52
for GF being Field
for V being VectSp of GF
for v being Element of V
for W being Subspace of V holds
( v in W iff (- v) + W = the carrier of W )
proofend;

theorem Th53: :: VECTSP_4:53
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v being Element of V
for W being Subspace of V holds
( u in W iff v + W = (v + u) + W )
proofend;

theorem :: VECTSP_4:54
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v being Element of V
for W being Subspace of V holds
( u in W iff v + W = (v - u) + W )
proofend;

theorem Th55: :: VECTSP_4:55
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v, u being Element of V
for W being Subspace of V holds
( v in u + W iff u + W = v + W )
proofend;

theorem Th56: :: VECTSP_4:56
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v1, v2 being Element of V
for W being Subspace of V st u in v1 + W &amp; u in v2 + W holds
v1 + W = v2 + W
proofend;

theorem :: VECTSP_4:57
for GF being Field
for V being VectSp of GF
for a being Element of GF
for v being Element of V
for W being Subspace of V st a <> 1_ GF &amp; a * v in v + W holds
v in W
proofend;

theorem Th58: :: VECTSP_4:58
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for v being Element of V
for W being Subspace of V st v in W holds
a * v in v + W
proofend;

theorem :: VECTSP_4:59
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V st v in W holds
- v in v + W
proofend;

theorem Th60: :: VECTSP_4:60
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v being Element of V
for W being Subspace of V holds
( u + v in v + W iff u in W )
proofend;

theorem :: VECTSP_4:61
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v, u being Element of V
for W being Subspace of V holds
( v - u in v + W iff u in W )
proofend;

theorem :: VECTSP_4:62
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v being Element of V
for W being Subspace of V holds
( u in v + W iff ex v1 being Element of V st
( v1 in W &amp; u = v - v1 ) )
proofend;

theorem Th63: :: VECTSP_4:63
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V
for W being Subspace of V holds
( ex v being Element of V st
( v1 in v + W &amp; v2 in v + W ) iff v1 - v2 in W )
proofend;

theorem Th64: :: VECTSP_4:64
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v, u being Element of V
for W being Subspace of V st v + W = u + W holds
ex v1 being Element of V st
( v1 in W &amp; v + v1 = u )
proofend;

theorem Th65: :: VECTSP_4:65
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v, u being Element of V
for W being Subspace of V st v + W = u + W holds
ex v1 being Element of V st
( v1 in W &amp; v - v1 = u )
proofend;

theorem Th66: :: VECTSP_4:66
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )
proofend;

theorem Th67: :: VECTSP_4:67
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v, u being Element of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
proofend;

theorem :: VECTSP_4:68
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for W being Subspace of V ex C being Coset of W st v in C
proofend;

theorem :: VECTSP_4:69
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
proofend;

theorem :: VECTSP_4:70
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
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
proofend;

theorem :: VECTSP_4:71
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V holds {v} is Coset of (0). V
proofend;

theorem :: VECTSP_4:72
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being Element of V st V1 = {v}
proofend;

theorem :: VECTSP_4:73
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V holds the carrier of W is Coset of W
proofend;

theorem :: VECTSP_4:74
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds the carrier of V is Coset of (Omega). V
proofend;

theorem :: VECTSP_4:75
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
proofend;

theorem :: VECTSP_4:76
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
proofend;

theorem Th77: :: VECTSP_4:77
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u being Element of V
for W being Subspace of V
for C being Coset of W holds
( u in C iff C = u + W )
proofend;

theorem :: VECTSP_4:78
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v being Element of V
for W being Subspace of V
for C being Coset of W st u in C &amp; v in C holds
ex v1 being Element of V st
( v1 in W &amp; u + v1 = v )
proofend;

theorem :: VECTSP_4:79
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u, v being Element of V
for W being Subspace of V
for C being Coset of W st u in C &amp; v in C holds
ex v1 being Element of V st
( v1 in W &amp; u - v1 = v )
proofend;

theorem :: VECTSP_4:80
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V
for W being Subspace of V holds
( ex C being Coset of W st
( v1 in C &amp; v2 in C ) iff v1 - v2 in W )
proofend;

theorem :: VECTSP_4:81
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for u being Element of V
for W being Subspace of V
for B, C being Coset of W st u in B &amp; u in C holds
B = C
proofend;

::
:: Auxiliary theorems.
::
theorem :: VECTSP_4:82
for GF being non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a, b being Element of GF
for v being Element of V holds (a - b) * v = (a * v) - (b * v) by Lm1;