set D = DivisibleMod V;
set Z = EMbedding V;
assume
not DivisibleMod V is torsion-free
; contradiction
then consider v being Vector of (DivisibleMod V) such that
P1:
( v <> 0. (DivisibleMod V) & v is torsion )
;
consider i being Element of INT.Ring such that
P2:
( i <> 0 & i * v = 0. (DivisibleMod V) )
by P1;
v in the carrier of (DivisibleMod V)
;
then A1:
v in Class (EQRZM V)
by defDivisibleMod;
reconsider vv = v as Element of Class (EQRZM V) by 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 iq = i as Element of F_Rat by NUMBERS:14;
A4:
( iq = i / 1 & 1 <> 0 )
;
A6: i * v =
((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . (i,v)
by defDivisibleMod
.=
(lmultCoset V) . (i,v)
by A1, FUNCT_1:49, ZFMISC_1:87
.=
Class ((EQRZM V),[(i * z),((1. INT.Ring) * a)])
by A1, A2, A4, ZMODUL04:def 4
.=
Class ((EQRZM V),[(i * z),a])
;
A7:
not a in {0}
by A2, TARSKI:def 1;
a in INT \ {0}
by A7, XBOOLE_0:def 5;
then A8:
[(i * z),a] in [: the carrier of V,(INT \ {0}):]
by ZFMISC_1:87;
Class ((EQRZM V),[(i * z),a]) =
zeroCoset V
by P2, A6, defDivisibleMod
.=
Class ((EQRZM V),[(0. V),a])
by A2, ZMODUL04:def 3
;
then
[[(i * z),a],[(0. V),a]] in EQRZM V
by A8, EQREL_1:35;
then
a * (0. V) = a * (i * z)
by ZMODUL04:3;
then A9: 0. V =
a * (i * z)
by ZMODUL01:1
.=
(a * i) * z
by VECTSP_1:def 16
;
A10:
z <> 0. V
z is torsion
by P2, A2, A9;
then
not V is torsion-free
by A10;
hence
contradiction
; verum