let L be Z_Lattice; :: thesis: for v, u being Dual of L holds v + u is Dual of L

let v, u be Dual of L; :: thesis: 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

let v, u be Dual of L; :: thesis: 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

hence
v + u is Dual of L
by defDualElement; :: thesis: verum
let x be Vector of (DivisibleMod L); :: thesis: ( x in EMbedding L implies (ScProductDM L) . ((v + u),x) in INT.Ring )

assume B1: x in EMbedding L ; :: thesis: (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 ; :: thesis: verum

end;assume B1: x in EMbedding L ; :: thesis: (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 ; :: thesis: verum