let L be Z_Lattice; :: thesis: ( ( for x being Vector of (EMbedding L) st ( for y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = 0 ) holds

x = 0. (EMbedding L) ) & ( for x, y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = (ScProductEM L) . (y,x) ) & ( for x, y, z being Vector of (EMbedding L)

for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) ) ) )

set Z = EMbedding L;

set f = ScProductEM L;

set T = MorphsZQ L;

thus for x being Vector of (EMbedding L) st ( for y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = 0 ) holds

x = 0. (EMbedding L) :: thesis: ( ( for x, y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = (ScProductEM L) . (y,x) ) & ( for x, y, z being Vector of (EMbedding L)

for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) ) ) )

for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) )

for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) ) :: thesis: verum

x = 0. (EMbedding L) ) & ( for x, y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = (ScProductEM L) . (y,x) ) & ( for x, y, z being Vector of (EMbedding L)

for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) ) ) )

set Z = EMbedding L;

set f = ScProductEM L;

set T = MorphsZQ L;

thus for x being Vector of (EMbedding L) st ( for y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = 0 ) holds

x = 0. (EMbedding L) :: thesis: ( ( for x, y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = (ScProductEM L) . (y,x) ) & ( for x, y, z being Vector of (EMbedding L)

for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) ) ) )

proof

thus
for x, y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = (ScProductEM L) . (y,x)
:: thesis: for x, y, z being Vector of (EMbedding L)
let x be Vector of (EMbedding L); :: thesis: ( ( for y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = 0 ) implies x = 0. (EMbedding L) )

assume B1: for y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = 0 ; :: thesis: x = 0. (EMbedding L)

consider xx being Vector of L such that

B2: (MorphsZQ L) . xx = x by ZMODUL08:22;

for yy being Vector of L holds <;xx,yy;> = 0

.= Class ((EQRZM L),[(0. L),1]) by ZMODUL04:def 6

.= zeroCoset L by ZMODUL04:def 3

.= 0. (EMbedding L) by ZMODUL08:def 3 ;

:: thesis: verum

end;assume B1: for y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = 0 ; :: thesis: x = 0. (EMbedding L)

consider xx being Vector of L such that

B2: (MorphsZQ L) . xx = x by ZMODUL08:22;

for yy being Vector of L holds <;xx,yy;> = 0

proof

hence x =
(MorphsZQ L) . (0. L)
by B2, ZMODLAT1:def 3
let yy be Vector of L; :: thesis: <;xx,yy;> = 0

(MorphsZQ L) . yy in rng (MorphsZQ L) by FUNCT_2:4;

then reconsider y = (MorphsZQ L) . yy as Vector of (EMbedding L) by ZMODUL08:def 3;

(ScProductEM L) . (x,y) = 0 by B1;

hence <;xx,yy;> = 0 by B2, defScProductEM; :: thesis: verum

end;(MorphsZQ L) . yy in rng (MorphsZQ L) by FUNCT_2:4;

then reconsider y = (MorphsZQ L) . yy as Vector of (EMbedding L) by ZMODUL08:def 3;

(ScProductEM L) . (x,y) = 0 by B1;

hence <;xx,yy;> = 0 by B2, defScProductEM; :: thesis: verum

.= Class ((EQRZM L),[(0. L),1]) by ZMODUL04:def 6

.= zeroCoset L by ZMODUL04:def 3

.= 0. (EMbedding L) by ZMODUL08:def 3 ;

:: thesis: verum

for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) )

proof

thus
for x, y, z being Vector of (EMbedding L)
let x, y be Vector of (EMbedding L); :: thesis: (ScProductEM L) . (x,y) = (ScProductEM L) . (y,x)

consider xx being Vector of L such that

B1: (MorphsZQ L) . xx = x by ZMODUL08:22;

consider yy being Vector of L such that

B2: (MorphsZQ L) . yy = y by ZMODUL08:22;

thus (ScProductEM L) . (x,y) = <;xx,yy;> by B1, B2, defScProductEM

