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 () st v in EMLat L holds
v in DualLat L
proof
let v be Vector of (); :: thesis: ( v in EMLat L implies v in DualLat L )
assume B1: v in EMLat L ; :: thesis:
set I = the Basis of ();
reconsider J = the Basis of () as Basis of () by ThELEM1;
for u being Vector of () st u in J holds
() . (v,u) in INT.Ring
proof
let u be Vector of (); :: thesis: ( u in J implies () . (v,u) in INT.Ring )
assume C1: u in J ; :: thesis: () . (v,u) in INT.Ring
reconsider vv = v as Vector of () by B1;
reconsider uu = u as Vector of () by C1;
ModuleStr(# the carrier of (), the addF of (), the ZeroF of (), the lmult of () #) = EMbedding L by ZMODLAT2:28;
then () . (v,u) = () . (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;
hence v in DualLat L by ; :: thesis: verum
end;
then EMLat L is Submodule of DualLat L by ;
then A3: ( the carrier of () c= the carrier of () & 0. () = 0. () & the addF of () = the addF of () || the carrier of () & the lmult of () = the lmult of () | [: the carrier of INT.Ring, the carrier of ():] ) by VECTSP_4:def 2;
A4: [: the carrier of (), the carrier of ():] c= [: the carrier of (), the carrier of ():] by ;
the scalar of () || the carrier of () = (() || the carrier of ()) || the carrier of () by defDualLat
.= () || the carrier of () by
.= () || (rng ()) by ZMODLAT2:def 4
.= ScProductEM L by ZMODLAT2:7
.= the scalar of () by ZMODLAT2:def 4 ;
hence EMLat L is Z_Sublattice of DualLat L by ; :: thesis: verum