let L be INTegral positive-definite Z_Lattice; :: thesis: EMLat L is Z_Sublattice of DualLat L

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

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: verum

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

then
EMLat L is Submodule of DualLat L
by A1, A2, ZMODUL01:44;
let v be Vector of (DivisibleMod L); :: thesis: ( v in EMLat L implies v in DualLat L )

assume B1: v in EMLat L ; :: thesis: v in DualLat L

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

end;assume B1: v in EMLat L ; :: thesis: v in DualLat L

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

hence
v in DualLat L
by LmDE21, ThDL1; :: thesis: verum
let u be Vector of (DivisibleMod L); :: thesis: ( u in J implies (ScProductDM L) . (v,u) in INT.Ring )

assume C1: u in J ; :: thesis: (ScProductDM L) . (v,u) in INT.Ring

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: verum

end;assume C1: u in J ; :: thesis: (ScProductDM L) . (v,u) in INT.Ring

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: verum

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: verum