let R be Ring; for V being LeftMod of R
for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s /\ W2s = W1 /\ W2
let V be LeftMod of R; for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s /\ W2s = W1 /\ W2
let W1, W2 be Subspace of V; for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s /\ W2s = W1 /\ W2
let W1s, W2s be strict Subspace of V; ( W1s = (Omega). W1 & W2s = (Omega). W2 implies W1s /\ W2s = W1 /\ W2 )
assume A1:
( W1s = (Omega). W1 & W2s = (Omega). W2 )
; W1s /\ W2s = W1 /\ W2
for x being Vector of V holds
( x in W1 /\ W2 iff x in W1s /\ W2s )
proof
let x be
Vector of
V;
( x in W1 /\ W2 iff x in W1s /\ W2s )
hereby ( x in W1s /\ W2s implies x in W1 /\ W2 )
end;
assume B1:
x in W1s /\ W2s
;
x in W1 /\ W2
x in ModuleStr(# the
carrier of
W1, the
addF of
W1, the
ZeroF of
W1, the
lmult of
W1 #)
by A1, B1, VECTSP_5:3;
then B2:
x in W1
;
x in ModuleStr(# the
carrier of
W2, the
addF of
W2, the
ZeroF of
W2, the
lmult of
W2 #)
by A1, B1, VECTSP_5:3;
then
x in W2
;
hence
x in W1 /\ W2
by B2, VECTSP_5:3;
verum
end;
hence
W1 /\ W2 = W1s /\ W2s
by VECTSP_4:30; verum