let L be Z_Lattice; :: thesis: for v being Dual of L

for a being Element of INT.Ring holds a * v is Dual of L

let v be Dual of L; :: thesis: for a being Element of INT.Ring holds a * v is Dual of L

let a be Element of INT.Ring; :: thesis: a * v is Dual of L

for x being Vector of (DivisibleMod L) st x in EMbedding L holds

(ScProductDM L) . ((a * v),x) in INT.Ring

for a being Element of INT.Ring holds a * v is Dual of L

let v be Dual of L; :: thesis: for a being Element of INT.Ring holds a * v is Dual of L

let a be Element of INT.Ring; :: thesis: a * v is Dual of L

for x being Vector of (DivisibleMod L) st x in EMbedding L holds

(ScProductDM L) . ((a * v),x) in INT.Ring

proof

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

assume B1: x in EMbedding L ; :: thesis: (ScProductDM L) . ((a * v),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) . ((a * v),x) = a * iv by ZMODLAT2:6;

hence (ScProductDM L) . ((a * v),x) in INT.Ring ; :: thesis: verum

end;assume B1: x in EMbedding L ; :: thesis: (ScProductDM L) . ((a * v),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) . ((a * v),x) = a * iv by ZMODLAT2:6;

hence (ScProductDM L) . ((a * v),x) in INT.Ring ; :: thesis: verum