let L be Z_Lattice; ( ( 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)
( ( 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)) ) ) )
thus
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,
y be
Vector of
(DivisibleMod L);
(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
;
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)) )
verumproof
let x,
y,
z be
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)) )let i be
Element of
INT.Ring;
( (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
;
(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
;
verum
end;