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

for i being Element of INT.Ring

for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

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

for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

let i be Element of INT.Ring; :: thesis: for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

let v be Element of V; :: thesis: ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

reconsider a = i mod p as Element of (GF p) by EC_PF_1:14;

reconsider t1 = ZMtoMQV (V,p,v) as Element of (Z_MQ_VectSp (V,p)) ;

reconsider t1 = t1 as Element of (VectQuot (V,(p (*) V))) ;

ZMtoMQV (V,p,v) = v + (p (*) V) ;

then Q1: v + (p (*) V) is Element of CosetSet (V,(p (*) V)) by VECTSP10:def 6;

thus ZMtoMQV (V,p,((i mod p) * v)) = a * (ZMtoMQV (V,p,v)) by ZMODUL03:30

.= (i mod p) * t1 by ZMODUL02:def 11

.= i * t1 by ZMODUL02:2

.= (lmultCoset (V,(p (*) V))) . (i,t1) by VECTSP10:def 6

.= ZMtoMQV (V,p,(i * v)) by Q1, VECTSP10:def 5 ; :: thesis: verum

for i being Element of INT.Ring

for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

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

for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

let i be Element of INT.Ring; :: thesis: for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

let v be Element of V; :: thesis: ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

reconsider a = i mod p as Element of (GF p) by EC_PF_1:14;

reconsider t1 = ZMtoMQV (V,p,v) as Element of (Z_MQ_VectSp (V,p)) ;

reconsider t1 = t1 as Element of (VectQuot (V,(p (*) V))) ;

ZMtoMQV (V,p,v) = v + (p (*) V) ;

then Q1: v + (p (*) V) is Element of CosetSet (V,(p (*) V)) by VECTSP10:def 6;

thus ZMtoMQV (V,p,((i mod p) * v)) = a * (ZMtoMQV (V,p,v)) by ZMODUL03:30

.= (i mod p) * t1 by ZMODUL02:def 11

.= i * t1 by ZMODUL02:2

.= (lmultCoset (V,(p (*) V))) . (i,t1) by VECTSP10:def 6

.= ZMtoMQV (V,p,(i * v)) by Q1, VECTSP10:def 5 ; :: thesis: verum