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