let L be RATional Z_Lattice; :: thesis: for b being OrdBasis of L holds GramMatrix b is Matrix of dim L,F_Rat
let b be OrdBasis of L; :: thesis: GramMatrix b is Matrix of dim L,F_Rat
X1: ( len (GramMatrix b) = dim L & width (GramMatrix b) = dim L & Indices (GramMatrix b) = [:(Seg (dim L)),(Seg (dim L)):] ) by MATRIX_0:24;
X3: len b = dim L by ZMATRLIN:49;
for i, j being Nat st [i,j] in Indices (GramMatrix b) holds
(GramMatrix b) * (i,j) in the carrier of F_Rat
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices (GramMatrix b) implies (GramMatrix b) * (i,j) in the carrier of F_Rat )
assume [i,j] in Indices (GramMatrix b) ; :: thesis: (GramMatrix b) * (i,j) in the carrier of F_Rat
then ( i in Seg (dim L) & j in Seg (dim L) ) by X1, ZFMISC_1:87;
then D1: ( i in dom b & j in dom b ) by X3, FINSEQ_1:def 3;
(GramMatrix b) * (i,j) = (InnerProduct L) . ((b /. i),(b /. j)) by D1, ZMODLAT1:def 32
.= <;(b /. i),(b /. j);> ;
hence (GramMatrix b) * (i,j) in the carrier of F_Rat by defRational; :: thesis: verum
end;
hence GramMatrix b is Matrix of dim L,F_Rat by ZMODLAT1:1; :: thesis: verum