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

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