let L be RATional Z_Lattice; :: thesis: for LX being Z_Lattice
for b being OrdBasis of LX st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
GramMatrix ((InnerProduct LX),b) is Matrix of dim LX,F_Rat
let LX be Z_Lattice; :: thesis: for b being OrdBasis of LX st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
GramMatrix ((InnerProduct LX),b) is Matrix of dim LX,F_Rat
let b be OrdBasis of LX; :: thesis: ( LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX implies GramMatrix ((InnerProduct LX),b) is Matrix of dim LX,F_Rat )
assume A1: ( LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX ) ; :: thesis: GramMatrix ((InnerProduct LX),b) is Matrix of dim LX,F_Rat
LX is RATional by A1, ThSLGM1;
then GramMatrix b is Matrix of dim LX,F_Rat by ZMODLAT2:45;
hence GramMatrix ((InnerProduct LX),b) is Matrix of dim LX,F_Rat ; :: thesis: verum