let L be Z_Lattice; :: thesis: EMLat L is Submodule of DivisibleMod L

A1: the carrier of (EMbedding L) = rng (MorphsZQ L) by ZMODUL08:def 3

.= the carrier of (EMLat L) by defEMLat ;

A2: the addF of (EMLat L) = (addCoset L) || (rng (MorphsZQ L)) by defEMLat

.= the addF of (EMbedding L) by ZMODUL08:def 3 ;

then reconsider ad = the addF of (EMbedding L) as BinOp of the carrier of (EMLat L) ;

A3: 0. (EMbedding L) = zeroCoset L by ZMODUL08:def 3

.= 0. (EMLat L) by defEMLat ;

then reconsider ze = 0. (EMbedding L) as Vector of (EMLat L) ;

A4: the lmult of (EMLat L) = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] by defEMLat

.= the lmult of (EMbedding L) by ZMODUL08:def 3 ;

then reconsider mu = the lmult of (EMbedding L) as Function of [: the carrier of INT.Ring, the carrier of (EMLat L):], the carrier of (EMLat L) ;

reconsider sc = the scalar of (EMLat L) as Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real by A1;

EMLat L = GenLat ((EMbedding L),sc) by A1, A2, A3, A4;

then A2: EMLat L is Submodule of EMbedding L by ZMODLAT1:2;

EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;

hence EMLat L is Submodule of DivisibleMod L by A2, ZMODUL01:42; :: thesis: verum

A1: the carrier of (EMbedding L) = rng (MorphsZQ L) by ZMODUL08:def 3

.= the carrier of (EMLat L) by defEMLat ;

A2: the addF of (EMLat L) = (addCoset L) || (rng (MorphsZQ L)) by defEMLat

.= the addF of (EMbedding L) by ZMODUL08:def 3 ;

then reconsider ad = the addF of (EMbedding L) as BinOp of the carrier of (EMLat L) ;

A3: 0. (EMbedding L) = zeroCoset L by ZMODUL08:def 3

.= 0. (EMLat L) by defEMLat ;

then reconsider ze = 0. (EMbedding L) as Vector of (EMLat L) ;

A4: the lmult of (EMLat L) = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] by defEMLat

.= the lmult of (EMbedding L) by ZMODUL08:def 3 ;

then reconsider mu = the lmult of (EMbedding L) as Function of [: the carrier of INT.Ring, the carrier of (EMLat L):], the carrier of (EMLat L) ;

reconsider sc = the scalar of (EMLat L) as Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real by A1;

EMLat L = GenLat ((EMbedding L),sc) by A1, A2, A3, A4;

then A2: EMLat L is Submodule of EMbedding L by ZMODLAT1:2;

EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;

hence EMLat L is Submodule of DivisibleMod L by A2, ZMODUL01:42; :: thesis: verum