let L be Z_Lattice; :: thesis: for r being Element of F_Rat holds EMLat (r,L) is Submodule of DivisibleMod L
let r be Element of F_Rat; :: thesis: EMLat (r,L) is Submodule of DivisibleMod L
A1: the carrier of (EMbedding (r,L)) = r * (rng (MorphsZQ L)) by ZMODUL08:def 6
.= the carrier of (EMLat (r,L)) by defrEMLat ;
A2: the addF of (EMLat (r,L)) = (addCoset L) || (r * (rng (MorphsZQ L))) by defrEMLat
.= the addF of (EMbedding (r,L)) by ZMODUL08:def 6 ;
then reconsider ad = the addF of (EMbedding (r,L)) as BinOp of the carrier of (EMLat (r,L)) ;
A3: 0. (EMbedding (r,L)) = zeroCoset L by ZMODUL08:def 6
.= 0. (EMLat (r,L)) by defrEMLat ;
then reconsider ze = 0. (EMbedding (r,L)) as Vector of (EMLat (r,L)) ;
A4: the lmult of (EMLat (r,L)) = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] by defrEMLat
.= the lmult of (EMbedding (r,L)) by ZMODUL08:def 6 ;
then reconsider mu = the lmult of (EMbedding (r,L)) as Function of [: the carrier of INT.Ring, the carrier of (EMLat (r,L)):], the carrier of (EMLat (r,L)) ;
reconsider sc = the scalar of (EMLat (r,L)) as Function of [: the carrier of (EMbedding (r,L)), the carrier of (EMbedding (r,L)):], the carrier of F_Real by A1;
EMLat (r,L) = GenLat ((EMbedding (r,L)),sc) by A1, A2, A3, A4;
then A2: EMLat (r,L) is Submodule of EMbedding (r,L) by ZMODLAT1:2;
EMbedding (r,L) is Submodule of DivisibleMod L by ZMODUL08:32;
hence EMLat (r,L) is Submodule of DivisibleMod L by A2, ZMODUL01:42; :: thesis: verum