let p, q be Element of INT.Ring; :: 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. (VectQuot (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. (VectQuot (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. (VectQuot (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. (VectQuot (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. (VectQuot (V,W)) )
v + W is Coset of W by VECTSP_4:def 6;
then v + W in CosetSet (V,W) ;
then reconsider x = v + W as VECTOR of (VectQuot (V,W)) by VECTSP10:def 6;
( 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;
a3: (i * pp) + (j * qq) = 1. INT.Ring by A3;
reconsider i = i, j = j as Element of INT.Ring by Lem1;
assume A4: q * v = 0. V ; :: thesis: v + W = 0. (VectQuot (V,W))
A5: x is Element of CosetSet (V,W) by VECTSP10:def 6;
A6: q * x = (lmultCoset (V,W)) . (q,x) by VECTSP10:def 6
.= (0. V) + W by A4, A5, VECTSP10:def 5
.= zeroCoset (V,W) by ZMODUL01:59
.= 0. (VectQuot (V,W)) by VECTSP10:def 6 ;
((i * p) + (j * q)) * x = ((i * p) * x) + ((j * q) * x) by VECTSP_1:def 15
.= ((i * p) * x) + (j * (q * x)) by VECTSP_1:def 16
.= ((i * p) * x) + (0. (VectQuot (V,W))) by A6, ZMODUL01:1
.= (i * p) * x by RLVECT_1:4
.= i * (p * x) by VECTSP_1:def 16
.= 0. (VectQuot (V,W)) by A1, Th1, ZMODUL01:1 ;
hence 0. (VectQuot (V,W)) = v + W by a3; :: thesis: verum