let p be Element of INT.Ring; :: thesis: for V being Z_Module

for W being Submodule of V

for x being VECTOR of (VectQuot (V,W)) st W = p (*) V holds

p * x = 0. (VectQuot (V,W))

let V be Z_Module; :: thesis: for W being Submodule of V

for x being VECTOR of (VectQuot (V,W)) st W = p (*) V holds

p * x = 0. (VectQuot (V,W))

let W be Submodule of V; :: thesis: for x being VECTOR of (VectQuot (V,W)) st W = p (*) V holds

p * x = 0. (VectQuot (V,W))

let x be VECTOR of (VectQuot (V,W)); :: thesis: ( W = p (*) V implies p * x = 0. (VectQuot (V,W)) )

assume A1: W = p (*) V ; :: thesis: p * x = 0. (VectQuot (V,W))

A2: x is Element of CosetSet (V,W) by VECTSP10:def 6;

then x in { A where A is Coset of W : verum } ;

then consider xx being Coset of W such that

A3: xx = x ;

consider v being VECTOR of V such that

A4: xx = v + W by VECTSP_4:def 6;

p * v in the carrier of W by A1;

then A5: p * v in W ;

thus p * x = (lmultCoset (V,W)) . (p,x) by VECTSP10:def 6

.= (p * v) + W by A2, A3, A4, VECTSP10:def 5

.= zeroCoset (V,W) by A5, ZMODUL01:63

.= 0. (VectQuot (V,W)) by VECTSP10:def 6 ; :: thesis: verum

for W being Submodule of V

for x being VECTOR of (VectQuot (V,W)) st W = p (*) V holds

p * x = 0. (VectQuot (V,W))

let V be Z_Module; :: thesis: for W being Submodule of V

for x being VECTOR of (VectQuot (V,W)) st W = p (*) V holds

p * x = 0. (VectQuot (V,W))

let W be Submodule of V; :: thesis: for x being VECTOR of (VectQuot (V,W)) st W = p (*) V holds

p * x = 0. (VectQuot (V,W))

let x be VECTOR of (VectQuot (V,W)); :: thesis: ( W = p (*) V implies p * x = 0. (VectQuot (V,W)) )

assume A1: W = p (*) V ; :: thesis: p * x = 0. (VectQuot (V,W))

A2: x is Element of CosetSet (V,W) by VECTSP10:def 6;

then x in { A where A is Coset of W : verum } ;

then consider xx being Coset of W such that

A3: xx = x ;

consider v being VECTOR of V such that

A4: xx = v + W by VECTSP_4:def 6;

p * v in the carrier of W by A1;

then A5: p * v in W ;

thus p * x = (lmultCoset (V,W)) . (p,x) by VECTSP10:def 6

.= (p * v) + W by A2, A3, A4, VECTSP10:def 5

.= zeroCoset (V,W) by A5, ZMODUL01:63

.= 0. (VectQuot (V,W)) by VECTSP10:def 6 ; :: thesis: verum