let L be positive-definite Z_Lattice; :: thesis: 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); :: thesis: ( (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 ;
hereby :: thesis: ( v = 0. (DivisibleMod L) implies (ScProductDM L) . (v,v) = 0 )
assume B1: (ScProductDM L) . (v,v) = 0 ; :: thesis: not v <> 0. (DivisibleMod L)
assume v <> 0. (DivisibleMod L) ; :: thesis: contradiction
then a * v <> 0. (DivisibleMod L) by a1, ZMODUL01:def 7;
then u <> zeroCoset L by ZMODUL08:def 4;
then ul <> 0. (EMLat L) by defEMLat;
hence contradiction by A2, A4, B1, ZMODLAT1:16; :: thesis: verum
end;
assume v = 0. (DivisibleMod L) ; :: thesis: (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; :: thesis: verum