let R be Ring; for V being LeftMod of R
for W1, W2 being Subspace of V
for WW1, WW2 being Subspace of W1 + W2 st WW1 = W1 & WW2 = W2 holds
W1 + W2 = WW1 + WW2
let V be LeftMod of R; for W1, W2 being Subspace of V
for WW1, WW2 being Subspace of W1 + W2 st WW1 = W1 & WW2 = W2 holds
W1 + W2 = WW1 + WW2
let W1, W2 be Subspace of V; for WW1, WW2 being Subspace of W1 + W2 st WW1 = W1 & WW2 = W2 holds
W1 + W2 = WW1 + WW2
let WW1, WW2 be Subspace of W1 + W2; ( WW1 = W1 & WW2 = W2 implies W1 + W2 = WW1 + WW2 )
assume A1:
( WW1 = W1 & WW2 = W2 )
; W1 + W2 = WW1 + WW2
A2:
WW1 + WW2 is Subspace of V
by VECTSP_4:26;
for x being object holds
( x in W1 + W2 iff x in WW1 + WW2 )
proof
let x be
object ;
( x in W1 + W2 iff x in WW1 + WW2 )
hereby ( x in WW1 + WW2 implies x in W1 + W2 )
end;
assume
x in WW1 + WW2
;
x in W1 + W2
then consider vv1,
vv2 being
Vector of
(W1 + W2) such that B1:
(
vv1 in WW1 &
vv2 in WW2 &
x = vv1 + vv2 )
by VECTSP_5:1;
thus
x in W1 + W2
by B1;
verum
end;
then
for x being Vector of V holds
( x in W1 + W2 iff x in WW1 + WW2 )
;
hence
W1 + W2 = WW1 + WW2
by A2, VECTSP_4:30; verum