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)) ) ) )

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)) )

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

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

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)
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

.= 0. (DivisibleMod L) by A1, ZMODUL01:26 ;

hence x = 0. (DivisibleMod L) by B2, ZMODUL01:def 7; :: thesis: verum

end;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

then xx =
0. (EMbedding L)
by ThSPEM1
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) by VECTSP_1:def 17;

y = yy by VECTSP_1:def 17;

then C1: ( 1. INT.Ring <> 0 & yy = (1. INT.Ring) * y ) by VECTSP_1:def 17;

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

end;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) by VECTSP_1:def 17;

y = yy by VECTSP_1:def 17;

then C1: ( 1. INT.Ring <> 0 & yy = (1. INT.Ring) * y ) by VECTSP_1:def 17;

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;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

.= 0. (DivisibleMod L) by A1, ZMODUL01:26 ;

hence x = 0. (DivisibleMod L) by B2, ZMODUL01:def 7; :: thesis: verum

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

thus
for x, y, z being Vector of (DivisibleMod L)
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;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

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;( (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