:: RLSUB_2 semantic presentation begin definition let V be RealLinearSpace; let W1, W2 be Subspace of V; funcW1 + W2 -> strict Subspace of V means :Def1: :: RLSUB_2:def 1 the carrier of it = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; existence ex b1 being strict Subspace of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } proof reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V by RLSUB_1:def_2; set VS = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } or x in the carrier of V ) assume x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; ::_thesis: x in the carrier of V then ex v1, v2 being VECTOR of V st ( x = v1 + v2 & v1 in W1 & v2 in W2 ) ; hence x in the carrier of V ; ::_thesis: verum end; then reconsider VS = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } as Subset of V ; A1: 0. V = (0. V) + (0. V) by RLVECT_1:4; ( 0. V in W1 & 0. V in W2 ) by RLSUB_1:17; then A2: 0. V in VS by A1; A3: VS = { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } proof thus VS c= { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } c= VS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in VS or x in { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } ) assume x in VS ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } then consider v, u being VECTOR of V such that A4: x = v + u and A5: ( v in W1 & u in W2 ) ; ( v in V1 & u in V2 ) by A5, STRUCT_0:def_5; hence x in { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } or x in VS ) assume x in { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } ; ::_thesis: x in VS then consider v, u being VECTOR of V such that A6: x = v + u and A7: ( v in V1 & u in V2 ) ; ( v in W1 & u in W2 ) by A7, STRUCT_0:def_5; hence x in VS by A6; ::_thesis: verum end; ( V1 is linearly-closed & V2 is linearly-closed ) by RLSUB_1:34; hence ex b1 being strict Subspace of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by A2, A3, RLSUB_1:6, RLSUB_1:35; ::_thesis: verum end; uniqueness for b1, b2 being strict Subspace of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } & the carrier of b2 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } holds b1 = b2 by RLSUB_1:30; end; :: deftheorem Def1 defines + RLSUB_2:def_1_:_ for V being RealLinearSpace for W1, W2 being Subspace of V for b4 being strict Subspace of V holds ( b4 = W1 + W2 iff the carrier of b4 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ); definition let V be RealLinearSpace; let W1, W2 be Subspace of V; funcW1 /\ W2 -> strict Subspace of V means :Def2: :: RLSUB_2:def 2 the carrier of it = the carrier of W1 /\ the carrier of W2; existence ex b1 being strict Subspace of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 proof set VW2 = the carrier of W2; set VW1 = the carrier of W1; set VV = the carrier of V; 0. V in W2 by RLSUB_1:17; then A1: 0. V in the carrier of W2 by STRUCT_0:def_5; ( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RLSUB_1:def_2; then the carrier of W1 /\ the carrier of W2 c= the carrier of V /\ the carrier of V by XBOOLE_1:27; then reconsider V1 = the carrier of W1, V2 = the carrier of W2, V3 = the carrier of W1 /\ the carrier of W2 as Subset of the carrier of V by RLSUB_1:def_2; ( V1 is linearly-closed & V2 is linearly-closed ) by RLSUB_1:34; then A2: V3 is linearly-closed by RLSUB_1:7; 0. V in W1 by RLSUB_1:17; then 0. V in the carrier of W1 by STRUCT_0:def_5; then the carrier of W1 /\ the carrier of W2 <> {} by A1, XBOOLE_0:def_4; hence ex b1 being strict Subspace of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 by A2, RLSUB_1:35; ::_thesis: verum end; uniqueness for b1, b2 being strict Subspace of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 & the carrier of b2 = the carrier of W1 /\ the carrier of W2 holds b1 = b2 by RLSUB_1:30; end; :: deftheorem Def2 defines /\ RLSUB_2:def_2_:_ for V being RealLinearSpace for W1, W2 being Subspace of V for b4 being strict Subspace of V holds ( b4 = W1 /\ W2 iff the carrier of b4 = the carrier of W1 /\ the carrier of W2 ); theorem Th1: :: RLSUB_2:1 for V being RealLinearSpace for W1, W2 being Subspace of V for x being set holds ( x in W1 + W2 iff ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V for x being set holds ( x in W1 + W2 iff ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) let W1, W2 be Subspace of V; ::_thesis: for x being set holds ( x in W1 + W2 iff ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) let x be set ; ::_thesis: ( x in W1 + W2 iff ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) thus ( x in W1 + W2 implies ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) ::_thesis: ( ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & x = v1 + v2 ) implies x in W1 + W2 ) proof assume x in W1 + W2 ; ::_thesis: ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & x = v1 + v2 ) then x in the carrier of (W1 + W2) by STRUCT_0:def_5; then x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by Def1; then consider v1, v2 being VECTOR of V such that A1: ( x = v1 + v2 & v1 in W1 & v2 in W2 ) ; take v1 ; ::_thesis: ex v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & x = v1 + v2 ) take v2 ; ::_thesis: ( v1 in W1 & v2 in W2 & x = v1 + v2 ) thus ( v1 in W1 & v2 in W2 & x = v1 + v2 ) by A1; ::_thesis: verum end; given v1, v2 being VECTOR of V such that A2: ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ; ::_thesis: x in W1 + W2 x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by A2; then x in the carrier of (W1 + W2) by Def1; hence x in W1 + W2 by STRUCT_0:def_5; ::_thesis: verum end; theorem Th2: :: RLSUB_2:2 for V being RealLinearSpace for W1, W2 being Subspace of V for v being VECTOR of V st ( v in W1 or v in W2 ) holds v in W1 + W2 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V for v being VECTOR of V st ( v in W1 or v in W2 ) holds v in W1 + W2 let W1, W2 be Subspace of V; ::_thesis: for v being VECTOR of V st ( v in W1 or v in W2 ) holds v in W1 + W2 let v be VECTOR of V; ::_thesis: ( ( v in W1 or v in W2 ) implies v in W1 + W2 ) assume A1: ( v in W1 or v in W2 ) ; ::_thesis: v in W1 + W2 now__::_thesis:_v_in_W1_+_W2 percases ( v in W1 or v in W2 ) by A1; supposeA2: v in W1 ; ::_thesis: v in W1 + W2 ( v = v + (0. V) & 0. V in W2 ) by RLSUB_1:17, RLVECT_1:4; hence v in W1 + W2 by A2, Th1; ::_thesis: verum end; supposeA3: v in W2 ; ::_thesis: v in W1 + W2 ( v = (0. V) + v & 0. V in W1 ) by RLSUB_1:17, RLVECT_1:4; hence v in W1 + W2 by A3, Th1; ::_thesis: verum end; end; end; hence v in W1 + W2 ; ::_thesis: verum end; theorem Th3: :: RLSUB_2:3 for V being RealLinearSpace for W1, W2 being Subspace of V for x being set holds ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V for x being set holds ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) let W1, W2 be Subspace of V; ::_thesis: for x being set holds ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) let x be set ; ::_thesis: ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) ( x in W1 /\ W2 iff x in the carrier of (W1 /\ W2) ) by STRUCT_0:def_5; then ( x in W1 /\ W2 iff x in the carrier of W1 /\ the carrier of W2 ) by Def2; then ( x in W1 /\ W2 iff ( x in the carrier of W1 & x in the carrier of W2 ) ) by XBOOLE_0:def_4; hence ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) by STRUCT_0:def_5; ::_thesis: verum end; Lm1: for V being RealLinearSpace for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1 let W1, W2 be Subspace of V; ::_thesis: W1 + W2 = W2 + W1 set A = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; set B = { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } ; A1: { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } c= { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ) assume x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } then ex v, u being VECTOR of V st ( x = v + u & v in W2 & u in W1 ) ; hence x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; ::_thesis: verum end; A2: the carrier of (W1 + W2) = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by Def1; { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } c= { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } ) assume x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } then ex v, u being VECTOR of V st ( x = v + u & v in W1 & u in W2 ) ; hence x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } ; ::_thesis: verum end; then { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } = { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } by A1, XBOOLE_0:def_10; hence W1 + W2 = W2 + W1 by A2, Def1; ::_thesis: verum end; Lm2: for V being RealLinearSpace for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2) let W1, W2 be Subspace of V; ::_thesis: the carrier of W1 c= the carrier of (W1 + W2) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 + W2) ) set A = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; assume x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 + W2) then reconsider v = x as Element of W1 ; reconsider v = v as VECTOR of V by RLSUB_1:10; A1: v = v + (0. V) by RLVECT_1:4; ( v in W1 & 0. V in W2 ) by RLSUB_1:17, STRUCT_0:def_5; then x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by A1; hence x in the carrier of (W1 + W2) by Def1; ::_thesis: verum end; Lm3: for V being RealLinearSpace for W1 being Subspace of V for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds W1 + W2 = W2 proof let V be RealLinearSpace; ::_thesis: for W1 being Subspace of V for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds W1 + W2 = W2 let W1 be Subspace of V; ::_thesis: for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds W1 + W2 = W2 let W2 be strict Subspace of V; ::_thesis: ( the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2 ) assume A1: the carrier of W1 c= the carrier of W2 ; ::_thesis: W1 + W2 = W2 A2: the carrier of (W1 + W2) c= the carrier of W2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of W2 ) assume x in the carrier of (W1 + W2) ; ::_thesis: x in the carrier of W2 then x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by Def1; then consider v, u being VECTOR of V such that A3: x = v + u and A4: v in W1 and A5: u in W2 ; W1 is Subspace of W2 by A1, RLSUB_1:28; then v in W2 by A4, RLSUB_1:8; then v + u in W2 by A5, RLSUB_1:20; hence x in the carrier of W2 by A3, STRUCT_0:def_5; ::_thesis: verum end; W1 + W2 = W2 + W1 by Lm1; then the carrier of W2 c= the carrier of (W1 + W2) by Lm2; then the carrier of (W1 + W2) = the carrier of W2 by A2, XBOOLE_0:def_10; hence W1 + W2 = W2 by RLSUB_1:30; ::_thesis: verum end; theorem :: RLSUB_2:4 for V being RealLinearSpace for W being strict Subspace of V holds W + W = W by Lm3; theorem :: RLSUB_2:5 for V being RealLinearSpace for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1 by Lm1; theorem Th6: :: RLSUB_2:6 for V being RealLinearSpace for W1, W2, W3 being Subspace of V holds W1 + (W2 + W3) = (W1 + W2) + W3 proof let V be RealLinearSpace; ::_thesis: for W1, W2, W3 being Subspace of V holds W1 + (W2 + W3) = (W1 + W2) + W3 let W1, W2, W3 be Subspace of V; ::_thesis: W1 + (W2 + W3) = (W1 + W2) + W3 set A = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; set B = { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W3 ) } ; set C = { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ; set D = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ; A1: the carrier of (W1 + (W2 + W3)) = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } by Def1; A2: { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ) assume x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } then consider v, u being VECTOR of V such that A3: x = v + u and A4: v in W1 + W2 and A5: u in W3 ; v in the carrier of (W1 + W2) by A4, STRUCT_0:def_5; then v in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by Def1; then consider u1, u2 being VECTOR of V such that A6: v = u1 + u2 and A7: u1 in W1 and A8: u2 in W2 ; u2 + u in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W3 ) } by A5, A8; then u2 + u in the carrier of (W2 + W3) by Def1; then A9: u2 + u in W2 + W3 by STRUCT_0:def_5; v + u = u1 + (u2 + u) by A6, RLVECT_1:def_3; hence x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } by A3, A7, A9; ::_thesis: verum end; { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } c= { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ) assume x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } then consider v, u being VECTOR of V such that A10: x = v + u and A11: v in W1 and A12: u in W2 + W3 ; u in the carrier of (W2 + W3) by A12, STRUCT_0:def_5; then u in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W3 ) } by Def1; then consider u1, u2 being VECTOR of V such that A13: u = u1 + u2 and A14: u1 in W2 and A15: u2 in W3 ; v + u1 in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by A11, A14; then v + u1 in the carrier of (W1 + W2) by Def1; then A16: v + u1 in W1 + W2 by STRUCT_0:def_5; v + u = (v + u1) + u2 by A13, RLVECT_1:def_3; hence x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } by A10, A15, A16; ::_thesis: verum end; then { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } = { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } by A2, XBOOLE_0:def_10; hence W1 + (W2 + W3) = (W1 + W2) + W3 by A1, Def1; ::_thesis: verum end; theorem Th7: :: RLSUB_2:7 for V being RealLinearSpace for W1, W2 being Subspace of V holds ( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds ( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 ) let W1, W2 be Subspace of V; ::_thesis: ( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 ) the carrier of W1 c= the carrier of (W1 + W2) by Lm2; hence W1 is Subspace of W1 + W2 by RLSUB_1:28; ::_thesis: W2 is Subspace of W1 + W2 the carrier of W2 c= the carrier of (W2 + W1) by Lm2; then the carrier of W2 c= the carrier of (W1 + W2) by Lm1; hence W2 is Subspace of W1 + W2 by RLSUB_1:28; ::_thesis: verum end; theorem Th8: :: RLSUB_2:8 for V being RealLinearSpace for W1 being Subspace of V for W2 being strict Subspace of V holds ( W1 is Subspace of W2 iff W1 + W2 = W2 ) proof let V be RealLinearSpace; ::_thesis: for W1 being Subspace of V for W2 being strict Subspace of V holds ( W1 is Subspace of W2 iff W1 + W2 = W2 ) let W1 be Subspace of V; ::_thesis: for W2 being strict Subspace of V holds ( W1 is Subspace of W2 iff W1 + W2 = W2 ) let W2 be strict Subspace of V; ::_thesis: ( W1 is Subspace of W2 iff W1 + W2 = W2 ) thus ( W1 is Subspace of W2 implies W1 + W2 = W2 ) ::_thesis: ( W1 + W2 = W2 implies W1 is Subspace of W2 ) proof assume W1 is Subspace of W2 ; ::_thesis: W1 + W2 = W2 then the carrier of W1 c= the carrier of W2 by RLSUB_1:def_2; hence W1 + W2 = W2 by Lm3; ::_thesis: verum end; thus ( W1 + W2 = W2 implies W1 is Subspace of W2 ) by Th7; ::_thesis: verum end; theorem Th9: :: RLSUB_2:9 for V being RealLinearSpace for W being strict Subspace of V holds ( ((0). V) + W = W & W + ((0). V) = W ) proof let V be RealLinearSpace; ::_thesis: for W being strict Subspace of V holds ( ((0). V) + W = W & W + ((0). V) = W ) let W be strict Subspace of V; ::_thesis: ( ((0). V) + W = W & W + ((0). V) = W ) (0). V is Subspace of W by RLSUB_1:39; then the carrier of ((0). V) c= the carrier of W by RLSUB_1:def_2; hence ((0). V) + W = W by Lm3; ::_thesis: W + ((0). V) = W hence W + ((0). V) = W by Lm1; ::_thesis: verum end; theorem :: RLSUB_2:10 for V being RealLinearSpace holds ( ((0). V) + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & ((Omega). V) + ((0). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) by Th9; theorem Th11: :: RLSUB_2:11 for V being RealLinearSpace for W being Subspace of V holds ( ((Omega). V) + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & W + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V holds ( ((Omega). V) + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & W + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) let W be Subspace of V; ::_thesis: ( ((Omega). V) + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & W + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) the carrier of W c= the carrier of V by RLSUB_1:def_2; then W + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm3; hence ( ((Omega). V) + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & W + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) by Lm1; ::_thesis: verum end; theorem :: RLSUB_2:12 for V being strict RealLinearSpace holds ((Omega). V) + ((Omega). V) = V by Th11; theorem :: RLSUB_2:13 for V being RealLinearSpace for W being strict Subspace of V holds W /\ W = W proof let V be RealLinearSpace; ::_thesis: for W being strict Subspace of V holds W /\ W = W let W be strict Subspace of V; ::_thesis: W /\ W = W the carrier of W = the carrier of W /\ the carrier of W ; hence W /\ W = W by Def2; ::_thesis: verum end; theorem Th14: :: RLSUB_2:14 for V being RealLinearSpace for W1, W2 being Subspace of V holds W1 /\ W2 = W2 /\ W1 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds W1 /\ W2 = W2 /\ W1 let W1, W2 be Subspace of V; ::_thesis: W1 /\ W2 = W2 /\ W1 the carrier of (W1 /\ W2) = the carrier of W2 /\ the carrier of W1 by Def2; hence W1 /\ W2 = W2 /\ W1 by Def2; ::_thesis: verum end; theorem Th15: :: RLSUB_2:15 for V being RealLinearSpace for W1, W2, W3 being Subspace of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 proof let V be RealLinearSpace; ::_thesis: for W1, W2, W3 being Subspace of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 let W1, W2, W3 be Subspace of V; ::_thesis: W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 set V1 = the carrier of W1; set V2 = the carrier of W2; set V3 = the carrier of W3; the carrier of (W1 /\ (W2 /\ W3)) = the carrier of W1 /\ the carrier of (W2 /\ W3) by Def2 .= the carrier of W1 /\ ( the carrier of W2 /\ the carrier of W3) by Def2 .= ( the carrier of W1 /\ the carrier of W2) /\ the carrier of W3 by XBOOLE_1:16 .= the carrier of (W1 /\ W2) /\ the carrier of W3 by Def2 ; hence W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 by Def2; ::_thesis: verum end; Lm4: for V being RealLinearSpace for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of W1 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of W1 let W1, W2 be Subspace of V; ::_thesis: the carrier of (W1 /\ W2) c= the carrier of W1 the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2; hence the carrier of (W1 /\ W2) c= the carrier of W1 by XBOOLE_1:17; ::_thesis: verum end; theorem Th16: :: RLSUB_2:16 for V being RealLinearSpace for W1, W2 being Subspace of V holds ( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds ( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 ) let W1, W2 be Subspace of V; ::_thesis: ( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 ) the carrier of (W1 /\ W2) c= the carrier of W1 by Lm4; hence W1 /\ W2 is Subspace of W1 by RLSUB_1:28; ::_thesis: W1 /\ W2 is Subspace of W2 the carrier of (W2 /\ W1) c= the carrier of W2 by Lm4; then the carrier of (W1 /\ W2) c= the carrier of W2 by Th14; hence W1 /\ W2 is Subspace of W2 by RLSUB_1:28; ::_thesis: verum end; theorem Th17: :: RLSUB_2:17 for V being RealLinearSpace for W2 being Subspace of V for W1 being strict Subspace of V holds ( W1 is Subspace of W2 iff W1 /\ W2 = W1 ) proof let V be RealLinearSpace; ::_thesis: for W2 being Subspace of V for W1 being strict Subspace of V holds ( W1 is Subspace of W2 iff W1 /\ W2 = W1 ) let W2 be Subspace of V; ::_thesis: for W1 being strict Subspace of V holds ( W1 is Subspace of W2 iff W1 /\ W2 = W1 ) let W1 be strict Subspace of V; ::_thesis: ( W1 is Subspace of W2 iff W1 /\ W2 = W1 ) thus ( W1 is Subspace of W2 implies W1 /\ W2 = W1 ) ::_thesis: ( W1 /\ W2 = W1 implies W1 is Subspace of W2 ) proof assume W1 is Subspace of W2 ; ::_thesis: W1 /\ W2 = W1 then A1: the carrier of W1 c= the carrier of W2 by RLSUB_1:def_2; the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2; hence W1 /\ W2 = W1 by A1, RLSUB_1:30, XBOOLE_1:28; ::_thesis: verum end; thus ( W1 /\ W2 = W1 implies W1 is Subspace of W2 ) by Th16; ::_thesis: verum end; theorem Th18: :: RLSUB_2:18 for V being RealLinearSpace for W being Subspace of V holds ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V ) proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V holds ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V ) let W be Subspace of V; ::_thesis: ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V ) 0. V in W by RLSUB_1:17; then 0. V in the carrier of W by STRUCT_0:def_5; then {(0. V)} c= the carrier of W by ZFMISC_1:31; then A1: {(0. V)} /\ the carrier of W = {(0. V)} by XBOOLE_1:28; the carrier of (((0). V) /\ W) = the carrier of ((0). V) /\ the carrier of W by Def2 .= {(0. V)} /\ the carrier of W by RLSUB_1:def_3 ; hence ((0). V) /\ W = (0). V by A1, RLSUB_1:def_3; ::_thesis: W /\ ((0). V) = (0). V hence W /\ ((0). V) = (0). V by Th14; ::_thesis: verum end; theorem :: RLSUB_2:19 for V being RealLinearSpace holds ( ((0). V) /\ ((Omega). V) = (0). V & ((Omega). V) /\ ((0). V) = (0). V ) by Th18; theorem Th20: :: RLSUB_2:20 for V being RealLinearSpace for W being strict Subspace of V holds ( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W ) proof let V be RealLinearSpace; ::_thesis: for W being strict Subspace of V holds ( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W ) let W be strict Subspace of V; ::_thesis: ( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W ) ( the carrier of (((Omega). V) /\ W) = the carrier of V /\ the carrier of W & the carrier of W c= the carrier of V ) by Def2, RLSUB_1:def_2; hence ((Omega). V) /\ W = W by RLSUB_1:30, XBOOLE_1:28; ::_thesis: W /\ ((Omega). V) = W hence W /\ ((Omega). V) = W by Th14; ::_thesis: verum end; theorem :: RLSUB_2:21 for V being strict RealLinearSpace holds ((Omega). V) /\ ((Omega). V) = V by Th20; Lm5: for V being RealLinearSpace for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2) let W1, W2 be Subspace of V; ::_thesis: the carrier of (W1 /\ W2) c= the carrier of (W1 + W2) ( the carrier of (W1 /\ W2) c= the carrier of W1 & the carrier of W1 c= the carrier of (W1 + W2) ) by Lm2, Lm4; hence the carrier of (W1 /\ W2) c= the carrier of (W1 + W2) by XBOOLE_1:1; ::_thesis: verum end; theorem :: RLSUB_2:22 for V being RealLinearSpace for W1, W2 being Subspace of V holds W1 /\ W2 is Subspace of W1 + W2 by Lm5, RLSUB_1:28; Lm6: for V being RealLinearSpace for W1, W2 being Subspace of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2 let W1, W2 be Subspace of V; ::_thesis: the carrier of ((W1 /\ W2) + W2) = the carrier of W2 thus the carrier of ((W1 /\ W2) + W2) c= the carrier of W2 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 /\ W2) + W2) or x in the carrier of W2 ) assume x in the carrier of ((W1 /\ W2) + W2) ; ::_thesis: x in the carrier of W2 then x in { (u + v) where u, v is VECTOR of V : ( u in W1 /\ W2 & v in W2 ) } by Def1; then consider u, v being VECTOR of V such that A1: x = u + v and A2: u in W1 /\ W2 and A3: v in W2 ; u in W2 by A2, Th3; then u + v in W2 by A3, RLSUB_1:20; hence x in the carrier of W2 by A1, 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 /\ W2) + W2) ) the carrier of W2 c= the carrier of (W2 + (W1 /\ W2)) by Lm2; then A4: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2) by Lm1; assume x in the carrier of W2 ; ::_thesis: x in the carrier of ((W1 /\ W2) + W2) hence x in the carrier of ((W1 /\ W2) + W2) by A4; ::_thesis: verum end; theorem :: RLSUB_2:23 for V being RealLinearSpace for W1 being Subspace of V for W2 being strict Subspace of V holds (W1 /\ W2) + W2 = W2 by Lm6, RLSUB_1:30; Lm7: for V being RealLinearSpace for W1, W2 being Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 let W1, W2 be Subspace of V; ::_thesis: the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 thus the carrier of (W1 /\ (W1 + W2)) c= the carrier of W1 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W1 c= the carrier of (W1 /\ (W1 + W2)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W1 /\ (W1 + W2)) or x in the carrier of W1 ) assume A1: x in the carrier of (W1 /\ (W1 + W2)) ; ::_thesis: x in the carrier of W1 the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 /\ the carrier of (W1 + W2) by Def2; hence x in the carrier of W1 by A1, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 /\ (W1 + W2)) ) assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 /\ (W1 + W2)) the carrier of W1 c= the carrier of V by RLSUB_1:def_2; then reconsider x1 = x as Element of V by A2; A3: ( x1 + (0. V) = x1 & 0. V in W2 ) by RLSUB_1:17, RLVECT_1:4; x in W1 by A2, STRUCT_0:def_5; then x in { (u + v) where u, v is VECTOR of V : ( u in W1 & v in W2 ) } by A3; then x in the carrier of (W1 + W2) by Def1; then x in the carrier of W1 /\ the carrier of (W1 + W2) by A2, XBOOLE_0:def_4; hence x in the carrier of (W1 /\ (W1 + W2)) by Def2; ::_thesis: verum end; theorem :: RLSUB_2:24 for V being RealLinearSpace for W2 being Subspace of V for W1 being strict Subspace of V holds W1 /\ (W1 + W2) = W1 by Lm7, RLSUB_1:30; Lm8: for V being RealLinearSpace for W1, W2, W3 being Subspace of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) proof let V be RealLinearSpace; ::_thesis: for W1, W2, W3 being Subspace of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) let W1, W2, W3 be Subspace of V; ::_thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) or x in the carrier of (W2 /\ (W1 + W3)) ) assume x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) ; ::_thesis: x in the carrier of (W2 /\ (W1 + W3)) then x in { (u + v) where u, v is VECTOR of V : ( u in W1 /\ W2 & v in W2 /\ W3 ) } by Def1; then consider u, v being VECTOR of V such that A1: x = u + v and A2: ( u in W1 /\ W2 & v in W2 /\ W3 ) ; ( u in W2 & v in W2 ) by A2, Th3; then A3: x in W2 by A1, RLSUB_1:20; ( u in W1 & v in W3 ) by A2, Th3; then x in W1 + W3 by A1, Th1; then x in W2 /\ (W1 + W3) by A3, Th3; hence x in the carrier of (W2 /\ (W1 + W3)) by STRUCT_0:def_5; ::_thesis: verum end; theorem :: RLSUB_2:25 for V being RealLinearSpace for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by Lm8, RLSUB_1:28; Lm9: for V being RealLinearSpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) proof let V be RealLinearSpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) ) assume A1: W1 is Subspace of W2 ; ::_thesis: the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) thus the carrier of (W2 /\ (W1 + W3)) c= the carrier of ((W1 /\ W2) + (W2 /\ W3)) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W2 /\ (W1 + W3)) or x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) ) assume x in the carrier of (W2 /\ (W1 + W3)) ; ::_thesis: x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) then A2: x in the carrier of W2 /\ the carrier of (W1 + W3) by Def2; then x in the carrier of (W1 + W3) by XBOOLE_0:def_4; then x in { (u + v) where u, v is VECTOR of V : ( u in W1 & v in W3 ) } by Def1; then consider u1, v1 being VECTOR of V such that A3: x = u1 + v1 and A4: u1 in W1 and A5: v1 in W3 ; A6: u1 in W2 by A1, A4, RLSUB_1:8; x in the carrier of W2 by A2, XBOOLE_0:def_4; then u1 + v1 in W2 by A3, STRUCT_0:def_5; then (v1 + u1) - u1 in W2 by A6, RLSUB_1:23; then v1 + (u1 - u1) in W2 by RLVECT_1:def_3; then v1 + (0. V) in W2 by RLVECT_1:15; then v1 in W2 by RLVECT_1:4; then A7: v1 in W2 /\ W3 by A5, Th3; u1 in W1 /\ W2 by A4, A6, Th3; then x in (W1 /\ W2) + (W2 /\ W3) by A3, A7, Th1; hence x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) by STRUCT_0:def_5; ::_thesis: verum end; thus the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) by Lm8; ::_thesis: verum end; theorem :: RLSUB_2:26 for V being RealLinearSpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by Lm9, RLSUB_1:30; Lm10: for V being RealLinearSpace for W2, W1, W3 being Subspace of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) proof let V be RealLinearSpace; ::_thesis: for W2, W1, W3 being Subspace of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) let W2, W1, W3 be Subspace of V; ::_thesis: the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W2 + (W1 /\ W3)) or x in the carrier of ((W1 + W2) /\ (W2 + W3)) ) assume x in the carrier of (W2 + (W1 /\ W3)) ; ::_thesis: x in the carrier of ((W1 + W2) /\ (W2 + W3)) then x in { (u + v) where u, v is VECTOR of V : ( u in W2 & v in W1 /\ W3 ) } by Def1; then consider u, v being VECTOR of V such that A1: ( x = u + v & u in W2 ) and A2: v in W1 /\ W3 ; v in W3 by A2, Th3; then x in { (u1 + u2) where u1, u2 is VECTOR of V : ( u1 in W2 & u2 in W3 ) } by A1; then A3: x in the carrier of (W2 + W3) by Def1; v in W1 by A2, Th3; then x in { (v1 + v2) where v1, v2 is VECTOR of V : ( v1 in W1 & v2 in W2 ) } by A1; then x in the carrier of (W1 + W2) by Def1; then x in the carrier of (W1 + W2) /\ the carrier of (W2 + W3) by A3, XBOOLE_0:def_4; hence x in the carrier of ((W1 + W2) /\ (W2 + W3)) by Def2; ::_thesis: verum end; theorem :: RLSUB_2:27 for V being RealLinearSpace for W2, W1, W3 being Subspace of V holds W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by Lm10, RLSUB_1:28; Lm11: for V being RealLinearSpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3)) proof let V be RealLinearSpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3)) let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3)) ) reconsider V2 = the carrier of W2 as Subset of V by RLSUB_1:def_2; A1: V2 is linearly-closed by RLSUB_1:34; assume W1 is Subspace of W2 ; ::_thesis: the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3)) then A2: the carrier of W1 c= the carrier of W2 by RLSUB_1:def_2; thus the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) by Lm10; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((W1 + W2) /\ (W2 + W3)) c= the carrier of (W2 + (W1 /\ W3)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 + W2) /\ (W2 + W3)) or x in the carrier of (W2 + (W1 /\ W3)) ) assume x in the carrier of ((W1 + W2) /\ (W2 + W3)) ; ::_thesis: x in the carrier of (W2 + (W1 /\ W3)) then x in the carrier of (W1 + W2) /\ the carrier of (W2 + W3) by Def2; then x in the carrier of (W1 + W2) by XBOOLE_0:def_4; then x in { (u1 + u2) where u1, u2 is VECTOR of V : ( u1 in W1 & u2 in W2 ) } by Def1; then consider u1, u2 being VECTOR of V such that A3: x = u1 + u2 and A4: ( u1 in W1 & u2 in W2 ) ; ( u1 in the carrier of W1 & u2 in the carrier of W2 ) by A4, STRUCT_0:def_5; then u1 + u2 in V2 by A2, A1, RLSUB_1:def_1; then A5: u1 + u2 in W2 by STRUCT_0:def_5; ( 0. V in W1 /\ W3 & (u1 + u2) + (0. V) = u1 + u2 ) by RLSUB_1:17, RLVECT_1:4; then x in { (u + v) where u, v is VECTOR of V : ( u in W2 & v in W1 /\ W3 ) } by A3, A5; hence x in the carrier of (W2 + (W1 /\ W3)) by Def1; ::_thesis: verum end; theorem :: RLSUB_2:28 for V being RealLinearSpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by Lm11, RLSUB_1:30; theorem Th29: :: RLSUB_2:29 for V being RealLinearSpace for W1, W3, W2 being Subspace of V st W1 is strict Subspace of W3 holds W1 + (W2 /\ W3) = (W1 + W2) /\ W3 proof let V be RealLinearSpace; ::_thesis: for W1, W3, W2 being Subspace of V st W1 is strict Subspace of W3 holds W1 + (W2 /\ W3) = (W1 + W2) /\ W3 let W1, W3, W2 be Subspace of V; ::_thesis: ( W1 is strict Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3 ) assume A1: W1 is strict Subspace of W3 ; ::_thesis: W1 + (W2 /\ W3) = (W1 + W2) /\ W3 thus (W1 + W2) /\ W3 = W3 /\ (W1 + W2) by Th14 .= (W1 /\ W3) + (W3 /\ W2) by A1, Lm9, RLSUB_1:30 .= W1 + (W3 /\ W2) by A1, Th17 .= W1 + (W2 /\ W3) by Th14 ; ::_thesis: verum end; theorem :: RLSUB_2:30 for V being RealLinearSpace for W1, W2 being strict Subspace of V holds ( W1 + W2 = W2 iff W1 /\ W2 = W1 ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being strict Subspace of V holds ( W1 + W2 = W2 iff W1 /\ W2 = W1 ) let W1, W2 be strict Subspace of V; ::_thesis: ( W1 + W2 = W2 iff W1 /\ W2 = W1 ) ( W1 + W2 = W2 iff W1 is Subspace of W2 ) by Th8; hence ( W1 + W2 = W2 iff W1 /\ W2 = W1 ) by Th17; ::_thesis: verum end; theorem :: RLSUB_2:31 for V being RealLinearSpace for W1 being Subspace of V for W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds W1 + W3 is Subspace of W2 + W3 proof let V be RealLinearSpace; ::_thesis: for W1 being Subspace of V for W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds W1 + W3 is Subspace of W2 + W3 let W1 be Subspace of V; ::_thesis: for W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds W1 + W3 is Subspace of W2 + W3 let W2, W3 be strict Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies W1 + W3 is Subspace of W2 + W3 ) assume A1: W1 is Subspace of W2 ; ::_thesis: W1 + W3 is Subspace of W2 + W3 (W1 + W3) + (W2 + W3) = (W1 + W3) + (W3 + W2) by Lm1 .= ((W1 + W3) + W3) + W2 by Th6 .= (W1 + (W3 + W3)) + W2 by Th6 .= (W1 + W3) + W2 by Lm3 .= W1 + (W3 + W2) by Th6 .= W1 + (W2 + W3) by Lm1 .= (W1 + W2) + W3 by Th6 .= W2 + W3 by A1, Th8 ; hence W1 + W3 is Subspace of W2 + W3 by Th8; ::_thesis: verum end; theorem :: RLSUB_2:32 for V being RealLinearSpace for W1, W2 being Subspace of V holds ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) let W1, W2 be Subspace of V; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) set VW1 = the carrier of W1; set VW2 = the carrier of W2; thus ( for W being Subspace of V holds not the carrier of W = the carrier of W1 \/ the carrier of W2 or W1 is Subspace of W2 or W2 is Subspace of W1 ) ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) proof given W being Subspace of V such that A1: the carrier of W = the carrier of W1 \/ the carrier of W2 ; ::_thesis: ( W1 is Subspace of W2 or W2 is Subspace of W1 ) set VW = the carrier of W; assume that A2: W1 is not Subspace of W2 and A3: W2 is not Subspace of W1 ; ::_thesis: contradiction not the carrier of W2 c= the carrier of W1 by A3, RLSUB_1:28; then consider y being set such that A4: y in the carrier of W2 and A5: not y in the carrier of W1 by TARSKI:def_3; reconsider y = y as Element of the carrier of W2 by A4; reconsider y = y as VECTOR of V by RLSUB_1:10; reconsider A1 = the carrier of W as Subset of V by RLSUB_1:def_2; A6: A1 is linearly-closed by RLSUB_1:34; not the carrier of W1 c= the carrier of W2 by A2, RLSUB_1:28; then consider x being set such that A7: x in the carrier of W1 and A8: not x in the carrier of W2 by TARSKI:def_3; reconsider x = x as Element of the carrier of W1 by A7; reconsider x = x as VECTOR of V by RLSUB_1:10; A9: now__::_thesis:_not_x_+_y_in_the_carrier_of_W2 reconsider A2 = the carrier of W2 as Subset of V by RLSUB_1:def_2; A10: A2 is linearly-closed by RLSUB_1:34; assume x + y in the carrier of W2 ; ::_thesis: contradiction then (x + y) - y in the carrier of W2 by A10, RLSUB_1:3; then x + (y - y) in the carrier of W2 by RLVECT_1:def_3; then x + (0. V) in the carrier of W2 by RLVECT_1:15; hence contradiction by A8, RLVECT_1:4; ::_thesis: verum end; A11: now__::_thesis:_not_x_+_y_in_the_carrier_of_W1 reconsider A2 = the carrier of W1 as Subset of V by RLSUB_1:def_2; A12: A2 is linearly-closed by RLSUB_1:34; assume x + y in the carrier of W1 ; ::_thesis: contradiction then (y + x) - x in the carrier of W1 by A12, RLSUB_1:3; then y + (x - x) in the carrier of W1 by RLVECT_1:def_3; then y + (0. V) in the carrier of W1 by RLVECT_1:15; hence contradiction by A5, RLVECT_1:4; ::_thesis: verum end; ( x in the carrier of W & y in the carrier of W ) by A1, XBOOLE_0:def_3; then x + y in the carrier of W by A6, RLSUB_1:def_1; hence contradiction by A1, A11, A9, XBOOLE_0:def_3; ::_thesis: verum end; A13: now__::_thesis:_(_W1_is_Subspace_of_W2_&_(_W1_is_Subspace_of_W2_or_W2_is_Subspace_of_W1_)_implies_ex_W_being_Subspace_of_V_st_the_carrier_of_W_=_the_carrier_of_W1_\/_the_carrier_of_W2_) assume W1 is Subspace of W2 ; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) then the carrier of W1 c= the carrier of W2 by RLSUB_1:def_2; then the carrier of W1 \/ the carrier of W2 = the carrier of W2 by XBOOLE_1:12; hence ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; ::_thesis: verum end; A14: now__::_thesis:_(_W2_is_Subspace_of_W1_&_(_W1_is_Subspace_of_W2_or_W2_is_Subspace_of_W1_)_implies_ex_W_being_Subspace_of_V_st_the_carrier_of_W_=_the_carrier_of_W1_\/_the_carrier_of_W2_) assume W2 is Subspace of W1 ; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) then the carrier of W2 c= the carrier of W1 by RLSUB_1:def_2; then the carrier of W1 \/ the carrier of W2 = the carrier of W1 by XBOOLE_1:12; hence ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; ::_thesis: verum end; assume ( W1 is Subspace of W2 or W2 is Subspace of W1 ) ; ::_thesis: ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 hence ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 by A13, A14; ::_thesis: verum end; definition let V be RealLinearSpace; func Subspaces V -> set means :Def3: :: RLSUB_2:def 3 for x being set holds ( x in it iff x is strict Subspace of V ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict Subspace of V ) proof defpred S1[ set , set ] means ex W being strict Subspace of V st ( \$2 = W & \$1 = the carrier of W ); defpred S2[ set ] means ex W being strict Subspace of V st \$1 = the carrier of W; consider B being set such that A1: for x being set holds ( x in B iff ( x in bool the carrier of V & S2[x] ) ) from XBOOLE_0:sch_1(); A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds y1 = y2 by RLSUB_1:30; consider f being Function such that A3: for x, y being set holds ( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch_1(A2); for x being set holds ( x in B iff ex y being set st [x,y] in f ) proof let x be set ; ::_thesis: ( x in B iff ex y being set st [x,y] in f ) thus ( x in B implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in B ) proof assume A4: x in B ; ::_thesis: ex y being set st [x,y] in f then consider W being strict Subspace of V such that A5: x = the carrier of W by A1; reconsider y = W as set ; take y ; ::_thesis: [x,y] in f thus [x,y] in f by A3, A4, A5; ::_thesis: verum end; given y being set such that A6: [x,y] in f ; ::_thesis: x in B thus x in B by A3, A6; ::_thesis: verum end; then A7: B = dom f by XTUPLE_0:def_12; for y being set holds ( y in rng f iff y is strict Subspace of V ) proof let y be set ; ::_thesis: ( y in rng f iff y is strict Subspace of V ) thus ( y in rng f implies y is strict Subspace of V ) ::_thesis: ( y is strict Subspace of V implies y in rng f ) proof assume y in rng f ; ::_thesis: y is strict Subspace of V then consider x being set such that A8: ( x in dom f & y = f . x ) by FUNCT_1:def_3; [x,y] in f by A8, FUNCT_1:def_2; then ex W being strict Subspace of V st ( y = W & x = the carrier of W ) by A3; hence y is strict Subspace of V ; ::_thesis: verum end; assume y is strict Subspace of V ; ::_thesis: y in rng f then reconsider W = y as strict Subspace of V ; reconsider x = the carrier of W as set ; the carrier of W c= the carrier of V by RLSUB_1:def_2; then A9: x in dom f by A1, A7; then [x,y] in f by A3, A7; then y = f . x by A9, FUNCT_1:def_2; hence y in rng f by A9, FUNCT_1:def_3; ::_thesis: verum end; hence ex b1 being set st for x being set holds ( x in b1 iff x is strict Subspace of V ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict Subspace of V ) ) & ( for x being set holds ( x in b2 iff x is strict Subspace of V ) ) holds b1 = b2 proof let D1, D2 be set ; ::_thesis: ( ( for x being set holds ( x in D1 iff x is strict Subspace of V ) ) & ( for x being set holds ( x in D2 iff x is strict Subspace of V ) ) implies D1 = D2 ) assume A10: for x being set holds ( x in D1 iff x is strict Subspace of V ) ; ::_thesis: ( ex x being set st ( ( x in D2 implies x is strict Subspace of V ) implies ( x is strict Subspace of V & not x in D2 ) ) or D1 = D2 ) assume A11: for x being set holds ( x in D2 iff x is strict Subspace of V ) ; ::_thesis: D1 = D2 now__::_thesis:_for_x_being_set_holds_ (_(_x_in_D1_implies_x_in_D2_)_&_(_x_in_D2_implies_x_in_D1_)_) let x be set ; ::_thesis: ( ( x in D1 implies x in D2 ) & ( x in D2 implies x in D1 ) ) thus ( x in D1 implies x in D2 ) ::_thesis: ( x in D2 implies x in D1 ) proof assume x in D1 ; ::_thesis: x in D2 then x is strict Subspace of V by A10; hence x in D2 by A11; ::_thesis: verum end; assume x in D2 ; ::_thesis: x in D1 then x is strict Subspace of V by A11; hence x in D1 by A10; ::_thesis: verum end; hence D1 = D2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def3 defines Subspaces RLSUB_2:def_3_:_ for V being RealLinearSpace for b2 being set holds ( b2 = Subspaces V iff for x being set holds ( x in b2 iff x is strict Subspace of V ) ); registration let V be RealLinearSpace; cluster Subspaces V -> non empty ; coherence not Subspaces V is empty proof set x = the strict Subspace of V; the strict Subspace of V in Subspaces V by Def3; hence not Subspaces V is empty ; ::_thesis: verum end; end; theorem :: RLSUB_2:33 for V being strict RealLinearSpace holds V in Subspaces V proof let V be strict RealLinearSpace; ::_thesis: V in Subspaces V (Omega). V in Subspaces V by Def3; hence V in Subspaces V ; ::_thesis: verum end; definition let V be RealLinearSpace; let W1, W2 be Subspace of V; predV is_the_direct_sum_of W1,W2 means :Def4: :: RLSUB_2:def 4 ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 & W1 /\ W2 = (0). V ); end; :: deftheorem Def4 defines is_the_direct_sum_of RLSUB_2:def_4_:_ for V being RealLinearSpace for W1, W2 being Subspace of V holds ( V is_the_direct_sum_of W1,W2 iff ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 & W1 /\ W2 = (0). V ) ); Lm12: for V being RealLinearSpace for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) proof let V be RealLinearSpace; ::_thesis: for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) let W be strict Subspace of V; ::_thesis: ( ( for v being VECTOR of V holds v in W ) implies W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) assume for v being VECTOR of V holds v in W ; ::_thesis: W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) then for v being VECTOR of V holds ( v in W iff v in (Omega). V ) by RLVECT_1:1; hence W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLSUB_1:31; ::_thesis: verum end; Lm13: for V being RealLinearSpace for W1, W2 being Subspace of V holds ( W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds ( W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) let W1, W2 be Subspace of V; ::_thesis: ( W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) thus ( W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) implies for v being VECTOR of V ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) ::_thesis: ( ( for v being VECTOR of V ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) implies W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) proof assume A1: W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; ::_thesis: for v being VECTOR of V ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) let v be VECTOR of V; ::_thesis: ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) v in RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLVECT_1:1; hence ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by A1, Th1; ::_thesis: verum end; assume A2: for v being VECTOR of V ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) ; ::_thesis: W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) now__::_thesis:_for_u_being_VECTOR_of_V_holds_u_in_W1_+_W2 let u be VECTOR of V; ::_thesis: u in W1 + W2 ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & u = v1 + v2 ) by A2; hence u in W1 + W2 by Th1; ::_thesis: verum end; hence W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm12; ::_thesis: verum end; Lm14: for V being non empty right_complementable add-associative right_zeroed addLoopStr for v, v1, v2 being Element of V holds ( v = v1 + v2 iff v1 = v - v2 ) proof let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, v1, v2 being Element of V holds ( v = v1 + v2 iff v1 = v - v2 ) let v, v1, v2 be Element of V; ::_thesis: ( v = v1 + v2 iff v1 = v - v2 ) thus ( v = v1 + v2 implies v1 = v - v2 ) ::_thesis: ( v1 = v - v2 implies v = v1 + v2 ) proof assume v = v1 + v2 ; ::_thesis: v1 = v - v2 hence v - v2 = v1 + (v2 - v2) by RLVECT_1:def_3 .= v1 + (0. V) by VECTSP_1:19 .= v1 by RLVECT_1:4 ; ::_thesis: verum end; thus ( v1 = v - v2 implies v = v1 + v2 ) ::_thesis: verum proof assume v1 = v - v2 ; ::_thesis: v = v1 + v2 hence v1 + v2 = v + ((- v2) + v2) by RLVECT_1:def_3 .= v + (0. V) by RLVECT_1:5 .= v by RLVECT_1:4 ; ::_thesis: verum end; end; Lm15: for V being RealLinearSpace for W being Subspace of V ex C being strict Subspace of V st V is_the_direct_sum_of C,W proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V ex C being strict Subspace of V st V is_the_direct_sum_of C,W let W be Subspace of V; ::_thesis: ex C being strict Subspace of V st V is_the_direct_sum_of C,W defpred S1[ set ] means ex W1 being strict Subspace of V st ( \$1 = W1 & W /\ W1 = (0). V ); consider X being set such that A1: for x being set holds ( x in X iff ( x in Subspaces V & S1[x] ) ) from XBOOLE_0:sch_1(); ( W /\ ((0). V) = (0). V & (0). V in Subspaces V ) by Def3, Th18; then reconsider X = X as non empty set by A1; defpred S2[ set , set ] means ex W1, W2 being strict Subspace of V st ( \$1 = W1 & \$2 = W2 & W1 is Subspace of W2 ); consider R being Relation of X such that A2: for x, y being Element of X holds ( [x,y] in R iff S2[x,y] ) from RELSET_1:sch_2(); defpred S3[ set , set ] means [\$1,\$2] in R; now__::_thesis:_for_x,_y,_z_being_Element_of_X_st_[x,y]_in_R_&_[y,z]_in_R_holds_ [x,z]_in_R let x, y, z be Element of X; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R ) assume that A3: [x,y] in R and A4: [y,z] in R ; ::_thesis: [x,z] in R consider W1, W2 being strict Subspace of V such that A5: x = W1 and A6: ( y = W2 & W1 is Subspace of W2 ) by A2, A3; consider W3, W4 being strict Subspace of V such that A7: y = W3 and A8: z = W4 and A9: W3 is Subspace of W4 by A2, A4; W1 is strict Subspace of W4 by A6, A7, A9, RLSUB_1:27; hence [x,z] in R by A2, A5, A8; ::_thesis: verum end; then A10: for x, y, z being Element of X st S3[x,y] & S3[y,z] holds S3[x,z] ; A11: now__::_thesis:_for_x_being_Element_of_X_holds_x_is_strict_Subspace_of_V let x be Element of X; ::_thesis: x is strict Subspace of V x in Subspaces V by A1; hence x is strict Subspace of V by Def3; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_X_holds_[x,x]_in_R let x be Element of X; ::_thesis: [x,x] in R reconsider W = x as strict Subspace of V by A11; W is Subspace of W by RLSUB_1:25; hence [x,x] in R by A2; ::_thesis: verum end; then A12: for x being Element of X holds S3[x,x] ; for Y being set st Y c= X & ( for x, y being Element of X st x in Y & y in Y & not [x,y] in R holds [y,x] in R ) holds ex y being Element of X st for x being Element of X st x in Y holds [x,y] in R proof let Y be set ; ::_thesis: ( Y c= X & ( for x, y being Element of X st x in Y & y in Y & not [x,y] in R holds [y,x] in R ) implies ex y being Element of X st for x being Element of X st x in Y holds [x,y] in R ) assume that A13: Y c= X and A14: for x, y being Element of X st x in Y & y in Y & not [x,y] in R holds [y,x] in R ; ::_thesis: ex y being Element of X st for x being Element of X st x in Y holds [x,y] in R now__::_thesis:_ex_y9_being_Element_of_X_st_ for_x_being_Element_of_X_st_x_in_Y_holds_ [x,y9]_in_R percases ( Y = {} or Y <> {} ) ; supposeA15: Y = {} ; ::_thesis: ex y9 being Element of X st for x being Element of X st x in Y holds [x,y9] in R set y = the Element of X; take y9 = the Element of X; ::_thesis: for x being Element of X st x in Y holds [x,y9] in R let x be Element of X; ::_thesis: ( x in Y implies [x,y9] in R ) assume x in Y ; ::_thesis: [x,y9] in R hence [x,y9] in R by A15; ::_thesis: verum end; supposeA16: Y <> {} ; ::_thesis: ex y being Element of X st for x being Element of X st x in Y holds [x,y] in R defpred S4[ set , set ] means ex W1 being strict Subspace of V st ( \$1 = W1 & \$2 = the carrier of W1 ); A17: for x being set st x in Y holds ex y being set st S4[x,y] proof let x be set ; ::_thesis: ( x in Y implies ex y being set st S4[x,y] ) assume x in Y ; ::_thesis: ex y being set st S4[x,y] then consider W1 being strict Subspace of V such that A18: x = W1 and W /\ W1 = (0). V by A1, A13; reconsider y = the carrier of W1 as set ; take y ; ::_thesis: S4[x,y] take W1 ; ::_thesis: ( x = W1 & y = the carrier of W1 ) thus ( x = W1 & y = the carrier of W1 ) by A18; ::_thesis: verum end; consider f being Function such that A19: dom f = Y and A20: for x being set st x in Y holds S4[x,f . x] from CLASSES1:sch_1(A17); set Z = union (rng f); now__::_thesis:_for_x_being_set_st_x_in_union_(rng_f)_holds_ x_in_the_carrier_of_V let x be set ; ::_thesis: ( x in union (rng f) implies x in the carrier of V ) assume x in union (rng f) ; ::_thesis: x in the carrier of V then consider Y9 being set such that A21: x in Y9 and A22: Y9 in rng f by TARSKI:def_4; consider y being set such that A23: y in dom f and A24: f . y = Y9 by A22, FUNCT_1:def_3; consider W1 being strict Subspace of V such that y = W1 and A25: f . y = the carrier of W1 by A19, A20, A23; the carrier of W1 c= the carrier of V by RLSUB_1:def_2; hence x in the carrier of V by A21, A24, A25; ::_thesis: verum end; then reconsider Z = union (rng f) as Subset of V by TARSKI:def_3; A26: Z is linearly-closed proof thus for v1, v2 being VECTOR of V st v1 in Z & v2 in Z holds v1 + v2 in Z :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of K93() for b2 being Element of the carrier of V holds ( not b2 in Z or b1 * b2 in Z ) proof let v1, v2 be VECTOR of V; ::_thesis: ( v1 in Z & v2 in Z implies v1 + v2 in Z ) assume that A27: v1 in Z and A28: v2 in Z ; ::_thesis: v1 + v2 in Z consider Y1 being set such that A29: v1 in Y1 and A30: Y1 in rng f by A27, TARSKI:def_4; consider y1 being set such that A31: y1 in dom f and A32: f . y1 = Y1 by A30, FUNCT_1:def_3; consider Y2 being set such that A33: v2 in Y2 and A34: Y2 in rng f by A28, TARSKI:def_4; consider y2 being set such that A35: y2 in dom f and A36: f . y2 = Y2 by A34, FUNCT_1:def_3; consider W1 being strict Subspace of V such that A37: y1 = W1 and A38: f . y1 = the carrier of W1 by A19, A20, A31; consider W2 being strict Subspace of V such that A39: y2 = W2 and A40: f . y2 = the carrier of W2 by A19, A20, A35; reconsider y1 = y1, y2 = y2 as Element of X by A13, A19, A31, A35; now__::_thesis:_v1_+_v2_in_Z percases ( [y1,y2] in R or [y2,y1] in R ) by A14, A19, A31, A35; suppose [y1,y2] in R ; ::_thesis: v1 + v2 in Z then ex W3, W4 being strict Subspace of V st ( y1 = W3 & y2 = W4 & W3 is Subspace of W4 ) by A2; then the carrier of W1 c= the carrier of W2 by A37, A39, RLSUB_1:def_2; then A41: v1 in W2 by A29, A32, A38, STRUCT_0:def_5; v2 in W2 by A33, A36, A40, STRUCT_0:def_5; then v1 + v2 in W2 by A41, RLSUB_1:20; then A42: v1 + v2 in the carrier of W2 by STRUCT_0:def_5; f . y2 in rng f by A35, FUNCT_1:def_3; hence v1 + v2 in Z by A40, A42, TARSKI:def_4; ::_thesis: verum end; suppose [y2,y1] in R ; ::_thesis: v1 + v2 in Z then ex W3, W4 being strict Subspace of V st ( y2 = W3 & y1 = W4 & W3 is Subspace of W4 ) by A2; then the carrier of W2 c= the carrier of W1 by A37, A39, RLSUB_1:def_2; then A43: v2 in W1 by A33, A36, A40, STRUCT_0:def_5; v1 in W1 by A29, A32, A38, STRUCT_0:def_5; then v1 + v2 in W1 by A43, RLSUB_1:20; then A44: v1 + v2 in the carrier of W1 by STRUCT_0:def_5; f . y1 in rng f by A31, FUNCT_1:def_3; hence v1 + v2 in Z by A38, A44, TARSKI:def_4; ::_thesis: verum end; end; end; hence v1 + v2 in Z ; ::_thesis: verum end; let a be Real; ::_thesis: for b1 being Element of the carrier of V holds ( not b1 in Z or a * b1 in Z ) let v1 be VECTOR of V; ::_thesis: ( not v1 in Z or a * v1 in Z ) assume v1 in Z ; ::_thesis: a * v1 in Z then consider Y1 being set such that A45: v1 in Y1 and A46: Y1 in rng f by TARSKI:def_4; consider y1 being set such that A47: y1 in dom f and A48: f . y1 = Y1 by A46, FUNCT_1:def_3; consider W1 being strict Subspace of V such that y1 = W1 and A49: f . y1 = the carrier of W1 by A19, A20, A47; v1 in W1 by A45, A48, A49, STRUCT_0:def_5; then a * v1 in W1 by RLSUB_1:21; then A50: a * v1 in the carrier of W1 by STRUCT_0:def_5; f . y1 in rng f by A47, FUNCT_1:def_3; hence a * v1 in Z by A49, A50, TARSKI:def_4; ::_thesis: verum end; set z = the Element of rng f; A51: rng f <> {} by A16, A19, RELAT_1:42; then consider z1 being set such that A52: z1 in dom f and A53: f . z1 = the Element of rng f by FUNCT_1:def_3; ex W3 being strict Subspace of V st ( z1 = W3 & f . z1 = the carrier of W3 ) by A19, A20, A52; then Z <> {} by A51, A53, ORDERS_1:6; then consider E being strict Subspace of V such that A54: Z = the carrier of E by A26, RLSUB_1:35; now__::_thesis:_for_u_being_VECTOR_of_V_holds_ (_(_u_in_W_/\_E_implies_u_in_(0)._V_)_&_(_u_in_(0)._V_implies_u_in_W_/\_E_)_) let u be VECTOR of V; ::_thesis: ( ( u in W /\ E implies u in (0). V ) & ( u in (0). V implies u in W /\ E ) ) thus ( u in W /\ E implies u in (0). V ) ::_thesis: ( u in (0). V implies u in W /\ E ) proof assume A55: u in W /\ E ; ::_thesis: u in (0). V then A56: u in W by Th3; u in E by A55, Th3; then u in Z by A54, STRUCT_0:def_5; then consider Y1 being set such that A57: u in Y1 and A58: Y1 in rng f by TARSKI:def_4; consider y1 being set such that A59: y1 in dom f and A60: f . y1 = Y1 by A58, FUNCT_1:def_3; A61: ex W2 being strict Subspace of V st ( y1 = W2 & W /\ W2 = (0). V ) by A1, A13, A19, A59; consider W1 being strict Subspace of V such that A62: y1 = W1 and A63: f . y1 = the carrier of W1 by A19, A20, A59; u in W1 by A57, A60, A63, STRUCT_0:def_5; hence u in (0). V by A62, A56, A61, Th3; ::_thesis: verum end; assume u in (0). V ; ::_thesis: u in W /\ E then u in the carrier of ((0). V) by STRUCT_0:def_5; then u in {(0. V)} by RLSUB_1:def_3; then u = 0. V by TARSKI:def_1; hence u in W /\ E by RLSUB_1:17; ::_thesis: verum end; then A64: W /\ E = (0). V by RLSUB_1:31; E in Subspaces V by Def3; then reconsider y9 = E as Element of X by A1, A64; take y = y9; ::_thesis: for x being Element of X st x in Y holds [x,y] in R let x be Element of X; ::_thesis: ( x in Y implies [x,y] in R ) assume A65: x in Y ; ::_thesis: [x,y] in R then consider W1 being strict Subspace of V such that A66: x = W1 and A67: f . x = the carrier of W1 by A20; now__::_thesis:_for_u_being_VECTOR_of_V_st_u_in_W1_holds_ u_in_E let u be VECTOR of V; ::_thesis: ( u in W1 implies u in E ) assume u in W1 ; ::_thesis: u in E then A68: u in the carrier of W1 by STRUCT_0:def_5; the carrier of W1 in rng f by A19, A65, A67, FUNCT_1:def_3; then u in Z by A68, TARSKI:def_4; hence u in E by A54, STRUCT_0:def_5; ::_thesis: verum end; then W1 is strict Subspace of E by RLSUB_1:29; hence [x,y] in R by A2, A66; ::_thesis: verum end; end; end; hence ex y being Element of X st for x being Element of X st x in Y holds [x,y] in R ; ::_thesis: verum end; then A69: for Y being set st Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S3[x,y] holds S3[y,x] ) holds ex y being Element of X st for x being Element of X st x in Y holds S3[x,y] ; now__::_thesis:_for_x,_y_being_Element_of_X_st_[x,y]_in_R_&_[y,x]_in_R_holds_ x_=_y let x, y be Element of X; ::_thesis: ( [x,y] in R & [y,x] in R implies x = y ) assume ( [x,y] in R & [y,x] in R ) ; ::_thesis: x = y then ( ex W1, W2 being strict Subspace of V st ( x = W1 & y = W2 & W1 is Subspace of W2 ) & ex W3, W4 being strict Subspace of V st ( y = W3 & x = W4 & W3 is Subspace of W4 ) ) by A2; hence x = y by RLSUB_1:26; ::_thesis: verum end; then A70: for x, y being Element of X st S3[x,y] & S3[y,x] holds x = y ; consider x being Element of X such that A71: for y being Element of X st x <> y holds not S3[x,y] from ORDERS_1:sch_1(A12, A70, A10, A69); consider L being strict Subspace of V such that A72: x = L and A73: W /\ L = (0). V by A1; take L ; ::_thesis: V is_the_direct_sum_of L,W thus RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = L + W :: according to RLSUB_2:def_4 ::_thesis: L /\ W = (0). V proof assume not RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = L + W ; ::_thesis: contradiction then consider v being VECTOR of V such that A74: for v1, v2 being VECTOR of V holds ( not v1 in L or not v2 in W or v <> v1 + v2 ) by Lm13; ( v = (0. V) + v & 0. V in W ) by RLSUB_1:17, RLVECT_1:4; then A75: not v in L by A74; set A = { (a * v) where a is Real : verum } ; A76: 1 * v in { (a * v) where a is Real : verum } ; now__::_thesis:_for_x_being_set_st_x_in__{__(a_*_v)_where_a_is_Real_:_verum__}__holds_ x_in_the_carrier_of_V let x be set ; ::_thesis: ( x in { (a * v) where a is Real : verum } implies x in the carrier of V ) assume x in { (a * v) where a is Real : verum } ; ::_thesis: x in the carrier of V then ex a being Real st x = a * v ; hence x in the carrier of V ; ::_thesis: verum end; then reconsider A = { (a * v) where a is Real : verum } as Subset of V by TARSKI:def_3; A is linearly-closed proof thus for v1, v2 being VECTOR of V st v1 in A & v2 in A holds v1 + v2 in A :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of K93() for b2 being Element of the carrier of V holds ( not b2 in A or b1 * b2 in A ) proof let v1, v2 be VECTOR of V; ::_thesis: ( v1 in A & v2 in A implies v1 + v2 in A ) assume v1 in A ; ::_thesis: ( not v2 in A or v1 + v2 in A ) then consider a1 being Real such that A77: v1 = a1 * v ; assume v2 in A ; ::_thesis: v1 + v2 in A then consider a2 being Real such that A78: v2 = a2 * v ; v1 + v2 = (a1 + a2) * v by A77, A78, RLVECT_1:def_6; hence v1 + v2 in A ; ::_thesis: verum end; let a be Real; ::_thesis: for b1 being Element of the carrier of V holds ( not b1 in A or a * b1 in A ) let v1 be VECTOR of V; ::_thesis: ( not v1 in A or a * v1 in A ) assume v1 in A ; ::_thesis: a * v1 in A then consider a1 being Real such that A79: v1 = a1 * v ; a * v1 = (a * a1) * v by A79, RLVECT_1:def_7; hence a * v1 in A ; ::_thesis: verum end; then consider Z being strict Subspace of V such that A80: the carrier of Z = A by A76, RLSUB_1:35; A81: not v in L + W by A74, Th1; now__::_thesis:_for_u_being_VECTOR_of_V_holds_ (_(_u_in_Z_/\_(W_+_L)_implies_u_in_(0)._V_)_&_(_u_in_(0)._V_implies_u_in_Z_/\_(W_+_L)_)_) let u be VECTOR of V; ::_thesis: ( ( u in Z /\ (W + L) implies u in (0). V ) & ( u in (0). V implies u in Z /\ (W + L) ) ) thus ( u in Z /\ (W + L) implies u in (0). V ) ::_thesis: ( u in (0). V implies u in Z /\ (W + L) ) proof assume A82: u in Z /\ (W + L) ; ::_thesis: u in (0). V then u in Z by Th3; then u in A by A80, STRUCT_0:def_5; then consider a being Real such that A83: u = a * v ; now__::_thesis:_not_a_<>_0 u in W + L by A82, Th3; then (a ") * (a * v) in W + L by A83, RLSUB_1:21; then A84: ((a ") * a) * v in W + L by RLVECT_1:def_7; assume a <> 0 ; ::_thesis: contradiction then 1 * v in W + L by A84, XCMPLX_0:def_7; then 1 * v in L + W by Lm1; hence contradiction by A81, RLVECT_1:def_8; ::_thesis: verum end; then u = 0. V by A83, RLVECT_1:10; hence u in (0). V by RLSUB_1:17; ::_thesis: verum end; assume u in (0). V ; ::_thesis: u in Z /\ (W + L) then u in the carrier of ((0). V) by STRUCT_0:def_5; then u in {(0. V)} by RLSUB_1:def_3; then u = 0. V by TARSKI:def_1; hence u in Z /\ (W + L) by RLSUB_1:17; ::_thesis: verum end; then A85: Z /\ (W + L) = (0). V by RLSUB_1:31; now__::_thesis:_for_u_being_VECTOR_of_V_holds_ (_(_u_in_(Z_+_L)_/\_W_implies_u_in_(0)._V_)_&_(_u_in_(0)._V_implies_u_in_(Z_+_L)_/\_W_)_) let u be VECTOR of V; ::_thesis: ( ( u in (Z + L) /\ W implies u in (0). V ) & ( u in (0). V implies u in (Z + L) /\ W ) ) thus ( u in (Z + L) /\ W implies u in (0). V ) ::_thesis: ( u in (0). V implies u in (Z + L) /\ W ) proof assume A86: u in (Z + L) /\ W ; ::_thesis: u in (0). V then u in Z + L by Th3; then consider v1, v2 being VECTOR of V such that A87: v1 in Z and A88: v2 in L and A89: u = v1 + v2 by Th1; A90: u in W by A86, Th3; then A91: u in W + L by Th2; ( v1 = u - v2 & v2 in W + L ) by A88, A89, Lm14, Th2; then v1 in W + L by A91, RLSUB_1:23; then v1 in Z /\ (W + L) by A87, Th3; then v1 in the carrier of ((0). V) by A85, STRUCT_0:def_5; then v1 in {(0. V)} by RLSUB_1:def_3; then v1 = 0. V by TARSKI:def_1; then v2 = u by A89, RLVECT_1:4; hence u in (0). V by A73, A88, A90, Th3; ::_thesis: verum end; assume u in (0). V ; ::_thesis: u in (Z + L) /\ W then u in the carrier of ((0). V) by STRUCT_0:def_5; then u in {(0. V)} by RLSUB_1:def_3; then u = 0. V by TARSKI:def_1; hence u in (Z + L) /\ W by RLSUB_1:17; ::_thesis: verum end; then (Z + L) /\ W = (0). V by RLSUB_1:31; then A92: W /\ (Z + L) = (0). V by Th14; Z + L in Subspaces V by Def3; then reconsider x1 = Z + L as Element of X by A1, A92; L is Subspace of Z + L by Th7; then A93: [x,x1] in R by A2, A72; v in A by A76, RLVECT_1:def_8; then v in Z by A80, STRUCT_0:def_5; then Z + L <> L by A75, Th2; hence contradiction by A71, A72, A93; ::_thesis: verum end; thus L /\ W = (0). V by A73, Th14; ::_thesis: verum end; definition let V be RealLinearSpace; let W be Subspace of V; mode Linear_Compl of W -> Subspace of V means :Def5: :: RLSUB_2:def 5 V is_the_direct_sum_of it,W; existence ex b1 being Subspace of V st V is_the_direct_sum_of b1,W proof ex C being strict Subspace of V st V is_the_direct_sum_of C,W by Lm15; hence ex b1 being Subspace of V st V is_the_direct_sum_of b1,W ; ::_thesis: verum end; end; :: deftheorem Def5 defines Linear_Compl RLSUB_2:def_5_:_ for V being RealLinearSpace for W, b3 being Subspace of V holds ( b3 is Linear_Compl of W iff V is_the_direct_sum_of b3,W ); registration let V be RealLinearSpace; let W be Subspace of V; cluster non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() for Linear_Compl of W; existence ex b1 being Linear_Compl of W st b1 is strict proof consider C being strict Subspace of V such that A1: V is_the_direct_sum_of C,W by Lm15; C is Linear_Compl of W by A1, Def5; hence ex b1 being Linear_Compl of W st b1 is strict ; ::_thesis: verum end; end; Lm16: for V being RealLinearSpace for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds V is_the_direct_sum_of W2,W1 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds V is_the_direct_sum_of W2,W1 let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1 ) assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: V is_the_direct_sum_of W2,W1 then W1 /\ W2 = (0). V by Def4; then A2: W2 /\ W1 = (0). V by Th14; RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 by A1, Def4; then RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W2 + W1 by Lm1; hence V is_the_direct_sum_of W2,W1 by A2, Def4; ::_thesis: verum end; theorem :: RLSUB_2:34 for V being RealLinearSpace for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds W2 is Linear_Compl of W1 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds W2 is Linear_Compl of W1 let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1 ) assume V is_the_direct_sum_of W1,W2 ; ::_thesis: W2 is Linear_Compl of W1 then V is_the_direct_sum_of W2,W1 by Lm16; hence W2 is Linear_Compl of W1 by Def5; ::_thesis: verum end; theorem Th35: :: RLSUB_2:35 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W holds ( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L ) proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W holds ( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L ) let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds ( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L ) let L be Linear_Compl of W; ::_thesis: ( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L ) thus V is_the_direct_sum_of L,W by Def5; ::_thesis: V is_the_direct_sum_of W,L hence V is_the_direct_sum_of W,L by Lm16; ::_thesis: verum end; theorem Th36: :: RLSUB_2:36 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W holds ( W + L = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & L + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W holds ( W + L = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & L + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds ( W + L = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & L + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) let L be Linear_Compl of W; ::_thesis: ( W + L = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & L + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) V is_the_direct_sum_of W,L by Th35; hence W + L = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Def4; ::_thesis: L + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) hence L + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm1; ::_thesis: verum end; theorem Th37: :: RLSUB_2:37 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W holds ( W /\ L = (0). V & L /\ W = (0). V ) proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W holds ( W /\ L = (0). V & L /\ W = (0). V ) let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds ( W /\ L = (0). V & L /\ W = (0). V ) let L be Linear_Compl of W; ::_thesis: ( W /\ L = (0). V & L /\ W = (0). V ) V is_the_direct_sum_of W,L by Th35; hence W /\ L = (0). V by Def4; ::_thesis: L /\ W = (0). V hence L /\ W = (0). V by Th14; ::_thesis: verum end; theorem :: RLSUB_2:38 for V being RealLinearSpace for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds V is_the_direct_sum_of W2,W1 by Lm16; theorem Th39: :: RLSUB_2:39 for V being RealLinearSpace holds ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) proof let V be RealLinearSpace; ::_thesis: ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) ( ((0). V) + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & (0). V = ((0). V) /\ ((Omega). V) ) by Th9, Th18; hence V is_the_direct_sum_of (0). V, (Omega). V by Def4; ::_thesis: V is_the_direct_sum_of (Omega). V, (0). V hence V is_the_direct_sum_of (Omega). V, (0). V by Lm16; ::_thesis: verum end; theorem :: RLSUB_2:40 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W holds W is Linear_Compl of L proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W holds W is Linear_Compl of L let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds W is Linear_Compl of L let L be Linear_Compl of W; ::_thesis: W is Linear_Compl of L V is_the_direct_sum_of L,W by Def5; then V is_the_direct_sum_of W,L by Lm16; hence W is Linear_Compl of L by Def5; ::_thesis: verum end; theorem :: RLSUB_2:41 for V being RealLinearSpace holds ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) proof let V be RealLinearSpace; ::_thesis: ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) by Th39; hence ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Def5; ::_thesis: verum end; theorem Th42: :: RLSUB_2:42 for V being RealLinearSpace for W1, W2 being Subspace of V for C1 being Coset of W1 for C2 being Coset of W2 st C1 meets C2 holds C1 /\ C2 is Coset of W1 /\ W2 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V for C1 being Coset of W1 for C2 being Coset of W2 st C1 meets C2 holds C1 /\ C2 is Coset of W1 /\ W2 let W1, W2 be Subspace of V; ::_thesis: for C1 being Coset of W1 for C2 being Coset of W2 st C1 meets C2 holds C1 /\ C2 is Coset of W1 /\ W2 let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 st C1 meets C2 holds C1 /\ C2 is Coset of W1 /\ W2 let C2 be Coset of W2; ::_thesis: ( C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2 ) set v = the Element of C1 /\ C2; set C = C1 /\ C2; assume A1: C1 /\ C2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: C1 /\ C2 is Coset of W1 /\ W2 then reconsider v = the Element of C1 /\ C2 as Element of V by TARSKI:def_3; v in C2 by A1, XBOOLE_0:def_4; then A2: C2 = v + W2 by RLSUB_1:78; v in C1 by A1, XBOOLE_0:def_4; then A3: C1 = v + W1 by RLSUB_1:78; C1 /\ C2 is Coset of W1 /\ W2 proof take v ; :: according to RLSUB_1:def_6 ::_thesis: C1 /\ C2 = v + (W1 /\ W2) thus C1 /\ C2 c= v + (W1 /\ W2) :: according to XBOOLE_0:def_10 ::_thesis: v + (W1 /\ W2) c= C1 /\ C2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in v + (W1 /\ W2) ) assume A4: x in C1 /\ C2 ; ::_thesis: x in v + (W1 /\ W2) then x in C1 by XBOOLE_0:def_4; then consider u1 being VECTOR of V such that A5: u1 in W1 and A6: x = v + u1 by A3, RLSUB_1:63; x in C2 by A4, XBOOLE_0:def_4; then consider u2 being VECTOR of V such that A7: u2 in W2 and A8: x = v + u2 by A2, RLSUB_1:63; u1 = u2 by A6, A8, RLVECT_1:8; then u1 in W1 /\ W2 by A5, A7, Th3; hence x in v + (W1 /\ W2) by A6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + (W1 /\ W2) or x in C1 /\ C2 ) assume x in v + (W1 /\ W2) ; ::_thesis: x in C1 /\ C2 then consider u being VECTOR of V such that A9: u in W1 /\ W2 and A10: x = v + u by RLSUB_1:63; u in W2 by A9, Th3; then A11: x in { (v + u2) where u2 is VECTOR of V : u2 in W2 } by A10; u in W1 by A9, Th3; then x in { (v + u1) where u1 is VECTOR of V : u1 in W1 } by A10; hence x in C1 /\ C2 by A3, A2, A11, XBOOLE_0:def_4; ::_thesis: verum end; hence C1 /\ C2 is Coset of W1 /\ W2 ; ::_thesis: verum end; Lm17: for V being RealLinearSpace for W being Subspace of V for v being VECTOR of V ex C being Coset of W st v in C proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for v being VECTOR of V ex C being Coset of W st v in C let W be Subspace of V; ::_thesis: for v being VECTOR of V ex C being Coset of W st v in C let v be VECTOR of V; ::_thesis: ex C being Coset of W st v in C reconsider C = v + W as Coset of W by RLSUB_1:def_6; take C ; ::_thesis: v in C thus v in C by RLSUB_1:43; ::_thesis: verum end; theorem Th43: :: RLSUB_2:43 for V being RealLinearSpace for W1, W2 being Subspace of V holds ( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1 for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds ( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1 for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} ) let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1 for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} ) set VW1 = the carrier of W1; set VW2 = the carrier of W2; 0. V in W2 by RLSUB_1:17; then A1: 0. V in the carrier of W2 by STRUCT_0:def_5; thus ( V is_the_direct_sum_of W1,W2 implies for C1 being Coset of W1 for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} ) ::_thesis: ( ( for C1 being Coset of W1 for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} ) implies V is_the_direct_sum_of W1,W2 ) proof assume A2: V is_the_direct_sum_of W1,W2 ; ::_thesis: for C1 being Coset of W1 for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} then A3: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 by Def4; let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} let C2 be Coset of W2; ::_thesis: ex v being VECTOR of V st C1 /\ C2 = {v} consider v1 being VECTOR of V such that A4: C1 = v1 + W1 by RLSUB_1:def_6; v1 in RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLVECT_1:1; then consider v11, v12 being VECTOR of V such that A5: v11 in W1 and A6: v12 in W2 and A7: v1 = v11 + v12 by A3, Th1; consider v2 being VECTOR of V such that A8: C2 = v2 + W2 by RLSUB_1:def_6; v2 in RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLVECT_1:1; then consider v21, v22 being VECTOR of V such that A9: v21 in W1 and A10: v22 in W2 and A11: v2 = v21 + v22 by A3, Th1; take v = v12 + v21; ::_thesis: C1 /\ C2 = {v} {v} = C1 /\ C2 proof thus A12: {v} c= C1 /\ C2 :: according to XBOOLE_0:def_10 ::_thesis: C1 /\ C2 c= {v} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in C1 /\ C2 ) assume x in {v} ; ::_thesis: x in C1 /\ C2 then A13: x = v by TARSKI:def_1; v21 = v2 - v22 by A11, Lm14; then v21 in C2 by A8, A10, RLSUB_1:64; then C2 = v21 + W2 by RLSUB_1:78; then A14: x in C2 by A6, A13; v12 = v1 - v11 by A7, Lm14; then v12 in C1 by A4, A5, RLSUB_1:64; then C1 = v12 + W1 by RLSUB_1:78; then x in C1 by A9, A13; hence x in C1 /\ C2 by A14, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in {v} ) assume A15: x in C1 /\ C2 ; ::_thesis: x in {v} then C1 meets C2 by XBOOLE_0:4; then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th42; A16: v in {v} by TARSKI:def_1; W1 /\ W2 = (0). V by A2, Def4; then ex u being VECTOR of V st C = {u} by RLSUB_1:73; hence x in {v} by A12, A15, A16, TARSKI:def_1; ::_thesis: verum end; hence C1 /\ C2 = {v} ; ::_thesis: verum end; assume A17: for C1 being Coset of W1 for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} ; ::_thesis: V is_the_direct_sum_of W1,W2 A18: the carrier of W2 is Coset of W2 by RLSUB_1:74; now__::_thesis:_for_u_being_VECTOR_of_V_holds_u_in_W1_+_W2 let u be VECTOR of V; ::_thesis: u in W1 + W2 consider C1 being Coset of W1 such that A19: u in C1 by Lm17; consider v being VECTOR of V such that A20: C1 /\ the carrier of W2 = {v} by A18, A17; A21: v in {v} by TARSKI:def_1; then v in C1 by A20, XBOOLE_0:def_4; then consider v1 being VECTOR of V such that A22: v1 in W1 and A23: u - v1 = v by A19, RLSUB_1:80; v in the carrier of W2 by A20, A21, XBOOLE_0:def_4; then A24: v in W2 by STRUCT_0:def_5; u = v1 + v by A23, Lm14; hence u in W1 + W2 by A24, A22, Th1; ::_thesis: verum end; hence RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 by Lm12; :: according to RLSUB_2:def_4 ::_thesis: W1 /\ W2 = (0). V the carrier of W1 is Coset of W1 by RLSUB_1:74; then consider v being VECTOR of V such that A25: the carrier of W1 /\ the carrier of W2 = {v} by A18, A17; 0. V in W1 by RLSUB_1:17; then 0. V in the carrier of W1 by STRUCT_0:def_5; then A26: 0. V in {v} by A25, A1, XBOOLE_0:def_4; the carrier of ((0). V) = {(0. V)} by RLSUB_1:def_3 .= the carrier of W1 /\ the carrier of W2 by A25, A26, TARSKI:def_1 .= the carrier of (W1 /\ W2) by Def2 ; hence W1 /\ W2 = (0). V by RLSUB_1:30; ::_thesis: verum end; theorem :: RLSUB_2:44 for V being RealLinearSpace for W1, W2 being Subspace of V holds ( W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st ( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) by Lm13; theorem Th45: :: RLSUB_2:45 for V being RealLinearSpace for W1, W2 being Subspace of V for v, v1, v2, u1, u2 being VECTOR of V st V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds ( v1 = u1 & v2 = u2 ) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V for v, v1, v2, u1, u2 being VECTOR of V st V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds ( v1 = u1 & v2 = u2 ) let W1, W2 be Subspace of V; ::_thesis: for v, v1, v2, u1, u2 being VECTOR of V st V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds ( v1 = u1 & v2 = u2 ) let v, v1, v2, u1, u2 be VECTOR of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies ( v1 = u1 & v2 = u2 ) ) reconsider C2 = v1 + W2 as Coset of W2 by RLSUB_1:def_6; reconsider C1 = the carrier of W1 as Coset of W1 by RLSUB_1:74; A1: v1 in C2 by RLSUB_1:43; assume V is_the_direct_sum_of W1,W2 ; ::_thesis: ( not v = v1 + v2 or not v = u1 + u2 or not v1 in W1 or not u1 in W1 or not v2 in W2 or not u2 in W2 or ( v1 = u1 & v2 = u2 ) ) then consider u being VECTOR of V such that A2: C1 /\ C2 = {u} by Th43; assume that A3: ( v = v1 + v2 & v = u1 + u2 ) and A4: v1 in W1 and A5: u1 in W1 and A6: ( v2 in W2 & u2 in W2 ) ; ::_thesis: ( v1 = u1 & v2 = u2 ) A7: v2 - u2 in W2 by A6, RLSUB_1:23; v1 in C1 by A4, STRUCT_0:def_5; then v1 in C1 /\ C2 by A1, XBOOLE_0:def_4; then A8: v1 = u by A2, TARSKI:def_1; u1 = (v1 + v2) - u2 by A3, Lm14 .= v1 + (v2 - u2) by RLVECT_1:def_3 ; then A9: u1 in C2 by A7; u1 in C1 by A5, STRUCT_0:def_5; then A10: u1 in C1 /\ C2 by A9, XBOOLE_0:def_4; hence v1 = u1 by A2, A8, TARSKI:def_1; ::_thesis: v2 = u2 u1 = u by A10, A2, TARSKI:def_1; hence v2 = u2 by A3, A8, RLVECT_1:8; ::_thesis: verum end; theorem :: RLSUB_2:46 for V being RealLinearSpace for W1, W2 being Subspace of V st V = W1 + W2 & ex v being VECTOR of V st for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds ( v1 = u1 & v2 = u2 ) holds V is_the_direct_sum_of W1,W2 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V = W1 + W2 & ex v being VECTOR of V st for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds ( v1 = u1 & v2 = u2 ) holds V is_the_direct_sum_of W1,W2 let W1, W2 be Subspace of V; ::_thesis: ( V = W1 + W2 & ex v being VECTOR of V st for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds ( v1 = u1 & v2 = u2 ) implies V is_the_direct_sum_of W1,W2 ) assume A1: V = W1 + W2 ; ::_thesis: ( for v being VECTOR of V ex v1, v2, u1, u2 being VECTOR of V st ( v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 & not ( v1 = u1 & v2 = u2 ) ) or V is_the_direct_sum_of W1,W2 ) ( the carrier of ((0). V) = {(0. V)} & (0). V is Subspace of W1 /\ W2 ) by RLSUB_1:39, RLSUB_1:def_3; then A2: {(0. V)} c= the carrier of (W1 /\ W2) by RLSUB_1:def_2; given v being VECTOR of V such that A3: for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds ( v1 = u1 & v2 = u2 ) ; ::_thesis: V is_the_direct_sum_of W1,W2 assume not V is_the_direct_sum_of W1,W2 ; ::_thesis: contradiction then W1 /\ W2 <> (0). V by A1, Def4; then the carrier of (W1 /\ W2) <> {(0. V)} by RLSUB_1:def_3; then {(0. V)} c< the carrier of (W1 /\ W2) by A2, XBOOLE_0:def_8; then consider x being set such that A4: x in the carrier of (W1 /\ W2) and A5: not x in {(0. V)} by XBOOLE_0:6; A6: x <> 0. V by A5, TARSKI:def_1; A7: x in W1 /\ W2 by A4, STRUCT_0:def_5; then x in V by RLSUB_1:9; then reconsider u = x as VECTOR of V by STRUCT_0:def_5; consider v1, v2 being VECTOR of V such that A8: v1 in W1 and A9: v2 in W2 and A10: v = v1 + v2 by A1, Lm13; A11: v = (v1 + v2) + (0. V) by A10, RLVECT_1:4 .= (v1 + v2) + (u - u) by RLVECT_1:15 .= ((v1 + v2) + u) - u by RLVECT_1:def_3 .= ((v1 + u) + v2) - u by RLVECT_1:def_3 .= (v1 + u) + (v2 - u) by RLVECT_1:def_3 ; x in W2 by A7, Th3; then A12: v2 - u in W2 by A9, RLSUB_1:23; x in W1 by A7, Th3; then v1 + u in W1 by A8, RLSUB_1:20; then v2 - u = v2 by A3, A8, A9, A10, A11, A12 .= v2 - (0. V) by RLVECT_1:13 ; hence contradiction by A6, RLVECT_1:23; ::_thesis: verum end; definition let V be RealLinearSpace; let v be VECTOR of V; let W1, W2 be Subspace of V; assume A1: V is_the_direct_sum_of W1,W2 ; funcv |-- (W1,W2) -> Element of [: the carrier of V, the carrier of V:] means :Def6: :: RLSUB_2:def 6 ( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 ); existence ex b1 being Element of [: the carrier of V, the carrier of V:] st ( v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 ) proof W1 + W2 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A1, Def4; then consider v1, v2 being VECTOR of V such that A2: ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by Lm13; take [v1,v2] ; ::_thesis: ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 ) [v1,v2] `1 = v1 by MCART_1:7; hence ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 ) by A2, MCART_1:7; ::_thesis: verum end; uniqueness for b1, b2 being Element of [: the carrier of V, the carrier of V:] st v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 & v = (b2 `1) + (b2 `2) & b2 `1 in W1 & b2 `2 in W2 holds b1 = b2 proof let t1, t2 be Element of [: the carrier of V, the carrier of V:]; ::_thesis: ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 implies t1 = t2 ) assume ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 ) ; ::_thesis: t1 = t2 then A3: ( t1 `1 = t2 `1 & t1 `2 = t2 `2 ) by A1, Th45; t1 = [(t1 `1),(t1 `2)] by MCART_1:21; hence t1 = t2 by A3, MCART_1:21; ::_thesis: verum end; end; :: deftheorem Def6 defines |-- RLSUB_2:def_6_:_ for V being RealLinearSpace for v being VECTOR of V for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds for b5 being Element of [: the carrier of V, the carrier of V:] holds ( b5 = v |-- (W1,W2) iff ( v = (b5 `1) + (b5 `2) & b5 `1 in W1 & b5 `2 in W2 ) ); theorem Th47: :: RLSUB_2:47 for V being RealLinearSpace for W1, W2 being Subspace of V for v being VECTOR of V st V is_the_direct_sum_of W1,W2 holds (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V for v being VECTOR of V st V is_the_direct_sum_of W1,W2 holds (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 let W1, W2 be Subspace of V; ::_thesis: for v being VECTOR of V st V is_the_direct_sum_of W1,W2 holds (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 let v be VECTOR of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 ) assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 then A2: (v |-- (W1,W2)) `2 in W2 by Def6; A3: V is_the_direct_sum_of W2,W1 by A1, Lm16; then A4: ( v = ((v |-- (W2,W1)) `2) + ((v |-- (W2,W1)) `1) & (v |-- (W2,W1)) `1 in W2 ) by Def6; A5: (v |-- (W2,W1)) `2 in W1 by A3, Def6; ( v = ((v |-- (W1,W2)) `1) + ((v |-- (W1,W2)) `2) & (v |-- (W1,W2)) `1 in W1 ) by A1, Def6; hence (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 by A1, A2, A4, A5, Th45; ::_thesis: verum end; theorem Th48: :: RLSUB_2:48 for V being RealLinearSpace for W1, W2 being Subspace of V for v being VECTOR of V st V is_the_direct_sum_of W1,W2 holds (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V for v being VECTOR of V st V is_the_direct_sum_of W1,W2 holds (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 let W1, W2 be Subspace of V; ::_thesis: for v being VECTOR of V st V is_the_direct_sum_of W1,W2 holds (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 let v be VECTOR of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 ) assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 then A2: (v |-- (W1,W2)) `2 in W2 by Def6; A3: V is_the_direct_sum_of W2,W1 by A1, Lm16; then A4: ( v = ((v |-- (W2,W1)) `2) + ((v |-- (W2,W1)) `1) & (v |-- (W2,W1)) `1 in W2 ) by Def6; A5: (v |-- (W2,W1)) `2 in W1 by A3, Def6; ( v = ((v |-- (W1,W2)) `1) + ((v |-- (W1,W2)) `2) & (v |-- (W1,W2)) `1 in W1 ) by A1, Def6; hence (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 by A1, A2, A4, A5, Th45; ::_thesis: verum end; theorem :: RLSUB_2:49 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds t = v |-- (W,L) proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds t = v |-- (W,L) let W be Subspace of V; ::_thesis: for L being Linear_Compl of W for v being VECTOR of V for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds t = v |-- (W,L) let L be Linear_Compl of W; ::_thesis: for v being VECTOR of V for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds t = v |-- (W,L) V is_the_direct_sum_of W,L by Th35; hence for v being VECTOR of V for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds t = v |-- (W,L) by Def6; ::_thesis: verum end; theorem :: RLSUB_2:50 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v let W be Subspace of V; ::_thesis: for L being Linear_Compl of W for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v let L be Linear_Compl of W; ::_thesis: for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v V is_the_direct_sum_of W,L by Th35; hence for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v by Def6; ::_thesis: verum end; theorem :: RLSUB_2:51 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V holds ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L ) proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V holds ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L ) let W be Subspace of V; ::_thesis: for L being Linear_Compl of W for v being VECTOR of V holds ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L ) let L be Linear_Compl of W; ::_thesis: for v being VECTOR of V holds ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L ) V is_the_direct_sum_of W,L by Th35; hence for v being VECTOR of V holds ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L ) by Def6; ::_thesis: verum end; theorem :: RLSUB_2:52 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2 proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2 let W be Subspace of V; ::_thesis: for L being Linear_Compl of W for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2 let L be Linear_Compl of W; ::_thesis: for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2 V is_the_direct_sum_of W,L by Th35; hence for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2 by Th47; ::_thesis: verum end; theorem :: RLSUB_2:53 for V being RealLinearSpace for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1 proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for L being Linear_Compl of W for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1 let W be Subspace of V; ::_thesis: for L being Linear_Compl of W for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1 let L be Linear_Compl of W; ::_thesis: for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1 V is_the_direct_sum_of W,L by Th35; hence for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1 by Th48; ::_thesis: verum end; definition let V be RealLinearSpace; func SubJoin V -> BinOp of (Subspaces V) means :Def7: :: RLSUB_2:def 7 for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds it . (A1,A2) = W1 + W2; existence ex b1 being BinOp of (Subspaces V) st for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b1 . (A1,A2) = W1 + W2 proof defpred S1[ Element of Subspaces V, Element of Subspaces V, Element of Subspaces V] means for W1, W2 being Subspace of V st \$1 = W1 & \$2 = W2 holds \$3 = W1 + W2; A1: for A1, A2 being Element of Subspaces V ex B being Element of Subspaces V st S1[A1,A2,B] proof let A1, A2 be Element of Subspaces V; ::_thesis: ex B being Element of Subspaces V st S1[A1,A2,B] reconsider W1 = A1, W2 = A2 as Subspace of V by Def3; reconsider C = W1 + W2 as Element of Subspaces V by Def3; take C ; ::_thesis: S1[A1,A2,C] thus S1[A1,A2,C] ; ::_thesis: verum end; ex o being BinOp of (Subspaces V) st for a, b being Element of Subspaces V holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); hence ex b1 being BinOp of (Subspaces V) st for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b1 . (A1,A2) = W1 + W2 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Subspaces V) st ( for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b2 . (A1,A2) = W1 + W2 ) holds b1 = b2 proof let o1, o2 be BinOp of (Subspaces V); ::_thesis: ( ( for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds o1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds o2 . (A1,A2) = W1 + W2 ) implies o1 = o2 ) assume A2: for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds o1 . (A1,A2) = W1 + W2 ; ::_thesis: ( ex A1, A2 being Element of Subspaces V ex W1, W2 being Subspace of V st ( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 + W2 ) or o1 = o2 ) assume A3: for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds o2 . (A1,A2) = W1 + W2 ; ::_thesis: o1 = o2 now__::_thesis:_for_x,_y_being_set_st_x_in_Subspaces_V_&_y_in_Subspaces_V_holds_ o1_._(x,y)_=_o2_._(x,y) let x, y be set ; ::_thesis: ( x in Subspaces V & y in Subspaces V implies o1 . (x,y) = o2 . (x,y) ) assume A4: ( x in Subspaces V & y in Subspaces V ) ; ::_thesis: o1 . (x,y) = o2 . (x,y) then reconsider A = x, B = y as Element of Subspaces V ; reconsider W1 = x, W2 = y as Subspace of V by A4, Def3; o1 . (A,B) = W1 + W2 by A2; hence o1 . (x,y) = o2 . (x,y) by A3; ::_thesis: verum end; hence o1 = o2 by BINOP_1:1; ::_thesis: verum end; end; :: deftheorem Def7 defines SubJoin RLSUB_2:def_7_:_ for V being RealLinearSpace for b2 being BinOp of (Subspaces V) holds ( b2 = SubJoin V iff for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b2 . (A1,A2) = W1 + W2 ); definition let V be RealLinearSpace; func SubMeet V -> BinOp of (Subspaces V) means :Def8: :: RLSUB_2:def 8 for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds it . (A1,A2) = W1 /\ W2; existence ex b1 being BinOp of (Subspaces V) st for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b1 . (A1,A2) = W1 /\ W2 proof defpred S1[ Element of Subspaces V, Element of Subspaces V, Element of Subspaces V] means for W1, W2 being Subspace of V st \$1 = W1 & \$2 = W2 holds \$3 = W1 /\ W2; A1: for A1, A2 being Element of Subspaces V ex B being Element of Subspaces V st S1[A1,A2,B] proof let A1, A2 be Element of Subspaces V; ::_thesis: ex B being Element of Subspaces V st S1[A1,A2,B] reconsider W1 = A1, W2 = A2 as Subspace of V by Def3; reconsider C = W1 /\ W2 as Element of Subspaces V by Def3; take C ; ::_thesis: S1[A1,A2,C] thus S1[A1,A2,C] ; ::_thesis: verum end; ex o being BinOp of (Subspaces V) st for a, b being Element of Subspaces V holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); hence ex b1 being BinOp of (Subspaces V) st for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b1 . (A1,A2) = W1 /\ W2 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Subspaces V) st ( for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b2 . (A1,A2) = W1 /\ W2 ) holds b1 = b2 proof let o1, o2 be BinOp of (Subspaces V); ::_thesis: ( ( for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds o1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds o2 . (A1,A2) = W1 /\ W2 ) implies o1 = o2 ) assume A2: for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds o1 . (A1,A2) = W1 /\ W2 ; ::_thesis: ( ex A1, A2 being Element of Subspaces V ex W1, W2 being Subspace of V st ( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 /\ W2 ) or o1 = o2 ) assume A3: for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds o2 . (A1,A2) = W1 /\ W2 ; ::_thesis: o1 = o2 now__::_thesis:_for_x,_y_being_set_st_x_in_Subspaces_V_&_y_in_Subspaces_V_holds_ o1_._(x,y)_=_o2_._(x,y) let x, y be set ; ::_thesis: ( x in Subspaces V & y in Subspaces V implies o1 . (x,y) = o2 . (x,y) ) assume A4: ( x in Subspaces V & y in Subspaces V ) ; ::_thesis: o1 . (x,y) = o2 . (x,y) then reconsider A = x, B = y as Element of Subspaces V ; reconsider W1 = x, W2 = y as Subspace of V by A4, Def3; o1 . (A,B) = W1 /\ W2 by A2; hence o1 . (x,y) = o2 . (x,y) by A3; ::_thesis: verum end; hence o1 = o2 by BINOP_1:1; ::_thesis: verum end; end; :: deftheorem Def8 defines SubMeet RLSUB_2:def_8_:_ for V being RealLinearSpace for b2 being BinOp of (Subspaces V) holds ( b2 = SubMeet V iff for A1, A2 being Element of Subspaces V for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds b2 . (A1,A2) = W1 /\ W2 ); theorem Th54: :: RLSUB_2:54 for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice proof let V be RealLinearSpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); A1: for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" B = B "/\" A proof let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" B = B "/\" A reconsider W1 = A, W2 = B as Subspace of V by Def3; thus A "/\" B = W1 /\ W2 by Def8 .= W2 /\ W1 by Th14 .= B "/\" A by Def8 ; ::_thesis: verum end; A2: for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds (A "/\" B) "\/" B = B proof let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: (A "/\" B) "\/" B = B reconsider W1 = A, W2 = B as strict Subspace of V by Def3; reconsider AB = W1 /\ W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; thus (A "/\" B) "\/" B = (SubJoin V) . (AB,B) by Def8 .= (W1 /\ W2) + W2 by Def7 .= B by Lm6, RLSUB_1:30 ; ::_thesis: verum end; A3: for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C proof let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "\/" (B "\/" C) = (A "\/" B) "\/" C reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3; reconsider AB = W1 + W2, BC = W2 + W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; thus A "\/" (B "\/" C) = (SubJoin V) . (A,BC) by Def7 .= W1 + (W2 + W3) by Def7 .= (W1 + W2) + W3 by Th6 .= (SubJoin V) . (AB,C) by Def7 .= (A "\/" B) "\/" C by Def7 ; ::_thesis: verum end; A4: for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (A "\/" B) = A proof let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" (A "\/" B) = A reconsider W1 = A, W2 = B as strict Subspace of V by Def3; reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; thus A "/\" (A "\/" B) = (SubMeet V) . (A,AB) by Def7 .= W1 /\ (W1 + W2) by Def8 .= A by Lm7, RLSUB_1:30 ; ::_thesis: verum end; A5: for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C proof let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" (B "/\" C) = (A "/\" B) "/\" C reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3; reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; thus A "/\" (B "/\" C) = (SubMeet V) . (A,BC) by Def8 .= W1 /\ (W2 /\ W3) by Def8 .= (W1 /\ W2) /\ W3 by Th15 .= (SubMeet V) . (AB,C) by Def8 .= (A "/\" B) "/\" C by Def8 ; ::_thesis: verum end; for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" B = B "\/" A proof let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "\/" B = B "\/" A reconsider W1 = A, W2 = B as Subspace of V by Def3; thus A "\/" B = W1 + W2 by Def7 .= W2 + W1 by Lm1 .= B "\/" A by Def7 ; ::_thesis: verum end; then ( LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-commutative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-associative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-absorbing & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-commutative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-associative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-absorbing ) by A3, A2, A1, A5, A4, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice ; ::_thesis: verum end; registration let V be RealLinearSpace; cluster LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) -> Lattice-like ; coherence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice-like by Th54; end; theorem Th55: :: RLSUB_2:55 for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded proof let V be RealLinearSpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ex C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) st for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds ( C "/\" A = C & A "/\" C = C ) proof reconsider C = (0). V as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; take C ; ::_thesis: for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds ( C "/\" A = C & A "/\" C = C ) let A be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: ( C "/\" A = C & A "/\" C = C ) reconsider W = A as Subspace of V by Def3; thus C "/\" A = ((0). V) /\ W by Def8 .= C by Th18 ; ::_thesis: A "/\" C = C hence A "/\" C = C ; ::_thesis: verum end; hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded by LATTICES:def_13; ::_thesis: verum end; theorem Th56: :: RLSUB_2:56 for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded proof let V be RealLinearSpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ex C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) st for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds ( C "\/" A = C & A "\/" C = C ) proof reconsider C = (Omega). V as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; take C ; ::_thesis: for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds ( C "\/" A = C & A "\/" C = C ) let A be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: ( C "\/" A = C & A "\/" C = C ) reconsider W = A as Subspace of V by Def3; thus C "\/" A = ((Omega). V) + W by Def7 .= C by Th11 ; ::_thesis: A "\/" C = C hence A "\/" C = C ; ::_thesis: verum end; hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded by LATTICES:def_14; ::_thesis: verum end; theorem Th57: :: RLSUB_2:57 for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice proof let V be RealLinearSpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded upper-bounded Lattice by Th55, Th56; hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice ; ::_thesis: verum end; theorem Th58: :: RLSUB_2:58 for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular proof let V be RealLinearSpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) st A [= C holds A "\/" (B "/\" C) = (A "\/" B) "/\" C proof let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: ( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C ) reconsider W1 = A, W2 = B, W3 = C as strict Subspace of V by Def3; assume A1: A [= C ; ::_thesis: A "\/" (B "/\" C) = (A "\/" B) "/\" C reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; reconsider BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; W1 + W3 = A "\/" C by Def7 .= W3 by A1, LATTICES:def_3 ; then A2: W1 is Subspace of W3 by Th8; thus A "\/" (B "/\" C) = (SubJoin V) . (A,BC) by Def8 .= W1 + (W2 /\ W3) by Def7 .= (W1 + W2) /\ W3 by A2, Th29 .= (SubMeet V) . (AB,C) by Def8 .= (A "\/" B) "/\" C by Def7 ; ::_thesis: verum end; hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular by LATTICES:def_12; ::_thesis: verum end; Lm18: for l being Lattice for a, b being Element of l holds ( a is_a_complement_of b iff ( a "\/" b = Top l & a "/\" b = Bottom l ) ) proof let l be Lattice; ::_thesis: for a, b being Element of l holds ( a is_a_complement_of b iff ( a "\/" b = Top l & a "/\" b = Bottom l ) ) let a, b be Element of l; ::_thesis: ( a is_a_complement_of b iff ( a "\/" b = Top l & a "/\" b = Bottom l ) ) ( ( not a "\/" b = Top l or not a "/\" b = Bottom l ) implies not a is_a_complement_of b ) proof assume ( not a "\/" b = Top l or not a "/\" b = Bottom l ) ; ::_thesis: not a is_a_complement_of b hence ( not a "\/" b = Top l or not b "\/" a = Top l or not a "/\" b = Bottom l or not b "/\" a = Bottom l ) ; :: according to LATTICES:def_18 ::_thesis: verum end; hence ( a is_a_complement_of b implies ( a "\/" b = Top l & a "/\" b = Bottom l ) ) ; ::_thesis: ( a "\/" b = Top l & a "/\" b = Bottom l implies a is_a_complement_of b ) assume ( a "\/" b = Top l & a "/\" b = Bottom l ) ; ::_thesis: a is_a_complement_of b hence ( a "\/" b = Top l & b "\/" a = Top l & a "/\" b = Bottom l & b "/\" a = Bottom l ) ; :: according to LATTICES:def_18 ::_thesis: verum end; Lm19: for l being Lattice for b being Element of l st ( for a being Element of l holds a "/\" b = b ) holds b = Bottom l proof let l be Lattice; ::_thesis: for b being Element of l st ( for a being Element of l holds a "/\" b = b ) holds b = Bottom l let b be Element of l; ::_thesis: ( ( for a being Element of l holds a "/\" b = b ) implies b = Bottom l ) assume A1: for a being Element of l holds a "/\" b = b ; ::_thesis: b = Bottom l then for a being Element of l holds ( a "/\" b = b & b "/\" a = b ) ; then l is lower-bounded by LATTICES:def_13; hence Bottom l = (Bottom l) "/\" b .= b by A1 ; ::_thesis: verum end; Lm20: for l being Lattice for b being Element of l st ( for a being Element of l holds a "\/" b = b ) holds b = Top l proof let l be Lattice; ::_thesis: for b being Element of l st ( for a being Element of l holds a "\/" b = b ) holds b = Top l let b be Element of l; ::_thesis: ( ( for a being Element of l holds a "\/" b = b ) implies b = Top l ) assume A1: for a being Element of l holds a "\/" b = b ; ::_thesis: b = Top l then for a being Element of l holds ( b "\/" a = b & a "\/" b = b ) ; then l is upper-bounded by LATTICES:def_14; hence Top l = (Top l) "\/" b .= b by A1 ; ::_thesis: verum end; theorem Th59: :: RLSUB_2:59 for V being RealLinearSpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented proof let V be RealLinearSpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented reconsider S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) as 01_Lattice by Th57; reconsider S0 = S as 0_Lattice ; reconsider S1 = S as 1_Lattice ; reconsider Z = (0). V, I = (Omega). V as Element of S by Def3; reconsider Z0 = Z as Element of S0 ; reconsider I1 = I as Element of S1 ; now__::_thesis:_for_A_being_Element_of_S0_holds_A_"/\"_Z0_=_Z0 let A be Element of S0; ::_thesis: A "/\" Z0 = Z0 reconsider W = A as Subspace of V by Def3; thus A "/\" Z0 = W /\ ((0). V) by Def8 .= Z0 by Th18 ; ::_thesis: verum end; then A1: Bottom S = Z by Lm19; now__::_thesis:_for_A_being_Element_of_S1_holds_A_"\/"_I1_=_(Omega)._V let A be Element of S1; ::_thesis: A "\/" I1 = (Omega). V reconsider W = A as Subspace of V by Def3; thus A "\/" I1 = W + ((Omega). V) by Def7 .= (Omega). V by Th11 ; ::_thesis: verum end; then A2: Top S = I by Lm20; now__::_thesis:_for_A_being_Element_of_S_ex_B_being_Element_of_S_st_B_is_a_complement_of_A let A be Element of S; ::_thesis: ex B being Element of S st B is_a_complement_of A reconsider W = A as Subspace of V by Def3; set L = the strict Linear_Compl of W; reconsider B9 = the strict Linear_Compl of W as Element of S by Def3; take B = B9; ::_thesis: B is_a_complement_of A A3: B "/\" A = the strict Linear_Compl of W /\ W by Def8 .= Bottom S by A1, Th37 ; B "\/" A = the strict Linear_Compl of W + W by Def7 .= Top S by A2, Th36 ; hence B is_a_complement_of A by A3, Lm18; ::_thesis: verum end; hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented by LATTICES:def_19; ::_thesis: verum end; registration let V be RealLinearSpace; cluster LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) -> modular lower-bounded upper-bounded complemented ; coherence ( LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented ) by Th55, Th56, Th58, Th59; end; theorem :: RLSUB_2:60 for V being RealLinearSpace for W1, W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds W1 /\ W3 is Subspace of W2 /\ W3 proof let V be RealLinearSpace; ::_thesis: for W1, W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds W1 /\ W3 is Subspace of W2 /\ W3 let W1, W2, W3 be strict Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 ) set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); reconsider A = W1, B = W2, C = W3, AC = W1 /\ W3, BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3; assume A1: W1 is Subspace of W2 ; ::_thesis: W1 /\ W3 is Subspace of W2 /\ W3 A "\/" B = W1 + W2 by Def7 .= B by A1, Th8 ; then A [= B by LATTICES:def_3; then A "/\" C [= B "/\" C by LATTICES:9; then A2: (A "/\" C) "\/" (B "/\" C) = B "/\" C by LATTICES:def_3; A3: B "/\" C = W2 /\ W3 by Def8; (A "/\" C) "\/" (B "/\" C) = (SubJoin V) . (((SubMeet V) . (A,C)),BC) by Def8 .= (SubJoin V) . (AC,BC) by Def8 .= (W1 /\ W3) + (W2 /\ W3) by Def7 ; hence W1 /\ W3 is Subspace of W2 /\ W3 by A2, A3, Th8; ::_thesis: verum end; theorem :: RLSUB_2:61 for V being non empty right_complementable add-associative right_zeroed addLoopStr for v, v1, v2 being Element of V holds ( v = v1 + v2 iff v1 = v - v2 ) by Lm14; theorem :: RLSUB_2:62 for V being RealLinearSpace for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm12; theorem :: RLSUB_2:63 for V being RealLinearSpace for W being Subspace of V for v being VECTOR of V ex C being Coset of W st v in C by Lm17; theorem :: RLSUB_2:64 for l being Lattice for b being Element of l st ( for a being Element of l holds a "/\" b = b ) holds b = Bottom l by Lm19; theorem :: RLSUB_2:65 for l being Lattice for b being Element of l st ( for a being Element of l holds a "\/" b = b ) holds b = Top l by Lm20;