:: by Wojciech A. Trybulec

::

:: Received July 27, 1990

:: Copyright (c) 1990-2017 Association of Mizar Users

Lm1: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a, b being Element of GF

for v being Element of V holds (a - b) * v = (a * v) - (b * v)

proof end;

definition
end;

:: deftheorem defines linearly-closed VECTSP_4:def 1 :

for GF being non empty multMagma

for V being non empty ModuleStr 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 ) ) );

for GF being non empty multMagma

for V being non empty ModuleStr 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 well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

0. V in V1

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

0. V in V1

proof end;

theorem Th2: :: VECTSP_4:2

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem :: VECTSP_4:3

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & u in V1 holds

v - u in V1

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & u in V1 holds

v - u in V1

proof end;

theorem Th4: :: VECTSP_4:4

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds {(0. V)} is linearly-closed

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds {(0. V)} is linearly-closed

proof end;

theorem :: VECTSP_4:5

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1 being Subset of V st the carrier of V = V1 holds

V1 is linearly-closed ;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1 being Subset of V st the carrier of V = V1 holds

V1 is linearly-closed ;

theorem :: VECTSP_4:6

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

proof end;

theorem :: VECTSP_4:7

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds

V1 /\ V2 is linearly-closed

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds

V1 /\ V2 is linearly-closed

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

ex b_{1} being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF st

( the carrier of b_{1} c= the carrier of V & 0. b_{1} = 0. V & the addF of b_{1} = the addF of V || the carrier of b_{1} & the lmult of b_{1} = the lmult of V | [: the carrier of GF, the carrier of b_{1}:] )

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

mode Subspace of V -> non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF means :Def2: :: VECTSP_4:def 2

( 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 lmult of it = the lmult of V | [: the carrier of GF, the carrier of it:] );

existence ( 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 lmult of it = the lmult of V | [: the carrier of GF, the carrier of it:] );

ex b

( the carrier of b

proof end;

:: deftheorem Def2 defines Subspace VECTSP_4:def 2 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V, b_{3} being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds

( b_{3} is Subspace of V iff ( the carrier of b_{3} c= the carrier of V & 0. b_{3} = 0. V & the addF of b_{3} = the addF of V || the carrier of b_{3} & the lmult of b_{3} = the lmult of V | [: the carrier of GF, the carrier of b_{3}:] ) );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V, b

( b

theorem :: VECTSP_4:8

for x being object

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V st x in W1 & W1 is Subspace of W2 holds

x in W2

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V st x in W1 & W1 is Subspace of W2 holds

x in W2

proof end;

theorem Th9: :: VECTSP_4:9

for x being object

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V st x in W holds

x in V

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V st x in W holds

x in V

proof end;

theorem Th10: :: VECTSP_4:10

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V

for w being Element of W holds w is Element of V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V

for w being Element of W holds w is Element of V

proof end;

theorem :: VECTSP_4:11

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds 0. W = 0. V by Def2;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V holds 0. W1 = 0. W2

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V holds 0. W1 = 0. W2

proof end;

theorem Th13: :: VECTSP_4:13

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V

for w1, w2 being Element of W st w1 = v & w2 = u holds

w1 + w2 = v + u

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V

for w1, w2 being Element of W st w1 = v & w2 = u holds

w1 + w2 = v + u

proof end;

theorem Th14: :: VECTSP_4:14

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem Th15: :: VECTSP_4:15

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem Th16: :: VECTSP_4:16

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V

for w1, w2 being Element of W st w1 = v & w2 = u holds

w1 - w2 = v - u

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V

for w1, w2 being Element of W st w1 = v & w2 = u holds

w1 - w2 = v - u

proof end;

Lm2: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem Th17: :: VECTSP_4:17

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds 0. V in W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds 0. V in W

proof end;

theorem :: VECTSP_4:18

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V holds 0. W1 in W2

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V holds 0. W1 in W2

proof end;

theorem :: VECTSP_4:19

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds 0. W in V by Th9, RLVECT_1:1;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V st u in W & v in W holds

u + v in W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V st u in W & v in W holds

u + v in W

proof end;

theorem Th21: :: VECTSP_4:21

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem Th22: :: VECTSP_4:22

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V st v in W holds

- v in W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V st v in W holds

- v in W

proof end;

theorem Th23: :: VECTSP_4:23

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V st u in W & v in W holds

u - v in W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V st u in W & v in W holds

u - v in W

proof end;

theorem Th24: :: VECTSP_4:24

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds V is Subspace of V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds V is Subspace of V

proof end;

theorem Th25: :: VECTSP_4:25

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for X, V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF st V is Subspace of X & X is Subspace of V holds

V = X

for X, V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF st V is Subspace of X & X is Subspace of V holds

V = X

proof end;

theorem Th26: :: VECTSP_4:26

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V, X, Y being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF st V is Subspace of X & X is Subspace of Y holds

V is Subspace of Y

for V, X, Y being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF st V is Subspace of X & X is Subspace of Y holds

V is Subspace of Y

proof end;

theorem Th27: :: VECTSP_4:27

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem Th28: :: VECTSP_4:28

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

registration

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

ex b_{1} being Subspace of V st b_{1} is strict

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 b

proof end;

theorem Th29: :: VECTSP_4:29

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds

W1 = W2

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds

W1 = W2

proof end;

theorem Th30: :: VECTSP_4:30

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem :: VECTSP_4:31

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of V st the carrier of W = the carrier of V holds

W = V

for V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of V st the carrier of W = the carrier of V holds

W = V

proof end;

theorem :: VECTSP_4:32

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of V st ( for v being Element of V holds v in W ) holds

W = V

for V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of V st ( for v being Element of V holds v in W ) holds

W = V

proof end;

theorem :: VECTSP_4:33

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

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;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

correctness

existence

ex b_{1} being strict Subspace of V st the carrier of b_{1} = {(0. V)};

uniqueness

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = {(0. V)} & the carrier of b_{2} = {(0. V)} holds

b_{1} = b_{2};

by Th4, Th29, Th34;

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

correctness

existence

ex b

uniqueness

for b

b

by Th4, Th29, Th34;

:: deftheorem Def3 defines (0). VECTSP_4:def 3 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for b_{3} being strict Subspace of V holds

( b_{3} = (0). V iff the carrier of b_{3} = {(0. V)} );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for b

( b

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

func (Omega). V -> strict Subspace of V equals :: VECTSP_4:def 4

ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);

coherence ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);

ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V

proof end;

:: deftheorem defines (Omega). VECTSP_4:def 4 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds (Omega). V = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds (Omega). V = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);

