let L be Z_Lattice; :: thesis: for v, u being Vector of (DivisibleMod L) holds
( (ScProductDM L) . ((- v),u) = - ((ScProductDM L) . (v,u)) & (ScProductDM L) . (u,(- v)) = - ((ScProductDM L) . (u,v)) )
let v, u be Vector of (DivisibleMod L); :: thesis: ( (ScProductDM L) . ((- v),u) = - ((ScProductDM L) . (v,u)) & (ScProductDM L) . (u,(- v)) = - ((ScProductDM L) . (u,v)) )
thus A1: (ScProductDM L) . ((- v),u) = (ScProductDM L) . (((- (1. INT.Ring)) * v),u) by ZMODUL01:2
.= (- 1) * ((ScProductDM L) . (v,u)) by ThSPDM1
.= - ((ScProductDM L) . (v,u)) ; :: thesis: (ScProductDM L) . (u,(- v)) = - ((ScProductDM L) . (u,v))
thus (ScProductDM L) . (u,(- v)) = (ScProductDM L) . ((- v),u) by ThSPDM1
.= - ((ScProductDM L) . (u,v)) by A1, ThSPDM1 ; :: thesis: verum