let L be positive-definite RATional Z_Lattice; :: thesis: for I being Basis of () holds DualBasis I is Basis of ()
let I be Basis of (); :: thesis: DualBasis I is Basis of ()
reconsider DL = DualLat L as Submodule of DivisibleMod L by ThDL2;
for v being Vector of () st v in DualBasis I holds
v in the carrier of ()
proof
let v be Vector of (); :: thesis: ( v in DualBasis I implies v in the carrier of () )
assume B1: v in DualBasis I ; :: thesis: v in the carrier of ()
v in DualLat L by ;
hence v in the carrier of () ; :: thesis: verum
end;
then DualBasis I c= the carrier of () ;
then reconsider DB = DualBasis I as linearly-independent Subset of DL by ZMODUL03:16;
A2: for v being Vector of () st v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #) holds
v in Lin ()
proof
let v be Vector of (); :: thesis: ( v in ModuleStr(# the carrier of DL, the addF of DL, the ZeroF of DL, the lmult of DL #) implies v in Lin () )
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 ()
v in DualLat L by B1;
hence v in Lin () by ; :: thesis: verum
end;
A3: for v being Vector of () st v in Lin () 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 (); :: thesis: ( v in Lin () 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 () ; :: 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 ;
reconsider J = I as Basis of () by ThELEM1;
for u being Vector of () st u in J holds
() . (v,u) in INT.Ring
proof
let u be Vector of (); :: thesis: ( u in J implies () . (v,u) in INT.Ring )
assume C1: u in J ; :: thesis: () . (v,u) in INT.Ring
C2: (ScProductDM L) . (u,v) = l . ((B2DB I) . u) by ;
u in dom (B2DB I) by ;
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 ; :: thesis: verum
end;
then v in DL by ;
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 (), the addF of (), the ZeroF of (), the lmult of () #) = Lin () by
.= Lin DB by ZMODUL03:20 ;
hence DualBasis I is Basis of () by VECTSP_7:def 3; :: thesis: verum