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

proof

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

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

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;

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;

end;

end;

hence v is Dual of L by LmDE21; :: thesis: verum