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 VECTSP_1:def 17, a3; :: thesis: verum

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 VECTSP_1:def 17, a3; :: thesis: verum