let p, i be Integer; :: thesis: for V being Z_Module
for W being Submodule of V
for x being VECTOR of (Z_ModuleQuot (V,W)) st p <> 0 & W = p (*) V holds
i * x = (i mod p) * x
let V be Z_Module; :: thesis: for W being Submodule of V
for x being VECTOR of (Z_ModuleQuot (V,W)) st p <> 0 & W = p (*) V holds
i * x = (i mod p) * x
let W be Submodule of V; :: thesis: for x being VECTOR of (Z_ModuleQuot (V,W)) st p <> 0 & W = p (*) V holds
i * x = (i mod p) * x
let x be VECTOR of (Z_ModuleQuot (V,W)); :: thesis: ( p <> 0 & W = p (*) V implies i * x = (i mod p) * x )
assume that
A1: p <> 0 and
A2: W = p (*) V ; :: thesis: i * x = (i mod p) * x
consider j being Integer such that
A3: j = i div p ;
thus i * x = ((j * p) + (i mod p)) * x by A1, A3, INT_1:59
.= ((j * p) * x) + ((i mod p) * x) by ZMODUL01:def 3
.= (j * (p * x)) + ((i mod p) * x) by ZMODUL01:def 4
.= (0. (Z_ModuleQuot (V,W))) + ((i mod p) * x) by A2, Th1, ZMODUL01:1
.= (i mod p) * x by RLVECT_1:4 ; :: thesis: verum