let V be RealLinearSpace; :: thesis: for W1, W2, W3 being Subspace of V holds W1 + (W2 + W3) = (W1 + W2) + W3

let W1, W2, W3 be Subspace of V; :: thesis: W1 + (W2 + W3) = (W1 + W2) + W3

set A = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ;

set B = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W3 ) } ;

set C = { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ;

set D = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ;

A1: the carrier of (W1 + (W2 + W3)) = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } by Def1;

A2: { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) }

hence W1 + (W2 + W3) = (W1 + W2) + W3 by A1, Def1; :: thesis: verum

let W1, W2, W3 be Subspace of V; :: thesis: W1 + (W2 + W3) = (W1 + W2) + W3

set A = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ;

set B = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W3 ) } ;

set C = { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ;

set D = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ;

A1: the carrier of (W1 + (W2 + W3)) = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } by Def1;

A2: { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) }

proof

{ (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } c= { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } or x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } )

assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) }

then consider u, v being VECTOR of V 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 VECTOR of V : ( v in W1 & u in W2 ) } by Def1;

then consider u2, u1 being VECTOR of V 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 VECTOR of V : ( 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 VECTOR of V : ( v in W1 & u in W2 + W3 ) } by A3, A7, A9; :: thesis: verum

end;assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) }

then consider u, v being VECTOR of V 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 VECTOR of V : ( v in W1 & u in W2 ) } by Def1;

then consider u2, u1 being VECTOR of V 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 VECTOR of V : ( 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 VECTOR of V : ( v in W1 & u in W2 + W3 ) } by A3, A7, A9; :: thesis: verum

proof

then
{ (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } = { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) }
by A2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } or x in { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } )

assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) }

then consider u, v being VECTOR of V 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 VECTOR of V : ( v in W2 & u in W3 ) } by Def1;

then consider u2, u1 being VECTOR of V 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 VECTOR of V : ( 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 VECTOR of V : ( v in W1 + W2 & u in W3 ) } by A10, A15, A16; :: thesis: verum

end;assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) }

then consider u, v being VECTOR of V 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 VECTOR of V : ( v in W2 & u in W3 ) } by Def1;

then consider u2, u1 being VECTOR of V 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 VECTOR of V : ( 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 VECTOR of V : ( v in W1 + W2 & u in W3 ) } by A10, A15, A16; :: thesis: verum

hence W1 + (W2 + W3) = (W1 + W2) + W3 by A1, Def1; :: thesis: verum