let L be positive-definite Z_Lattice; :: thesis: for b being OrdBasis of L
for e being OrdBasis of EMLat L st e = (MorphsZQ L) * b holds
GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e)
let b be OrdBasis of L; :: thesis: for e being OrdBasis of EMLat L st e = (MorphsZQ L) * b holds
GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e)
let e be OrdBasis of EMLat L; :: thesis: ( e = (MorphsZQ L) * b implies GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e) )
assume AS: e = (MorphsZQ L) * b ; :: thesis: GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e)
R1: rank L = rank (EMLat L) by ZMODLAT2:42;
R2: ( len (GramMatrix ((InnerProduct L),b)) = rank L & width (GramMatrix ((InnerProduct L),b)) = rank L & Indices (GramMatrix ((InnerProduct L),b)) = [:(Seg (rank L)),(Seg (rank L)):] ) by MATRIX_0:24;
S2: ( len (GramMatrix ((InnerProduct (EMLat L)),e)) = rank (EMLat L) & width (GramMatrix ((InnerProduct (EMLat L)),e)) = rank (EMLat L) & Indices (GramMatrix ((InnerProduct (EMLat L)),e)) = [:(Seg (rank (EMLat L))),(Seg (rank (EMLat L))):] ) by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices (GramMatrix ((InnerProduct L),b)) holds
(GramMatrix ((InnerProduct L),b)) * (i,j) = (GramMatrix ((InnerProduct (EMLat L)),e)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (GramMatrix ((InnerProduct L),b)) implies (GramMatrix ((InnerProduct L),b)) * (i,j) = (GramMatrix ((InnerProduct (EMLat L)),e)) * (i,j) )
assume [i,j] in Indices (GramMatrix ((InnerProduct L),b)) ; :: thesis: (GramMatrix ((InnerProduct L),b)) * (i,j) = (GramMatrix ((InnerProduct (EMLat L)),e)) * (i,j)
then X1: ( i in Seg (rank L) & j in Seg (rank L) ) by R2, ZFMISC_1:87;
then A2: ( i in dom b & j in dom b ) by R2, FINSEQ_1:def 3, MATRIX_0:24;
then A3: (GramMatrix ((InnerProduct L),b)) * (i,j) = (InnerProduct L) . ((b /. i),(b /. j)) by ZMODLAT1:def 32;
A4: ( i in dom e & j in dom e ) by R1, S2, X1, FINSEQ_1:def 3, MATRIX_0:24;
Y0: the carrier of (EMLat L) = rng (MorphsZQ L) by ZMODLAT2:def 4
.= the carrier of (EMbedding L) by ZMODUL08:def 3 ;
Y1: e /. i = e . i by A4, PARTFUN1:def 6
.= (MorphsZQ L) . (b . i) by A2, AS, FUNCT_1:13
.= (MorphsZQ L) . (b /. i) by A2, PARTFUN1:def 6 ;
Y2: e /. j = e . j by A4, PARTFUN1:def 6
.= (MorphsZQ L) . (b . j) by A2, AS, FUNCT_1:13
.= (MorphsZQ L) . (b /. j) by A2, PARTFUN1:def 6 ;
reconsider ei = e /. i, ej = e /. j as Vector of (EMbedding L) by Y0;
(InnerProduct (EMLat L)) . ((e /. i),(e /. j)) = (ScProductEM L) . (ei,ej) by ZMODLAT2:def 4
.= <;(b /. i),(b /. j);> by Y1, Y2, ZMODLAT2:def 2
.= (InnerProduct L) . ((b /. i),(b /. j)) ;
hence (GramMatrix ((InnerProduct L),b)) * (i,j) = (GramMatrix ((InnerProduct (EMLat L)),e)) * (i,j) by A3, A4, ZMODLAT1:def 32; :: thesis: verum

end;

hence GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e) by MATRIX_0:27, R1; :: thesis: verum