let p, i 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 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 (VectQuot (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 (VectQuot (V,W)) st p <> 0 & W = p (*) V holds

i * x = (i mod p) * x

let x be VECTOR of (VectQuot (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 Element of INT.Ring 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 VECTSP_1:def 15

.= (j * (p * x)) + ((i mod p) * x) by VECTSP_1:def 16

.= (0. (VectQuot (V,W))) + ((i mod p) * x) by A2, Th1, ZMODUL01:1

.= (i mod p) * x by RLVECT_1:4 ; :: thesis: verum

for W being Submodule of V

for x being VECTOR of (VectQuot (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 (VectQuot (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 (VectQuot (V,W)) st p <> 0 & W = p (*) V holds

i * x = (i mod p) * x

let x be VECTOR of (VectQuot (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 Element of INT.Ring 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 VECTSP_1:def 15

.= (j * (p * x)) + ((i mod p) * x) by VECTSP_1:def 16

.= (0. (VectQuot (V,W))) + ((i mod p) * x) by A2, Th1, ZMODUL01:1

.= (i mod p) * x by RLVECT_1:4 ; :: thesis: verum