let L be INTegral Z_Lattice; for r being non zero Element of F_Rat
for a being Rational
for v, u being Vector of (EMLat (r,L)) st r = a holds
((a ") * (a ")) * <;v,u;> in INT
let r be non zero Element of F_Rat; for a being Rational
for v, u being Vector of (EMLat (r,L)) st r = a holds
((a ") * (a ")) * <;v,u;> in INT
let a be Rational; for v, u being Vector of (EMLat (r,L)) st r = a holds
((a ") * (a ")) * <;v,u;> in INT
let v, u be Vector of (EMLat (r,L)); ( r = a implies ((a ") * (a ")) * <;v,u;> in INT )
assume A1:
r = a
; ((a ") * (a ")) * <;v,u;> in INT
consider m0, n0 being Integer such that
A2:
( n0 <> 0 & a = m0 / n0 )
by RAT_1:2;
reconsider n = n0, m = m0 as Element of INT.Ring by INT_1:def 2;
consider vv being Vector of (EMLat L) such that
A3:
n * v = m * vv
by A1, A2, ThrEMLat1;
consider uu being Vector of (EMLat L) such that
A4:
n * u = m * uu
by A1, A2, ThrEMLat1;
r <> 0. F_Rat
;
then A5:
m <> 0
by A1, A2;
A6: (n * n) * <;v,u;> =
n * (n * <;v,u;>)
.=
n * <;v,(n * u);>
by ZMODLAT1:9
.=
<;(n * v),(n * u);>
by ZMODLAT1:def 3
.=
<;(m * vv),(m * uu);>
by A3, A4, ThrEMLat2
.=
m * <;vv,(m * uu);>
by ZMODLAT1:def 3
.=
m * (m * <;vv,uu;>)
by ZMODLAT1:9
.=
(m * m) * <;vv,uu;>
;
A7: ((1 / m0) * (1 / m0)) * ((n0 * n0) * <;v,u;>) =
((n0 / m0) * (n0 / m0)) * <;v,u;>
.=
((a ") * (n0 / m0)) * <;v,u;>
by A2, XCMPLX_1:213
.=
((a ") * (a ")) * <;v,u;>
by A2, XCMPLX_1:213
;
((1 / m0) * (1 / m0)) * ((m0 * m0) * <;vv,uu;>) =
(m0 * (1 / m0)) * ((m0 * (1 / m0)) * <;vv,uu;>)
.=
1 * ((m0 * (1 / m0)) * <;vv,uu;>)
by A5, XCMPLX_1:106
.=
(1. F_Real) * <;vv,uu;>
by A5, XCMPLX_1:106
.=
<;vv,uu;>
;
hence
((a ") * (a ")) * <;v,u;> in INT
by A6, A7, ZMODLAT1:def 5; verum