let p, q be Integer; :: thesis: for V being Z_Module
for W being Submodule of V
for v being VECTOR of V st W = p (*) V & p > 1 & q > 1 & p,q are_coprime & q * v = 0. V holds
v + W = 0. (Z_ModuleQuot (V,W))
let V be Z_Module; :: thesis: for W being Submodule of V
for v being VECTOR of V st W = p (*) V & p > 1 & q > 1 & p,q are_coprime & q * v = 0. V holds
v + W = 0. (Z_ModuleQuot (V,W))
let W be Submodule of V; :: thesis: for v being VECTOR of V st W = p (*) V & p > 1 & q > 1 & p,q are_coprime & q * v = 0. V holds
v + W = 0. (Z_ModuleQuot (V,W))
let v be VECTOR of V; :: thesis: ( W = p (*) V & p > 1 & q > 1 & p,q are_coprime & q * v = 0. V implies v + W = 0. (Z_ModuleQuot (V,W)) )
assume that
A1: W = p (*) V and
A2: ( p > 1 & q > 1 & p,q are_coprime ) ; :: thesis: ( not q * v = 0. V or v + W = 0. (Z_ModuleQuot (V,W)) )
v + W is Coset of W by ZMODUL01:def 13;
then v + W in CosetSet (V,W) ;
then reconsider x = v + W as VECTOR of (Z_ModuleQuot (V,W)) by Def10;
( p in NAT & q in NAT ) by A2, INT_1:3;
then reconsider pp = p, qq = q as Nat ;
consider i, j being Integer such that
A3: (i * pp) + (j * qq) = 1 by A2, EULER_1:10;
assume A4: q * v = 0. V ; :: thesis: v + W = 0. (Z_ModuleQuot (V,W))
A5: x is Element of CosetSet (V,W) by Def10;
A6: q * x = (lmultCoset (V,W)) . (q,x) by Def10
.= (0. V) + W by A4, A5, Def9
.= zeroCoset (V,W) by ZMODUL01:59
.= 0. (Z_ModuleQuot (V,W)) by Def10 ;
((i * p) + (j * q)) * x = ((i * p) * x) + ((j * q) * x) by ZMODUL01:def 3
.= ((i * p) * x) + (j * (q * x)) by ZMODUL01:def 4
.= ((i * p) * x) + (0. (Z_ModuleQuot (V,W))) by A6, ZMODUL01:1
.= (i * p) * x by RLVECT_1:4
.= i * (p * x) by ZMODUL01:def 4
.= 0. (Z_ModuleQuot (V,W)) by A1, Th1, ZMODUL01:1 ;
hence 0. (Z_ModuleQuot (V,W)) = v + W by A3, ZMODUL01:def 5; :: thesis: verum