let R be Ring; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( W1s = (Omega). W1 & W2s = (Omega). W2 implies W1s /\ W2s = W1 /\ W2 )

assume A1: ( W1s = (Omega). W1 & W2s = (Omega). W2 ) ; :: thesis: W1s /\ W2s = W1 /\ W2

for x being Vector of V holds

( x in W1 /\ W2 iff x in W1s /\ W2s )

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; :: thesis: 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; :: thesis: 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; :: thesis: ( W1s = (Omega). W1 & W2s = (Omega). W2 implies W1s /\ W2s = W1 /\ W2 )

assume A1: ( W1s = (Omega). W1 & W2s = (Omega). W2 ) ; :: thesis: W1s /\ W2s = W1 /\ W2

for x being Vector of V holds

( x in W1 /\ W2 iff x in W1s /\ W2s )

proof

hence
W1 /\ W2 = W1s /\ W2s
by VECTSP_4:30; :: thesis: verum
let x be Vector of V; :: thesis: ( x in W1 /\ W2 iff x in W1s /\ W2s )

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; :: thesis: verum

end;hereby :: thesis: ( x in W1s /\ W2s implies x in W1 /\ W2 )

assume B1:
x in W1s /\ W2s
; :: thesis: x in W1 /\ W2assume
x in W1 /\ W2
; :: thesis: x in W1s /\ W2s

then B1: ( x in W1 & x in W2 ) by VECTSP_5:3;

B2: x in W1s by A1, B1;

x in W2s by A1, B1;

hence x in W1s /\ W2s by B2, VECTSP_5:3; :: thesis: verum

end;then B1: ( x in W1 & x in W2 ) by VECTSP_5:3;

B2: x in W1s by A1, B1;

x in W2s by A1, B1;

hence x in W1s /\ W2s by B2, VECTSP_5:3; :: thesis: verum

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; :: thesis: verum