let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for M being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3
let M be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3
let W1, W2, W3 be Subspace of M; :: thesis: W1 + (W2 + W3) = (W1 + W2) + W3
set A = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where v, u is Element of M : ( v in W2 & u in W3 ) } ;
set C = { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } ;
set D = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } ;
A1:
( the carrier of (W1 + (W2 + W3)) = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } & the carrier of ((W1 + W2) + W3) = { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } )
by Def1;
A2:
{ (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } c= { (v + u) where v, u is Element of M : ( 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 Element of M : ( v in W1 & u in W2 + W3 ) } or x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } )
assume
x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) }
;
:: thesis: x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) }
then consider v,
u being
Element of
M such that A3:
x = v + u
and A4:
v in W1
and A5:
u in W2 + W3
;
u in the
carrier of
(W2 + W3)
by A5, STRUCT_0:def 5;
then
u in { (v + u) where v, u is Element of M : ( v in W2 & u in W3 ) }
by Def1;
then consider u1,
u2 being
Element of
M such that A6:
u = u1 + u2
and A7:
u1 in W2
and A8:
u2 in W3
;
A9:
v + u = (v + u1) + u2
by A6, RLVECT_1:def 6;
v + u1 in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) }
by A4, A7;
then
v + u1 in the
carrier of
(W1 + W2)
by Def1;
then
v + u1 in W1 + W2
by STRUCT_0:def 5;
hence
x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) }
by A3, A8, A9;
:: thesis: verum
end;
{ (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where v, u is Element of M : ( 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 Element of M : ( v in W1 + W2 & u in W3 ) } or x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } )
assume
x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) }
;
:: thesis: x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) }
then consider v,
u being
Element of
M such that A10:
x = v + u
and A11:
v in W1 + W2
and A12:
u in W3
;
v in the
carrier of
(W1 + W2)
by A11, STRUCT_0:def 5;
then
v in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) }
by Def1;
then consider u1,
u2 being
Element of
M such that A13:
v = u1 + u2
and A14:
u1 in W1
and A15:
u2 in W2
;
A16:
v + u = u1 + (u2 + u)
by A13, RLVECT_1:def 6;
u2 + u in { (v + u) where v, u is Element of M : ( v in W2 & u in W3 ) }
by A12, A15;
then
u2 + u in the
carrier of
(W2 + W3)
by Def1;
then
u2 + u in W2 + W3
by STRUCT_0:def 5;
hence
x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) }
by A10, A14, A16;
:: thesis: verum
end;
then
{ (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } = { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) }
by A2, XBOOLE_0:def 10;
hence
W1 + (W2 + W3) = (W1 + W2) + W3
by A1, VECTSP_4:37; :: thesis: verum