let L be positive-definite Z_Lattice; for v being Vector of (DivisibleMod L) holds
( (ScProductDM L) . (v,v) = 0 iff v = 0. (DivisibleMod L) )
let v be Vector of (DivisibleMod L); ( (ScProductDM L) . (v,v) = 0 iff v = 0. (DivisibleMod L) )
consider a being Element of INT.Ring such that
A1:
( a <> 0 & a * v in EMbedding L )
by ZMODUL08:29;
a1:
a <> 0. INT.Ring
by A1;
reconsider u = a * v as Vector of (EMbedding L) by A1;
u in the carrier of (EMbedding L)
;
then
u in rng (MorphsZQ L)
by ZMODUL08:def 3;
then reconsider ul = u as Vector of (EMLat L) by defEMLat;
A2: (a * a) * ((ScProductDM L) . (v,v)) =
a * (a * ((ScProductDM L) . (v,v)))
.=
a * ((ScProductDM L) . ((a * v),v))
by ThSPDM1
.=
a * ((ScProductDM L) . (v,(a * v)))
by ThSPDM1
.=
(ScProductDM L) . ((a * v),(a * v))
by ThSPDM1
;
ScProductEM L =
(ScProductDM L) || (rng (MorphsZQ L))
by ThSPEM2
.=
(ScProductDM L) || the carrier of (EMbedding L)
by ZMODUL08:def 3
;
then A4: (ScProductDM L) . ((a * v),(a * v)) =
(ScProductEM L) . (u,u)
by FUNCT_1:49, ZFMISC_1:87
.=
||.ul.||
by defEMLat
;
assume
v = 0. (DivisibleMod L)
; (ScProductDM L) . (v,v) = 0
then u =
0. (DivisibleMod L)
by ZMODUL01:1
.=
zeroCoset L
by ZMODUL08:def 4
.=
0. (EMLat L)
by defEMLat
;
hence
(ScProductDM L) . (v,v) = 0
by A1, A2, A4, ZMODLAT1:16; verum