let V be torsion-free Z_Module; for v being Vector of (DivisibleMod V) ex a being Element of INT.Ring st
( a <> 0 & a * v in EMbedding V )
let v be Vector of (DivisibleMod V); ex a being Element of INT.Ring st
( a <> 0 & a * v in EMbedding V )
A1:
v in the carrier of (DivisibleMod V)
;
reconsider vv = v as Element of Class (EQRZM V) by defDivisibleMod;
AX1:
v in Class (EQRZM V)
by A1, defDivisibleMod;
v is Element of ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #)
by defDivisibleMod;
then consider a being Element of INT.Ring, z being Vector of V such that
A2:
( a <> 0 & v = Class ((EQRZM V),[z,a]) )
by ZMODUL04:5;
reconsider aq = a as Element of F_Rat by NUMBERS:14;
A3:
( aq = a / 1 & 1 <> 0 )
;
AX4:
v in Class (EQRZM V)
by A1, defDivisibleMod;
a * v =
((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . (a,v)
by defDivisibleMod
.=
(lmultCoset V) . (a,v)
by AX4, FUNCT_1:49, ZFMISC_1:87
.=
Class ((EQRZM V),[(a * z),((1. INT.Ring) * a)])
by AX1, A2, A3, ZMODUL04:def 4
.=
Class ((EQRZM V),[z,(1. INT.Ring)])
by A2, ZMODUL04:4
;
hence
ex a being Element of INT.Ring st
( a <> 0 & a * v in EMbedding V )
by A2, ThEM1; verum