theorem :: VECTSP_4:35

for x being object

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds

( x in (0). V iff x = 0. V )

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds

( x in (0). V iff x = 0. V )

proof end;

theorem Th36: :: VECTSP_4:36

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds (0). W = (0). V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds (0). W = (0). V

proof end;

theorem Th37: :: VECTSP_4:37

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V holds (0). W1 = (0). W2

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V holds (0). W1 = (0). W2

proof end;

theorem :: VECTSP_4:38

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds (0). W is Subspace of V by Th26;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds (0). V is Subspace of W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds (0). V is Subspace of W

proof end;

theorem :: VECTSP_4:40

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2

proof end;

theorem :: VECTSP_4:41

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds V is Subspace of (Omega). V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds V is Subspace of (Omega). V

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let v be Element of V;

let W be Subspace of V;

coherence

{ (v + u) where u is Element of V : u in W } is Subset of V

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let v be Element of V;

let W be Subspace of V;

coherence

{ (v + u) where u is Element of V : u in W } is Subset of V

proof end;

:: deftheorem defines + VECTSP_4:def 5 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 } ;

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds (0. V) + W = the carrier of W

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let W be Subspace of V;

ex b_{1} being Subset of V ex v being Element of V st b_{1} = v + W

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 v being Element of V st it = v + W;

ex b

proof end;

:: deftheorem Def6 defines Coset VECTSP_4:def 6 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V

for b_{4} being Subset of V holds

( b_{4} is Coset of W iff ex v being Element of V st b_{4} = v + W );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V

for b

( b

theorem Th42: :: VECTSP_4:42

for x being object

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & x = v + u ) )

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & x = v + u ) )

proof end;

theorem Th43: :: VECTSP_4:43

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V holds

( 0. V in v + W iff v in W )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V holds

( 0. V in v + W iff v in W )

proof end;

theorem Th44: :: VECTSP_4:44

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V holds v in v + W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V holds v in v + W

proof end;

theorem :: VECTSP_4:45

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds (0. V) + W = the carrier of W by Lm3;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V holds v + ((0). V) = {v}

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V holds v + ((0). V) = {v}

proof end;

Lm4: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

proof end;

