let p be prime Element of INT.Ring; for V being free Z_Module
for s being Element of V
for a being Element of INT.Ring
for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
let V be free Z_Module; for s being Element of V
for a being Element of INT.Ring
for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
let s be Element of V; for a being Element of INT.Ring
for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
let a be Element of INT.Ring; for b being Element of (GF p) st a = b holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
let b be Element of (GF p); ( a = b implies b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s)) )
set t = ZMtoMQV (V,p,s);
assume A1:
a = b
; b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))
A2:
ZMtoMQV (V,p,s) = s + (p (*) V)
;
reconsider t1 = ZMtoMQV (V,p,s) as Element of (VectQuot (V,(p (*) V))) ;
A3:
s + (p (*) V) is Element of CosetSet (V,(p (*) V))
by A2, VECTSP10:def 6;
reconsider i = b as Nat ;
A4:
b = i mod p
by NAT_1:44, NAT_D:24;
i in INT
by INT_1:def 2;
then reconsider i = i as Element of INT.Ring ;
thus b * (ZMtoMQV (V,p,s)) =
(i mod p) * t1
by A4, ZMODUL02:def 11
.=
(lmultCoset (V,(p (*) V))) . ((i mod p),(s + (p (*) V)))
by VECTSP10:def 6
.=
ZMtoMQV (V,p,(a * s))
by A1, A4, A3, VECTSP10:def 5
; verum