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)) ) ) )
proof
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
proof
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;
hence x = (MorphsZQ L) . (0. L) by B2, ZMODLAT1:def 3
.= 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;
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)
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
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;
thus 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)) ) :: 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;