let L be positive-definite Z_Lattice; :: thesis: GramDet (InnerProduct L) = GramDet (InnerProduct (EMLat L))

set b = the OrdBasis of L;

reconsider e = (MorphsZQ L) * the OrdBasis of L as OrdBasis of EMLat L by ZMODLAT2:41;

P1: GramMatrix ((InnerProduct L), the OrdBasis of L) = GramMatrix ((InnerProduct (EMLat L)),e) by LmEMDetX3;

GramDet (InnerProduct L) = Det (GramMatrix ((InnerProduct L), the OrdBasis of L)) by ZMODLAT1:def 35

.= Det (GramMatrix ((InnerProduct (EMLat L)),e)) by P1, ZMODLAT2:42

.= GramDet (InnerProduct (EMLat L)) by ZMODLAT1:def 35 ;

hence GramDet (InnerProduct L) = GramDet (InnerProduct (EMLat L)) ; :: thesis: verum

set b = the OrdBasis of L;

reconsider e = (MorphsZQ L) * the OrdBasis of L as OrdBasis of EMLat L by ZMODLAT2:41;

P1: GramMatrix ((InnerProduct L), the OrdBasis of L) = GramMatrix ((InnerProduct (EMLat L)),e) by LmEMDetX3;

GramDet (InnerProduct L) = Det (GramMatrix ((InnerProduct L), the OrdBasis of L)) by ZMODLAT1:def 35

.= Det (GramMatrix ((InnerProduct (EMLat L)),e)) by P1, ZMODLAT2:42

.= GramDet (InnerProduct (EMLat L)) by ZMODLAT1:def 35 ;

hence GramDet (InnerProduct L) = GramDet (InnerProduct (EMLat L)) ; :: thesis: verum