let L be Z_Lattice; :: thesis: for v being Vector of (DivisibleMod L) holds (ScProductDM L) . ((0. (DivisibleMod L)),v) in INT.Ring
let v be Vector of (DivisibleMod L); :: thesis: (ScProductDM L) . ((0. (DivisibleMod L)),v) in INT.Ring
reconsider m1 = - 1 as Element of INT.Ring by INT_1:def 2;
A1: - (1. INT.Ring) = - 1 ;
(ScProductDM L) . ((0. (DivisibleMod L)),v) = (ScProductDM L) . ((v + (- v)),v) by RLVECT_1:5
.= ((ScProductDM L) . (v,v)) + ((ScProductDM L) . ((- v),v)) by ZMODLAT2:6
.= ((ScProductDM L) . (v,v)) + ((ScProductDM L) . ((m1 * v),v)) by A1, ZMODUL01:2
.= ((ScProductDM L) . (v,v)) + ((- 1) * ((ScProductDM L) . (v,v))) by ZMODLAT2:6
.= 0. INT.Ring ;
hence (ScProductDM L) . ((0. (DivisibleMod L)),v) in INT.Ring ; :: thesis: verum