let R be Ring; :: thesis: for V being LeftMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let V be LeftMod of R; :: thesis: for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let W1, W2 be Submodule 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 /\ (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 VECTSP_5:def 2;
hence x in the carrier of W1 by A1, XBOOLE_0:def 4; :: thesis: verum
end;
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)) )
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 VECTSP_4:def 2;
then reconsider x1 = x as Element of V by A2;
A3: ( x1 + (0. V) = x1 & 0. V in W2 ) by Th33, RLVECT_1:4;
x in W1 by A2;
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 VECTSP_5:def 1;
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 VECTSP_5:def 2; :: thesis: verum