let L be INTegral positive-definite Z_Lattice; :: thesis:
A1: EMLat L is Submodule of DivisibleMod L by ZMODLAT2:20;
A2: DualLat L is Submodule of DivisibleMod L by ThDL2;
for v being Vector of (DivisibleMod L) st v in EMLat L holds
v in DualLat L

proof

let v be Vector of (DivisibleMod L); :: thesis:
assume B1: v in EMLat L ; :: thesis:
set I = the Basis of (EMLat L);
reconsider J = the Basis of (EMLat L) as Basis of (EMbedding L) by ThELEM1;
for u being Vector of (DivisibleMod L) st u in J holds
(ScProductDM L) . (v,u) in INT.Ring

proof

let u be Vector of (DivisibleMod L); :: thesis:
assume C1: u in J ; :: thesis:
reconsider vv = v as Vector of (EMLat L) by B1;
reconsider uu = u as Vector of (EMLat L) by C1;
ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = EMbedding L by ZMODLAT2:28;
then (ScProductDM L) . (v,u) = (ScProductEM L) . (vv,uu) by ZMODLAT2:8
.= <;vv,uu;> by ZMODLAT2:def 4 ;
hence (ScProductDM L) . (v,u) in INT.Ring by ZMODLAT1:def 5; :: thesis:

end;

hence v in DualLat L by LmDE21, ThDL1; :: thesis:

end;

then EMLat L is Submodule of DualLat L by A1, A2, ZMODUL01:44;
then A3: ( the carrier of (EMLat L) c= the carrier of (DualLat L) & 0. (EMLat L) = 0. (DualLat L) & the addF of (EMLat L) = the addF of (DualLat L) || the carrier of (EMLat L) & the lmult of (EMLat L) = the lmult of (DualLat L) | [: the carrier of INT.Ring, the carrier of (EMLat L):] ) by VECTSP_4:def 2;
A4: [: the carrier of (EMLat L), the carrier of (EMLat L):] c= [: the carrier of (DualLat L), the carrier of (DualLat L):] by A3, ZFMISC_1:96;
the scalar of (DualLat L) || the carrier of (EMLat L) = ((ScProductDM L) || the carrier of (DualLat L)) || the carrier of (EMLat L) by defDualLat
.= (ScProductDM L) || the carrier of (EMLat L) by A4, FUNCT_1:51
.= (ScProductDM L) || (rng (MorphsZQ L)) by ZMODLAT2:def 4
.= ScProductEM L by ZMODLAT2:7
.= the scalar of (EMLat L) by ZMODLAT2:def 4 ;
hence EMLat L is Z_Sublattice of DualLat L by A3, ZMODLAT1:def 9; :: thesis: