let V be RealUnitarySpace; 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; ( 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
; 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))
XBOOLE_0:def 10 the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))proof
let x be
object ;
TARSKI:def 3 ( 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))
;
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, RUSUB_1:1;
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, RUSUB_1:17;
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;
verum
end;
thus
the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
by Lm8; verum