let L be Z_Lattice; :: thesis: ( ( 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)) ) ) )
set D = DivisibleMod L;
set Z = EMbedding L;
set f = ScProductDM L;
A1: EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;
thus 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) :: thesis: ( ( 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)) ) ) )

proof

let x be Vector of (DivisibleMod L); :: thesis: ( ( for y being Vector of (DivisibleMod L) holds (ScProductDM L) . (x,y) = 0 ) implies x = 0. (DivisibleMod L) )
assume B1: for y being Vector of (DivisibleMod L) holds (ScProductDM L) . (x,y) = 0 ; :: thesis: x = 0. (DivisibleMod L)
consider a being Element of INT.Ring such that
B2: ( a <> 0. INT.Ring & a * x in EMbedding L ) by ZMODUL08:29;
reconsider xx = a * x as Vector of (EMbedding L) by B2;
for yy being Vector of (EMbedding L) holds (ScProductEM L) . (xx,yy) = 0

proof

let yy be Vector of (EMbedding L); :: thesis: (ScProductEM L) . (xx,yy) = 0
set b = 1. INT.Ring;
yy in EMbedding L ;
then yy in DivisibleMod L by A1, ZMODUL01:24;
then reconsider y = (1. INT.Ring) * yy as Vector of (DivisibleMod L) ;
C1: ( 1. INT.Ring <> 0 & yy = (1. INT.Ring) * y ) ;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af = a, bf = 1. INT.Ring as Element of F_Real ;
C2: (ScProductDM L) . (x,y) = ((af ") * (bf ")) * ((ScProductEM L) . (xx,yy)) by B2, C1, defScProductDM;
thus (ScProductEM L) . (xx,yy) = 0 :: thesis: verum

proof

assume (ScProductEM L) . (xx,yy) <> 0 ; :: thesis: contradiction
then XX1: ( af " = 0 or bf " = 0 ) by B1, C2;
( af <> 0. F_Real & bf <> 0. F_Real ) by B2;
hence contradiction by XX1, VECTSP_1:25; :: thesis: verum

end;

end;

then xx = 0. (EMbedding L) by ThSPEM1
.= 0. (DivisibleMod L) by A1, ZMODUL01:26 ;
hence x = 0. (DivisibleMod L) by B2, ZMODUL01:def 7; :: thesis: verum

end;

thus for x, y being Vector of (DivisibleMod L) holds (ScProductDM L) . (x,y) = (ScProductDM L) . (y,x) :: thesis: 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)) )

proof

let x, y be Vector of (DivisibleMod L); :: thesis: (ScProductDM L) . (x,y) = (ScProductDM L) . (y,x)
consider a being Element of INT.Ring such that
B1: ( a <> 0 & a * x in EMbedding L ) by ZMODUL08:29;
reconsider xx = a * x as Vector of (EMbedding L) by B1;
consider b being Element of INT.Ring such that
B2: ( b <> 0 & b * y in EMbedding L ) by ZMODUL08:29;
reconsider yy = b * y as Vector of (EMbedding L) by B2;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af = a, bf = b as Element of F_Real ;
thus (ScProductDM L) . (x,y) = ((af ") * (bf ")) * ((ScProductEM L) . (xx,yy)) by B1, B2, defScProductDM
.= ((bf ") * (af ")) * ((ScProductEM L) . (yy,xx)) by ThSPEM1
.= (ScProductDM L) . (y,x) by B1, B2, defScProductDM ; :: thesis: verum

end;

thus for x, y, z being Vector of (DivisibleMod L)
for i being Element of INT.Ring holds
( (ScProductDM L) . ((x + y),z) = ((ScProductDM L) . (x,z)) + ((ScProductDM L) . (y,z)) & (ScProductDM L) . ((i * x),y) = i * ((ScProductDM L) . (x,y)) ) :: thesis: verum

proof

