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 holds W1 + (W2 + W3) = (W1 + 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 holds W1 + (W2 + W3) = (W1 + W2) + W3
let W1, W2, W3 be Subspace of M; W1 + (W2 + W3) = (W1 + W2) + W3
set A = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where u, v is Element of M : ( v in W2 & u in W3 ) } ;
set C = { (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) } ;
set D = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) } ;
A1:
the carrier of (W1 + (W2 + W3)) = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) }
by Def1;
A2:
{ (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in { (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) } or x in { (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) } )
assume
x in { (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) }
;
x in { (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) }
then consider u,
v being
Element of
M such that A3:
x = v + u
and A4:
v in W1 + W2
and A5:
u in W3
;
v in the
carrier of
(W1 + W2)
by A4, STRUCT_0:def 5;
then
v in { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) }
by Def1;
then consider u2,
u1 being
Element of
M such that A6:
v = u1 + u2
and A7:
u1 in W1
and A8:
u2 in W2
;
u2 + u in { (v + u) where u, v is Element of M : ( v in W2 & u in W3 ) }
by A5, A8;
then
u2 + u in the
carrier of
(W2 + W3)
by Def1;
then A9:
u2 + u in W2 + W3
by STRUCT_0:def 5;
v + u = u1 + (u2 + u)
by A6, RLVECT_1:def 3;
hence
x in { (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) }
by A3, A7, A9;
verum
end;
{ (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) } c= { (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in { (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) } or x in { (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) } )
assume
x in { (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) }
;
x in { (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) }
then consider u,
v being
Element of
M such that A10:
x = v + u
and A11:
v in W1
and A12:
u in W2 + W3
;
u in the
carrier of
(W2 + W3)
by A12, STRUCT_0:def 5;
then
u in { (v + u) where u, v is Element of M : ( v in W2 & u in W3 ) }
by Def1;
then consider u2,
u1 being
Element of
M such that A13:
u = u1 + u2
and A14:
u1 in W2
and A15:
u2 in W3
;
v + u1 in { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) }
by A11, A14;
then
v + u1 in the
carrier of
(W1 + W2)
by Def1;
then A16:
v + u1 in W1 + W2
by STRUCT_0:def 5;
v + u = (v + u1) + u2
by A13, RLVECT_1:def 3;
hence
x in { (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) }
by A10, A15, A16;
verum
end;
then
{ (v + u) where u, v is Element of M : ( v in W1 & u in W2 + W3 ) } = { (v + u) where u, v is Element of M : ( v in W1 + W2 & u in W3 ) }
by A2;
hence
W1 + (W2 + W3) = (W1 + W2) + W3
by A1, Def1; verum