theorem ThSPDM1:
for
L being
Z_Lattice holds
( ( for
x being
Vector of
(DivisibleMod L) st ( for
y being
Vector of
(DivisibleMod L) holds
(ScProductDM L) . (
x,
y)
= 0 ) holds
x = 0. (DivisibleMod L) ) & ( for
x,
y being
Vector of
(DivisibleMod L) holds
(ScProductDM L) . (
x,
y)
= (ScProductDM L) . (
y,
x) ) & ( for
x,
y,
z being
Vector of
(DivisibleMod L) for
a being
Element of
INT.Ring holds
(
(ScProductDM L) . (
(x + y),
z)
= ((ScProductDM L) . (x,z)) + ((ScProductDM L) . (y,z)) &
(ScProductDM L) . (
(a * x),
y)
= a * ((ScProductDM L) . (x,y)) ) ) )