theorem Th47: :: VECTSP_4:47

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V holds v + ((Omega). V) = the carrier of V by RLVECT_1:1, Lm4;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V holds v + ((Omega). V) = the carrier of V by RLVECT_1:1, Lm4;

theorem Th48: :: VECTSP_4:48

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 ) by Th43, Lm4;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 ) by Th43, Lm4;

theorem :: VECTSP_4:49

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 by Th21, Lm4;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 by Th21, Lm4;

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 & (a * v) + W = the carrier of W holds

v in W

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 & (a * v) + W = the carrier of W holds

v in W

proof end;

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 )

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 )

proof end;

theorem Th53: :: VECTSP_4:53

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

proof end;

theorem :: VECTSP_4:54

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

proof end;

theorem Th55: :: VECTSP_4:55

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V holds

( v in u + W iff u + W = v + W )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V holds

( v in u + W iff u + W = v + W )

proof end;

theorem Th56: :: VECTSP_4:56

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v1, v2 being Element of V

for W being Subspace of V st u in v1 + W & u in v2 + W holds

v1 + W = v2 + W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v1, v2 being Element of V

for W being Subspace of V st u in v1 + W & u in v2 + W holds

v1 + W = v2 + W

proof end;

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 & a * v in v + W holds

v in W

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 & a * v in v + W holds

v in W

proof end;

theorem Th58: :: VECTSP_4:58

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem :: VECTSP_4:59

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V st v in W holds

- v in v + W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V st v in W holds

- v in v + W

proof end;

theorem Th60: :: VECTSP_4:60

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

proof end;

theorem :: VECTSP_4:61

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V holds

( v - u in v + W iff u in W )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W being Subspace of V holds

( v - u in v + W iff u in W )

proof end;

theorem :: VECTSP_4:62

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & u = v - v1 ) )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & u = v - v1 ) )

proof end;

theorem Th63: :: VECTSP_4:63

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & v2 in v + W ) iff v1 - v2 in W )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & v2 in v + W ) iff v1 - v2 in W )

proof end;

theorem Th64: :: VECTSP_4:64

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v 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 & v + v1 = u )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v 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 & v + v1 = u )

proof end;

theorem Th65: :: VECTSP_4:65

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v 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 & v - v1 = u )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v 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 & v - v1 = u )

proof end;

theorem Th66: :: VECTSP_4:66

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

proof end;

theorem Th67: :: VECTSP_4:67

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds

W1 = W2

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v being Element of V

for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds

W1 = W2

proof end;

theorem :: VECTSP_4:68

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V ex C being Coset of W st v in C

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V ex C being Coset of W st v in C

proof end;

theorem :: VECTSP_4:69

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

proof end;

theorem :: VECTSP_4:70

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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

proof end;

theorem :: VECTSP_4:71

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V holds {v} is Coset of (0). V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V holds {v} is Coset of (0). V

proof end;

theorem :: VECTSP_4:72

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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}

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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}

proof end;

theorem :: VECTSP_4:73

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds the carrier of W is Coset of W

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of V holds the carrier of W is Coset of W

proof end;

theorem :: VECTSP_4:74

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds the carrier of V is Coset of (Omega). V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds the carrier of V is Coset of (Omega). V

proof end;

theorem :: VECTSP_4:75

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1 being Subset of V st V1 is Coset of (Omega). V holds

V1 = the carrier of V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1 being Subset of V st V1 is Coset of (Omega). V holds

V1 = the carrier of V

proof end;

theorem :: VECTSP_4:76

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

proof end;

theorem Th77: :: VECTSP_4:77

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 )

proof end;

theorem :: VECTSP_4:78

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & v in C holds

ex v1 being Element of V st

( v1 in W & u + v1 = v )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & v in C holds

ex v1 being Element of V st

( v1 in W & u + v1 = v )

proof end;

theorem :: VECTSP_4:79

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & v in C holds

ex v1 being Element of V st

( v1 in W & u - v1 = v )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & v in C holds

ex v1 being Element of V st

( v1 in W & u - v1 = v )

proof end;

theorem :: VECTSP_4:80

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & v2 in C ) iff v1 - v2 in W )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & v2 in C ) iff v1 - v2 in W )

proof end;

theorem :: VECTSP_4:81

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & u in C holds

B = C

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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 & u in C holds

B = C

proof end;

theorem :: VECTSP_4:82

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr 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;

:: Auxiliary theorems.

::