let L be Z_Lattice; for v, u being Dual of L holds v + u is Dual of L
let v, u be Dual of L; v + u is Dual of L
for x being Vector of (DivisibleMod L) st x in EMbedding L holds
(ScProductDM L) . ((v + u),x) in INT.Ring
proof
let x be
Vector of
(DivisibleMod L);
( x in EMbedding L implies (ScProductDM L) . ((v + u),x) in INT.Ring )
assume B1:
x in EMbedding L
;
(ScProductDM L) . ((v + u),x) in INT.Ring
(ScProductDM L) . (
v,
x)
in INT.Ring
by B1, defDualElement;
then reconsider iv =
(ScProductDM L) . (
v,
x) as
Element of
INT.Ring ;
(ScProductDM L) . (
u,
x)
in INT.Ring
by B1, defDualElement;
then reconsider iu =
(ScProductDM L) . (
u,
x) as
Element of
INT.Ring ;
set iiv =
iv;
set iiu =
iu;
(ScProductDM L) . (
(v + u),
x) =
((ScProductDM L) . (v,x)) + ((ScProductDM L) . (u,x))
by ZMODLAT2:6
.=
iv + iu
;
hence
(ScProductDM L) . (
(v + u),
x)
in INT.Ring
;
verum
end;
hence
v + u is Dual of L
by defDualElement; verum