:: RLSUB_1 semantic presentation begin definition let V be RealLinearSpace; let V1 be Subset of V; attrV1 is linearly-closed means :Def1: :: RLSUB_1:def 1 ( ( for v, u being VECTOR of V st v in V1 & u in V1 holds v + u in V1 ) & ( for a being Real for v being VECTOR of V st v in V1 holds a * v in V1 ) ); end; :: deftheorem Def1 defines linearly-closed RLSUB_1:def_1_:_ for V being RealLinearSpace for V1 being Subset of V holds ( V1 is linearly-closed iff ( ( for v, u being VECTOR of V st v in V1 & u in V1 holds v + u in V1 ) & ( for a being Real for v being VECTOR of V st v in V1 holds a * v in V1 ) ) ); theorem Th1: :: RLSUB_1:1 for V being RealLinearSpace for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds 0. V in V1 proof let V be RealLinearSpace; ::_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 * x in V1 by A1, A2, Def1; hence 0. V in V1 by RLVECT_1:10; ::_thesis: verum end; theorem Th2: :: RLSUB_1:2 for V being RealLinearSpace for V1 being Subset of V st V1 is linearly-closed holds for v being VECTOR of V st v in V1 holds - v in V1 proof let V be RealLinearSpace; ::_thesis: for V1 being Subset of V st V1 is linearly-closed holds for v being VECTOR 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 VECTOR of V st v in V1 holds - v in V1 ) assume A1: V1 is linearly-closed ; ::_thesis: for v being VECTOR of V st v in V1 holds - v in V1 let v be VECTOR of V; ::_thesis: ( v in V1 implies - v in V1 ) assume v in V1 ; ::_thesis: - v in V1 then (- 1) * v in V1 by A1, Def1; hence - v in V1 by RLVECT_1:16; ::_thesis: verum end; theorem :: RLSUB_1:3 for V being RealLinearSpace for V1 being Subset of V st V1 is linearly-closed holds for v, u being VECTOR of V st v in V1 & u in V1 holds v - u in V1 proof let V be RealLinearSpace; ::_thesis: for V1 being Subset of V st V1 is linearly-closed holds for v, u being VECTOR 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 VECTOR 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 VECTOR of V st v in V1 & u in V1 holds v - u in V1 let v, u be VECTOR 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: :: RLSUB_1:4 for V being RealLinearSpace holds {(0. V)} is linearly-closed proof let V be RealLinearSpace; ::_thesis: {(0. V)} is linearly-closed thus for v, u being VECTOR of V st v in {(0. V)} & u in {(0. V)} holds v + u in {(0. V)} :: according to RLSUB_1:def_1 ::_thesis: for a being Real for v being VECTOR of V st v in {(0. V)} holds a * v in {(0. V)} proof let v, u be VECTOR 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 Real; ::_thesis: for v being VECTOR of V st v in {(0. V)} holds a * v in {(0. V)} let v be VECTOR 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, RLVECT_1:10; ::_thesis: verum end; theorem :: RLSUB_1:5 for V being RealLinearSpace for V1 being Subset of V st the carrier of V = V1 holds V1 is linearly-closed proof let V be RealLinearSpace; ::_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 VECTOR of V st v in V1 & u in V1 holds v + u in V1 ; :: according to RLSUB_1:def_1 ::_thesis: for a being Real for v being VECTOR of V st v in V1 holds a * v in V1 let a be Real; ::_thesis: for v being VECTOR of V st v in V1 holds a * v in V1 let v be VECTOR 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 :: RLSUB_1:6 for V being RealLinearSpace for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } holds V3 is linearly-closed proof let V be RealLinearSpace; ::_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 VECTOR 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 VECTOR 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 VECTOR of V : ( v in V1 & u in V2 ) } ; ::_thesis: V3 is linearly-closed thus for v, u being VECTOR of V st v in V3 & u in V3 holds v + u in V3 :: according to RLSUB_1:def_1 ::_thesis: for a being Real for v being VECTOR of V st v in V3 holds a * v in V3 proof let v, u be VECTOR 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 VECTOR of V such that A5: v = v1 + v2 and A6: ( v1 in V1 & v2 in V2 ) by A2, A3; consider u1, u2 being VECTOR 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 Real; ::_thesis: for v being VECTOR of V st v in V3 holds a * v in V3 let v be VECTOR 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 VECTOR 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, RLVECT_1:def_5; ( a * v1 in V1 & a * v2 in V2 ) by A1, A11, Def1; hence a * v in V3 by A2, A12; ::_thesis: verum end; theorem :: RLSUB_1:7 for V being RealLinearSpace for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds V1 /\ V2 is linearly-closed proof let V be RealLinearSpace; ::_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 VECTOR of V st v in V1 /\ V2 & u in V1 /\ V2 holds v + u in V1 /\ V2 :: according to RLSUB_1:def_1 ::_thesis: for a being Real for v being VECTOR of V st v in V1 /\ V2 holds a * v in V1 /\ V2 proof let v, u be VECTOR 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 Real; ::_thesis: for v being VECTOR of V st v in V1 /\ V2 holds a * v in V1 /\ V2 let v be VECTOR 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 V be RealLinearSpace; mode Subspace of V -> RealLinearSpace means :Def2: :: RLSUB_1: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 Mult of it = the Mult of V | [:REAL, the carrier of it:] ); existence ex b1 being RealLinearSpace st ( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:REAL, the carrier of b1:] ) proof ( the addF of V = the addF of V || the carrier of V & the Mult of V = the Mult of V | [:REAL, the carrier of V:] ) by RELSET_1:19; hence ex b1 being RealLinearSpace st ( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:REAL, the carrier of b1:] ) ; ::_thesis: verum end; end; :: deftheorem Def2 defines Subspace RLSUB_1:def_2_:_ for V, b2 being RealLinearSpace holds ( b2 is Subspace of V iff ( the carrier of b2 c= the carrier of V & 0. b2 = 0. V & the addF of b2 = the addF of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:REAL, the carrier of b2:] ) ); theorem :: RLSUB_1:8 for V being RealLinearSpace for x being set for W1, W2 being Subspace of V st x in W1 & W1 is Subspace of W2 holds x in W2 proof let V be RealLinearSpace; ::_thesis: for x being set for W1, W2 being Subspace of V st x in W1 & W1 is Subspace of W2 holds x in W2 let x be set ; ::_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: :: RLSUB_1:9 for V being RealLinearSpace for x being set for W being Subspace of V st x in W holds x in V proof let V be RealLinearSpace; ::_thesis: for x being set for W being Subspace of V st x in W holds x in V let x be set ; ::_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: :: RLSUB_1:10 for V being RealLinearSpace for W being Subspace of V for w being VECTOR of W holds w is VECTOR of V proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for w being VECTOR of W holds w is VECTOR of V let W be Subspace of V; ::_thesis: for w being VECTOR of W holds w is VECTOR of V let w be VECTOR of W; ::_thesis: w is VECTOR of V w in V by Th9, RLVECT_1:1; hence w is VECTOR of V by STRUCT_0:def_5; ::_thesis: verum end; theorem :: RLSUB_1:11 for V being RealLinearSpace for W being Subspace of V holds 0. W = 0. V by Def2; theorem :: RLSUB_1:12 for V being RealLinearSpace for W1, W2 being Subspace of V holds 0. W1 = 0. W2 proof let V be RealLinearSpace; ::_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: :: RLSUB_1:13 for V being RealLinearSpace for v, u being VECTOR of V for W being Subspace of V for w1, w2 being VECTOR of W st w1 = v & w2 = u holds w1 + w2 = v + u proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for W being Subspace of V for w1, w2 being VECTOR of W st w1 = v & w2 = u holds w1 + w2 = v + u let v, u be VECTOR of V; ::_thesis: for W being Subspace of V for w1, w2 being VECTOR of W st w1 = v & w2 = u holds w1 + w2 = v + u let W be Subspace of V; ::_thesis: for w1, w2 being VECTOR of W st w1 = v & w2 = u holds w1 + w2 = v + u let w1, w2 be VECTOR 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: :: RLSUB_1:14 for V being RealLinearSpace for v being VECTOR of V for a being Real for W being Subspace of V for w being VECTOR of W st w = v holds a * w = a * v proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for a being Real for W being Subspace of V for w being VECTOR of W st w = v holds a * w = a * v let v be VECTOR of V; ::_thesis: for a being Real for W being Subspace of V for w being VECTOR of W st w = v holds a * w = a * v let a be Real; ::_thesis: for W being Subspace of V for w being VECTOR of W st w = v holds a * w = a * v let W be Subspace of V; ::_thesis: for w being VECTOR of W st w = v holds a * w = a * v let w be VECTOR of W; ::_thesis: ( w = v implies a * w = a * v ) assume A1: w = v ; ::_thesis: a * w = a * v a * w = ( the Mult of V | [:REAL, the carrier of W:]) . [a,w] by Def2; hence a * w = a * v by A1, FUNCT_1:49; ::_thesis: verum end; theorem Th15: :: RLSUB_1:15 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V for w being VECTOR of W st w = v holds - v = - w proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V for w being VECTOR of W st w = v holds - v = - w let v be VECTOR of V; ::_thesis: for W being Subspace of V for w being VECTOR of W st w = v holds - v = - w let W be Subspace of V; ::_thesis: for w being VECTOR of W st w = v holds - v = - w let w be VECTOR of W; ::_thesis: ( w = v implies - v = - w ) A1: ( - v = (- 1) * v & - w = (- 1) * w ) by RLVECT_1:16; assume w = v ; ::_thesis: - v = - w hence - v = - w by A1, Th14; ::_thesis: verum end; theorem Th16: :: RLSUB_1:16 for V being RealLinearSpace for v, u being VECTOR of V for W being Subspace of V for w1, w2 being VECTOR of W st w1 = v & w2 = u holds w1 - w2 = v - u proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for W being Subspace of V for w1, w2 being VECTOR of W st w1 = v & w2 = u holds w1 - w2 = v - u let v, u be VECTOR of V; ::_thesis: for W being Subspace of V for w1, w2 being VECTOR of W st w1 = v & w2 = u holds w1 - w2 = v - u let W be Subspace of V; ::_thesis: for w1, w2 being VECTOR of W st w1 = v & w2 = u holds w1 - w2 = v - u let w1, w2 be VECTOR 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; Lm1: for V being RealLinearSpace for V1 being Subset of V for W being Subspace of V st the carrier of W = V1 holds V1 is linearly-closed proof let V be RealLinearSpace; ::_thesis: for V1 being Subset of V for W being Subspace of V st the carrier of W = V1 holds V1 is linearly-closed let V1 be Subset of V; ::_thesis: for W being Subspace of V st the carrier of W = V1 holds V1 is linearly-closed let W be Subspace of V; ::_thesis: ( the carrier of W = V1 implies V1 is linearly-closed ) set VW = the carrier of W; reconsider WW = W as RealLinearSpace ; assume A1: the carrier of W = V1 ; ::_thesis: V1 is linearly-closed thus for v, u being VECTOR of V st v in V1 & u in V1 holds v + u in V1 :: according to RLSUB_1:def_1 ::_thesis: for a being Real for v being VECTOR of V st v in V1 holds a * v in V1 proof let v, u be VECTOR 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 VECTOR 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 Real; ::_thesis: for v being VECTOR of V st v in V1 holds a * v in V1 let v be VECTOR 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 VECTOR 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: :: RLSUB_1:17 for V being RealLinearSpace for W being Subspace of V holds 0. V in W proof let V be RealLinearSpace; ::_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 :: RLSUB_1:18 for V being RealLinearSpace for W1, W2 being Subspace of V holds 0. W1 in W2 proof let V be RealLinearSpace; ::_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 :: RLSUB_1:19 for V being RealLinearSpace for W being Subspace of V holds 0. W in V by Th9, RLVECT_1:1; theorem Th20: :: RLSUB_1:20 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V st u in W & v in W holds u + v in W proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V for W being Subspace of V st u in W & v in W holds u + v in W let u, v be VECTOR 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 Lm1; 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: :: RLSUB_1:21 for V being RealLinearSpace for v being VECTOR of V for a being Real for W being Subspace of V st v in W holds a * v in W proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for a being Real for W being Subspace of V st v in W holds a * v in W let v be VECTOR of V; ::_thesis: for a being Real for W being Subspace of V st v in W holds a * v in W let a be Real; ::_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 Lm1; 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: :: RLSUB_1:22 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V st v in W holds - v in W proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V st v in W holds - v in W let v be VECTOR 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) * v in W by Th21; hence - v in W by RLVECT_1:16; ::_thesis: verum end; theorem Th23: :: RLSUB_1:23 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V st u in W & v in W holds u - v in W proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V for W being Subspace of V st u in W & v in W holds u - v in W let u, v be VECTOR 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: :: RLSUB_1:24 for V being RealLinearSpace for V1 being Subset of V for D being non empty set for d1 being Element of D for A being BinOp of D for M being Function of [:REAL,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds RLSStruct(# D,d1,A,M #) is Subspace of V proof let V be RealLinearSpace; ::_thesis: for V1 being Subset of V for D being non empty set for d1 being Element of D for A being BinOp of D for M being Function of [:REAL,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds RLSStruct(# D,d1,A,M #) is Subspace of V let V1 be Subset of V; ::_thesis: for D being non empty set for d1 being Element of D for A being BinOp of D for M being Function of [:REAL,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds RLSStruct(# D,d1,A,M #) is Subspace of V let D be non empty set ; ::_thesis: for d1 being Element of D for A being BinOp of D for M being Function of [:REAL,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds RLSStruct(# D,d1,A,M #) is Subspace of V let d1 be Element of D; ::_thesis: for A being BinOp of D for M being Function of [:REAL,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds RLSStruct(# D,d1,A,M #) is Subspace of V let A be BinOp of D; ::_thesis: for M being Function of [:REAL,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds RLSStruct(# D,d1,A,M #) is Subspace of V let M be Function of [:REAL,D:],D; ::_thesis: ( V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] implies RLSStruct(# D,d1,A,M #) is Subspace of V ) assume that A1: V1 = D and A2: d1 = 0. V and A3: A = the addF of V || V1 and A4: M = the Mult of V | [:REAL,V1:] ; ::_thesis: RLSStruct(# D,d1,A,M #) is Subspace of V set W = RLSStruct(# D,d1,A,M #); A5: for a being Real for x being VECTOR of RLSStruct(# D,d1,A,M #) holds a * x = the Mult of V . (a,x) proof let a be Real; ::_thesis: for x being VECTOR of RLSStruct(# D,d1,A,M #) holds a * x = the Mult of V . (a,x) let x be VECTOR of RLSStruct(# D,d1,A,M #); ::_thesis: a * x = the Mult of V . (a,x) thus a * x = the Mult of V . [a,x] by A1, A4, FUNCT_1:49 .= the Mult of V . (a,x) ; ::_thesis: verum end; A6: for x, y being VECTOR of RLSStruct(# D,d1,A,M #) holds x + y = the addF of V . (x,y) proof let x, y be VECTOR of RLSStruct(# D,d1,A,M #); ::_thesis: x + y = the addF of V . (x,y) thus x + y = the addF of V . [x,y] by A1, A3, FUNCT_1:49 .= the addF of V . (x,y) ; ::_thesis: verum end; A7: ( RLSStruct(# D,d1,A,M #) is Abelian & RLSStruct(# D,d1,A,M #) is add-associative & RLSStruct(# D,d1,A,M #) is right_zeroed & RLSStruct(# D,d1,A,M #) is right_complementable & RLSStruct(# D,d1,A,M #) is vector-distributive & RLSStruct(# D,d1,A,M #) is scalar-distributive & RLSStruct(# D,d1,A,M #) is scalar-associative & RLSStruct(# D,d1,A,M #) is scalar-unital ) proof set MV = the Mult of V; set AV = the addF of V; thus RLSStruct(# D,d1,A,M #) is Abelian ::_thesis: ( RLSStruct(# D,d1,A,M #) is add-associative & RLSStruct(# D,d1,A,M #) is right_zeroed & RLSStruct(# D,d1,A,M #) is right_complementable & RLSStruct(# D,d1,A,M #) is vector-distributive & RLSStruct(# D,d1,A,M #) is scalar-distributive & RLSStruct(# D,d1,A,M #) is scalar-associative & RLSStruct(# D,d1,A,M #) is scalar-unital ) proof let x, y be VECTOR of RLSStruct(# D,d1,A,M #); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def_3; thus x + y = x1 + y1 by A6 .= y1 + x1 .= y + x by A6 ; ::_thesis: verum end; thus RLSStruct(# D,d1,A,M #) is add-associative ::_thesis: ( RLSStruct(# D,d1,A,M #) is right_zeroed & RLSStruct(# D,d1,A,M #) is right_complementable & RLSStruct(# D,d1,A,M #) is vector-distributive & RLSStruct(# D,d1,A,M #) is scalar-distributive & RLSStruct(# D,d1,A,M #) is scalar-associative & RLSStruct(# D,d1,A,M #) is scalar-unital ) proof let x, y, z be VECTOR of RLSStruct(# D,d1,A,M #); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z) reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def_3; thus (x + y) + z = the addF of V . ((x + y),z1) by A6 .= (x1 + y1) + z1 by A6 .= x1 + (y1 + z1) by RLVECT_1:def_3 .= the addF of V . (x1,(y + z)) by A6 .= x + (y + z) by A6 ; ::_thesis: verum end; thus RLSStruct(# D,d1,A,M #) is right_zeroed ::_thesis: ( RLSStruct(# D,d1,A,M #) is right_complementable & RLSStruct(# D,d1,A,M #) is vector-distributive & RLSStruct(# D,d1,A,M #) is scalar-distributive & RLSStruct(# D,d1,A,M #) is scalar-associative & RLSStruct(# D,d1,A,M #) is scalar-unital ) proof let x be VECTOR of RLSStruct(# D,d1,A,M #); :: according to RLVECT_1:def_4 ::_thesis: x + (0. RLSStruct(# D,d1,A,M #)) = x reconsider y = x as VECTOR of V by A1, TARSKI:def_3; thus x + (0. RLSStruct(# D,d1,A,M #)) = y + (0. V) by A2, A6 .= x by RLVECT_1:4 ; ::_thesis: verum end; thus RLSStruct(# D,d1,A,M #) is right_complementable ::_thesis: ( RLSStruct(# D,d1,A,M #) is vector-distributive & RLSStruct(# D,d1,A,M #) is scalar-distributive & RLSStruct(# D,d1,A,M #) is scalar-associative & RLSStruct(# D,d1,A,M #) is scalar-unital ) proof let x be VECTOR of RLSStruct(# D,d1,A,M #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable reconsider x1 = x as VECTOR of V by A1, TARSKI:def_3; consider v being VECTOR of V such that A8: x1 + v = 0. V by ALGSTR_0:def_11; v = - x1 by A8, RLVECT_1:def_10 .= (- 1) * x1 by RLVECT_1:16 .= (- 1) * x by A5 ; then reconsider y = v as VECTOR of RLSStruct(# D,d1,A,M #) ; take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. RLSStruct(# D,d1,A,M #) thus x + y = 0. RLSStruct(# D,d1,A,M #) by A2, A6, A8; ::_thesis: verum end; thus for a being real number for x, y being VECTOR of RLSStruct(# D,d1,A,M #) holds a * (x + y) = (a * x) + (a * y) :: according to RLVECT_1:def_5 ::_thesis: ( RLSStruct(# D,d1,A,M #) is scalar-distributive & RLSStruct(# D,d1,A,M #) is scalar-associative & RLSStruct(# D,d1,A,M #) is scalar-unital ) proof let a be real number ; ::_thesis: for x, y being VECTOR of RLSStruct(# D,d1,A,M #) holds a * (x + y) = (a * x) + (a * y) let x, y be VECTOR of RLSStruct(# D,d1,A,M #); ::_thesis: a * (x + y) = (a * x) + (a * y) reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def_3; reconsider a = a as Real by XREAL_0:def_1; a * (x + y) = the Mult of V . (a,(x + y)) by A5 .= a * (x1 + y1) by A6 .= (a * x1) + (a * y1) by RLVECT_1:def_5 .= the addF of V . (( the Mult of V . (a,x1)),(a * y)) by A5 .= the addF of V . ((a * x),(a * y)) by A5 .= (a * x) + (a * y) by A6 ; hence a * (x + y) = (a * x) + (a * y) ; ::_thesis: verum end; thus for a, b being real number for x being VECTOR of RLSStruct(# D,d1,A,M #) holds (a + b) * x = (a * x) + (b * x) :: according to RLVECT_1:def_6 ::_thesis: ( RLSStruct(# D,d1,A,M #) is scalar-associative & RLSStruct(# D,d1,A,M #) is scalar-unital ) proof let a, b be real number ; ::_thesis: for x being VECTOR of RLSStruct(# D,d1,A,M #) holds (a + b) * x = (a * x) + (b * x) let x be VECTOR of RLSStruct(# D,d1,A,M #); ::_thesis: (a + b) * x = (a * x) + (b * x) reconsider y = x as VECTOR of V by A1, TARSKI:def_3; reconsider a = a, b = b as Real by XREAL_0:def_1; (a + b) * x = (a + b) * y by A5 .= (a * y) + (b * y) by RLVECT_1:def_6 .= the addF of V . (( the Mult of V . (a,y)),(b * x)) by A5 .= the addF of V . ((a * x),(b * x)) by A5 .= (a * x) + (b * x) by A6 ; hence (a + b) * x = (a * x) + (b * x) ; ::_thesis: verum end; thus for a, b being real number for x being VECTOR of RLSStruct(# D,d1,A,M #) holds (a * b) * x = a * (b * x) :: according to RLVECT_1:def_7 ::_thesis: RLSStruct(# D,d1,A,M #) is scalar-unital proof let a, b be real number ; ::_thesis: for x being VECTOR of RLSStruct(# D,d1,A,M #) holds (a * b) * x = a * (b * x) let x be VECTOR of RLSStruct(# D,d1,A,M #); ::_thesis: (a * b) * x = a * (b * x) reconsider y = x as VECTOR of V by A1, TARSKI:def_3; reconsider a = a, b = b as Real by XREAL_0:def_1; (a * b) * x = (a * b) * y by A5 .= a * (b * y) by RLVECT_1:def_7 .= the Mult of V . (a,(b * x)) by A5 .= a * (b * x) by A5 ; hence (a * b) * x = a * (b * x) ; ::_thesis: verum end; let x be VECTOR of RLSStruct(# D,d1,A,M #); :: according to RLVECT_1:def_8 ::_thesis: 1 * x = x reconsider y = x as VECTOR of V by A1, TARSKI:def_3; thus 1 * x = 1 * y by A5 .= x by RLVECT_1:def_8 ; ::_thesis: verum end; 0. RLSStruct(# D,d1,A,M #) = 0. V by A2; hence RLSStruct(# D,d1,A,M #) is Subspace of V by A1, A3, A4, A7, Def2; ::_thesis: verum end; theorem Th25: :: RLSUB_1:25 for V being RealLinearSpace holds V is Subspace of V proof let V be RealLinearSpace; ::_thesis: V is Subspace of V thus ( the carrier of V c= the carrier of V & 0. V = 0. V ) ; :: according to RLSUB_1:def_2 ::_thesis: ( the addF of V = the addF of V || the carrier of V & the Mult of V = the Mult of V | [:REAL, the carrier of V:] ) thus ( the addF of V = the addF of V || the carrier of V & the Mult of V = the Mult of V | [:REAL, the carrier of V:] ) by RELSET_1:19; ::_thesis: verum end; theorem Th26: :: RLSUB_1:26 for V, X being strict RealLinearSpace st V is Subspace of X & X is Subspace of V holds V = X proof let V, X be strict RealLinearSpace; ::_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 Mult of X; set MV = the Mult of V; A5: the Mult of X = the Mult of V | [:REAL, the carrier of X:] by A2, Def2; ( 0. V = 0. X & the Mult of V = the Mult of X | [:REAL, the carrier of V:] ) by A1, Def2; hence V = X by A3, A4, A5, RELAT_1:72; ::_thesis: verum end; theorem Th27: :: RLSUB_1:27 for V, X, Y being RealLinearSpace st V is Subspace of X & X is Subspace of Y holds V is Subspace of Y proof let V, X, Y be RealLinearSpace; ::_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; hence the carrier of V c= the carrier of Y by XBOOLE_1:1; :: according to RLSUB_1:def_2 ::_thesis: ( 0. V = 0. Y & the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:REAL, the carrier of V:] ) 0. V = 0. X by A1, Def2; hence 0. V = 0. Y by A2, Def2; ::_thesis: ( the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:REAL, the carrier of V:] ) thus the addF of V = the addF of Y || the carrier of V ::_thesis: the Mult of V = the Mult of Y | [:REAL, 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 A3: [: 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 A3, FUNCT_1:51; ::_thesis: verum end; set MY = the Mult of Y; set MX = the Mult of X; set MV = the Mult 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 A4: [:REAL, the carrier of V:] c= [:REAL, the carrier of X:] by ZFMISC_1:95; the Mult of V = the Mult of X | [:REAL, the carrier of V:] by A1, Def2; then the Mult of V = ( the Mult of Y | [:REAL, the carrier of X:]) | [:REAL, the carrier of V:] by A2, Def2; hence the Mult of V = the Mult of Y | [:REAL, the carrier of V:] by A4, FUNCT_1:51; ::_thesis: verum end; theorem Th28: :: RLSUB_1:28 for V being RealLinearSpace 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 V be RealLinearSpace; ::_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 AV = the addF of V; set MV = the Mult of V; assume A1: the carrier of W1 c= the carrier of W2 ; ::_thesis: W1 is Subspace of W2 then A2: [: the carrier of W1, the carrier of W1:] c= [: the carrier of W2, the carrier of W2:] by ZFMISC_1:96; 0. W1 = 0. V by Def2; hence ( the carrier of W1 c= the carrier of W2 & 0. W1 = 0. W2 ) by A1, Def2; :: according to RLSUB_1:def_2 ::_thesis: ( the addF of W1 = the addF of W2 || the carrier of W1 & the Mult of W1 = the Mult of W2 | [:REAL, the carrier of W1:] ) ( 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; hence the addF of W1 = the addF of W2 || the carrier of W1 by A2, FUNCT_1:51; ::_thesis: the Mult of W1 = the Mult of W2 | [:REAL, the carrier of W1:] A3: [:REAL, the carrier of W1:] c= [:REAL, the carrier of W2:] by A1, ZFMISC_1:95; ( the Mult of W1 = the Mult of V | [:REAL, the carrier of W1:] & the Mult of W2 = the Mult of V | [:REAL, the carrier of W2:] ) by Def2; hence the Mult of W1 = the Mult of W2 | [:REAL, the carrier of W1:] by A3, FUNCT_1:51; ::_thesis: verum end; theorem :: RLSUB_1:29 for V being RealLinearSpace for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds v in W2 ) holds W1 is Subspace of W2 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds v in W2 ) holds W1 is Subspace of W2 let W1, W2 be Subspace of V; ::_thesis: ( ( for v being VECTOR of V st v in W1 holds v in W2 ) implies W1 is Subspace of W2 ) assume A1: for v being VECTOR 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 VECTOR 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 Th28; ::_thesis: verum end; registration let V be RealLinearSpace; cluster non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() for Subspace of V; existence ex b1 being Subspace of V st b1 is strict proof ( the carrier of V is Subset of V iff the carrier of V c= the carrier of V ) ; then reconsider V1 = the carrier of V as Subset of V ; ( the addF of V = the addF of V || V1 & the Mult of V = the Mult of V | [:REAL,V1:] ) by RELSET_1:19; then RLSStruct(# the carrier of V,(0. V), the addF of V, the Mult of V #) is Subspace of V by Th24; hence ex b1 being Subspace of V st b1 is strict ; ::_thesis: verum end; end; theorem Th30: :: RLSUB_1:30 for V being RealLinearSpace for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds W1 = W2 proof let V be RealLinearSpace; ::_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 Th28; hence W1 = W2 by Th26; ::_thesis: verum end; theorem Th31: :: RLSUB_1:31 for V being RealLinearSpace for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds ( v in W1 iff v in W2 ) ) holds W1 = W2 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds ( v in W1 iff v in W2 ) ) holds W1 = W2 let W1, W2 be strict Subspace of V; ::_thesis: ( ( for v being VECTOR of V holds ( v in W1 iff v in W2 ) ) implies W1 = W2 ) assume A1: for v being VECTOR 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 VECTOR 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 VECTOR 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 Th30; ::_thesis: verum end; theorem :: RLSUB_1:32 for V being strict RealLinearSpace for W being strict Subspace of V st the carrier of W = the carrier of V holds W = V proof let V be strict RealLinearSpace; ::_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 Th25; hence W = V by A1, Th30; ::_thesis: verum end; theorem :: RLSUB_1:33 for V being strict RealLinearSpace for W being strict Subspace of V st ( for v being VECTOR of V holds ( v in W iff v in V ) ) holds W = V proof let V be strict RealLinearSpace; ::_thesis: for W being strict Subspace of V st ( for v being VECTOR of V holds ( v in W iff v in V ) ) holds W = V let W be strict Subspace of V; ::_thesis: ( ( for v being VECTOR of V holds ( v in W iff v in V ) ) implies W = V ) assume A1: for v being VECTOR of V holds ( v in W iff v in V ) ; ::_thesis: W = V V is Subspace of V by Th25; hence W = V by A1, Th31; ::_thesis: verum end; theorem :: RLSUB_1:34 for V being RealLinearSpace for V1 being Subset of V for W being Subspace of V st the carrier of W = V1 holds V1 is linearly-closed by Lm1; theorem Th35: :: RLSUB_1:35 for V being RealLinearSpace 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 V be RealLinearSpace; ::_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; set M = the Mult of V | [:REAL,V1:]; set VV = the carrier of V; dom the Mult of V = [:REAL, the carrier of V:] by FUNCT_2:def_1; then A3: dom ( the Mult of V | [:REAL,V1:]) = [:REAL, the carrier of V:] /\ [:REAL,V1:] by RELAT_1:61; [:REAL,V1:] c= [:REAL, the carrier of V:] by ZFMISC_1:95; then A4: dom ( the Mult of V | [:REAL,V1:]) = [:REAL,D:] by A3, XBOOLE_1:28; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_D_implies_ex_x_being_set_st_ (_x_in_dom_(_the_Mult_of_V_|_[:REAL,V1:])_&_y_=_(_the_Mult_of_V_|_[:REAL,V1:])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(_the_Mult_of_V_|_[:REAL,V1:])_&_y_=_(_the_Mult_of_V_|_[:REAL,V1:])_._x_)_implies_y_in_D_)_) let y be set ; ::_thesis: ( ( y in D implies ex x being set st ( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) ) & ( ex x being set st ( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) implies y in D ) ) thus ( y in D implies ex x being set st ( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) ) ::_thesis: ( ex x being set st ( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) implies y in D ) proof assume A5: y in D ; ::_thesis: ex x being set st ( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) then reconsider v1 = y as Element of the carrier of V ; A6: [1,y] in [:REAL,D:] by A5, ZFMISC_1:87; then ( the Mult of V | [:REAL,V1:]) . [1,y] = 1 * v1 by FUNCT_1:49 .= y by RLVECT_1:def_8 ; hence ex x being set st ( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) by A4, A6; ::_thesis: verum end; given x being set such that A7: x in dom ( the Mult of V | [:REAL,V1:]) and A8: y = ( the Mult of V | [:REAL,V1:]) . x ; ::_thesis: y in D consider x1, x2 being set such that A9: x1 in REAL and A10: x2 in D and A11: x = [x1,x2] by A4, A7, ZFMISC_1:def_2; reconsider xx1 = x1 as Real by A9; reconsider v2 = x2 as Element of the carrier of V by A10; [x1,x2] in [:REAL,V1:] by A9, A10, ZFMISC_1:87; then y = xx1 * v2 by A8, A11, FUNCT_1:49; hence y in D by A2, A10, Def1; ::_thesis: verum end; then D = rng ( the Mult of V | [:REAL,V1:]) by FUNCT_1:def_3; then reconsider M = the Mult of V | [:REAL,V1:] as Function of [:REAL,D:],D by A4, FUNCT_2:def_1, RELSET_1:4; set A = the addF of V || V1; reconsider d1 = 0. V as Element of D by A2, Th1; dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1; then dom ( the addF of V || V1) = [: the carrier of V, the carrier of V:] /\ [:V1,V1:] by RELAT_1:61; then A12: dom ( the addF of V || V1) = [:D,D:] by XBOOLE_1:28; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_D_implies_ex_x_being_set_st_ (_x_in_dom_(_the_addF_of_V_||_V1)_&_y_=_(_the_addF_of_V_||_V1)_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(_the_addF_of_V_||_V1)_&_y_=_(_the_addF_of_V_||_V1)_._x_)_implies_y_in_D_)_) let y be set ; ::_thesis: ( ( y in D implies ex x being set st ( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) ) & ( ex x being set st ( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D ) ) thus ( y in D implies ex x being set st ( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) ) ::_thesis: ( ex x being set st ( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D ) proof assume A13: y in D ; ::_thesis: ex x being set st ( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) then reconsider v1 = y, v0 = d1 as Element of the carrier of V ; A14: [d1,y] in [:D,D:] by A13, ZFMISC_1:87; then ( the addF of V || V1) . [d1,y] = v0 + v1 by FUNCT_1:49 .= y by RLVECT_1:4 ; hence ex x being set st ( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) by A12, A14; ::_thesis: verum end; given x being set such that A15: x in dom ( the addF of V || V1) and A16: y = ( the addF of V || V1) . x ; ::_thesis: y in D consider x1, x2 being set such that A17: ( x1 in D & x2 in D ) and A18: x = [x1,x2] by A12, A15, ZFMISC_1:def_2; reconsider v1 = x1, v2 = x2 as Element of the carrier of V by A17; [x1,x2] in [:V1,V1:] by A17, ZFMISC_1:87; then y = v1 + v2 by A16, A18, FUNCT_1:49; hence y in D by A2, A17, Def1; ::_thesis: verum end; then D = rng ( the addF of V || V1) by FUNCT_1:def_3; then reconsider A = the addF of V || V1 as Function of [:D,D:],D by A12, FUNCT_2:def_1, RELSET_1:4; set W = RLSStruct(# D,d1,A,M #); RLSStruct(# D,d1,A,M #) is Subspace of V by Th24; hence ex W being strict Subspace of V st V1 = the carrier of W ; ::_thesis: verum end; definition let V be RealLinearSpace; func (0). V -> strict Subspace of V means :Def3: :: RLSUB_1: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, Th30, Th35; end; :: deftheorem Def3 defines (0). RLSUB_1:def_3_:_ for V being RealLinearSpace for b2 being strict Subspace of V holds ( b2 = (0). V iff the carrier of b2 = {(0. V)} ); definition let V be RealLinearSpace; func (Omega). V -> strict Subspace of V equals :: RLSUB_1:def 4 RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); coherence RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V proof set W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); A1: for u, v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (u + v) + w = u + (v + w) proof let u, v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (u + v) + w = u + (v + w) reconsider u9 = u, v9 = v, w9 = w as VECTOR of V ; thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def_3 .= u + (v + w) ; ::_thesis: verum end; A2: for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v proof let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v reconsider v9 = v as VECTOR of V ; thus v + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v9 + (0. V) .= v by RLVECT_1:4 ; ::_thesis: verum end; A3: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable proof let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable reconsider v9 = v as VECTOR of V ; consider w9 being VECTOR of V such that A4: v9 + w9 = 0. V by ALGSTR_0:def_11; reconsider w = w9 as VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) thus v + w = 0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A4; ::_thesis: verum end; A5: for a being real number for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w) proof let a be real number ; ::_thesis: for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w) let v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: a * (v + w) = (a * v) + (a * w) reconsider v9 = v, w9 = w as VECTOR of V ; thus a * (v + w) = a * (v9 + w9) .= (a * v9) + (a * w9) by RLVECT_1:def_5 .= (a * v) + (a * w) ; ::_thesis: verum end; A6: for a, b being real number for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v) proof let a, b be real number ; ::_thesis: for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v) let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (a * b) * v = a * (b * v) reconsider v9 = v as VECTOR of V ; thus (a * b) * v = (a * b) * v9 .= a * (b * v9) by RLVECT_1:def_7 .= a * (b * v) ; ::_thesis: verum end; A7: for a, b being real number for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v) proof let a, b be real number ; ::_thesis: for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v) let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (a + b) * v = (a * v) + (b * v) reconsider v9 = v as VECTOR of V ; thus (a + b) * v = (a + b) * v9 .= (a * v9) + (b * v9) by RLVECT_1:def_6 .= (a * v) + (b * v) ; ::_thesis: verum end; A8: for a being Real for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) for v9, w9 being VECTOR of V st v = v9 & w = w9 holds ( v + w = v9 + w9 & a * v = a * v9 ) ; A9: for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + w = w + v proof let v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v + w = w + v reconsider v9 = v, w9 = w as VECTOR of V ; thus v + w = w9 + v9 by A8 .= w + v ; ::_thesis: verum end; for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds 1 * v = v proof let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: 1 * v = v reconsider v9 = v as VECTOR of V ; thus 1 * v = 1 * v9 .= v by RLVECT_1:def_8 ; ::_thesis: verum end; then reconsider W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) as RealLinearSpace by A9, A1, A2, A3, A5, A7, A6, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; A10: the Mult of W = the Mult of V | [:REAL, 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 RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V by A10, Def2; ::_thesis: verum end; end; :: deftheorem defines (Omega). RLSUB_1:def_4_:_ for V being RealLinearSpace holds (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); theorem Th36: :: RLSUB_1:36 for V being RealLinearSpace for W being Subspace of V holds (0). W = (0). V proof let V be RealLinearSpace; ::_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 Th27; hence (0). W = (0). V by A1, Th30; ::_thesis: verum end; theorem Th37: :: RLSUB_1:37 for V being RealLinearSpace for W1, W2 being Subspace of V holds (0). W1 = (0). W2 proof let V be RealLinearSpace; ::_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 :: RLSUB_1:38 for V being RealLinearSpace for W being Subspace of V holds (0). W is Subspace of V by Th27; theorem :: RLSUB_1:39 for V being RealLinearSpace for W being Subspace of V holds (0). V is Subspace of W proof let V be RealLinearSpace; ::_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 the carrier of ((0). V) = {(0. V)} by Def3 .= {(0. W)} by Def2 ; hence (0). V is Subspace of W by Th28; ::_thesis: verum end; theorem :: RLSUB_1:40 for V being RealLinearSpace for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2 proof let V be RealLinearSpace; ::_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 :: RLSUB_1:41 for V being strict RealLinearSpace holds V is Subspace of (Omega). V ; definition let V be RealLinearSpace; let v be VECTOR of V; let W be Subspace of V; funcv + W -> Subset of V equals :: RLSUB_1:def 5 { (v + u) where u is VECTOR of V : u in W } ; coherence { (v + u) where u is VECTOR of V : u in W } is Subset of V proof set Y = { (v + u) where u is VECTOR of V : u in W } ; defpred S1[ set ] means ex u being VECTOR 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 VECTOR 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 VECTOR of V : u in W } or x in X ) assume x in { (v + u) where u is VECTOR of V : u in W } ; ::_thesis: x in X then ex u being VECTOR 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 VECTOR 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 VECTOR of V : u in W } ) assume x in X ; ::_thesis: x in { (v + u) where u is VECTOR of V : u in W } then ex u being VECTOR of V st ( x = v + u & u in W ) by A1; hence x in { (v + u) where u is VECTOR of V : u in W } ; ::_thesis: verum end; hence { (v + u) where u is VECTOR of V : u in W } is Subset of V by A2, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem defines + RLSUB_1:def_5_:_ for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ; Lm2: for V being RealLinearSpace for W being Subspace of V holds (0. V) + W = the carrier of W proof let V be RealLinearSpace; ::_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 VECTOR of V : u in W } ; A1: the carrier of W c= { ((0. V) + u) where u is VECTOR 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 VECTOR of V : u in W } ) assume x in the carrier of W ; ::_thesis: x in { ((0. V) + u) where u is VECTOR 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 VECTOR of V : u in W } by A2; ::_thesis: verum end; { ((0. V) + u) where u is VECTOR 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 VECTOR of V : u in W } or x in the carrier of W ) assume x in { ((0. V) + u) where u is VECTOR of V : u in W } ; ::_thesis: x in the carrier of W then consider u being VECTOR 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 V be RealLinearSpace; let W be Subspace of V; mode Coset of W -> Subset of V means :Def6: :: RLSUB_1:def 6 ex v being VECTOR of V st it = v + W; existence ex b1 being Subset of V ex v being VECTOR of V st b1 = v + W proof reconsider VW = the carrier of W as Subset of V by Def2; take VW ; ::_thesis: ex v being VECTOR of V st VW = v + W take 0. V ; ::_thesis: VW = (0. V) + W thus VW = (0. V) + W by Lm2; ::_thesis: verum end; end; :: deftheorem Def6 defines Coset RLSUB_1:def_6_:_ for V being RealLinearSpace for W being Subspace of V for b3 being Subset of V holds ( b3 is Coset of W iff ex v being VECTOR of V st b3 = v + W ); theorem Th42: :: RLSUB_1:42 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds ( 0. V in v + W iff v in W ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V holds ( 0. V in v + W iff v in W ) let v be VECTOR 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 VECTOR of V such that A1: 0. V = v + u and A2: u in W ; v = - u by A1, RLVECT_1:def_10; 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 RLVECT_1:15 .= v + (- v) ; hence 0. V in v + W by A3; ::_thesis: verum end; theorem Th43: :: RLSUB_1:43 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds v in v + W proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V holds v in v + W let v be VECTOR 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 :: RLSUB_1:44 for V being RealLinearSpace for W being Subspace of V holds (0. V) + W = the carrier of W by Lm2; theorem Th45: :: RLSUB_1:45 for V being RealLinearSpace for v being VECTOR of V holds v + ((0). V) = {v} proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds v + ((0). V) = {v} let v be VECTOR 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 VECTOR 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; Lm3: for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds ( v in W iff v + W = the carrier of W ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V holds ( v in W iff v + W = the carrier of W ) let v be VECTOR 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 VECTOR 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 VECTOR 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 VECTOR of V by Th10; A5: z + (y - z) = (y + z) - z by RLVECT_1:def_3 .= y + (z - z) by RLVECT_1:def_3 .= y + (0. W) by RLVECT_1:15 .= 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 Th46: :: RLSUB_1:46 for V being RealLinearSpace for v being VECTOR of V holds v + ((Omega). V) = the carrier of V proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds v + ((Omega). V) = the carrier of V let v be VECTOR of V; ::_thesis: v + ((Omega). V) = the carrier of V v in (Omega). V by STRUCT_0:def_5; hence v + ((Omega). V) = the carrier of V by Lm3; ::_thesis: verum end; theorem Th47: :: RLSUB_1:47 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds ( 0. V in v + W iff v + W = the carrier of W ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V holds ( 0. V in v + W iff v + W = the carrier of W ) let v be VECTOR 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 Th42; hence ( 0. V in v + W iff v + W = the carrier of W ) by Lm3; ::_thesis: verum end; theorem :: RLSUB_1:48 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds ( v in W iff v + W = the carrier of W ) by Lm3; theorem Th49: :: RLSUB_1:49 for V being RealLinearSpace for v being VECTOR of V for a being Real for W being Subspace of V st v in W holds (a * v) + W = the carrier of W proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for a being Real for W being Subspace of V st v in W holds (a * v) + W = the carrier of W let v be VECTOR of V; ::_thesis: for a being Real for W being Subspace of V st v in W holds (a * v) + W = the carrier of W let a be Real; ::_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 A1: v in W ; ::_thesis: (a * v) + W = the carrier of W thus (a * v) + W c= the carrier of W :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W c= (a * v) + W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (a * v) + W or x in the carrier of W ) assume x in (a * v) + W ; ::_thesis: x in the carrier of W then consider u being VECTOR of V such that A2: x = (a * v) + u and A3: u in W ; a * v in W by A1, Th21; then (a * v) + u in W by A3, Th20; hence x in the carrier of W by A2, 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 (a * v) + W ) assume A4: x in the carrier of W ; ::_thesis: x in (a * v) + W then A5: x in W by STRUCT_0:def_5; the carrier of W c= the carrier of V by Def2; then reconsider y = x as Element of V by A4; A6: (a * v) + (y - (a * v)) = (y + (a * v)) - (a * v) by RLVECT_1:def_3 .= y + ((a * v) - (a * v)) by RLVECT_1:def_3 .= y + (0. V) by RLVECT_1:15 .= x by RLVECT_1:4 ; a * v in W by A1, Th21; then y - (a * v) in W by A5, Th23; hence x in (a * v) + W by A6; ::_thesis: verum end; theorem Th50: :: RLSUB_1:50 for V being RealLinearSpace for v being VECTOR of V for a being Real for W being Subspace of V st a <> 0 & (a * v) + W = the carrier of W holds v in W proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for a being Real for W being Subspace of V st a <> 0 & (a * v) + W = the carrier of W holds v in W let v be VECTOR of V; ::_thesis: for a being Real for W being Subspace of V st a <> 0 & (a * v) + W = the carrier of W holds v in W let a be Real; ::_thesis: for W being Subspace of V st a <> 0 & (a * v) + W = the carrier of W holds v in W let W be Subspace of V; ::_thesis: ( a <> 0 & (a * v) + W = the carrier of W implies v in W ) assume that A1: a <> 0 and A2: (a * v) + W = the carrier of W ; ::_thesis: v in W assume not v in W ; ::_thesis: contradiction then not 1 * v in W by RLVECT_1:def_8; then not ((a ") * a) * v in W by A1, XCMPLX_0:def_7; then not (a ") * (a * v) in W by RLVECT_1:def_7; 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 Th51: :: RLSUB_1:51 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds ( v in W iff (- v) + W = the carrier of W ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V holds ( v in W iff (- v) + W = the carrier of W ) let v be VECTOR 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 ) ( v in W iff ((- 1) * v) + W = the carrier of W ) by Th49, Th50; hence ( v in W iff (- v) + W = the carrier of W ) by RLVECT_1:16; ::_thesis: verum end; theorem Th52: :: RLSUB_1:52 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V holds ( u in W iff v + W = (v + u) + W ) proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V for W being Subspace of V holds ( u in W iff v + W = (v + u) + W ) let u, v be VECTOR 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 VECTOR 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 RLVECT_1:15 .= 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 VECTOR 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 VECTOR of V such that A9: v = (v + u) + u1 and A10: u1 in W ; ( v = v + (0. V) & v = v + (u + u1) ) by A9, RLVECT_1:4, RLVECT_1:def_3; then u + u1 = 0. V by RLVECT_1:8; then u = - u1 by RLVECT_1:def_10; hence u in W by A10, Th22; ::_thesis: verum end; theorem :: RLSUB_1:53 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V holds ( u in W iff v + W = (v - u) + W ) proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V for W being Subspace of V holds ( u in W iff v + W = (v - u) + W ) let u, v be VECTOR 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 Th52; hence ( u in W iff v + W = (v - u) + W ) by A1, Th22; ::_thesis: verum end; theorem Th54: :: RLSUB_1:54 for V being RealLinearSpace for v, u being VECTOR of V for W being Subspace of V holds ( v in u + W iff u + W = v + W ) proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for W being Subspace of V holds ( v in u + W iff u + W = v + W ) let v, u be VECTOR 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 VECTOR 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 VECTOR 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 RLVECT_1:15 .= 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 VECTOR 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 Th43; ::_thesis: verum end; theorem Th55: :: RLSUB_1:55 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds ( v + W = (- v) + W iff v in W ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V holds ( v + W = (- v) + W iff v in W ) let v be VECTOR of V; ::_thesis: for W being Subspace of V holds ( v + W = (- v) + W iff v in W ) let W be Subspace of V; ::_thesis: ( v + W = (- v) + W iff v in W ) thus ( v + W = (- v) + W implies v in W ) ::_thesis: ( v in W implies v + W = (- v) + W ) proof assume v + W = (- v) + W ; ::_thesis: v in W then v in (- v) + W by Th43; then consider u being VECTOR of V such that A1: v = (- v) + u and A2: u in W ; 0. V = v - ((- v) + u) by A1, RLVECT_1:15 .= (v - (- v)) - u by RLVECT_1:27 .= (v + v) - u by RLVECT_1:17 .= ((1 * v) + v) - u by RLVECT_1:def_8 .= ((1 * v) + (1 * v)) - u by RLVECT_1:def_8 .= ((1 + 1) * v) - u by RLVECT_1:def_6 .= (2 * v) - u ; then (2 ") * (2 * v) = (2 ") * u by RLVECT_1:21; then ((2 ") * 2) * v = (2 ") * u by RLVECT_1:def_7; then v = (2 ") * u by RLVECT_1:def_8; hence v in W by A2, Th21; ::_thesis: verum end; assume A3: v in W ; ::_thesis: v + W = (- v) + W then v + W = the carrier of W by Lm3; hence v + W = (- v) + W by A3, Th51; ::_thesis: verum end; theorem Th56: :: RLSUB_1:56 for V being RealLinearSpace for u, v1, v2 being VECTOR of V for W being Subspace of V st u in v1 + W & u in v2 + W holds v1 + W = v2 + W proof let V be RealLinearSpace; ::_thesis: for u, v1, v2 being VECTOR 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 VECTOR 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 consider x1 being VECTOR of V such that A3: u = v1 + x1 and A4: x1 in W by A1; consider x2 being VECTOR of V such that A5: u = v2 + x2 and A6: x2 in W by A2; thus v1 + W c= v2 + W :: according to XBOOLE_0:def_10 ::_thesis: v2 + W c= v1 + W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v1 + W or x in v2 + W ) assume x in v1 + W ; ::_thesis: x in v2 + W then consider u1 being VECTOR of V such that A7: x = v1 + u1 and A8: u1 in W ; x2 - x1 in W by A4, A6, Th23; then A9: (x2 - x1) + u1 in W by A8, Th20; u - x1 = v1 + (x1 - x1) by A3, RLVECT_1:def_3 .= v1 + (0. V) by RLVECT_1:15 .= v1 by RLVECT_1:4 ; then x = (v2 + (x2 - x1)) + u1 by A5, A7, RLVECT_1:def_3 .= v2 + ((x2 - x1) + u1) by RLVECT_1:def_3 ; hence x in v2 + W by A9; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v2 + W or x in v1 + W ) assume x in v2 + W ; ::_thesis: x in v1 + W then consider u1 being VECTOR of V such that A10: x = v2 + u1 and A11: u1 in W ; x1 - x2 in W by A4, A6, Th23; then A12: (x1 - x2) + u1 in W by A11, Th20; u - x2 = v2 + (x2 - x2) by A5, RLVECT_1:def_3 .= v2 + (0. V) by RLVECT_1:15 .= v2 by RLVECT_1:4 ; then x = (v1 + (x1 - x2)) + u1 by A3, A10, RLVECT_1:def_3 .= v1 + ((x1 - x2) + u1) by RLVECT_1:def_3 ; hence x in v1 + W by A12; ::_thesis: verum end; theorem :: RLSUB_1:57 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V st u in v + W & u in (- v) + W holds v in W proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V for W being Subspace of V st u in v + W & u in (- v) + W holds v in W let u, v be VECTOR of V; ::_thesis: for W being Subspace of V st u in v + W & u in (- v) + W holds v in W let W be Subspace of V; ::_thesis: ( u in v + W & u in (- v) + W implies v in W ) assume ( u in v + W & u in (- v) + W ) ; ::_thesis: v in W then v + W = (- v) + W by Th56; hence v in W by Th55; ::_thesis: verum end; theorem Th58: :: RLSUB_1:58 for V being RealLinearSpace for v being VECTOR of V for a being Real for W being Subspace of V st a <> 1 & a * v in v + W holds v in W proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for a being Real for W being Subspace of V st a <> 1 & a * v in v + W holds v in W let v be VECTOR of V; ::_thesis: for a being Real for W being Subspace of V st a <> 1 & a * v in v + W holds v in W let a be Real; ::_thesis: for W being Subspace of V st a <> 1 & a * v in v + W holds v in W let W be Subspace of V; ::_thesis: ( a <> 1 & a * v in v + W implies v in W ) assume that A1: a <> 1 and A2: a * v in v + W ; ::_thesis: v in W A3: a - 1 <> 0 by A1; consider u being VECTOR 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 RLVECT_1:15 .= (a * v) - v by A4, RLVECT_1:def_3 .= (a * v) - (1 * v) by RLVECT_1:def_8 .= (a - 1) * v by RLVECT_1:35 ; then ((a - 1) ") * u = (((a - 1) ") * (a - 1)) * v by RLVECT_1:def_7; then 1 * v = ((a - 1) ") * u by A3, XCMPLX_0:def_7; then v = ((a - 1) ") * u by RLVECT_1:def_8; hence v in W by A5, Th21; ::_thesis: verum end; theorem Th59: :: RLSUB_1:59 for V being RealLinearSpace for v being VECTOR of V for a being Real for W being Subspace of V st v in W holds a * v in v + W proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for a being Real for W being Subspace of V st v in W holds a * v in v + W let v be VECTOR of V; ::_thesis: for a being Real for W being Subspace of V st v in W holds a * v in v + W let a be Real; ::_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 A1: (a - 1) * v in W by Th21; a * v = ((a - 1) + 1) * v .= ((a - 1) * v) + (1 * v) by RLVECT_1:def_6 .= v + ((a - 1) * v) by RLVECT_1:def_8 ; hence a * v in v + W by A1; ::_thesis: verum end; theorem :: RLSUB_1:60 for V being RealLinearSpace for v being VECTOR of V for W being Subspace of V holds ( - v in v + W iff v in W ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W being Subspace of V holds ( - v in v + W iff v in W ) let v be VECTOR of V; ::_thesis: for W being Subspace of V holds ( - v in v + W iff v in W ) let W be Subspace of V; ::_thesis: ( - v in v + W iff v in W ) (- 1) * v = - v by RLVECT_1:16; hence ( - v in v + W iff v in W ) by Th58, Th59; ::_thesis: verum end; theorem Th61: :: RLSUB_1:61 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V holds ( u + v in v + W iff u in W ) proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V for W being Subspace of V holds ( u + v in v + W iff u in W ) let u, v be VECTOR 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 VECTOR 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 :: RLSUB_1:62 for V being RealLinearSpace for v, u being VECTOR of V for W being Subspace of V holds ( v - u in v + W iff u in W ) proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for W being Subspace of V holds ( v - u in v + W iff u in W ) let v, u be VECTOR 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, Th61, RLVECT_1:17; ::_thesis: verum end; theorem Th63: :: RLSUB_1:63 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V holds ( u in v + W iff ex v1 being VECTOR of V st ( v1 in W & u = v + v1 ) ) proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V for W being Subspace of V holds ( u in v + W iff ex v1 being VECTOR of V st ( v1 in W & u = v + v1 ) ) let u, v be VECTOR of V; ::_thesis: for W being Subspace of V holds ( u in v + W iff ex v1 being VECTOR of V st ( v1 in W & u = v + v1 ) ) let W be Subspace of V; ::_thesis: ( u in v + W iff ex v1 being VECTOR of V st ( v1 in W & u = v + v1 ) ) thus ( u in v + W implies ex v1 being VECTOR of V st ( v1 in W & u = v + v1 ) ) ::_thesis: ( ex v1 being VECTOR of V st ( v1 in W & u = v + v1 ) implies u in v + W ) proof assume u in v + W ; ::_thesis: ex v1 being VECTOR of V st ( v1 in W & u = v + v1 ) then ex v1 being VECTOR of V st ( u = v + v1 & v1 in W ) ; hence ex v1 being VECTOR of V st ( v1 in W & u = v + v1 ) ; ::_thesis: verum end; given v1 being VECTOR of V such that A1: ( v1 in W & u = v + v1 ) ; ::_thesis: u in v + W thus u in v + W by A1; ::_thesis: verum end; theorem :: RLSUB_1:64 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V holds ( u in v + W iff ex v1 being VECTOR of V st ( v1 in W & u = v - v1 ) ) proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V for W being Subspace of V holds ( u in v + W iff ex v1 being VECTOR of V st ( v1 in W & u = v - v1 ) ) let u, v be VECTOR of V; ::_thesis: for W being Subspace of V holds ( u in v + W iff ex v1 being VECTOR of V st ( v1 in W & u = v - v1 ) ) let W be Subspace of V; ::_thesis: ( u in v + W iff ex v1 being VECTOR of V st ( v1 in W & u = v - v1 ) ) thus ( u in v + W implies ex v1 being VECTOR of V st ( v1 in W & u = v - v1 ) ) ::_thesis: ( ex v1 being VECTOR of V st ( v1 in W & u = v - v1 ) implies u in v + W ) proof assume u in v + W ; ::_thesis: ex v1 being VECTOR of V st ( v1 in W & u = v - v1 ) then consider v1 being VECTOR 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 VECTOR 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 Th65: :: RLSUB_1:65 for V being RealLinearSpace for v1, v2 being VECTOR of V for W being Subspace of V holds ( ex v being VECTOR of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) proof let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V for W being Subspace of V holds ( ex v being VECTOR of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) let v1, v2 be VECTOR of V; ::_thesis: for W being Subspace of V holds ( ex v being VECTOR 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 VECTOR of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) thus ( ex v being VECTOR 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 VECTOR of V st ( v1 in v + W & v2 in v + W ) ) proof given v being VECTOR of V such that A1: v1 in v + W and A2: v2 in v + W ; ::_thesis: v1 - v2 in W consider u2 being VECTOR of V such that A3: u2 in W and A4: v2 = v + u2 by A2, Th63; consider u1 being VECTOR of V such that A5: u1 in W and A6: v1 = v + u1 by A1, Th63; v1 - v2 = (u1 + v) + ((- v) - u2) by A6, A4, RLVECT_1:30 .= ((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 VECTOR 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 Th43; ::_thesis: v2 in v1 + W v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by RLVECT_1:33 .= (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 Th66: :: RLSUB_1:66 for V being RealLinearSpace for v, u being VECTOR of V for W being Subspace of V st v + W = u + W holds ex v1 being VECTOR of V st ( v1 in W & v + v1 = u ) proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for W being Subspace of V st v + W = u + W holds ex v1 being VECTOR of V st ( v1 in W & v + v1 = u ) let v, u be VECTOR of V; ::_thesis: for W being Subspace of V st v + W = u + W holds ex v1 being VECTOR of V st ( v1 in W & v + v1 = u ) let W be Subspace of V; ::_thesis: ( v + W = u + W implies ex v1 being VECTOR of V st ( v1 in W & v + v1 = u ) ) assume v + W = u + W ; ::_thesis: ex v1 being VECTOR of V st ( v1 in W & v + v1 = u ) then v in u + W by Th43; then consider u1 being VECTOR 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, RLVECT_1:15 .= u1 + (u - v) by RLVECT_1:def_3 ; then v1 = - u1 by RLVECT_1:def_10; 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 RLVECT_1:15 .= u by RLVECT_1:4 ; ::_thesis: verum end; theorem Th67: :: RLSUB_1:67 for V being RealLinearSpace for v, u being VECTOR of V for W being Subspace of V st v + W = u + W holds ex v1 being VECTOR of V st ( v1 in W & v - v1 = u ) proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for W being Subspace of V st v + W = u + W holds ex v1 being VECTOR of V st ( v1 in W & v - v1 = u ) let v, u be VECTOR of V; ::_thesis: for W being Subspace of V st v + W = u + W holds ex v1 being VECTOR of V st ( v1 in W & v - v1 = u ) let W be Subspace of V; ::_thesis: ( v + W = u + W implies ex v1 being VECTOR of V st ( v1 in W & v - v1 = u ) ) assume v + W = u + W ; ::_thesis: ex v1 being VECTOR of V st ( v1 in W & v - v1 = u ) then u in v + W by Th43; then consider u1 being VECTOR 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, RLVECT_1:15 .= u1 + (v - u) by RLVECT_1:def_3 ; then v1 = - u1 by RLVECT_1:def_10; 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 RLVECT_1:15 .= u by RLVECT_1:4 ; ::_thesis: verum end; theorem Th68: :: RLSUB_1:68 for V being RealLinearSpace for v being VECTOR of V for W1, W2 being strict Subspace of V holds ( v + W1 = v + W2 iff W1 = W2 ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for W1, W2 being strict Subspace of V holds ( v + W1 = v + W2 iff W1 = W2 ) let v be VECTOR 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 VECTOR 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 VECTOR 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 Th30; ::_thesis: verum end; thus ( W1 = W2 implies v + W1 = v + W2 ) ; ::_thesis: verum end; theorem Th69: :: RLSUB_1:69 for V being RealLinearSpace for v, u being VECTOR of V for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds W1 = W2 proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds W1 = W2 let v, u be VECTOR 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 VECTOR 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 RLVECT_1:15 .= (- v) + (u + u1) by A5, RLVECT_1:def_3 ; then A7: (v + ((- v) + (u + u1))) + W1 = v + W1 by A4, Th52; v + ((- v) + (u + u1)) = (v - v) + (u + u1) by RLVECT_1:def_3 .= (0. V) + (u + u1) by RLVECT_1:15 .= u + u1 by RLVECT_1:4 ; then (u + u1) + W2 = (u + u1) + W1 by A1, A6, A7, Th52; hence contradiction by A2, Th68; ::_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 VECTOR 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 RLVECT_1:15 .= (- u) + (v + u1) by A10, RLVECT_1:def_3 ; then A12: (u + ((- u) + (v + u1))) + W2 = u + W2 by A9, Th52; u + ((- u) + (v + u1)) = (u - u) + (v + u1) by RLVECT_1:def_3 .= (0. V) + (v + u1) by RLVECT_1:15 .= v + u1 by RLVECT_1:4 ; then (v + u1) + W1 = (v + u1) + W2 by A1, A11, A12, Th52; hence contradiction by A2, Th68; ::_thesis: verum end; the carrier of W1 <> the carrier of W2 by A2, Th30; 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 :: RLSUB_1:70 for V being RealLinearSpace 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 V be RealLinearSpace; ::_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 VECTOR of V such that A2: C = v + W by Def6; C <> {} by A2, Th43; then 0. V in v + W by A1, A2, Th1; hence C = the carrier of W by A2, Th47; ::_thesis: verum end; thus ( C = the carrier of W implies C is linearly-closed ) by Lm1; ::_thesis: verum end; theorem :: RLSUB_1:71 for V being RealLinearSpace 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 V be RealLinearSpace; ::_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 VECTOR of V st C1 = v1 + W1 & ex v2 being VECTOR of V st C2 = v2 + W2 ) by Def6; hence ( C1 = C2 implies W1 = W2 ) by Th69; ::_thesis: verum end; theorem :: RLSUB_1:72 for V being RealLinearSpace for v being VECTOR of V holds {v} is Coset of (0). V proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds {v} is Coset of (0). V let v be VECTOR of V; ::_thesis: {v} is Coset of (0). V v + ((0). V) = {v} by Th45; hence {v} is Coset of (0). V by Def6; ::_thesis: verum end; theorem :: RLSUB_1:73 for V being RealLinearSpace for V1 being Subset of V st V1 is Coset of (0). V holds ex v being VECTOR of V st V1 = {v} proof let V be RealLinearSpace; ::_thesis: for V1 being Subset of V st V1 is Coset of (0). V holds ex v being VECTOR of V st V1 = {v} let V1 be Subset of V; ::_thesis: ( V1 is Coset of (0). V implies ex v being VECTOR of V st V1 = {v} ) assume V1 is Coset of (0). V ; ::_thesis: ex v being VECTOR of V st V1 = {v} then consider v being VECTOR of V such that A1: V1 = v + ((0). V) by Def6; take v ; ::_thesis: V1 = {v} thus V1 = {v} by A1, Th45; ::_thesis: verum end; theorem :: RLSUB_1:74 for V being RealLinearSpace for W being Subspace of V holds the carrier of W is Coset of W proof let V be RealLinearSpace; ::_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 Lm2; hence the carrier of W is Coset of W by Def6; ::_thesis: verum end; theorem :: RLSUB_1:75 for V being RealLinearSpace holds the carrier of V is Coset of (Omega). V proof let V be RealLinearSpace; ::_thesis: the carrier of V is Coset of (Omega). V set v = the VECTOR of V; ( the carrier of V is Subset of V iff the carrier of V c= the carrier of V ) ; then reconsider A = the carrier of V as Subset of V ; A = the VECTOR of V + ((Omega). V) by Th46; hence the carrier of V is Coset of (Omega). V by Def6; ::_thesis: verum end; theorem :: RLSUB_1:76 for V being RealLinearSpace for V1 being Subset of V st V1 is Coset of (Omega). V holds V1 = the carrier of V proof let V be RealLinearSpace; ::_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 VECTOR of V st V1 = v + ((Omega). V) by Def6; hence V1 = the carrier of V by Th46; ::_thesis: verum end; theorem :: RLSUB_1:77 for V being RealLinearSpace 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 V be RealLinearSpace; ::_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 VECTOR of V st C = v + W by Def6; hence ( 0. V in C iff C = the carrier of W ) by Th47; ::_thesis: verum end; theorem Th78: :: RLSUB_1:78 for V being RealLinearSpace for u being VECTOR of V for W being Subspace of V for C being Coset of W holds ( u in C iff C = u + W ) proof let V be RealLinearSpace; ::_thesis: for u being VECTOR 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 VECTOR 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 VECTOR of V st C = v + W by Def6; hence C = u + W by A1, Th54; ::_thesis: verum end; thus ( C = u + W implies u in C ) by Th43; ::_thesis: verum end; theorem :: RLSUB_1:79 for V being RealLinearSpace for u, v being VECTOR 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 VECTOR of V st ( v1 in W & u + v1 = v ) proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR 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 VECTOR of V st ( v1 in W & u + v1 = v ) let u, v be VECTOR 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 VECTOR 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 VECTOR 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 VECTOR of V st ( v1 in W & u + v1 = v ) ) assume ( u in C & v in C ) ; ::_thesis: ex v1 being VECTOR of V st ( v1 in W & u + v1 = v ) then ( C = u + W & C = v + W ) by Th78; hence ex v1 being VECTOR of V st ( v1 in W & u + v1 = v ) by Th66; ::_thesis: verum end; theorem :: RLSUB_1:80 for V being RealLinearSpace for u, v being VECTOR 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 VECTOR of V st ( v1 in W & u - v1 = v ) proof let V be RealLinearSpace; ::_thesis: for u, v being VECTOR 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 VECTOR of V st ( v1 in W & u - v1 = v ) let u, v be VECTOR 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 VECTOR 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 VECTOR 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 VECTOR of V st ( v1 in W & u - v1 = v ) ) assume ( u in C & v in C ) ; ::_thesis: ex v1 being VECTOR of V st ( v1 in W & u - v1 = v ) then ( C = u + W & C = v + W ) by Th78; hence ex v1 being VECTOR of V st ( v1 in W & u - v1 = v ) by Th67; ::_thesis: verum end; theorem :: RLSUB_1:81 for V being RealLinearSpace for v1, v2 being VECTOR 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 V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR 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 VECTOR 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 VECTOR of V st C = v + W by Def6; hence v1 - v2 in W by A1, Th65; ::_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 VECTOR of V such that A2: ( v1 in v + W & v2 in v + W ) by Th65; 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 :: RLSUB_1:82 for V being RealLinearSpace for u being VECTOR 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 V be RealLinearSpace; ::_thesis: for u being VECTOR 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 VECTOR 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 VECTOR of V st B = v1 + W & ex v2 being VECTOR of V st C = v2 + W ) by Def6; hence B = C by A1, Th56; ::_thesis: verum end;