let L be Z_Lattice; :: thesis: for r being non zero Element of F_Rat
for m, n being Element of INT.Ring
for m1, n1 being Element of INT
for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of (EMLat L) st n * v = m * x
let r be non zero Element of F_Rat; :: thesis: for m, n being Element of INT.Ring
for m1, n1 being Element of INT
for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of (EMLat L) st n * v = m * x
let m, n be Element of INT.Ring; :: thesis: for m1, n1 being Element of INT
for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of (EMLat L) st n * v = m * x
let m1, n1 be Element of INT ; :: thesis: for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of (EMLat L) st n * v = m * x
let v be Vector of (EMLat (r,L)); :: thesis: ( m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 implies ex x being Vector of (EMLat L) st n * v = m * x )
assume A1: ( m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 ) ; :: thesis: ex x being Vector of (EMLat L) st n * v = m * x
consider T being linear-transformation of (EMbedding L),(EMbedding (r,L)) such that
A2: ( ( for u being Element of (Z_MQ_VectSp L) st u in EMbedding L holds
T . u = r * u ) & T is bijective ) by ZMODUL08:27;
v in the carrier of (EMLat (r,L)) ;
then v in r * (rng (MorphsZQ L)) by defrEMLat;
then v in the carrier of (EMbedding (r,L)) by ZMODUL08:def 6;
then v in rng T by A2, FUNCT_2:def 3;
then consider ve being object such that
A3: ( ve in the carrier of (EMbedding L) & v = T . ve ) by FUNCT_2:11;
reconsider vz = ve as Vector of (Z_MQ_VectSp L) by A3, ZMODUL08:19;
reconsider vd = vz as Vector of (DivisibleMod L) by ZMODUL08:30;
consider zvd being Vector of (DivisibleMod L) such that
A4: ( vd = n * zvd & r * vz = m * zvd ) by A1, ZMODUL08:31;
A5: vz in EMbedding L by A3;
vz in rng (MorphsZQ L) by A3, ZMODUL08:def 3;
then reconsider x = vz as Vector of (EMLat L) by defEMLat;
B1: EMLat L is Submodule of DivisibleMod L by ThDivisibleL1;
B2: EMLat (r,L) is Submodule of DivisibleMod L by ThDivisibleL2;
A7: m * x = m * vd by B1, ZMODUL01:29
.= (m * n) * zvd by A4, VECTSP_1:def 16
.= n * (m * zvd) by VECTSP_1:def 16
.= n * v by A2, A3, A4, A5, B2, ZMODUL01:29 ;
take x ; :: thesis: n * v = m * x
thus n * v = m * x by A7; :: thesis: verum