let L be positive-definite RATional Z_Lattice; :: thesis: for I being Basis of (EMLat L)

for v being Vector of (DivisibleMod L) st v in DualBasis I holds

v is Dual of L

let I be Basis of (EMLat L); :: thesis: for v being Vector of (DivisibleMod L) st v in DualBasis I holds

v is Dual of L

let v be Vector of (DivisibleMod L); :: thesis: ( v in DualBasis I implies v is Dual of L )

assume A1: v in DualBasis I ; :: thesis: v is Dual of L

consider u being Vector of (EMLat L) such that

A2: ( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) by A1, defDualBasis;

reconsider J = I as Basis of (EMbedding L) by ThELEM1;

for w being Vector of (DivisibleMod L) st w in J holds

(ScProductDM L) . (v,w) in INT.Ring

for v being Vector of (DivisibleMod L) st v in DualBasis I holds

v is Dual of L

let I be Basis of (EMLat L); :: thesis: for v being Vector of (DivisibleMod L) st v in DualBasis I holds

v is Dual of L

let v be Vector of (DivisibleMod L); :: thesis: ( v in DualBasis I implies v is Dual of L )

assume A1: v in DualBasis I ; :: thesis: v is Dual of L

consider u being Vector of (EMLat L) such that

A2: ( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds

(ScProductDM L) . (w,v) = 0 ) ) by A1, defDualBasis;

reconsider J = I as Basis of (EMbedding L) by ThELEM1;

for w being Vector of (DivisibleMod L) st w in J holds

(ScProductDM L) . (v,w) in INT.Ring

proof

hence
v is Dual of L
by LmDE21; :: thesis: verum
let w be Vector of (DivisibleMod L); :: thesis: ( w in J implies (ScProductDM L) . (v,w) in INT.Ring )

assume B1: w in J ; :: thesis: (ScProductDM L) . (v,w) in INT.Ring

end;assume B1: w in J ; :: thesis: (ScProductDM L) . (v,w) in INT.Ring

per cases
( u <> w or u = w )
;

end;

suppose
u <> w
; :: thesis: (ScProductDM L) . (v,w) in INT.Ring

then
(ScProductDM L) . (w,v) = 0
by A2, B1;

then (ScProductDM L) . (v,w) = 0 by ZMODLAT2:6;

hence (ScProductDM L) . (v,w) in INT.Ring ; :: thesis: verum

end;then (ScProductDM L) . (v,w) = 0 by ZMODLAT2:6;

hence (ScProductDM L) . (v,w) in INT.Ring ; :: thesis: verum

suppose
u = w
; :: thesis: (ScProductDM L) . (v,w) in INT.Ring

then
(ScProductDM L) . (v,w) = 1
by A2, ZMODLAT2:6;

hence (ScProductDM L) . (v,w) in INT.Ring ; :: thesis: verum

end;hence (ScProductDM L) . (v,w) in INT.Ring ; :: thesis: verum