let x, y, z be Vector of (DivisibleMod L); :: thesis: for i being Element of INT.Ring holds
( (ScProductDM L) . ((x + y),z) = ((ScProductDM L) . (x,z)) + ((ScProductDM L) . (y,z)) & (ScProductDM L) . ((i * x),y) = i * ((ScProductDM L) . (x,y)) )
let i be Element of INT.Ring; :: thesis: ( (ScProductDM L) . ((x + y),z) = ((ScProductDM L) . (x,z)) + ((ScProductDM L) . (y,z)) & (ScProductDM L) . ((i * x),y) = i * ((ScProductDM L) . (x,y)) )
consider a being Element of INT.Ring such that
B1: ( a <> 0 & a * x in EMbedding L ) by ZMODUL08:29;
reconsider xx = a * x as Vector of (EMbedding L) by B1;
consider b being Element of INT.Ring such that
B2: ( b <> 0 & b * y in EMbedding L ) by ZMODUL08:29;
reconsider yy = b * y as Vector of (EMbedding L) by B2;
consider c being Element of INT.Ring such that
B3: ( c <> 0 & c * z in EMbedding L ) by ZMODUL08:29;
reconsider zz = c * z as Vector of (EMbedding L) by B3;
B41: b * (a * x) = b * xx by A1, ZMODUL01:29;
B42: a * (b * y) = a * yy by A1, ZMODUL01:29;
B4: (a * b) * (x + y) = ((a * b) * x) + ((a * b) * y) by VECTSP_1:def 14
.= ((b * a) * x) + (a * (b * y)) by VECTSP_1:def 16
.= (b * (a * x)) + (a * (b * y)) by VECTSP_1:def 16
.= (b * xx) + (a * yy) by A1, B41, B42, ZMODUL01:28 ;
then reconsider xy = (a * b) * (x + y) as Vector of (EMbedding L) ;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af = a, bf = b, cf = c as Element of F_Real ;
X2: ( af <> 0. F_Real & bf <> 0. F_Real ) by B1, B2;
then X1: ((af * bf) ") * (cf ") = ((af ") * (bf ")) * (cf ") by VECTSP_2:11;
thus (ScProductDM L) . ((x + y),z) = (((af ") * (bf ")) * (cf ")) * ((ScProductEM L) . (xy,zz)) by B1, B2, B3, X1, defScProductDM
.= (((af ") * (bf ")) * (cf ")) * (((ScProductEM L) . ((b * xx),zz)) + ((ScProductEM L) . ((a * yy),zz))) by B4, ThSPEM1
.= ((((af ") * (bf ")) * (cf ")) * ((ScProductEM L) . ((b * xx),zz))) + ((((af ") * (bf ")) * (cf ")) * ((ScProductEM L) . ((a * yy),zz)))
.= ((((af ") * (bf ")) * (cf ")) * (b * ((ScProductEM L) . (xx,zz)))) + ((((af ") * (bf ")) * (cf ")) * ((ScProductEM L) . ((a * yy),zz))) by ThSPEM1
.= ((((af ") * ((bf ") * bf)) * (cf ")) * ((ScProductEM L) . (xx,zz))) + ((((af ") * (bf ")) * (cf ")) * ((ScProductEM L) . ((a * yy),zz)))
.= ((((af ") * (1. F_Real)) * (cf ")) * ((ScProductEM L) . (xx,zz))) + ((((af ") * (bf ")) * (cf ")) * ((ScProductEM L) . ((a * yy),zz))) by VECTSP_1:def 10, X2
.= (((af ") * (cf ")) * ((ScProductEM L) . (xx,zz))) + ((((af ") * (bf ")) * (cf ")) * (a * ((ScProductEM L) . (yy,zz)))) by ThSPEM1
.= (((af ") * (cf ")) * ((ScProductEM L) . (xx,zz))) + ((((bf ") * (af * (af "))) * (cf ")) * ((ScProductEM L) . (yy,zz)))
.= (((af ") * (cf ")) * ((ScProductEM L) . (xx,zz))) + ((((bf ") * (1. F_Real)) * (cf ")) * ((ScProductEM L) . (yy,zz))) by VECTSP_1:def 10, X2
.= ((ScProductDM L) . (x,z)) + (((bf ") * (cf ")) * ((ScProductEM L) . (yy,zz))) by B1, B3, defScProductDM
.= ((ScProductDM L) . (x,z)) + ((ScProductDM L) . (y,z)) by B2, B3, defScProductDM ; :: thesis: (ScProductDM L) . ((i * x),y) = i * ((ScProductDM L) . (x,y))
a * (i * x) = (a * i) * x by VECTSP_1:def 16
.= i * (a * x) by VECTSP_1:def 16
.= i * xx by A1, ZMODUL01:29 ;
hence (ScProductDM L) . ((i * x),y) = ((af ") * (bf ")) * ((ScProductEM L) . ((i * xx),yy)) by B1, B2, defScProductDM
.= ((af ") * (bf ")) * (i * ((ScProductEM L) . (xx,yy))) by ThSPEM1
.= i * (((af ") * (bf ")) * ((ScProductEM L) . (xx,yy)))
.= i * ((ScProductDM L) . (x,y)) by B1, B2, defScProductDM ;
:: thesis: verum

end;