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)

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

hence
GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e)
by MATRIX_0:27, R1; :: thesis: verum
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;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