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

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

hence
GramMatrix b is Matrix of dim L,F_Rat
by ZMODLAT1:1; :: thesis: verum
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;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