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

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