let V be torsion-free Z_Module; :: thesis: ( ( for x, y being Vector of (DivisibleMod V)
for v, u being Vector of (Z_MQ_VectSp V) st x = v & y = u holds
x + y = v + u ) & ( for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for a being Element of INT.Ring
for aq being Element of F_Rat st z = w & a = aq holds
a * z = aq * w ) & ( for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for aq being Element of F_Rat
for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w ) & ( for x being Vector of (DivisibleMod V)
for v being Vector of (Z_MQ_VectSp V)
for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y ) ) )
A1: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by ZMODUL04:def 5;
thus for x, y being Vector of (DivisibleMod V)
for v, u being Vector of (Z_MQ_VectSp V) st x = v & y = u holds
x + y = v + u by A1, defDivisibleMod; :: thesis: ( ( for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for a being Element of INT.Ring
for aq being Element of F_Rat st z = w & a = aq holds
a * z = aq * w ) & ( for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for aq being Element of F_Rat
for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w ) & ( for x being Vector of (DivisibleMod V)
for v being Vector of (Z_MQ_VectSp V)
for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y ) ) )
thus A2: for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for a being Element of INT.Ring
for aq being Element of F_Rat st z = w & a = aq holds
a * z = aq * w :: thesis: ( ( for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for aq being Element of F_Rat
for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w ) & ( for x being Vector of (DivisibleMod V)
for v being Vector of (Z_MQ_VectSp V)
for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y ) ) )

proof

let z be Vector of (DivisibleMod V); :: thesis: for w being Vector of (Z_MQ_VectSp V)
for a being Element of INT.Ring
for aq being Element of F_Rat st z = w & a = aq holds
a * z = aq * w
let w be Vector of (Z_MQ_VectSp V); :: thesis: for a being Element of INT.Ring
for aq being Element of F_Rat st z = w & a = aq holds
a * z = aq * w
let a be Element of INT.Ring; :: thesis: for aq being Element of F_Rat st z = w & a = aq holds
a * z = aq * w
let aq be Element of F_Rat; :: thesis: ( z = w & a = aq implies a * z = aq * w )
assume B1: ( z = w & a = aq ) ; :: thesis: a * z = aq * w
thus a * z = ((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . (a,z) by defDivisibleMod
.= aq * w by A1, B1, FUNCT_1:49, ZFMISC_1:87 ; :: thesis: verum

end;

thus A3: for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for aq being Element of F_Rat
for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w :: thesis: for x being Vector of (DivisibleMod V)
for v being Vector of (Z_MQ_VectSp V)
for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y )

proof

let z be Vector of (DivisibleMod V); :: thesis: for w being Vector of (Z_MQ_VectSp V)
for aq being Element of F_Rat
for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w
let w be Vector of (Z_MQ_VectSp V); :: thesis: for aq being Element of F_Rat
for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w
let aq be Element of F_Rat; :: thesis: for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w
let a be Element of INT.Ring; :: thesis: ( a <> 0 & aq = a & a * z = aq * w implies z = w )
assume B1: ( a <> 0 & aq = a & a * z = aq * w ) ; :: thesis: z = w
assume B2: z <> w ; :: thesis: contradiction
reconsider ww = w as Vector of (DivisibleMod V) by ThDivisibleX1;
B4: a * ww = a * z by A2, B1;
a * (z - ww) = (a * z) - (a * ww) by ZMODUL01:8
.= 0. (DivisibleMod V) by B4, RLVECT_1:15 ;
then z - ww is torsion by B1;
hence contradiction by B2, RLVECT_1:21, ZMODUL06:def 3; :: thesis: verum

end;

thus for x being Vector of (DivisibleMod V)
for v being Vector of (Z_MQ_VectSp V)
for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y ) :: thesis: verum

proof

let x be Vector of (DivisibleMod V); :: thesis: for v being Vector of (Z_MQ_VectSp V)
for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y )
let v be Vector of (Z_MQ_VectSp V); :: thesis: for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y )
let r be Element of F_Rat; :: thesis: for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y )
let m, n be Element of INT.Ring; :: thesis: for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y )
let mi, ni be Integer; :: thesis: ( m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni implies ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y ) )
assume B1: ( m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni ) ; :: thesis: ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y )
consider y being Vector of (DivisibleMod V) such that
B2: n * y = x by B1, ThDivisible1;
take y ; :: thesis: ( x = n * y & r * v = m * y )
reconsider mq = m, nq = n as Element of F_Rat by NUMBERS:14;
B3: nq * r = mq by B1, XCMPLX_1:87;
B4: n * (m * y) = (n * m) * y by VECTSP_1:def 16
.= m * x by B2, VECTSP_1:def 16 ;
nq * (r * v) = mq * v by B3, VECTSP_1:def 16;
then n * (m * y) = nq * (r * v) by A2, B1, B4;
hence ( x = n * y & r * v = m * y ) by A3, B1, B2; :: thesis: verum

end;