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 ;

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

( (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
v = 0. (DivisibleMod L)
; :: thesis: (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: 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

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