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 ) }
proof
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 ;
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 ;
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;
{ (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 ) }
proof
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 ;
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 ;
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 ;
hence x in { (v + u) where u, v is VECTOR of V : ( v in W1 + W2 & u in W3 ) } by ; :: thesis: verum
end;
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;
hence W1 + (W2 + W3) = (W1 + W2) + W3 by ; :: thesis: verum