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

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