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))

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;

x in W1 by A2, STRUCT_0:def 5;

then x in { (u + v) where v, u 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

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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W1 or x in the carrier of (W1 /\ (W1 + W2)) )
let x be object ; :: 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;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

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;

x in W1 by A2, STRUCT_0:def 5;

then x in { (u + v) where v, u 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