let L be positive-definite Z_Lattice; 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; 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; ( e = (MorphsZQ L) * b implies GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e) )
assume AS:
e = (MorphsZQ L) * b
; 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;
( [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))
;
(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;
verum
end;
hence
GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e)
by MATRIX_0:27, R1; verum