let L be positive-definite RATional Z_Lattice; :: thesis: for I being Basis of ()
for v being Vector of () st v in DualBasis I holds
v is Dual of L

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

let v be Vector of (); :: 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 () such that
A2: ( u in I & () . (u,v) = 1 & ( for w being Vector of () st w in I & u <> w holds
() . (w,v) = 0 ) ) by ;
reconsider J = I as Basis of () by ThELEM1;
for w being Vector of () st w in J holds
() . (v,w) in INT.Ring
proof
let w be Vector of (); :: thesis: ( w in J implies () . (v,w) in INT.Ring )
assume B1: w in J ; :: thesis: () . (v,w) in INT.Ring
per cases ( u <> w or u = w ) ;
suppose u = w ; :: thesis: () . (v,w) in INT.Ring
then (ScProductDM L) . (v,w) = 1 by ;
hence (ScProductDM L) . (v,w) in INT.Ring ; :: thesis: verum
end;
end;
end;
hence v is Dual of L by LmDE21; :: thesis: verum