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

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