let V be torsion-free Z_Module; for v being Vector of (DivisibleMod V)
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of (DivisibleMod V) st a * u = v
thus
for v being Vector of (DivisibleMod V)
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of (DivisibleMod V) st a * u = v
verumproof
let v be
Vector of
(DivisibleMod V);
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of (DivisibleMod V) st a * u = v
assume AS:
ex
a being
Element of
INT.Ring st
(
a <> 0 & ( for
u being
Vector of
(DivisibleMod V) holds
a * u <> v ) )
;
contradiction
consider a being
Element of
INT.Ring such that B1:
(
a <> 0 & ( for
u being
Vector of
(DivisibleMod V) holds
a * u <> v ) )
by AS;
reconsider vv =
v as
Element of
Class (EQRZM V) by defDivisibleMod;
set Z =
Z_MQ_VectSp V;
reconsider Z =
Z_MQ_VectSp V as
VectSp of
F_Rat ;
BX:
Z = ModuleStr(#
(Class (EQRZM V)),
(addCoset V),
(zeroCoset V),
(lmultCoset V) #)
by ZMODUL04:def 5;
reconsider vv =
vv as
Element of
Z by BX;
reconsider aa =
a as
Element of
F_Rat by NUMBERS:14;
B2:
aa <> 0. F_Rat
by B1;
reconsider ai =
aa " as
Element of
F_Rat ;
B3:
aa * ai = 1. F_Rat
by B2, VECTSP_1:def 10;
set uu =
ai * vv;
reconsider uu =
ai * vv as
Element of
Z ;
reconsider u =
uu as
Element of
(DivisibleMod V) by BX, defDivisibleMod;
aa * uu =
(aa * ai) * vv
by VECTSP_1:def 16
.=
vv
by B3, VECTSP_1:def 17
;
then v =
((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . [a,u]
by BX, FUNCT_1:49, ZFMISC_1:87
.=
a * u
by defDivisibleMod
;
hence
contradiction
by B1;
verum
end;