let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; for W1, W2, W3 being Subspace of M 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 M; ( 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 v, u is Element of M : ( u in W1 & v in W3 ) }
by Def1;
then consider v1,
u1 being
Element of
M such that A3:
x = u1 + v1
and A4:
u1 in W1
and A5:
v1 in W3
;
A6:
u1 in W2
by A1, A4, VECTSP_4: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, VECTSP_4:23;
then
v1 + (u1 - u1) in W2
by RLVECT_1:def 3;
then
v1 + (0. M) in W2
by VECTSP_1:19;
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 Lm12; verum