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)

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)

v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult 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

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

then
DualBasis I c= the carrier of (DualLat L)
;
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;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

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

A3:
for v being Vector of (DivisibleMod L) st v in Lin (DualBasis I) holds
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;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

v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #)

proof

(Omega). DL is Submodule of DL
;
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

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

end;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

then
v in DL
by LmDE21, ThDL1;
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;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

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

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