:: VECTSP_4 semantic presentation 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) proof let GF be non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a, b being Element of GF for v being Element of V holds (a - b) * v = (a * v) - (b * v) let a, b be Element of GF; ::_thesis: for v being Element of V holds (a - b) * v = (a * v) - (b * v) let v be Element of V; ::_thesis: (a - b) * v = (a * v) - (b * v) thus (a - b) * v = (a * v) + ((- b) * v) by VECTSP_1:def_15 .= (a * v) - (b * v) by VECTSP_1:21 ; ::_thesis: verum end; 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 <> {} & V1 is linearly-closed holds 0. V in V1 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 <> {} & V1 is linearly-closed holds 0. V in V1 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds 0. V in V1 let V1 be Subset of V; ::_thesis: ( V1 <> {} & V1 is linearly-closed implies 0. V in V1 ) assume that A1: V1 <> {} and A2: V1 is linearly-closed ; ::_thesis: 0. V in V1 set x = the Element of V1; reconsider x = the Element of V1 as Element of V by A1, TARSKI:def_3; (0. GF) * x in V1 by A1, A2, Def1; hence 0. V in V1 by VECTSP_1:14; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed implies for v being Element of V st v in V1 holds - v in V1 ) assume A1: V1 is linearly-closed ; ::_thesis: for v being Element of V st v in V1 holds - v in V1 let v be Element of V; ::_thesis: ( v in V1 implies - v in V1 ) assume v in V1 ; ::_thesis: - v in V1 then (- (1_ GF)) * v in V1 by A1, Def1; hence - v in V1 by VECTSP_1:14; ::_thesis: verum end; 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 & u in V1 holds v - u in V1 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & u in V1 holds v - u in V1 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed implies for v, u being Element of V st v in V1 & u in V1 holds v - u in V1 ) assume A1: V1 is linearly-closed ; ::_thesis: for v, u being Element of V st v in V1 & u in V1 holds v - u in V1 let v, u be Element of V; ::_thesis: ( v in V1 & u in V1 implies v - u in V1 ) assume that A2: v in V1 and A3: u in V1 ; ::_thesis: v - u in V1 - u in V1 by A1, A3, Th2; hence v - u in V1 by A1, A2, Def1; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: {(0. V)} is linearly-closed thus for v, u being Element of V st v in {(0. V)} & u in {(0. V)} holds v + u in {(0. V)} :: according to VECTSP_4:def_1 ::_thesis: for a being Element of GF for v being Element of V st v in {(0. V)} holds a * v in {(0. V)} proof let v, u be Element of V; ::_thesis: ( v in {(0. V)} & u in {(0. V)} implies v + u in {(0. V)} ) assume ( v in {(0. V)} & u in {(0. V)} ) ; ::_thesis: v + u in {(0. V)} then ( v = 0. V & u = 0. V ) by TARSKI:def_1; then v + u = 0. V by RLVECT_1:4; hence v + u in {(0. V)} by TARSKI:def_1; ::_thesis: verum end; let a be Element of GF; ::_thesis: for v being Element of V st v in {(0. V)} holds a * v in {(0. V)} let v be Element of V; ::_thesis: ( v in {(0. V)} implies a * v in {(0. V)} ) assume A1: v in {(0. V)} ; ::_thesis: a * v in {(0. V)} then v = 0. V by TARSKI:def_1; hence a * v in {(0. V)} by A1, VECTSP_1:14; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for V1 being Subset of V st the carrier of V = V1 holds V1 is linearly-closed let V1 be Subset of V; ::_thesis: ( the carrier of V = V1 implies V1 is linearly-closed ) assume A1: the carrier of V = V1 ; ::_thesis: V1 is linearly-closed hence for v, u being Element of V st v in V1 & u in V1 holds v + u in V1 ; :: according to VECTSP_4:def_1 ::_thesis: for a being Element of GF for v being Element of V st v in V1 holds a * v in V1 let a be Element of GF; ::_thesis: for v being Element of V st v in V1 holds a * v in V1 let v be Element of V; ::_thesis: ( v in V1 implies a * v in V1 ) assume v in V1 ; ::_thesis: a * v in V1 thus a * v in V1 by A1; ::_thesis: verum end; 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 & 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 let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let V1, V2, V3 be Subset of V; ::_thesis: ( V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } implies V3 is linearly-closed ) assume that A1: ( V1 is linearly-closed & V2 is linearly-closed ) and A2: V3 = { (v + u) where v, u is Element of V : ( v in V1 & u in V2 ) } ; ::_thesis: V3 is linearly-closed thus for v, u being Element of V st v in V3 & u in V3 holds v + u in V3 :: according to VECTSP_4:def_1 ::_thesis: for a being Element of GF for v being Element of V st v in V3 holds a * v in V3 proof let v, u be Element of V; ::_thesis: ( v in V3 & u in V3 implies v + u in V3 ) assume that A3: v in V3 and A4: u in V3 ; ::_thesis: v + u in V3 consider v1, v2 being Element of V such that A5: v = v1 + v2 and A6: ( v1 in V1 & v2 in V2 ) by A2, A3; consider u1, u2 being Element of V such that A7: u = u1 + u2 and A8: ( u1 in V1 & u2 in V2 ) by A2, A4; A9: v + u = ((v1 + v2) + u1) + u2 by A5, A7, RLVECT_1:def_3 .= ((v1 + u1) + v2) + u2 by RLVECT_1:def_3 .= (v1 + u1) + (v2 + u2) by RLVECT_1:def_3 ; ( v1 + u1 in V1 & v2 + u2 in V2 ) by A1, A6, A8, Def1; hence v + u in V3 by A2, A9; ::_thesis: verum end; let a be Element of GF; ::_thesis: for v being Element of V st v in V3 holds a * v in V3 let v be Element of V; ::_thesis: ( v in V3 implies a * v in V3 ) assume v in V3 ; ::_thesis: a * v in V3 then consider v1, v2 being Element of V such that A10: v = v1 + v2 and A11: ( v1 in V1 & v2 in V2 ) by A2; A12: a * v = (a * v1) + (a * v2) by A10, VECTSP_1:def_14; ( a * v1 in V1 & a * v2 in V2 ) by A1, A11, Def1; hence a * v in V3 by A2, A12; ::_thesis: verum end; 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 & V2 is linearly-closed holds V1 /\ V2 is linearly-closed proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & V2 is linearly-closed holds V1 /\ V2 is linearly-closed let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds V1 /\ V2 is linearly-closed let V1, V2 be Subset of V; ::_thesis: ( V1 is linearly-closed & V2 is linearly-closed implies V1 /\ V2 is linearly-closed ) assume that A1: V1 is linearly-closed and A2: V2 is linearly-closed ; ::_thesis: V1 /\ V2 is linearly-closed thus for v, u being Element of V st v in V1 /\ V2 & u in V1 /\ V2 holds v + u in V1 /\ V2 :: according to VECTSP_4:def_1 ::_thesis: for a being Element of GF for v being Element of V st v in V1 /\ V2 holds a * v in V1 /\ V2 proof let v, u be Element of V; ::_thesis: ( v in V1 /\ V2 & u in V1 /\ V2 implies v + u in V1 /\ V2 ) assume A3: ( v in V1 /\ V2 & u in V1 /\ V2 ) ; ::_thesis: v + u in V1 /\ V2 then ( v in V2 & u in V2 ) by XBOOLE_0:def_4; then A4: v + u in V2 by A2, Def1; ( v in V1 & u in V1 ) by A3, XBOOLE_0:def_4; then v + u in V1 by A1, Def1; hence v + u in V1 /\ V2 by A4, XBOOLE_0:def_4; ::_thesis: verum end; let a be Element of GF; ::_thesis: for v being Element of V st v in V1 /\ V2 holds a * v in V1 /\ V2 let v be Element of V; ::_thesis: ( v in V1 /\ V2 implies a * v in V1 /\ V2 ) assume A5: v in V1 /\ V2 ; ::_thesis: a * v in V1 /\ V2 then v in V2 by XBOOLE_0:def_4; then A6: a * v in V2 by A2, Def1; v in V1 by A5, XBOOLE_0:def_4; then a * v in V1 by A1, Def1; hence a * v in V1 /\ V2 by A6, XBOOLE_0:def_4; ::_thesis: verum end; 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 & 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 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 & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the lmult of b1 = the lmult of V | [: the carrier of GF, the carrier of b1:] ) proof take V ; ::_thesis: ( the carrier of V c= the carrier of V & 0. V = 0. V & the addF of V = the addF of V || the carrier of V & the lmult of V = the lmult of V | [: the carrier of GF, the carrier of V:] ) thus ( the carrier of V c= the carrier of V & 0. V = 0. V ) ; ::_thesis: ( the addF of V = the addF of V || the carrier of V & the lmult of V = the lmult of V | [: the carrier of GF, the carrier of V:] ) thus ( the addF of V = the addF of V || the carrier of V & the lmult of V = the lmult of V | [: the carrier of GF, the carrier of V:] ) by RELSET_1:19; ::_thesis: verum end; 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 & 0. b3 = 0. V & the addF of b3 = the addF of V || the carrier of b3 & 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 & W1 is Subspace of W2 holds x in W2 proof let x be set ; ::_thesis: 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 & W1 is Subspace of W2 holds x in W2 let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & W1 is Subspace of W2 holds x in W2 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of V st x in W1 & W1 is Subspace of W2 holds x in W2 let W1, W2 be Subspace of V; ::_thesis: ( x in W1 & W1 is Subspace of W2 implies x in W2 ) assume ( x in W1 & W1 is Subspace of W2 ) ; ::_thesis: x in W2 then ( x in the carrier of W1 & the carrier of W1 c= the carrier of W2 ) by Def2, STRUCT_0:def_5; hence x in W2 by STRUCT_0:def_5; ::_thesis: verum end; 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 proof let x be set ; ::_thesis: 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 let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V st x in W holds x in V let W be Subspace of V; ::_thesis: ( x in W implies x in V ) assume x in W ; ::_thesis: x in V then A1: x in the carrier of W by STRUCT_0:def_5; the carrier of W c= the carrier of V by Def2; hence x in V by A1, STRUCT_0:def_5; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V for w being Element of W holds w is Element of V let W be Subspace of V; ::_thesis: for w being Element of W holds w is Element of V let w be Element of W; ::_thesis: w is Element of V w in V by Th9, RLVECT_1:1; hence w is Element of V by STRUCT_0:def_5; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of V holds 0. W1 = 0. W2 let W1, W2 be Subspace of V; ::_thesis: 0. W1 = 0. W2 thus 0. W1 = 0. V by Def2 .= 0. W2 by Def2 ; ::_thesis: verum end; 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 & w2 = u holds w1 + w2 = v + u proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & w2 = u holds w1 + w2 = v + u let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let v, u be Element of V; ::_thesis: for W being Subspace of V for w1, w2 being Element of W st w1 = v & w2 = u holds w1 + w2 = v + u let W be Subspace of V; ::_thesis: for w1, w2 being Element of W st w1 = v & w2 = u holds w1 + w2 = v + u let w1, w2 be Element of W; ::_thesis: ( w1 = v & w2 = u implies w1 + w2 = v + u ) assume A1: ( v = w1 & u = w2 ) ; ::_thesis: w1 + w2 = v + u w1 + w2 = ( the addF of V || the carrier of W) . [w1,w2] by Def2; hence w1 + w2 = v + u by A1, FUNCT_1:49; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let a be Element of GF; ::_thesis: 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 let v be Element of V; ::_thesis: for W being Subspace of V for w being Element of W st w = v holds a * w = a * v let W be Subspace of V; ::_thesis: for w being Element of W st w = v holds a * w = a * v let w be Element of W; ::_thesis: ( w = v implies a * w = a * v ) assume A1: w = v ; ::_thesis: a * w = a * v a * w = ( the lmult of V | [: the carrier of GF, the carrier of W:]) . [a,w] by Def2; hence a * w = a * v by A1, FUNCT_1:49; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for W being Subspace of V for w being Element of W st w = v holds - v = - w let v be Element of V; ::_thesis: for W being Subspace of V for w being Element of W st w = v holds - v = - w let W be Subspace of V; ::_thesis: for w being Element of W st w = v holds - v = - w let w be Element of W; ::_thesis: ( w = v implies - v = - w ) A1: ( - v = (- (1_ GF)) * v & - w = (- (1_ GF)) * w ) by VECTSP_1:14; assume w = v ; ::_thesis: - v = - w hence - v = - w by A1, Th14; ::_thesis: verum end; 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 & w2 = u holds w1 - w2 = v - u proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & w2 = u holds w1 - w2 = v - u let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let v, u be Element of V; ::_thesis: for W being Subspace of V for w1, w2 being Element of W st w1 = v & w2 = u holds w1 - w2 = v - u let W be Subspace of V; ::_thesis: for w1, w2 being Element of W st w1 = v & w2 = u holds w1 - w2 = v - u let w1, w2 be Element of W; ::_thesis: ( w1 = v & w2 = u implies w1 - w2 = v - u ) assume that A1: w1 = v and A2: w2 = u ; ::_thesis: w1 - w2 = v - u - w2 = - u by A2, Th15; hence w1 - w2 = v - u by A1, Th13; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V for V1 being Subset of V st the carrier of W = V1 holds V1 is linearly-closed let W be Subspace of V; ::_thesis: for V1 being Subset of V st the carrier of W = V1 holds V1 is linearly-closed let V1 be Subset of V; ::_thesis: ( the carrier of W = V1 implies V1 is linearly-closed ) set VW = the carrier of W; reconsider WW = W as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF ; assume A1: the carrier of W = V1 ; ::_thesis: V1 is linearly-closed thus for v, u being Element of V st v in V1 & u in V1 holds v + u in V1 :: according to VECTSP_4:def_1 ::_thesis: for a being Element of GF for v being Element of V st v in V1 holds a * v in V1 proof let v, u be Element of V; ::_thesis: ( v in V1 & u in V1 implies v + u in V1 ) assume ( v in V1 & u in V1 ) ; ::_thesis: v + u in V1 then reconsider vv = v, uu = u as Element of WW by A1; reconsider vw = vv + uu as Element of the carrier of W ; vw in V1 by A1; hence v + u in V1 by Th13; ::_thesis: verum end; let a be Element of GF; ::_thesis: for v being Element of V st v in V1 holds a * v in V1 let v be Element of V; ::_thesis: ( v in V1 implies a * v in V1 ) assume v in V1 ; ::_thesis: a * v in V1 then reconsider vv = v as Element of WW by A1; reconsider vw = a * vv as Element of the carrier of W ; vw in V1 by A1; hence a * v in V1 by Th14; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V holds 0. V in W let W be Subspace of V; ::_thesis: 0. V in W 0. W in W by RLVECT_1:1; hence 0. V in W by Def2; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of V holds 0. W1 in W2 let W1, W2 be Subspace of V; ::_thesis: 0. W1 in W2 0. W1 = 0. V by Def2; hence 0. W1 in W2 by Th17; ::_thesis: verum end; 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 & v in W holds u + v in W proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v in W holds u + v in W let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let u, v be Element of V; ::_thesis: for W being Subspace of V st u in W & v in W holds u + v in W let W be Subspace of V; ::_thesis: ( u in W & v in W implies u + v in W ) reconsider VW = the carrier of W as Subset of V by Def2; assume ( u in W & v in W ) ; ::_thesis: u + v in W then A1: ( u in the carrier of W & v in the carrier of W ) by STRUCT_0:def_5; VW is linearly-closed by Lm2; then u + v in the carrier of W by A1, Def1; hence u + v in W by STRUCT_0:def_5; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let a be Element of GF; ::_thesis: for v being Element of V for W being Subspace of V st v in W holds a * v in W let v be Element of V; ::_thesis: for W being Subspace of V st v in W holds a * v in W let W be Subspace of V; ::_thesis: ( v in W implies a * v in W ) reconsider VW = the carrier of W as Subset of V by Def2; assume v in W ; ::_thesis: a * v in W then A1: v in the carrier of W by STRUCT_0:def_5; VW is linearly-closed by Lm2; then a * v in the carrier of W by A1, Def1; hence a * v in W by STRUCT_0:def_5; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for W being Subspace of V st v in W holds - v in W let v be Element of V; ::_thesis: for W being Subspace of V st v in W holds - v in W let W be Subspace of V; ::_thesis: ( v in W implies - v in W ) assume v in W ; ::_thesis: - v in W then (- (1_ GF)) * v in W by Th21; hence - v in W by VECTSP_1:14; ::_thesis: verum end; 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 & v in W holds u - v in W proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v in W holds u - v in W let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let u, v be Element of V; ::_thesis: for W being Subspace of V st u in W & v in W holds u - v in W let W be Subspace of V; ::_thesis: ( u in W & v in W implies u - v in W ) assume that A1: u in W and A2: v in W ; ::_thesis: u - v in W - v in W by A2, Th22; hence u - v in W by A1, Th20; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: V is Subspace of V A1: the lmult of V = the lmult of V | [: the carrier of GF, the carrier of V:] by RELSET_1:19; ( 0. V = 0. V & the addF of V = the addF of V || the carrier of V ) by RELSET_1:19; hence V is Subspace of V by A1, Def2; ::_thesis: verum end; 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 & X is Subspace of V holds V = X proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & X is Subspace of V holds V = X let X, V be non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: ( V is Subspace of X & X is Subspace of V implies V = X ) assume that A1: V is Subspace of X and A2: X is Subspace of V ; ::_thesis: V = X set VX = the carrier of X; set VV = the carrier of V; ( the carrier of V c= the carrier of X & the carrier of X c= the carrier of V ) by A1, A2, Def2; then A3: the carrier of V = the carrier of X by XBOOLE_0:def_10; set AX = the addF of X; set AV = the addF of V; ( the addF of V = the addF of X || the carrier of V & the addF of X = the addF of V || the carrier of X ) by A1, A2, Def2; then A4: the addF of V = the addF of X by A3, RELAT_1:72; set MX = the lmult of X; set MV = the lmult of V; A5: the lmult of X = the lmult of V | [: the carrier of GF, the carrier of X:] by A2, Def2; ( 0. V = 0. X & the lmult of V = the lmult of X | [: the carrier of GF, the carrier of V:] ) by A1, Def2; hence V = X by A3, A4, A5, RELAT_1:72; ::_thesis: verum end; 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 & X is Subspace of Y holds V is Subspace of Y proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & X is Subspace of Y holds V is Subspace of Y let V, X, Y be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: ( V is Subspace of X & X is Subspace of Y implies V is Subspace of Y ) assume that A1: V is Subspace of X and A2: X is Subspace of Y ; ::_thesis: V is Subspace of Y ( the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y ) by A1, A2, Def2; then A3: the carrier of V c= the carrier of Y by XBOOLE_1:1; A4: the addF of V = the addF of Y || the carrier of V proof set AY = the addF of Y; set VX = the carrier of X; set AX = the addF of X; set VV = the carrier of V; set AV = the addF of V; the carrier of V c= the carrier of X by A1, Def2; then A5: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96; the addF of V = the addF of X || the carrier of V by A1, Def2; then the addF of V = ( the addF of Y || the carrier of X) || the carrier of V by A2, Def2; hence the addF of V = the addF of Y || the carrier of V by A5, FUNCT_1:51; ::_thesis: verum end; set MY = the lmult of Y; set MX = the lmult of X; set MV = the lmult of V; set VX = the carrier of X; set VV = the carrier of V; the carrier of V c= the carrier of X by A1, Def2; then A6: [: the carrier of GF, the carrier of V:] c= [: the carrier of GF, the carrier of X:] by ZFMISC_1:95; the lmult of V = the lmult of X | [: the carrier of GF, the carrier of V:] by A1, Def2; then the lmult of V = ( the lmult of Y | [: the carrier of GF, the carrier of X:]) | [: the carrier of GF, the carrier of V:] by A2, Def2; then A7: the lmult of V = the lmult of Y | [: the carrier of GF, the carrier of V:] by A6, FUNCT_1:51; 0. V = 0. X by A1, Def2; then 0. V = 0. Y by A2, Def2; hence V is Subspace of Y by A3, A4, A7, Def2; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds W1 is Subspace of W2 let W1, W2 be Subspace of V; ::_thesis: ( the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2 ) set VW1 = the carrier of W1; set VW2 = the carrier of W2; set MW1 = the lmult of W1; set MW2 = the lmult of W2; set AV = the addF of V; set MV = the lmult of V; A1: ( the addF of W1 = the addF of V || the carrier of W1 & the addF of W2 = the addF of V || the carrier of W2 ) by Def2; assume A2: the carrier of W1 c= the carrier of W2 ; ::_thesis: W1 is Subspace of W2 then [: the carrier of W1, the carrier of W1:] c= [: the carrier of W2, the carrier of W2:] by ZFMISC_1:96; then A3: the addF of W1 = the addF of W2 || the carrier of W1 by A1, FUNCT_1:51; A4: ( the lmult of W1 = the lmult of V | [: the carrier of GF, the carrier of W1:] & the lmult of W2 = the lmult of V | [: the carrier of GF, the carrier of W2:] ) by Def2; [: the carrier of GF, the carrier of W1:] c= [: the carrier of GF, the carrier of W2:] by A2, ZFMISC_1:95; then A5: the lmult of W1 = the lmult of W2 | [: the carrier of GF, the carrier of W1:] by A4, FUNCT_1:51; ( 0. W1 = 0. V & 0. W2 = 0. V ) by Def2; hence W1 is Subspace of W2 by A2, A3, A5, Def2; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let W1, W2 be Subspace of V; ::_thesis: ( ( for v being Element of V st v in W1 holds v in W2 ) implies W1 is Subspace of W2 ) assume A1: for v being Element of V st v in W1 holds v in W2 ; ::_thesis: W1 is Subspace of W2 the carrier of W1 c= the carrier of W2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of W2 ) assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of W2 the carrier of W1 c= the carrier of V by Def2; then reconsider v = x as Element of V by A2; v in W1 by A2, STRUCT_0:def_5; then v in W2 by A1; hence x in the carrier of W2 by STRUCT_0:def_5; ::_thesis: verum end; hence W1 is Subspace of W2 by Th27; ::_thesis: verum end; 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 proof set M = the lmult of V; set W = VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); A1: VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is vector-distributive proof let a be Element of GF; :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds a * (b1 + b2) = (a * b1) + (a * b2) let v, w be Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); ::_thesis: a * (v + w) = (a * v) + (a * w) reconsider x = v, y = w as Element of V ; thus a * (v + w) = a * (x + y) .= (a * x) + (a * y) by VECTSP_1:def_14 .= (a * v) + (a * w) ; ::_thesis: verum end; A2: VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-distributive proof let a, b be Element of GF; :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds (a + b) * b1 = (a * b1) + (b * b1) let v be Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); ::_thesis: (a + b) * v = (a * v) + (b * v) reconsider x = v as Element of V ; thus (a + b) * v = (a + b) * x .= (a * x) + (b * x) by VECTSP_1:def_15 .= (a * v) + (b * v) ; ::_thesis: verum end; A3: VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-associative proof let a, b be Element of GF; :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds (a * b) * b1 = a * (b * b1) let v be Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); ::_thesis: (a * b) * v = a * (b * v) reconsider x = v as Element of V ; thus (a * b) * v = (a * b) * x .= a * (b * x) by VECTSP_1:def_16 .= a * (b * v) ; ::_thesis: verum end; A4: VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-unital proof let v be Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to VECTSP_1:def_17 ::_thesis: (1. GF) * v = v reconsider x = v as Element of V ; thus (1. GF) * v = (1_ GF) * x .= v by VECTSP_1:def_17 ; ::_thesis: verum end; A5: for a, b being Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) for x, y being Element of V st x = a & b = y holds a + b = x + y ; ( VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Abelian & VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable ) proof thus VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Abelian ::_thesis: ( VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable ) proof let a, b be Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a reconsider x = a, y = b as Element of V ; thus a + b = y + x by A5 .= b + a ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_3 ::_thesis: ( VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable ) let a, b, c be Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); ::_thesis: (a + b) + c = a + (b + c) reconsider x = a, y = b, z = c as Element of V ; thus (a + b) + c = (x + y) + z .= x + (y + z) by RLVECT_1:def_3 .= a + (b + c) ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_4 ::_thesis: VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable let a be Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); ::_thesis: a + (0. VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) = a reconsider x = a as Element of V ; thus a + (0. VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) = x + (0. V) .= a by RLVECT_1:4 ; ::_thesis: verum end; let a be Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable reconsider x = a as Element of V ; reconsider b = (comp V) . x as Element of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) ; take b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) thus a + b = x + (- x) by VECTSP_1:def_13 .= 0. VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) by RLVECT_1:5 ; ::_thesis: verum end; then reconsider W = VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF by A1, A2, A3, A4; A6: ( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19; the lmult of W = the lmult of V | [: the carrier of GF, the carrier of W:] by RELSET_1:19; then reconsider W = W as Subspace of V by A6, Def2; take W ; ::_thesis: W is strict thus W is strict ; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds W1 = W2 let W1, W2 be strict Subspace of V; ::_thesis: ( the carrier of W1 = the carrier of W2 implies W1 = W2 ) assume the carrier of W1 = the carrier of W2 ; ::_thesis: W1 = W2 then ( W1 is Subspace of W2 & W2 is Subspace of W1 ) by Th27; hence W1 = W2 by Th25; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let W1, W2 be strict Subspace of V; ::_thesis: ( ( for v being Element of V holds ( v in W1 iff v in W2 ) ) implies W1 = W2 ) assume A1: for v being Element of V holds ( v in W1 iff v in W2 ) ; ::_thesis: W1 = W2 for x being set holds ( x in the carrier of W1 iff x in the carrier of W2 ) proof let x be set ; ::_thesis: ( x in the carrier of W1 iff x in the carrier of W2 ) thus ( x in the carrier of W1 implies x in the carrier of W2 ) ::_thesis: ( x in the carrier of W2 implies x in the carrier of W1 ) proof assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of W2 the carrier of W1 c= the carrier of V by Def2; then reconsider v = x as Element of V by A2; v in W1 by A2, STRUCT_0:def_5; then v in W2 by A1; hence x in the carrier of W2 by STRUCT_0:def_5; ::_thesis: verum end; assume A3: x in the carrier of W2 ; ::_thesis: x in the carrier of W1 the carrier of W2 c= the carrier of V by Def2; then reconsider v = x as Element of V by A3; v in W2 by A3, STRUCT_0:def_5; then v in W1 by A1; hence x in the carrier of W1 by STRUCT_0:def_5; ::_thesis: verum end; then the carrier of W1 = the carrier of W2 by TARSKI:1; hence W1 = W2 by Th29; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being strict Subspace of V st the carrier of W = the carrier of V holds W = V let W be strict Subspace of V; ::_thesis: ( the carrier of W = the carrier of V implies W = V ) assume A1: the carrier of W = the carrier of V ; ::_thesis: W = V V is Subspace of V by Th24; hence W = V by A1, Th29; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being strict Subspace of V st ( for v being Element of V holds v in W ) holds W = V let W be strict Subspace of V; ::_thesis: ( ( for v being Element of V holds v in W ) implies W = V ) assume for v being Element of V holds v in W ; ::_thesis: W = V then A1: for v being Element of V holds ( v in W iff v in V ) by RLVECT_1:1; V is Subspace of V by Th24; hence W = V by A1, Th30; ::_thesis: verum end; 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 <> {} & V1 is linearly-closed holds ex W being strict Subspace of V st V1 = the carrier of W proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 <> {} & V1 is linearly-closed holds ex W being strict Subspace of V st V1 = the carrier of W let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let V1 be Subset of V; ::_thesis: ( V1 <> {} & V1 is linearly-closed implies ex W being strict Subspace of V st V1 = the carrier of W ) assume that A1: V1 <> {} and A2: V1 is linearly-closed ; ::_thesis: ex W being strict Subspace of V st V1 = the carrier of W reconsider D = V1 as non empty set by A1; reconsider d = 0. V as Element of D by A2, Th1; set VV = the carrier of V; set C = (comp V) | D; dom (comp V) = the carrier of V by FUNCT_2:def_1; then A3: dom ((comp V) | D) = D by RELAT_1:62; A4: rng ((comp V) | D) c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((comp V) | D) or x in D ) assume x in rng ((comp V) | D) ; ::_thesis: x in D then consider y being set such that A5: y in dom ((comp V) | D) and A6: ((comp V) | D) . y = x by FUNCT_1:def_3; reconsider y = y as Element of V by A3, A5; x = (comp V) . y by A5, A6, FUNCT_1:47 .= - y by VECTSP_1:def_13 ; hence x in D by A2, A3, A5, Th2; ::_thesis: verum end; set M = the lmult of V | [: the carrier of GF,D:]; dom the lmult of V = [: the carrier of GF, the carrier of V:] by FUNCT_2:def_1; then A7: dom ( the lmult of V | [: the carrier of GF,D:]) = [: the carrier of GF,D:] by RELAT_1:62, ZFMISC_1:96; A8: rng ( the lmult of V | [: the carrier of GF,D:]) c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the lmult of V | [: the carrier of GF,D:]) or x in D ) assume x in rng ( the lmult of V | [: the carrier of GF,D:]) ; ::_thesis: x in D then consider y being set such that A9: y in dom ( the lmult of V | [: the carrier of GF,D:]) and A10: ( the lmult of V | [: the carrier of GF,D:]) . y = x by FUNCT_1:def_3; consider y1, y2 being set such that A11: [y1,y2] = y by A7, A9, RELAT_1:def_1; reconsider y1 = y1 as Element of GF by A7, A9, A11, ZFMISC_1:87; A12: y2 in V1 by A7, A9, A11, ZFMISC_1:87; then reconsider y2 = y2 as Element of V ; x = y1 * y2 by A9, A10, A11, FUNCT_1:47; hence x in D by A2, A12, Def1; ::_thesis: verum end; set A = the addF of V || D; dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1; then A13: dom ( the addF of V || D) = [:D,D:] by RELAT_1:62, ZFMISC_1:96; A14: rng ( the addF of V || D) c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the addF of V || D) or x in D ) assume x in rng ( the addF of V || D) ; ::_thesis: x in D then consider y being set such that A15: y in dom ( the addF of V || D) and A16: ( the addF of V || D) . y = x by FUNCT_1:def_3; consider y1, y2 being set such that A17: [y1,y2] = y by A13, A15, RELAT_1:def_1; A18: ( y1 in D & y2 in D ) by A13, A15, A17, ZFMISC_1:87; then reconsider y1 = y1, y2 = y2 as Element of V ; x = y1 + y2 by A15, A16, A17, FUNCT_1:47; hence x in D by A2, A18, Def1; ::_thesis: verum end; reconsider M = the lmult of V | [: the carrier of GF,D:] as Function of [: the carrier of GF,D:],D by A7, A8, FUNCT_2:def_1, RELSET_1:4; reconsider C = (comp V) | D as UnOp of D by A3, A4, FUNCT_2:def_1, RELSET_1:4; reconsider A = the addF of V || D as BinOp of D by A13, A14, FUNCT_2:def_1, RELSET_1:4; set W = VectSpStr(# D,A,d,M #); A19: for a, b being Element of VectSpStr(# D,A,d,M #) for x, y being Element of V st x = a & b = y holds a + b = x + y proof let a, b be Element of VectSpStr(# D,A,d,M #); ::_thesis: for x, y being Element of V st x = a & b = y holds a + b = x + y let x, y be Element of V; ::_thesis: ( x = a & b = y implies a + b = x + y ) assume A20: ( x = a & b = y ) ; ::_thesis: a + b = x + y thus a + b = A . [a,b] .= x + y by A13, A20, FUNCT_1:47 ; ::_thesis: verum end; A21: ( VectSpStr(# D,A,d,M #) is Abelian & VectSpStr(# D,A,d,M #) is add-associative & VectSpStr(# D,A,d,M #) is right_zeroed & VectSpStr(# D,A,d,M #) is right_complementable ) proof thus VectSpStr(# D,A,d,M #) is Abelian ::_thesis: ( VectSpStr(# D,A,d,M #) is add-associative & VectSpStr(# D,A,d,M #) is right_zeroed & VectSpStr(# D,A,d,M #) is right_complementable ) proof let a, b be Element of VectSpStr(# D,A,d,M #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a reconsider x = a, y = b as Element of V by TARSKI:def_3; thus a + b = y + x by A19 .= b + a by A19 ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_3 ::_thesis: ( VectSpStr(# D,A,d,M #) is right_zeroed & VectSpStr(# D,A,d,M #) is right_complementable ) let a, b, c be Element of VectSpStr(# D,A,d,M #); ::_thesis: (a + b) + c = a + (b + c) reconsider x = a, y = b, z = c as Element of V by TARSKI:def_3; A22: b + c = y + z by A19; a + b = x + y by A19; hence (a + b) + c = (x + y) + z by A19 .= x + (y + z) by RLVECT_1:def_3 .= a + (b + c) by A19, A22 ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_4 ::_thesis: VectSpStr(# D,A,d,M #) is right_complementable let a be Element of VectSpStr(# D,A,d,M #); ::_thesis: a + (0. VectSpStr(# D,A,d,M #)) = a reconsider x = a as Element of V by TARSKI:def_3; thus a + (0. VectSpStr(# D,A,d,M #)) = x + (0. V) by A19 .= a by RLVECT_1:4 ; ::_thesis: verum end; let a be Element of VectSpStr(# D,A,d,M #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable reconsider x = a as Element of V by TARSKI:def_3; reconsider a9 = a as Element of D ; reconsider b = C . a9 as Element of D ; reconsider b = b as Element of VectSpStr(# D,A,d,M #) ; take b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. VectSpStr(# D,A,d,M #) thus a + b = x + ((comp V) . x) by A3, A19, FUNCT_1:47 .= x + (- x) by VECTSP_1:def_13 .= 0. VectSpStr(# D,A,d,M #) by RLVECT_1:5 ; ::_thesis: verum end; A23: VectSpStr(# D,A,d,M #) is vector-distributive proof let a be Element of GF; :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of VectSpStr(# D,A,d,M #) holds a * (b1 + b2) = (a * b1) + (a * b2) let v, w be Element of VectSpStr(# D,A,d,M #); ::_thesis: a * (v + w) = (a * v) + (a * w) reconsider x = v, y = w as Element of V by TARSKI:def_3; A24: now__::_thesis:_for_a_being_Element_of_GF for_x_being_Element_of_VectSpStr(#_D,A,d,M_#) for_y_being_Element_of_V_st_y_=_x_holds_ a_*_x_=_a_*_y let a be Element of GF; ::_thesis: for x being Element of VectSpStr(# D,A,d,M #) for y being Element of V st y = x holds a * x = a * y let x be Element of VectSpStr(# D,A,d,M #); ::_thesis: for y being Element of V st y = x holds a * x = a * y let y be Element of V; ::_thesis: ( y = x implies a * x = a * y ) assume A25: y = x ; ::_thesis: a * x = a * y [a,x] in dom M by A7; hence a * x = a * y by A25, FUNCT_1:47; ::_thesis: verum end; then A26: a * v = a * x ; A27: a * w = a * y by A24; v + w = x + y by A19; hence a * (v + w) = a * (x + y) by A24 .= (a * x) + (a * y) by VECTSP_1:def_14 .= (a * v) + (a * w) by A19, A26, A27 ; ::_thesis: verum end; A28: VectSpStr(# D,A,d,M #) is scalar-distributive proof let a, b be Element of GF; :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of VectSpStr(# D,A,d,M #) holds (a + b) * b1 = (a * b1) + (b * b1) let v be Element of VectSpStr(# D,A,d,M #); ::_thesis: (a + b) * v = (a * v) + (b * v) reconsider x = v as Element of V by TARSKI:def_3; A29: now__::_thesis:_for_a_being_Element_of_GF for_x_being_Element_of_VectSpStr(#_D,A,d,M_#) for_y_being_Element_of_V_st_y_=_x_holds_ a_*_x_=_a_*_y let a be Element of GF; ::_thesis: for x being Element of VectSpStr(# D,A,d,M #) for y being Element of V st y = x holds a * x = a * y let x be Element of VectSpStr(# D,A,d,M #); ::_thesis: for y being Element of V st y = x holds a * x = a * y let y be Element of V; ::_thesis: ( y = x implies a * x = a * y ) assume A30: y = x ; ::_thesis: a * x = a * y [a,x] in dom M by A7; hence a * x = a * y by A30, FUNCT_1:47; ::_thesis: verum end; then A31: a * v = a * x ; A32: b * v = b * x by A29; thus (a + b) * v = (a + b) * x by A29 .= (a * x) + (b * x) by VECTSP_1:def_15 .= (a * v) + (b * v) by A19, A32, A31 ; ::_thesis: verum end; A33: VectSpStr(# D,A,d,M #) is scalar-associative proof let a, b be Element of GF; :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of VectSpStr(# D,A,d,M #) holds (a * b) * b1 = a * (b * b1) let v be Element of VectSpStr(# D,A,d,M #); ::_thesis: (a * b) * v = a * (b * v) reconsider x = v as Element of V by TARSKI:def_3; A34: now__::_thesis:_for_a_being_Element_of_GF for_x_being_Element_of_VectSpStr(#_D,A,d,M_#) for_y_being_Element_of_V_st_y_=_x_holds_ a_*_x_=_a_*_y let a be Element of GF; ::_thesis: for x being Element of VectSpStr(# D,A,d,M #) for y being Element of V st y = x holds a * x = a * y let x be Element of VectSpStr(# D,A,d,M #); ::_thesis: for y being Element of V st y = x holds a * x = a * y let y be Element of V; ::_thesis: ( y = x implies a * x = a * y ) assume A35: y = x ; ::_thesis: a * x = a * y [a,x] in dom M by A7; hence a * x = a * y by A35, FUNCT_1:47; ::_thesis: verum end; then A36: b * v = b * x ; thus (a * b) * v = (a * b) * x by A34 .= a * (b * x) by VECTSP_1:def_16 .= a * (b * v) by A34, A36 ; ::_thesis: verum end; VectSpStr(# D,A,d,M #) is scalar-unital proof let v be Element of VectSpStr(# D,A,d,M #); :: according to VECTSP_1:def_17 ::_thesis: (1. GF) * v = v reconsider x = v as Element of V by TARSKI:def_3; now__::_thesis:_for_a_being_Element_of_GF for_x_being_Element_of_VectSpStr(#_D,A,d,M_#) for_y_being_Element_of_V_st_y_=_x_holds_ a_*_x_=_a_*_y let a be Element of GF; ::_thesis: for x being Element of VectSpStr(# D,A,d,M #) for y being Element of V st y = x holds a * x = a * y let x be Element of VectSpStr(# D,A,d,M #); ::_thesis: for y being Element of V st y = x holds a * x = a * y let y be Element of V; ::_thesis: ( y = x implies a * x = a * y ) assume A37: y = x ; ::_thesis: a * x = a * y [a,x] in dom M by A7; hence a * x = a * y by A37, FUNCT_1:47; ::_thesis: verum end; hence (1. GF) * v = (1_ GF) * x .= v by VECTSP_1:def_17 ; ::_thesis: verum end; then reconsider W = VectSpStr(# D,A,d,M #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF by A21, A23, A28, A33; 0. W = 0. V ; then reconsider W = W as strict Subspace of V by Def2; take W ; ::_thesis: V1 = the carrier of W thus V1 = the carrier of W ; ::_thesis: verum end; 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)} & 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 proof set W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); A1: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is vector-distributive proof let x be Element of GF; :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) holds x * (b1 + b2) = (x * b1) + (x * b2) let v, w be Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); ::_thesis: x * (v + w) = (x * v) + (x * w) reconsider v9 = v, w9 = w as Element of V ; thus x * (v + w) = x * (v9 + w9) .= (x * v9) + (x * w9) by VECTSP_1:def_14 .= (x * v) + (x * w) ; ::_thesis: verum end; A2: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-distributive proof let x, y be Element of GF; :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) holds (x + y) * b1 = (x * b1) + (y * b1) let v be Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); ::_thesis: (x + y) * v = (x * v) + (y * v) reconsider v9 = v as Element of V ; thus (x + y) * v = (x + y) * v9 .= (x * v9) + (y * v9) by VECTSP_1:def_15 .= (x * v) + (y * v) ; ::_thesis: verum end; A3: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-associative proof let x, y be Element of GF; :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) holds (x * y) * b1 = x * (y * b1) let v be Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); ::_thesis: (x * y) * v = x * (y * v) reconsider v9 = v as Element of V ; thus (x * y) * v = (x * y) * v9 .= x * (y * v9) by VECTSP_1:def_16 .= x * (y * v) ; ::_thesis: verum end; A4: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-unital proof let v be Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: according to VECTSP_1:def_17 ::_thesis: (1. GF) * v = v reconsider v9 = v as Element of V ; thus (1. GF) * v = (1_ GF) * v9 .= v by VECTSP_1:def_17 ; ::_thesis: verum end; A5: for a being Element of GF for v, w being Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) for v9, w9 being Element of V st v = v9 & w = w9 holds ( v + w = v9 + w9 & a * v = a * v9 ) ; ( VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is Abelian & VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is add-associative & VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_complementable ) proof thus VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is Abelian ::_thesis: ( VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is add-associative & VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_complementable ) proof let x, y be Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x reconsider x9 = x, y9 = y as Element of V ; thus x + y = y9 + x9 by A5 .= y + x ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_3 ::_thesis: ( VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_complementable ) let x, y, z be Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); ::_thesis: (x + y) + z = x + (y + z) reconsider x9 = x, y9 = y, z9 = z as Element of V ; thus (x + y) + z = (x9 + y9) + z9 .= x9 + (y9 + z9) by RLVECT_1:def_3 .= x + (y + z) ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_4 ::_thesis: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_complementable let x be Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); ::_thesis: x + (0. VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)) = x reconsider x9 = x as Element of V ; thus x + (0. VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)) = x9 + (0. V) .= x by RLVECT_1:4 ; ::_thesis: verum end; let x be Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable reconsider x9 = x as Element of V ; consider b being Element of V such that A6: x9 + b = 0. V by ALGSTR_0:def_11; reconsider b9 = b as Element of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ; take b9 ; :: according to ALGSTR_0:def_11 ::_thesis: x + b9 = 0. VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) thus x + b9 = 0. VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A6; ::_thesis: verum end; then reconsider W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF by A4, A1, A2, A3; A7: the lmult of W = the lmult of V | [: the carrier of GF, the carrier of W:] by RELSET_1:19; ( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19; hence VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V by A7, Def2; ::_thesis: verum end; 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 ) proof let x be set ; ::_thesis: 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 ) let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: ( x in (0). V iff x = 0. V ) thus ( x in (0). V implies x = 0. V ) ::_thesis: ( x = 0. V implies x in (0). V ) proof assume x in (0). V ; ::_thesis: x = 0. V then x in the carrier of ((0). V) by STRUCT_0:def_5; then x in {(0. V)} by Def3; hence x = 0. V by TARSKI:def_1; ::_thesis: verum end; thus ( x = 0. V implies x in (0). V ) by Th17; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V holds (0). W = (0). V let W be Subspace of V; ::_thesis: (0). W = (0). V ( the carrier of ((0). W) = {(0. W)} & the carrier of ((0). V) = {(0. V)} ) by Def3; then A1: the carrier of ((0). W) = the carrier of ((0). V) by Def2; (0). W is Subspace of V by Th26; hence (0). W = (0). V by A1, Th29; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of V holds (0). W1 = (0). W2 let W1, W2 be Subspace of V; ::_thesis: (0). W1 = (0). W2 (0). W1 = (0). V by Th36; hence (0). W1 = (0). W2 by Th36; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V holds (0). V is Subspace of W let W be Subspace of V; ::_thesis: (0). V is Subspace of W (0). W = (0). V by Th36; hence (0). V is Subspace of W ; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2 let W1, W2 be Subspace of V; ::_thesis: (0). W1 is Subspace of W2 (0). W1 = (0). W2 by Th37; hence (0). W1 is Subspace of W2 ; ::_thesis: verum end; 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 proof set Y = { (v + u) where u is Element of V : u in W } ; defpred S1[ set ] means ex u being Element of V st ( $1 = v + u & u in W ); consider X being set such that A1: for x being set holds ( x in X iff ( x in the carrier of V & S1[x] ) ) from XBOOLE_0:sch_1(); X c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of V ) assume x in X ; ::_thesis: x in the carrier of V hence x in the carrier of V by A1; ::_thesis: verum end; then reconsider X = X as Subset of V ; A2: { (v + u) where u is Element of V : u in W } c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where u is Element of V : u in W } or x in X ) assume x in { (v + u) where u is Element of V : u in W } ; ::_thesis: x in X then ex u being Element of V st ( x = v + u & u in W ) ; hence x in X by A1; ::_thesis: verum end; X c= { (v + u) where u is Element of V : u in W } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in { (v + u) where u is Element of V : u in W } ) assume x in X ; ::_thesis: x in { (v + u) where u is Element of V : u in W } then ex u being Element of V st ( x = v + u & u in W ) by A1; hence x in { (v + u) where u is Element of V : u in W } ; ::_thesis: verum end; hence { (v + u) where u is Element of V : u in W } is Subset of V by A2, XBOOLE_0:def_10; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V holds (0. V) + W = the carrier of W let W be Subspace of V; ::_thesis: (0. V) + W = the carrier of W set A = { ((0. V) + u) where u is Element of V : u in W } ; A1: the carrier of W c= { ((0. V) + u) where u is Element of V : u in W } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in { ((0. V) + u) where u is Element of V : u in W } ) assume x in the carrier of W ; ::_thesis: x in { ((0. V) + u) where u is Element of V : u in W } then A2: x in W by STRUCT_0:def_5; then x in V by Th9; then reconsider y = x as Element of V by STRUCT_0:def_5; (0. V) + y = x by RLVECT_1:4; hence x in { ((0. V) + u) where u is Element of V : u in W } by A2; ::_thesis: verum end; { ((0. V) + u) where u is Element of V : u in W } c= the carrier of W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((0. V) + u) where u is Element of V : u in W } or x in the carrier of W ) assume x in { ((0. V) + u) where u is Element of V : u in W } ; ::_thesis: x in the carrier of W then consider u being Element of V such that A3: x = (0. V) + u and A4: u in W ; x = u by A3, RLVECT_1:4; hence x in the carrier of W by A4, STRUCT_0:def_5; ::_thesis: verum end; hence (0. V) + W = the carrier of W by A1, XBOOLE_0:def_10; ::_thesis: verum end; 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 proof reconsider VW = the carrier of W as Subset of V by Def2; take VW ; ::_thesis: ex v being Element of V st VW = v + W take 0. V ; ::_thesis: VW = (0. V) + W thus VW = (0. V) + W by Lm3; ::_thesis: verum end; 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 & x = v + u ) ) proof let x be set ; ::_thesis: 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 & x = v + u ) ) let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & x = v + u ) ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) ) let v be Element of V; ::_thesis: 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 ) ) let W be Subspace of V; ::_thesis: ( x in v + W iff ex u being Element of V st ( u in W & x = v + u ) ) thus ( x in v + W implies ex u being Element of V st ( u in W & x = v + u ) ) ::_thesis: ( ex u being Element of V st ( u in W & x = v + u ) implies x in v + W ) proof assume x in v + W ; ::_thesis: ex u being Element of V st ( u in W & x = v + u ) then consider u being Element of V such that A1: ( x = v + u & u in W ) ; take u ; ::_thesis: ( u in W & x = v + u ) thus ( u in W & x = v + u ) by A1; ::_thesis: verum end; given u being Element of V such that A2: ( u in W & x = v + u ) ; ::_thesis: x in v + W thus x in v + W by A2; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for W being Subspace of V holds ( 0. V in v + W iff v in W ) let v be Element of V; ::_thesis: for W being Subspace of V holds ( 0. V in v + W iff v in W ) let W be Subspace of V; ::_thesis: ( 0. V in v + W iff v in W ) thus ( 0. V in v + W implies v in W ) ::_thesis: ( v in W implies 0. V in v + W ) proof assume 0. V in v + W ; ::_thesis: v in W then consider u being Element of V such that A1: 0. V = v + u and A2: u in W ; v = - u by A1, VECTSP_1:16; hence v in W by A2, Th22; ::_thesis: verum end; assume v in W ; ::_thesis: 0. V in v + W then A3: - v in W by Th22; 0. V = v + (- v) by VECTSP_1:19; hence 0. V in v + W by A3; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for W being Subspace of V holds v in v + W let v be Element of V; ::_thesis: for W being Subspace of V holds v in v + W let W be Subspace of V; ::_thesis: v in v + W ( v + (0. V) = v & 0. V in W ) by Th17, RLVECT_1:4; hence v in v + W ; ::_thesis: verum end; 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} proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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} let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V holds v + ((0). V) = {v} let v be Element of V; ::_thesis: v + ((0). V) = {v} thus v + ((0). V) c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= v + ((0). V) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + ((0). V) or x in {v} ) assume x in v + ((0). V) ; ::_thesis: x in {v} then consider u being Element of V such that A1: x = v + u and A2: u in (0). V ; A3: the carrier of ((0). V) = {(0. V)} by Def3; u in the carrier of ((0). V) by A2, STRUCT_0:def_5; then u = 0. V by A3, TARSKI:def_1; then x = v by A1, RLVECT_1:4; hence x in {v} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in v + ((0). V) ) assume x in {v} ; ::_thesis: x in v + ((0). V) then A4: x = v by TARSKI:def_1; ( 0. V in (0). V & v = v + (0. V) ) by Th17, RLVECT_1:4; hence x in v + ((0). V) by A4; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for W being Subspace of V holds ( v in W iff v + W = the carrier of W ) let v be Element of V; ::_thesis: for W being Subspace of V holds ( v in W iff v + W = the carrier of W ) let W be Subspace of V; ::_thesis: ( v in W iff v + W = the carrier of W ) ( 0. V in W & v + (0. V) = v ) by Th17, RLVECT_1:4; then A1: v in { (v + u) where u is Element of V : u in W } ; thus ( v in W implies v + W = the carrier of W ) ::_thesis: ( v + W = the carrier of W implies v in W ) proof assume A2: v in W ; ::_thesis: v + W = the carrier of W thus v + W c= the carrier of W :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W c= v + W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in the carrier of W ) assume x in v + W ; ::_thesis: x in the carrier of W then consider u being Element of V such that A3: x = v + u and A4: u in W ; v + u in W by A2, A4, Th20; hence x in the carrier of W by A3, STRUCT_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in v + W ) assume x in the carrier of W ; ::_thesis: x in v + W then reconsider y = x, z = v as Element of W by A2, STRUCT_0:def_5; reconsider y1 = y, z1 = z as Element of V by Th10; A5: z + (y - z) = y + (z + (- z)) by RLVECT_1:def_3 .= y + (0. W) by VECTSP_1:19 .= x by RLVECT_1:4 ; y - z in W by STRUCT_0:def_5; then A6: y1 - z1 in W by Th16; y - z = y1 - z1 by Th16; then z1 + (y1 - z1) = x by A5, Th13; hence x in v + W by A6; ::_thesis: verum end; assume A7: v + W = the carrier of W ; ::_thesis: v in W assume not v in W ; ::_thesis: contradiction hence contradiction by A7, A1, STRUCT_0:def_5; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V holds v + ((Omega). V) = the carrier of V let v be Element of V; ::_thesis: v + ((Omega). V) = the carrier of V v in (Omega). V by RLVECT_1:1; hence v + ((Omega). V) = the carrier of V by Lm4; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) let v be Element of V; ::_thesis: for W being Subspace of V holds ( 0. V in v + W iff v + W = the carrier of W ) let W be Subspace of V; ::_thesis: ( 0. V in v + W iff v + W = the carrier of W ) ( 0. V in v + W iff v in W ) by Th43; hence ( 0. V in v + W iff v + W = the carrier of W ) by Lm4; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let a be Element of GF; ::_thesis: for v being Element of V for W being Subspace of V st v in W holds (a * v) + W = the carrier of W let v be Element of V; ::_thesis: for W being Subspace of V st v in W holds (a * v) + W = the carrier of W let W be Subspace of V; ::_thesis: ( v in W implies (a * v) + W = the carrier of W ) assume v in W ; ::_thesis: (a * v) + W = the carrier of W then a * v in W by Th21; hence (a * v) + W = the carrier of W by Lm4; ::_thesis: verum end; 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 proof let GF be Field; ::_thesis: 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 let V be VectSp of GF; ::_thesis: 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 let a be Element of GF; ::_thesis: 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 let v be Element of V; ::_thesis: for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds v in W let W be Subspace of V; ::_thesis: ( a <> 0. GF & (a * v) + W = the carrier of W implies v in W ) assume that A1: a <> 0. GF and A2: (a * v) + W = the carrier of W ; ::_thesis: v in W assume not v in W ; ::_thesis: contradiction then not (1_ GF) * v in W by VECTSP_1:def_17; then not ((a ") * a) * v in W by A1, VECTSP_1:def_10; then not (a ") * (a * v) in W by VECTSP_1:def_16; then A3: not a * v in W by Th21; ( 0. V in W & (a * v) + (0. V) = a * v ) by Th17, RLVECT_1:4; then a * v in { ((a * v) + u) where u is Vector of V : u in W } ; hence contradiction by A2, A3, STRUCT_0:def_5; ::_thesis: verum 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 ) proof let GF be Field; ::_thesis: 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 ) let V be VectSp of GF; ::_thesis: for v being Element of V for W being Subspace of V holds ( v in W iff (- v) + W = the carrier of W ) let v be Element of V; ::_thesis: for W being Subspace of V holds ( v in W iff (- v) + W = the carrier of W ) let W be Subspace of V; ::_thesis: ( v in W iff (- v) + W = the carrier of W ) - (1_ GF) <> 0. GF by VECTSP_2:3; then ( v in W iff ((- (1_ GF)) * v) + W = the carrier of W ) by Th50, Th51; hence ( v in W iff (- v) + W = the carrier of W ) by VECTSP_1:14; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for u, v being Element of V for W being Subspace of V holds ( u in W iff v + W = (v + u) + W ) let u, v be Element of V; ::_thesis: for W being Subspace of V holds ( u in W iff v + W = (v + u) + W ) let W be Subspace of V; ::_thesis: ( u in W iff v + W = (v + u) + W ) thus ( u in W implies v + W = (v + u) + W ) ::_thesis: ( v + W = (v + u) + W implies u in W ) proof assume A1: u in W ; ::_thesis: v + W = (v + u) + W thus v + W c= (v + u) + W :: according to XBOOLE_0:def_10 ::_thesis: (v + u) + W c= v + W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in (v + u) + W ) assume x in v + W ; ::_thesis: x in (v + u) + W then consider v1 being Element of V such that A2: x = v + v1 and A3: v1 in W ; A4: (v + u) + (v1 - u) = v + (u + (v1 - u)) by RLVECT_1:def_3 .= v + ((v1 + u) - u) by RLVECT_1:def_3 .= v + (v1 + (u - u)) by RLVECT_1:def_3 .= v + (v1 + (0. V)) by VECTSP_1:19 .= x by A2, RLVECT_1:4 ; v1 - u in W by A1, A3, Th23; hence x in (v + u) + W by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (v + u) + W or x in v + W ) assume x in (v + u) + W ; ::_thesis: x in v + W then consider v2 being Element of V such that A5: x = (v + u) + v2 and A6: v2 in W ; A7: x = v + (u + v2) by A5, RLVECT_1:def_3; u + v2 in W by A1, A6, Th20; hence x in v + W by A7; ::_thesis: verum end; assume A8: v + W = (v + u) + W ; ::_thesis: u in W ( 0. V in W & v + (0. V) = v ) by Th17, RLVECT_1:4; then v in (v + u) + W by A8; then consider u1 being Element of V such that A9: v = (v + u) + u1 and A10: u1 in W ; v = v + (u + u1) by A9, RLVECT_1:def_3; then u + u1 = 0. V by RLVECT_1:9; then u = - u1 by VECTSP_1:16; hence u in W by A10, Th22; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for u, v being Element of V for W being Subspace of V holds ( u in W iff v + W = (v - u) + W ) let u, v be Element of V; ::_thesis: for W being Subspace of V holds ( u in W iff v + W = (v - u) + W ) let W be Subspace of V; ::_thesis: ( u in W iff v + W = (v - u) + W ) A1: ( - u in W implies u in W ) proof assume - u in W ; ::_thesis: u in W then - (- u) in W by Th22; hence u in W by RLVECT_1:17; ::_thesis: verum end; ( - u in W iff v + W = (v + (- u)) + W ) by Th53; hence ( u in W iff v + W = (v - u) + W ) by A1, Th22; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v, u being Element of V for W being Subspace of V holds ( v in u + W iff u + W = v + W ) let v, u be Element of V; ::_thesis: for W being Subspace of V holds ( v in u + W iff u + W = v + W ) let W be Subspace of V; ::_thesis: ( v in u + W iff u + W = v + W ) thus ( v in u + W implies u + W = v + W ) ::_thesis: ( u + W = v + W implies v in u + W ) proof assume v in u + W ; ::_thesis: u + W = v + W then consider z being Element of V such that A1: v = u + z and A2: z in W ; thus u + W c= v + W :: according to XBOOLE_0:def_10 ::_thesis: v + W c= u + W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in u + W or x in v + W ) assume x in u + W ; ::_thesis: x in v + W then consider v1 being Element of V such that A3: x = u + v1 and A4: v1 in W ; v - z = u + (z - z) by A1, RLVECT_1:def_3 .= u + (0. V) by VECTSP_1:19 .= u by RLVECT_1:4 ; then A5: x = v + (v1 + (- z)) by A3, RLVECT_1:def_3 .= v + (v1 - z) ; v1 - z in W by A2, A4, Th23; hence x in v + W by A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in u + W ) assume x in v + W ; ::_thesis: x in u + W then consider v2 being Element of V such that A6: ( x = v + v2 & v2 in W ) ; ( z + v2 in W & x = u + (z + v2) ) by A1, A2, A6, Th20, RLVECT_1:def_3; hence x in u + W ; ::_thesis: verum end; thus ( u + W = v + W implies v in u + W ) by Th44; ::_thesis: verum end; 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 & u in v2 + W holds v1 + W = v2 + W proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & u in v2 + W holds v1 + W = v2 + W let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let u, v1, v2 be Element of V; ::_thesis: for W being Subspace of V st u in v1 + W & u in v2 + W holds v1 + W = v2 + W let W be Subspace of V; ::_thesis: ( u in v1 + W & u in v2 + W implies v1 + W = v2 + W ) assume that A1: u in v1 + W and A2: u in v2 + W ; ::_thesis: v1 + W = v2 + W thus v1 + W = u + W by A1, Th55 .= v2 + W by A2, Th55 ; ::_thesis: verum 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 proof let GF be Field; ::_thesis: 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 let V be VectSp of GF; ::_thesis: 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 let a be Element of GF; ::_thesis: 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 let v be Element of V; ::_thesis: for W being Subspace of V st a <> 1_ GF & a * v in v + W holds v in W let W be Subspace of V; ::_thesis: ( a <> 1_ GF & a * v in v + W implies v in W ) assume that A1: a <> 1_ GF and A2: a * v in v + W ; ::_thesis: v in W A3: a - (1_ GF) <> 0. GF by A1, RLVECT_1:21; consider u being Element of V such that A4: a * v = v + u and A5: u in W by A2; u = u + (0. V) by RLVECT_1:4 .= u + (v - v) by VECTSP_1:19 .= (a * v) - v by A4, RLVECT_1:def_3 .= (a * v) - ((1_ GF) * v) by VECTSP_1:def_17 .= (a - (1_ GF)) * v by Lm1 ; then ((a - (1_ GF)) ") * u = (((a - (1_ GF)) ") * (a - (1_ GF))) * v by VECTSP_1:def_16; then (1_ GF) * v = ((a - (1_ GF)) ") * u by A3, VECTSP_1:def_10; then v = ((a - (1_ GF)) ") * u by VECTSP_1:def_17; hence v in W by A5, Th21; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let a be Element of GF; ::_thesis: for v being Element of V for W being Subspace of V st v in W holds a * v in v + W let v be Element of V; ::_thesis: for W being Subspace of V st v in W holds a * v in v + W let W be Subspace of V; ::_thesis: ( v in W implies a * v in v + W ) assume v in W ; ::_thesis: a * v in v + W then ( v + W = the carrier of W & a * v in W ) by Lm4, Th21; hence a * v in v + W by STRUCT_0:def_5; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for W being Subspace of V st v in W holds - v in v + W let v be Element of V; ::_thesis: for W being Subspace of V st v in W holds - v in v + W let W be Subspace of V; ::_thesis: ( v in W implies - v in v + W ) assume v in W ; ::_thesis: - v in v + W then (- (1_ GF)) * v in v + W by Th58; hence - v in v + W by VECTSP_1:14; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for u, v being Element of V for W being Subspace of V holds ( u + v in v + W iff u in W ) let u, v be Element of V; ::_thesis: for W being Subspace of V holds ( u + v in v + W iff u in W ) let W be Subspace of V; ::_thesis: ( u + v in v + W iff u in W ) thus ( u + v in v + W implies u in W ) ::_thesis: ( u in W implies u + v in v + W ) proof assume u + v in v + W ; ::_thesis: u in W then ex v1 being Element of V st ( u + v = v + v1 & v1 in W ) ; hence u in W by RLVECT_1:8; ::_thesis: verum end; assume u in W ; ::_thesis: u + v in v + W hence u + v in v + W ; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v, u being Element of V for W being Subspace of V holds ( v - u in v + W iff u in W ) let v, u be Element of V; ::_thesis: for W being Subspace of V holds ( v - u in v + W iff u in W ) let W be Subspace of V; ::_thesis: ( v - u in v + W iff u in W ) A1: v - u = (- u) + v ; A2: ( - u in W implies - (- u) in W ) by Th22; ( u in W implies - u in W ) by Th22; hence ( v - u in v + W iff u in W ) by A1, A2, Th60, RLVECT_1:17; ::_thesis: verum end; 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 & u = v - v1 ) ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & u = v - v1 ) ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) ) let u, v be Element of V; ::_thesis: 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 ) ) let W be Subspace of V; ::_thesis: ( u in v + W iff ex v1 being Element of V st ( v1 in W & u = v - v1 ) ) thus ( u in v + W implies ex v1 being Element of V st ( v1 in W & u = v - v1 ) ) ::_thesis: ( ex v1 being Element of V st ( v1 in W & u = v - v1 ) implies u in v + W ) proof assume u in v + W ; ::_thesis: ex v1 being Element of V st ( v1 in W & u = v - v1 ) then consider v1 being Element of V such that A1: u = v + v1 and A2: v1 in W ; take x = - v1; ::_thesis: ( x in W & u = v - x ) thus x in W by A2, Th22; ::_thesis: u = v - x thus u = v - x by A1, RLVECT_1:17; ::_thesis: verum end; given v1 being Element of V such that A3: v1 in W and A4: u = v - v1 ; ::_thesis: u in v + W - v1 in W by A3, Th22; hence u in v + W by A4; ::_thesis: verum end; 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 & v2 in v + W ) iff v1 - v2 in W ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v2 in v + W ) iff v1 - v2 in W ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) let v1, v2 be Element of V; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: ( ex v being Element of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) thus ( ex v being Element of V st ( v1 in v + W & v2 in v + W ) implies v1 - v2 in W ) ::_thesis: ( v1 - v2 in W implies ex v being Element of V st ( v1 in v + W & v2 in v + W ) ) proof given v being Element of V such that A1: v1 in v + W and A2: v2 in v + W ; ::_thesis: v1 - v2 in W consider u2 being Element of V such that A3: u2 in W and A4: v2 = v + u2 by A2, Th42; consider u1 being Element of V such that A5: u1 in W and A6: v1 = v + u1 by A1, Th42; v1 - v2 = (u1 + v) + ((- v) - u2) by A6, A4, VECTSP_1:17 .= ((u1 + v) + (- v)) - u2 by RLVECT_1:def_3 .= (u1 + (v + (- v))) - u2 by RLVECT_1:def_3 .= (u1 + (0. V)) - u2 by RLVECT_1:5 .= u1 - u2 by RLVECT_1:4 ; hence v1 - v2 in W by A5, A3, Th23; ::_thesis: verum end; assume v1 - v2 in W ; ::_thesis: ex v being Element of V st ( v1 in v + W & v2 in v + W ) then A7: - (v1 - v2) in W by Th22; take v1 ; ::_thesis: ( v1 in v1 + W & v2 in v1 + W ) thus v1 in v1 + W by Th44; ::_thesis: v2 in v1 + W v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by VECTSP_1:17 .= (v1 + (- v1)) + v2 by RLVECT_1:def_3 .= (0. V) + v2 by RLVECT_1:5 .= v2 by RLVECT_1:4 ; hence v2 in v1 + W by A7; ::_thesis: verum end; 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 & v + v1 = u ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v + v1 = u ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 & v + v1 = u ) let v, u be Element of V; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: ( v + W = u + W implies ex v1 being Element of V st ( v1 in W & v + v1 = u ) ) assume v + W = u + W ; ::_thesis: ex v1 being Element of V st ( v1 in W & v + v1 = u ) then v in u + W by Th44; then consider u1 being Element of V such that A1: v = u + u1 and A2: u1 in W ; take v1 = u - v; ::_thesis: ( v1 in W & v + v1 = u ) 0. V = (u + u1) - v by A1, VECTSP_1:19 .= u1 + (u - v) by RLVECT_1:def_3 ; then v1 = - u1 by VECTSP_1:16; hence v1 in W by A2, Th22; ::_thesis: v + v1 = u thus v + v1 = (u + v) - v by RLVECT_1:def_3 .= u + (v - v) by RLVECT_1:def_3 .= u + (0. V) by VECTSP_1:19 .= u by RLVECT_1:4 ; ::_thesis: verum end; 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 & v - v1 = u ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v - v1 = u ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 & v - v1 = u ) let v, u be Element of V; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: ( v + W = u + W implies ex v1 being Element of V st ( v1 in W & v - v1 = u ) ) assume v + W = u + W ; ::_thesis: ex v1 being Element of V st ( v1 in W & v - v1 = u ) then u in v + W by Th44; then consider u1 being Element of V such that A1: u = v + u1 and A2: u1 in W ; take v1 = v - u; ::_thesis: ( v1 in W & v - v1 = u ) 0. V = (v + u1) - u by A1, VECTSP_1:19 .= u1 + (v - u) by RLVECT_1:def_3 ; then v1 = - u1 by VECTSP_1:16; hence v1 in W by A2, Th22; ::_thesis: v - v1 = u thus v - v1 = (v - v) + u by RLVECT_1:29 .= (0. V) + u by VECTSP_1:19 .= u by RLVECT_1:4 ; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for W1, W2 being strict Subspace of V holds ( v + W1 = v + W2 iff W1 = W2 ) let v be Element of V; ::_thesis: for W1, W2 being strict Subspace of V holds ( v + W1 = v + W2 iff W1 = W2 ) let W1, W2 be strict Subspace of V; ::_thesis: ( v + W1 = v + W2 iff W1 = W2 ) thus ( v + W1 = v + W2 implies W1 = W2 ) ::_thesis: ( W1 = W2 implies v + W1 = v + W2 ) proof assume A1: v + W1 = v + W2 ; ::_thesis: W1 = W2 the carrier of W1 = the carrier of W2 proof A2: the carrier of W1 c= the carrier of V by Def2; thus the carrier of W1 c= the carrier of W2 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W2 c= the carrier of W1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of W2 ) assume A3: x in the carrier of W1 ; ::_thesis: x in the carrier of W2 then reconsider y = x as Element of V by A2; set z = v + y; x in W1 by A3, STRUCT_0:def_5; then v + y in v + W2 by A1; then consider u being Element of V such that A4: v + y = v + u and A5: u in W2 ; y = u by A4, RLVECT_1:8; hence x in the carrier of W2 by A5, STRUCT_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W2 or x in the carrier of W1 ) assume A6: x in the carrier of W2 ; ::_thesis: x in the carrier of W1 the carrier of W2 c= the carrier of V by Def2; then reconsider y = x as Element of V by A6; set z = v + y; x in W2 by A6, STRUCT_0:def_5; then v + y in v + W1 by A1; then consider u being Element of V such that A7: v + y = v + u and A8: u in W1 ; y = u by A7, RLVECT_1:8; hence x in the carrier of W1 by A8, STRUCT_0:def_5; ::_thesis: verum end; hence W1 = W2 by Th29; ::_thesis: verum end; thus ( W1 = W2 implies v + W1 = v + W2 ) ; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v, u being Element of V for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds W1 = W2 let v, u be Element of V; ::_thesis: for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds W1 = W2 let W1, W2 be strict Subspace of V; ::_thesis: ( v + W1 = u + W2 implies W1 = W2 ) assume A1: v + W1 = u + W2 ; ::_thesis: W1 = W2 set V2 = the carrier of W2; set V1 = the carrier of W1; assume A2: W1 <> W2 ; ::_thesis: contradiction A3: now__::_thesis:_not_the_carrier_of_W1_\_the_carrier_of_W2_<>_{} set x = the Element of the carrier of W1 \ the carrier of W2; assume the carrier of W1 \ the carrier of W2 <> {} ; ::_thesis: contradiction then the Element of the carrier of W1 \ the carrier of W2 in the carrier of W1 by XBOOLE_0:def_5; then A4: the Element of the carrier of W1 \ the carrier of W2 in W1 by STRUCT_0:def_5; then the Element of the carrier of W1 \ the carrier of W2 in V by Th9; then reconsider x = the Element of the carrier of W1 \ the carrier of W2 as Element of V by STRUCT_0:def_5; set z = v + x; v + x in u + W2 by A1, A4; then consider u1 being Element of V such that A5: v + x = u + u1 and A6: u1 in W2 ; x = (0. V) + x by RLVECT_1:4 .= (v + (- v)) + x by VECTSP_1:19 .= (- v) + (u + u1) by A5, RLVECT_1:def_3 ; then A7: (v + ((- v) + (u + u1))) + W1 = v + W1 by A4, Th53; v + ((- v) + (u + u1)) = (v + (- v)) + (u + u1) by RLVECT_1:def_3 .= (0. V) + (u + u1) by VECTSP_1:19 .= u + u1 by RLVECT_1:4 ; then (u + u1) + W2 = (u + u1) + W1 by A1, A6, A7, Th53; hence contradiction by A2, Th66; ::_thesis: verum end; A8: now__::_thesis:_not_the_carrier_of_W2_\_the_carrier_of_W1_<>_{} set x = the Element of the carrier of W2 \ the carrier of W1; assume the carrier of W2 \ the carrier of W1 <> {} ; ::_thesis: contradiction then the Element of the carrier of W2 \ the carrier of W1 in the carrier of W2 by XBOOLE_0:def_5; then A9: the Element of the carrier of W2 \ the carrier of W1 in W2 by STRUCT_0:def_5; then the Element of the carrier of W2 \ the carrier of W1 in V by Th9; then reconsider x = the Element of the carrier of W2 \ the carrier of W1 as Element of V by STRUCT_0:def_5; set z = u + x; u + x in v + W1 by A1, A9; then consider u1 being Element of V such that A10: u + x = v + u1 and A11: u1 in W1 ; x = (0. V) + x by RLVECT_1:4 .= (u + (- u)) + x by VECTSP_1:19 .= (- u) + (v + u1) by A10, RLVECT_1:def_3 ; then A12: (u + ((- u) + (v + u1))) + W2 = u + W2 by A9, Th53; u + ((- u) + (v + u1)) = (u + (- u)) + (v + u1) by RLVECT_1:def_3 .= (0. V) + (v + u1) by VECTSP_1:19 .= v + u1 by RLVECT_1:4 ; then (v + u1) + W1 = (v + u1) + W2 by A1, A11, A12, Th53; hence contradiction by A2, Th66; ::_thesis: verum end; the carrier of W1 <> the carrier of W2 by A2, Th29; then ( not the carrier of W1 c= the carrier of W2 or not the carrier of W2 c= the carrier of W1 ) by XBOOLE_0:def_10; hence contradiction by A3, A8, XBOOLE_1:37; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for W being Subspace of V ex C being Coset of W st v in C let v be Element of V; ::_thesis: for W being Subspace of V ex C being Coset of W st v in C let W be Subspace of V; ::_thesis: ex C being Coset of W st v in C reconsider C = v + W as Coset of W by Def6; take C ; ::_thesis: v in C thus v in C by Th44; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V for C being Coset of W holds ( C is linearly-closed iff C = the carrier of W ) let W be Subspace of V; ::_thesis: for C being Coset of W holds ( C is linearly-closed iff C = the carrier of W ) let C be Coset of W; ::_thesis: ( C is linearly-closed iff C = the carrier of W ) thus ( C is linearly-closed implies C = the carrier of W ) ::_thesis: ( C = the carrier of W implies C is linearly-closed ) proof assume A1: C is linearly-closed ; ::_thesis: C = the carrier of W consider v being Element of V such that A2: C = v + W by Def6; C <> {} by A2, Th44; then 0. V in v + W by A1, A2, Th1; hence C = the carrier of W by A2, Th48; ::_thesis: verum end; thus ( C = the carrier of W implies C is linearly-closed ) by Lm2; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let W1, W2 be strict Subspace of V; ::_thesis: for C1 being Coset of W1 for C2 being Coset of W2 st C1 = C2 holds W1 = W2 let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 st C1 = C2 holds W1 = W2 let C2 be Coset of W2; ::_thesis: ( C1 = C2 implies W1 = W2 ) ( ex v1 being Element of V st C1 = v1 + W1 & ex v2 being Element of V st C2 = v2 + W2 ) by Def6; hence ( C1 = C2 implies W1 = W2 ) by Th67; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V holds {v} is Coset of (0). V let v be Element of V; ::_thesis: {v} is Coset of (0). V v + ((0). V) = {v} by Th46; hence {v} is Coset of (0). V by Def6; ::_thesis: verum end; 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} proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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} let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for V1 being Subset of V st V1 is Coset of (0). V holds ex v being Element of V st V1 = {v} let V1 be Subset of V; ::_thesis: ( V1 is Coset of (0). V implies ex v being Element of V st V1 = {v} ) assume V1 is Coset of (0). V ; ::_thesis: ex v being Element of V st V1 = {v} then consider v being Element of V such that A1: V1 = v + ((0). V) by Def6; take v ; ::_thesis: V1 = {v} thus V1 = {v} by A1, Th46; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V holds the carrier of W is Coset of W let W be Subspace of V; ::_thesis: the carrier of W is Coset of W the carrier of W = (0. V) + W by Lm3; hence the carrier of W is Coset of W by Def6; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: the carrier of V is Coset of (Omega). V set v = the Element of V; the carrier of V c= the carrier of V ; then reconsider A = the carrier of V as Subset of V ; A = the Element of V + ((Omega). V) by Th47; hence the carrier of V is Coset of (Omega). V by Def6; ::_thesis: verum end; 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 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for V1 being Subset of V st V1 is Coset of (Omega). V holds V1 = the carrier of V let V1 be Subset of V; ::_thesis: ( V1 is Coset of (Omega). V implies V1 = the carrier of V ) assume V1 is Coset of (Omega). V ; ::_thesis: V1 = the carrier of V then ex v being Element of V st V1 = v + ((Omega). V) by Def6; hence V1 = the carrier of V by Th47; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of V for C being Coset of W holds ( 0. V in C iff C = the carrier of W ) let W be Subspace of V; ::_thesis: for C being Coset of W holds ( 0. V in C iff C = the carrier of W ) let C be Coset of W; ::_thesis: ( 0. V in C iff C = the carrier of W ) ex v being Element of V st C = v + W by Def6; hence ( 0. V in C iff C = the carrier of W ) by Th48; ::_thesis: verum end; 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 ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) let u be Element of V; ::_thesis: for W being Subspace of V for C being Coset of W holds ( u in C iff C = u + W ) let W be Subspace of V; ::_thesis: for C being Coset of W holds ( u in C iff C = u + W ) let C be Coset of W; ::_thesis: ( u in C iff C = u + W ) thus ( u in C implies C = u + W ) ::_thesis: ( C = u + W implies u in C ) proof assume A1: u in C ; ::_thesis: C = u + W ex v being Element of V st C = v + W by Def6; hence C = u + W by A1, Th55; ::_thesis: verum end; thus ( C = u + W implies u in C ) by Th44; ::_thesis: verum end; 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 & v in C holds ex v1 being Element of V st ( v1 in W & u + v1 = v ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v in C holds ex v1 being Element of V st ( v1 in W & u + v1 = v ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) let u, v be Element of V; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: 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 ) let C be Coset of W; ::_thesis: ( u in C & v in C implies ex v1 being Element of V st ( v1 in W & u + v1 = v ) ) assume ( u in C & v in C ) ; ::_thesis: ex v1 being Element of V st ( v1 in W & u + v1 = v ) then ( C = u + W & C = v + W ) by Th77; hence ex v1 being Element of V st ( v1 in W & u + v1 = v ) by Th64; ::_thesis: verum end; 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 & v in C holds ex v1 being Element of V st ( v1 in W & u - v1 = v ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v in C holds ex v1 being Element of V st ( v1 in W & u - v1 = v ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) let u, v be Element of V; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: 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 ) let C be Coset of W; ::_thesis: ( u in C & v in C implies ex v1 being Element of V st ( v1 in W & u - v1 = v ) ) assume ( u in C & v in C ) ; ::_thesis: ex v1 being Element of V st ( v1 in W & u - v1 = v ) then ( C = u + W & C = v + W ) by Th77; hence ex v1 being Element of V st ( v1 in W & u - v1 = v ) by Th65; ::_thesis: verum end; 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 & v2 in C ) iff v1 - v2 in W ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & v2 in C ) iff v1 - v2 in W ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) let v1, v2 be Element of V; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: ( ex C being Coset of W st ( v1 in C & v2 in C ) iff v1 - v2 in W ) thus ( ex C being Coset of W st ( v1 in C & v2 in C ) implies v1 - v2 in W ) ::_thesis: ( v1 - v2 in W implies ex C being Coset of W st ( v1 in C & v2 in C ) ) proof given C being Coset of W such that A1: ( v1 in C & v2 in C ) ; ::_thesis: v1 - v2 in W ex v being Element of V st C = v + W by Def6; hence v1 - v2 in W by A1, Th63; ::_thesis: verum end; assume v1 - v2 in W ; ::_thesis: ex C being Coset of W st ( v1 in C & v2 in C ) then consider v being Element of V such that A2: ( v1 in v + W & v2 in v + W ) by Th63; reconsider C = v + W as Coset of W by Def6; take C ; ::_thesis: ( v1 in C & v2 in C ) thus ( v1 in C & v2 in C ) by A2; ::_thesis: verum end; 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 & u in C holds B = C proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 & u in C holds B = C let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 let u be Element of V; ::_thesis: for W being Subspace of V for B, C being Coset of W st u in B & u in C holds B = C let W be Subspace of V; ::_thesis: for B, C being Coset of W st u in B & u in C holds B = C let B, C be Coset of W; ::_thesis: ( u in B & u in C implies B = C ) assume A1: ( u in B & u in C ) ; ::_thesis: B = C ( ex v1 being Element of V st B = v1 + W & ex v2 being Element of V st C = v2 + W ) by Def6; hence B = C by A1, Th56; ::_thesis: verum end; 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;