:: VECTSP_4 semantic presentation

Lm1: for GF being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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

let GF be non empty HGrStr ;
let V be non empty VectSpStr of GF;
let V1 be Subset of V;
attr V1 is lineary-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 lineary-closed VECTSP_4:def 1 :

theorem :: VECTSP_4:1

canceled;

theorem :: VECTSP_4:2

canceled;

theorem :: VECTSP_4:3

canceled;

theorem Th4: :: VECTSP_4:4

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for V1 being Subset of V st V1 <> {} & V1 is lineary-closed holds
0. V in V1

proof end;

theorem Th5: :: VECTSP_4:5

proof end;

theorem :: VECTSP_4:6

proof end;

theorem Th7: :: VECTSP_4:7

proof end;

theorem :: VECTSP_4:8

proof end;

theorem :: VECTSP_4:9

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for V1, V2, V3 being Subset of V st V1 is lineary-closed & V2 is lineary-closed & V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } holds
V3 is lineary-closed

proof end;

theorem :: VECTSP_4:10

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for V1, V2 being Subset of V st V1 is lineary-closed & V2 is lineary-closed holds
V1 /\ V2 is lineary-closed

proof end;

definition

let GF be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF;
mode Subspace of V -> non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF means :Def2: :: VECTSP_4:def 2
( the carrier of it c= the carrier of V & the Zero of it = the Zero of V & the add of it = the add of V || the carrier of it & the lmult of it = the lmult of V | [:the carrier of GF,the carrier of it:] );
existence

proof end;

end;

:: deftheorem Def2 defines Subspace VECTSP_4:def 2 :

theorem :: VECTSP_4:11

canceled;

theorem :: VECTSP_4:12

canceled;

theorem :: VECTSP_4:13

canceled;

theorem :: VECTSP_4:14

canceled;

theorem :: VECTSP_4:15

canceled;

theorem :: VECTSP_4:16

for x being set
for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W1, W2 being Subspace of V st x in W1 & W1 is Subspace of W2 holds
x in W2

proof end;

theorem Th17: :: VECTSP_4:17

proof end;

theorem Th18: :: VECTSP_4:18

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W being Subspace of V
for w being Element of W holds w is Element of V

proof end;

theorem Th19: :: VECTSP_4:19

theorem :: VECTSP_4:20

proof end;

theorem Th21: :: VECTSP_4:21

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for v, u 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 Th22: :: VECTSP_4:22

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 Th23: :: VECTSP_4:23

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 Th24: :: VECTSP_4:24

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for v, u 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is lineary-closed

proof end;

theorem Th25: :: VECTSP_4:25

proof end;

theorem :: VECTSP_4:26

proof end;

theorem :: VECTSP_4:27

proof end;

theorem Th28: :: VECTSP_4:28

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 Th29: :: VECTSP_4:29

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 Th30: :: VECTSP_4:30

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for v being Element of V
for W being Subspace of V st v in W holds
- v in W

proof end;

theorem Th31: :: VECTSP_4:31

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 Th32: :: VECTSP_4:32

proof end;

theorem Th33: :: VECTSP_4:33

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for X, V being non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of GF st V is Subspace of X & X is Subspace of V holds
V = X

proof end;

theorem Th34: :: VECTSP_4:34

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V, X, Y being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF st V is Subspace of X & X is Subspace of Y holds
V is Subspace of Y

proof end;

theorem Th35: :: VECTSP_4:35

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 :: VECTSP_4:36

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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

proof end;

end;

theorem Th37: :: VECTSP_4:37

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2

proof end;

theorem Th38: :: VECTSP_4:38

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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:39

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of 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:40

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of 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:41

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is lineary-closed by Lm2;

theorem Th42: :: VECTSP_4:42

proof end;

definition

proof end;

end;

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

definition

proof end;

end;

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

theorem :: VECTSP_4:43

canceled;

theorem :: VECTSP_4:44

canceled;

theorem :: VECTSP_4:45

canceled;

theorem :: VECTSP_4:46

proof end;

theorem Th47: :: VECTSP_4:47

proof end;

theorem Th48: :: VECTSP_4:48

proof end;

theorem :: VECTSP_4:49

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W being Subspace of V holds (0). W is Subspace of V by Th34;

theorem :: VECTSP_4:50

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W being Subspace of V holds (0). V is Subspace of W

proof end;

theorem :: VECTSP_4:51

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2

proof end;

theorem :: VECTSP_4:52

canceled;

theorem :: VECTSP_4:53

definition

proof end;

end;

:: deftheorem defines + VECTSP_4:def 5 :

Lm3: for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W being Subspace of V holds (0. V) + W = the carrier of W

proof end;

definition

proof end;

end;

:: deftheorem Def6 defines Coset VECTSP_4:def 6 :

theorem :: VECTSP_4:54

canceled;

theorem :: VECTSP_4:55

canceled;

theorem :: VECTSP_4:56

canceled;

theorem Th57: :: VECTSP_4:57

for x being set
for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 Th58: :: VECTSP_4:58

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 Th59: :: VECTSP_4:59

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for v being Element of V
for W being Subspace of V holds v in v + W

proof end;

theorem :: VECTSP_4:60

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for W being Subspace of V holds (0. V) + W = the carrier of W by Lm3;

theorem Th61: :: VECTSP_4:61

proof end;

Lm4: for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr 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 Th62: :: VECTSP_4:62

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for v being Element of V holds v + ((Omega). V) = the carrier of V

proof end;

theorem Th63: :: VECTSP_4:63

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 )

proof end;

theorem :: VECTSP_4:64

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr 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 ) by Lm4;

theorem Th65: :: VECTSP_4:65

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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

proof end;

theorem Th66: :: VECTSP_4:66

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

proof end;

theorem :: VECTSP_4:67

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 )

proof end;

theorem Th68: :: VECTSP_4:68

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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:69

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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 Th70: :: VECTSP_4:70

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
for v, u being Element of V
for W being Subspace of V holds
( v in u + W iff u + W = v + W )

proof end;

theorem Th71: :: VECTSP_4:71

for GF being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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:72

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

proof end;

theorem Th73: :: VECTSP_4:73