.= <;yy,xx;> by ZMODLAT1:def 3

.= (ScProductEM L) . (y,x) by B1, B2, defScProductEM ; :: thesis: verum

end;consider xx being Vector of L such that

B1: (MorphsZQ L) . xx = x by ZMODUL08:22;

consider yy being Vector of L such that

B2: (MorphsZQ L) . yy = y by ZMODUL08:22;

thus (ScProductEM L) . (x,y) = <;xx,yy;> by B1, B2, defScProductEM

.= <;yy,xx;> by ZMODLAT1:def 3

.= (ScProductEM L) . (y,x) by B1, B2, defScProductEM ; :: thesis: verum

for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) ) :: thesis: verum

proof

let x, y, z be Vector of (EMbedding L); :: thesis: for a being Element of INT.Ring holds

( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) )

let a be Element of INT.Ring; :: thesis: ( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) )

consider xx being Vector of L such that

B1: (MorphsZQ L) . xx = x by ZMODUL08:22;

consider yy being Vector of L such that

B2: (MorphsZQ L) . yy = y by ZMODUL08:22;

consider zz being Vector of L such that

B3: (MorphsZQ L) . zz = z by ZMODUL08:22;

B4: (MorphsZQ L) . (xx + yy) = ((MorphsZQ L) . xx) + ((MorphsZQ L) . yy) by ZMODUL04:def 6

.= x + y by B1, B2, ZMODUL08:19 ;

reconsider aq = a as Element of F_Rat by NUMBERS:14;

B5: (MorphsZQ L) . (a * xx) = aq * ((MorphsZQ L) . xx) by ZMODUL04:def 6

.= a * x by B1, ZMODUL08:19 ;

thus (ScProductEM L) . ((x + y),z) = <;(xx + yy),zz;> by B3, B4, defScProductEM

.= <;xx,zz;> + <;yy,zz;> by ZMODLAT1:def 3

.= ((ScProductEM L) . (x,z)) + <;yy,zz;> by B1, B3, defScProductEM

.= ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) by B2, B3, defScProductEM ; :: thesis: (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y))

thus (ScProductEM L) . ((a * x),y) = <;(a * xx),yy;> by B2, B5, defScProductEM

.= a * <;xx,yy;> by ZMODLAT1:def 3

.= a * ((ScProductEM L) . (x,y)) by B1, B2, defScProductEM ; :: thesis: verum

end;( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) )

let a be Element of INT.Ring; :: thesis: ( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) )

consider xx being Vector of L such that

B1: (MorphsZQ L) . xx = x by ZMODUL08:22;

consider yy being Vector of L such that

B2: (MorphsZQ L) . yy = y by ZMODUL08:22;

consider zz being Vector of L such that

B3: (MorphsZQ L) . zz = z by ZMODUL08:22;

B4: (MorphsZQ L) . (xx + yy) = ((MorphsZQ L) . xx) + ((MorphsZQ L) . yy) by ZMODUL04:def 6

.= x + y by B1, B2, ZMODUL08:19 ;

reconsider aq = a as Element of F_Rat by NUMBERS:14;

B5: (MorphsZQ L) . (a * xx) = aq * ((MorphsZQ L) . xx) by ZMODUL04:def 6

.= a * x by B1, ZMODUL08:19 ;

thus (ScProductEM L) . ((x + y),z) = <;(xx + yy),zz;> by B3, B4, defScProductEM

.= <;xx,zz;> + <;yy,zz;> by ZMODLAT1:def 3

.= ((ScProductEM L) . (x,z)) + <;yy,zz;> by B1, B3, defScProductEM

.= ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) by B2, B3, defScProductEM ; :: thesis: (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y))

thus (ScProductEM L) . ((a * x),y) = <;(a * xx),yy;> by B2, B5, defScProductEM

.= a * <;xx,yy;> by ZMODLAT1:def 3

.= a * ((ScProductEM L) . (x,y)) by B1, B2, defScProductEM ; :: thesis: verum