let L be INTegral Z_Lattice; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: ( r = a implies ((a ") * (a ")) * <;v,u;> in INT )
assume A1: r = a ; :: thesis: ((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; :: thesis: verum