let L be positive-definite RATional Z_Lattice; for I being Basis of (EMLat L) holds DualBasis I is Basis of (DualLat L)
let I be Basis of (EMLat L); 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)
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)
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);
( 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)
;
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
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 #)
;
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; verum