let L be positive-definite RATional Z_Lattice; :: thesis: for I being Basis of (EMLat L) holds DualBasis I is Basis of (DualLat L)
let I be Basis of (EMLat L); :: thesis: DualBasis I is Basis of (DualLat L)
reconsider DL = DualLat L as Submodule of DivisibleMod L by ThDL2;
for v being Vector of (DivisibleMod L) st v in DualBasis I holds
v in the carrier of (DualLat L)

proof

let v be Vector of (DivisibleMod L); :: thesis: ( v in DualBasis I implies v in the carrier of (DualLat L) )
assume B1: v in DualBasis I ; :: thesis: v in the carrier of (DualLat L)
v in DualLat L by B1, ThDB2, ThDL1;
hence v in the carrier of (DualLat L) ; :: thesis: verum

end;

then DualBasis I c= the carrier of (DualLat L) ;
then reconsider DB = DualBasis I as linearly-independent Subset of DL by ZMODUL03:16;
A2: for v being Vector of (DivisibleMod L) st v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #) holds
v in Lin (DualBasis I)

proof

let v be Vector of (DivisibleMod L); :: thesis: ( v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #) implies v in Lin (DualBasis I) )
assume B1: v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #) ; :: thesis: v in Lin (DualBasis I)
v in DualLat L by B1;
hence v in Lin (DualBasis I) by ThDE3, ThDL1; :: thesis: verum

end;

A3: for v being Vector of (DivisibleMod L) st v in Lin (DualBasis I) holds
v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #)

proof

let v be Vector of (DivisibleMod L); :: thesis: ( v in Lin (DualBasis I) implies v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #) )
assume B1: v in Lin (DualBasis I) ; :: thesis: v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #)
consider l being Linear_Combination of DualBasis I such that
B2: v = Sum l by B1, VECTSP_7:7;
reconsider J = I as Basis of (EMbedding L) by ThELEM1;
for u being Vector of (DivisibleMod L) st u in J holds
(ScProductDM L) . (v,u) in INT.Ring

proof

let u be Vector of (DivisibleMod L); :: thesis: ( u in J implies (ScProductDM L) . (v,u) in INT.Ring )
assume C1: u in J ; :: thesis: (ScProductDM L) . (v,u) in INT.Ring
C2: (ScProductDM L) . (u,v) = l . ((B2DB I) . u) by B2, C1, LmDE32;
u in dom (B2DB I) by C1, defB2DB;
then (B2DB I) . u in rng (B2DB I) by FUNCT_1:3;
then (B2DB I) . u in DualBasis I ;
then l . ((B2DB I) . u) in the carrier of INT.Ring by FUNCT_2:5;
hence (ScProductDM L) . (v,u) in INT.Ring by C2, ZMODLAT2:6; :: thesis: verum

end;

then v in DL by LmDE21, ThDL1;
hence v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #) ; :: thesis: verum

end;

(Omega). DL is Submodule of DL ;
then ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #) is Submodule of DivisibleMod L by ZMODUL01:42;
then ModuleStr(# the carrier of (DualLat L), the addF of (DualLat L), the ZeroF of (DualLat L), the lmult of (DualLat L) #) = Lin (DualBasis I) by A2, A3, ZMODUL01:46
.= Lin DB by ZMODUL03:20 ;
hence DualBasis I is Basis of (DualLat L) by VECTSP_7:def 3; :: thesis: verum