let R be commutative Ring; :: thesis: for V being LeftMod of R
for W being Subspace of V holds (1. R) (*) W = (Omega). W
let V be LeftMod of R; :: thesis: for W being Subspace of V holds (1. R) (*) W = (Omega). W
let W be Subspace of V; :: thesis: (1. R) (*) W = (Omega). W
for v being Vector of V st v in (Omega). W holds
v in (1. R) (*) W
proof
let v be Vector of V; :: thesis: ( v in (Omega). W implies v in (1. R) (*) W )
assume B1: v in (Omega). W ; :: thesis: v in (1. R) (*) W
reconsider vv = v as Vector of W by B1;
(1. R) * vv in (1. R) (*) W ;
hence v in (1. R) (*) W by VECTSP_1:def 17; :: thesis: verum
end;
then A2: for v being Vector of V holds
( v in (1. R) (*) W iff v in (Omega). W ) ;
A3: (Omega). W is Subspace of V by ZMODUL01:42;
(1. R) (*) W is Subspace of V by ZMODUL01:42;
hence (1. R) (*) W = (Omega). W by A2, A3, ZMODUL01:46; :: thesis: verum