:: Dual Lattice of $\mathbb Z$-module Lattice
:: by Yuichi Futa and Yasunari Shidama
::
:: Received June 27, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


theorem ThSLGM1: :: ZMODLAT3:1
for L being RATional Z_Lattice
for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
LX is RATional
proof end;

registration
let L be RATional Z_Lattice;
cluster EMLat L -> RATional ;
correctness
coherence
EMLat L is RATional
;
proof end;
end;

registration
let L be RATional Z_Lattice;
let r be Element of F_Rat;
cluster EMLat (r,L) -> RATional ;
correctness
coherence
EMLat (r,L) is RATional
;
proof end;
end;

definition
let L be Z_Lattice;
let F be FinSequence of L;
let f be Function of L,INT.Ring;
let v be Vector of L;
func ScFS (v,f,F) -> FinSequence of F_Real means :defScFS: :: ZMODLAT3:def 1
( len it = len F & ( for i being Nat st i in dom it holds
it . i = <;v,((f . (F /. i)) * (F /. i));> ) );
existence
ex b1 being FinSequence of F_Real st
( len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = <;v,((f . (F /. i)) * (F /. i));> ) )
proof end;
uniqueness
for b1, b2 being FinSequence of F_Real st len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = <;v,((f . (F /. i)) * (F /. i));> ) & len b2 = len F & ( for i being Nat st i in dom b2 holds
b2 . i = <;v,((f . (F /. i)) * (F /. i));> ) holds
b1 = b2
proof end;
end;

:: deftheorem defScFS defines ScFS ZMODLAT3:def 1 :
for L being Z_Lattice
for F being FinSequence of L
for f being Function of L,INT.Ring
for v being Vector of L
for b5 being FinSequence of F_Real holds
( b5 = ScFS (v,f,F) iff ( len b5 = len F & ( for i being Nat st i in dom b5 holds
b5 . i = <;v,((f . (F /. i)) * (F /. i));> ) ) );

theorem ThScFS1: :: ZMODLAT3:2
for L being Z_Lattice
for f being Function of L,INT.Ring
for F being FinSequence of L
for v, u being Vector of L
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = <;v,((f . u) * u);>
proof end;

theorem ThScFS3: :: ZMODLAT3:3
for L being Z_Lattice
for f being Function of L,INT.Ring
for v, u being Vector of L holds ScFS (v,f,<*u*>) = <*<;v,((f . u) * u);>*>
proof end;

theorem ThScFS6: :: ZMODLAT3:4
for L being Z_Lattice
for f being Function of L,INT.Ring
for F, G being FinSequence of L
for v being Vector of L holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))
proof end;

definition
let L be Z_Lattice;
let l be Linear_Combination of L;
let v be Vector of L;
func SumSc (v,l) -> Element of F_Real means :defSumSc: :: ZMODLAT3:def 2
ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & it = Sum (ScFS (v,l,F)) );
existence
ex b1 being Element of F_Real ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & b1 = Sum (ScFS (v,l,F)) )
proof end;
uniqueness
for b1, b2 being Element of F_Real st ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & b1 = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & b2 = Sum (ScFS (v,l,F)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defSumSc defines SumSc ZMODLAT3:def 2 :
for L being Z_Lattice
for l being Linear_Combination of L
for v being Vector of L
for b4 being Element of F_Real holds
( b4 = SumSc (v,l) iff ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & b4 = Sum (ScFS (v,l,F)) ) );

theorem LmSumSc11: :: ZMODLAT3:5
for L being Z_Lattice
for v being Vector of L holds SumSc (v,(ZeroLC L)) = 0. F_Real
proof end;

theorem :: ZMODLAT3:6
for L being Z_Lattice
for v being Vector of L
for l being Linear_Combination of {} the carrier of L holds SumSc (v,l) = 0. F_Real
proof end;

theorem LmSumSc13: :: ZMODLAT3:7
for L being Z_Lattice
for v being Vector of L
for l being Linear_Combination of L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real
proof end;

theorem LmSumSc14: :: ZMODLAT3:8
for L being Z_Lattice
for v, u being Vector of L
for l being Linear_Combination of {u} holds SumSc (v,l) = <;v,((l . u) * u);>
proof end;

theorem LmSumSc1X: :: ZMODLAT3:9
for L being Z_Lattice
for v being Vector of L
for l1, l2 being Linear_Combination of L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))
proof end;

theorem ThSumSc1: :: ZMODLAT3:10
for L being Z_Lattice
for l being Linear_Combination of L
for v being Vector of L holds <;v,(Sum l);> = SumSc (v,l)
proof end;

definition
let L be Z_Lattice;
let F be FinSequence of (DivisibleMod L);
let f be Function of (DivisibleMod L),INT.Ring;
let v be Vector of (DivisibleMod L);
func ScFS (v,f,F) -> FinSequence of F_Real means :defScFSDM: :: ZMODLAT3:def 3
( len it = len F & ( for i being Nat st i in dom it holds
it . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) );
existence
ex b1 being FinSequence of F_Real st
( len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of F_Real st len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) & len b2 = len F & ( for i being Nat st i in dom b2 holds
b2 . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) holds
b1 = b2
proof end;
end;

:: deftheorem defScFSDM defines ScFS ZMODLAT3:def 3 :
for L being Z_Lattice
for F being FinSequence of (DivisibleMod L)
for f being Function of (DivisibleMod L),INT.Ring
for v being Vector of (DivisibleMod L)
for b5 being FinSequence of F_Real holds
( b5 = ScFS (v,f,F) iff ( len b5 = len F & ( for i being Nat st i in dom b5 holds
b5 . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) ) );

theorem ThScFSDM1: :: ZMODLAT3:11
for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for F being FinSequence of (DivisibleMod L)
for v, u being Vector of (DivisibleMod L)
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))
proof end;

theorem ThScFSDM3: :: ZMODLAT3:12
for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for v, u being Vector of (DivisibleMod L) holds ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>
proof end;

theorem ThScFSDM6: :: ZMODLAT3:13
for L being Z_Lattice
for f being Function of (DivisibleMod L),INT.Ring
for F, G being FinSequence of (DivisibleMod L)
for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))
proof end;

definition
let L be Z_Lattice;
let l be Linear_Combination of DivisibleMod L;
let v be Vector of (DivisibleMod L);
func SumSc (v,l) -> Element of F_Real means :defSumScDM: :: ZMODLAT3:def 4
ex F being FinSequence of (DivisibleMod L) st
( F is one-to-one & rng F = Carrier l & it = Sum (ScFS (v,l,F)) );
existence
ex b1 being Element of F_Real ex F being FinSequence of (DivisibleMod L) st
( F is one-to-one & rng F = Carrier l & b1 = Sum (ScFS (v,l,F)) )
proof end;
uniqueness
for b1, b2 being Element of F_Real st ex F being FinSequence of (DivisibleMod L) st
( F is one-to-one & rng F = Carrier l & b1 = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of (DivisibleMod L) st
( F is one-to-one & rng F = Carrier l & b2 = Sum (ScFS (v,l,F)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defSumScDM defines SumSc ZMODLAT3:def 4 :
for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L)
for b4 being Element of F_Real holds
( b4 = SumSc (v,l) iff ex F being FinSequence of (DivisibleMod L) st
( F is one-to-one & rng F = Carrier l & b4 = Sum (ScFS (v,l,F)) ) );

theorem LmSumScDM11: :: ZMODLAT3:14
for L being Z_Lattice
for v being Vector of (DivisibleMod L) holds SumSc (v,(ZeroLC (DivisibleMod L))) = 0. F_Real
proof end;

theorem :: ZMODLAT3:15
for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of {} the carrier of (DivisibleMod L) holds SumSc (v,l) = 0. F_Real
proof end;

theorem LmSumScDM13: :: ZMODLAT3:16
for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of DivisibleMod L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real
proof end;

theorem LmSumScDM14: :: ZMODLAT3:17
for L being Z_Lattice
for v, u being Vector of (DivisibleMod L)
for l being Linear_Combination of {u} holds SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u))
proof end;

theorem LmSumScDM1X: :: ZMODLAT3:18
for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for l1, l2 being Linear_Combination of DivisibleMod L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))
proof end;

theorem ThSumScDM1: :: ZMODLAT3:19
for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)
proof end;

theorem INVMN1: :: ZMODLAT3:20
for n being Nat
for M being Matrix of n,F_Real
for H being Matrix of n,F_Rat st M = H & M is invertible holds
( H is invertible & M ~ = H ~ )
proof end;

theorem INVMN2: :: ZMODLAT3:21
for n being Nat
for M being Matrix of n,F_Real st M is Matrix of n,F_Rat & M is invertible holds
M ~ is Matrix of n,F_Rat
proof end;

theorem ThGM3: :: ZMODLAT3:22
for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L holds (GramMatrix b) ~ is Matrix of dim L,F_Rat
proof end;

theorem LmDE311A: :: ZMODLAT3:23
for X being finite Subset of RAT ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
proof end;

theorem LmDE311: :: ZMODLAT3:24
for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L ex a being Element of F_Real st
( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )
proof end;

LM0: for n being Nat
for F being FinSequence of F_Real st F = (Seg n) --> (0. F_Real) holds
Sum F = 0. F_Real

proof end;

LM1: for L being Z_Lattice
for F, F0 being FinSequence of L
for l being Linear_Combination of L
for v being Vector of L st F is one-to-one & F0 is one-to-one & Carrier l c= rng F & canFS (Carrier l) = F0 holds
Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0))

proof end;

theorem LmDE31: :: ZMODLAT3:25
for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of EMLat L
for i being Nat st i in dom b holds
ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) )
proof end;

LmDE00: for L being Z_Lattice
for v being Vector of (DivisibleMod L) holds (ScProductDM L) . ((0. (DivisibleMod L)),v) in INT.Ring

proof end;

definition
let L be Z_Lattice;
mode Dual of L -> Vector of (DivisibleMod L) means :defDualElement: :: ZMODLAT3:def 5
for v being Vector of (DivisibleMod L) st v in EMbedding L holds
(ScProductDM L) . (it,v) in INT.Ring ;
existence
ex b1 being Vector of (DivisibleMod L) st
for v being Vector of (DivisibleMod L) st v in EMbedding L holds
(ScProductDM L) . (b1,v) in INT.Ring
proof end;
end;

:: deftheorem defDualElement defines Dual ZMODLAT3:def 5 :
for L being Z_Lattice
for b2 being Vector of (DivisibleMod L) holds
( b2 is Dual of L iff for v being Vector of (DivisibleMod L) st v in EMbedding L holds
(ScProductDM L) . (b2,v) in INT.Ring );

theorem LmDE0: :: ZMODLAT3:26
for L being Z_Lattice holds 0. (DivisibleMod L) is Dual of L
proof end;

theorem LmDE1: :: ZMODLAT3:27
for L being Z_Lattice
for v, u being Dual of L holds v + u is Dual of L
proof end;

theorem LmDE2: :: ZMODLAT3:28
for L being Z_Lattice
for v being Dual of L
for a being Element of INT.Ring holds a * v is Dual of L
proof end;

definition
let L be Z_Lattice;
func DualSet L -> non empty Subset of (DivisibleMod L) equals :: ZMODLAT3:def 6
{ v where v is Dual of L : verum } ;
correctness
coherence
{ v where v is Dual of L : verum } is non empty Subset of (DivisibleMod L)
;
proof end;
end;

:: deftheorem defines DualSet ZMODLAT3:def 6 :
for L being Z_Lattice holds DualSet L = { v where v is Dual of L : verum } ;

registration
let L be Z_Lattice;
cluster DualSet L -> non empty linearly-closed ;
coherence
DualSet L is linearly-closed
proof end;
end;

definition
let L be Z_Lattice;
func DualLatMod L -> non empty strict LatticeStr over INT.Ring means :defDualMod: :: ZMODLAT3:def 7
( the carrier of it = DualSet L & the addF of it = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of it = 0. (DivisibleMod L) & the lmult of it = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of it = (ScProductDM L) | [:(DualSet L),(DualSet L):] );
existence
ex b1 being non empty strict LatticeStr over INT.Ring st
( the carrier of b1 = DualSet L & the addF of b1 = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b1 = 0. (DivisibleMod L) & the lmult of b1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b1 = (ScProductDM L) | [:(DualSet L),(DualSet L):] )
proof end;
uniqueness
for b1, b2 being non empty strict LatticeStr over INT.Ring st the carrier of b1 = DualSet L & the addF of b1 = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b1 = 0. (DivisibleMod L) & the lmult of b1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b1 = (ScProductDM L) | [:(DualSet L),(DualSet L):] & the carrier of b2 = DualSet L & the addF of b2 = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b2 = 0. (DivisibleMod L) & the lmult of b2 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b2 = (ScProductDM L) | [:(DualSet L),(DualSet L):] holds
b1 = b2
;
end;

:: deftheorem defDualMod defines DualLatMod ZMODLAT3:def 7 :
for L being Z_Lattice
for b2 being non empty strict LatticeStr over INT.Ring holds
( b2 = DualLatMod L iff ( the carrier of b2 = DualSet L & the addF of b2 = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b2 = 0. (DivisibleMod L) & the lmult of b2 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b2 = (ScProductDM L) | [:(DualSet L),(DualSet L):] ) );

theorem :: ZMODLAT3:29
for L being Z_Lattice holds DualLatMod L is Submodule of DivisibleMod L
proof end;

theorem LmDE21: :: ZMODLAT3:30
for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring ) holds
v is Dual of L
proof end;

definition
let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);
func DualBasis I -> Subset of (DivisibleMod L) means :defDualBasis: :: ZMODLAT3:def 8
for v being Vector of (DivisibleMod L) holds
( v in it iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) );
existence
ex b1 being Subset of (DivisibleMod L) st
for v being Vector of (DivisibleMod L) holds
( v in b1 iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of (DivisibleMod L) st ( for v being Vector of (DivisibleMod L) holds
( v in b1 iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) ) ) & ( for v being Vector of (DivisibleMod L) holds
( v in b2 iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defDualBasis defines DualBasis ZMODLAT3:def 8 :
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for b3 being Subset of (DivisibleMod L) holds
( b3 = DualBasis I iff for v being Vector of (DivisibleMod L) holds
( v in b3 iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) ) );

definition
let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);
func B2DB I -> Function of I,(DualBasis I) means :defB2DB: :: ZMODLAT3:def 9
( dom it = I & rng it = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(it . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(it . v)) = 0 ) ) ) );
existence
ex b1 being Function of I,(DualBasis I) st
( dom b1 = I & rng b1 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(b1 . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(b1 . v)) = 0 ) ) ) )
proof end;
uniqueness
for b1, b2 being Function of I,(DualBasis I) st dom b1 = I & rng b1 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(b1 . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(b1 . v)) = 0 ) ) ) & dom b2 = I & rng b2 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(b2 . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(b2 . v)) = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defB2DB defines B2DB ZMODLAT3:def 9 :
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for b3 being Function of I,(DualBasis I) holds
( b3 = B2DB I iff ( dom b3 = I & rng b3 = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(b3 . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(b3 . v)) = 0 ) ) ) ) );

registration
let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);
cluster B2DB I -> one-to-one onto ;
correctness
coherence
( B2DB I is onto & B2DB I is one-to-one )
;
proof end;
end;

theorem ThDB1: :: ZMODLAT3:31
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L) holds card I = card (DualBasis I)
proof end;

registration
let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);
cluster DualBasis I -> finite ;
correctness
coherence
DualBasis I is finite
;
proof end;
end;

registration
let L be non trivial positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);
cluster DualBasis I -> non empty ;
correctness
coherence
not DualBasis I is empty
;
proof end;
end;

theorem LmDE32: :: ZMODLAT3:32
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of DualBasis I st v in I holds
(ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)
proof end;

theorem ThDE3: :: ZMODLAT3:33
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for v being Vector of (DivisibleMod L) st v is Dual of L holds
v in Lin (DualBasis I)
proof end;

registration
let L be positive-definite RATional Z_Lattice;
let I be Basis of (EMLat L);
cluster DualBasis I -> linearly-independent ;
correctness
coherence
DualBasis I is linearly-independent
;
proof end;
end;

definition
let L be positive-definite RATional Z_Lattice;
func DualLat L -> strict Z_Lattice means :defDualLat: :: ZMODLAT3:def 10
( the carrier of it = DualSet L & 0. it = 0. (DivisibleMod L) & the addF of it = the addF of (DivisibleMod L) || the carrier of it & the lmult of it = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of it:] & the scalar of it = (ScProductDM L) || the carrier of it );
existence
ex b1 being strict Z_Lattice st
( the carrier of b1 = DualSet L & 0. b1 = 0. (DivisibleMod L) & the addF of b1 = the addF of (DivisibleMod L) || the carrier of b1 & the lmult of b1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b1:] & the scalar of b1 = (ScProductDM L) || the carrier of b1 )
proof end;
uniqueness
for b1, b2 being strict Z_Lattice st the carrier of b1 = DualSet L & 0. b1 = 0. (DivisibleMod L) & the addF of b1 = the addF of (DivisibleMod L) || the carrier of b1 & the lmult of b1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b1:] & the scalar of b1 = (ScProductDM L) || the carrier of b1 & the carrier of b2 = DualSet L & 0. b2 = 0. (DivisibleMod L) & the addF of b2 = the addF of (DivisibleMod L) || the carrier of b2 & the lmult of b2 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b2:] & the scalar of b2 = (ScProductDM L) || the carrier of b2 holds
b1 = b2
;
end;

:: deftheorem defDualLat defines DualLat ZMODLAT3:def 10 :
for L being positive-definite RATional Z_Lattice
for b2 being strict Z_Lattice holds
( b2 = DualLat L iff ( the carrier of b2 = DualSet L & 0. b2 = 0. (DivisibleMod L) & the addF of b2 = the addF of (DivisibleMod L) || the carrier of b2 & the lmult of b2 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b2:] & the scalar of b2 = (ScProductDM L) || the carrier of b2 ) );

theorem ThDL1: :: ZMODLAT3:34
for L being positive-definite RATional Z_Lattice
for v being Vector of (DivisibleMod L) holds
( v in DualLat L iff v is Dual of L )
proof end;

theorem ThDL2: :: ZMODLAT3:35
for L being positive-definite RATional Z_Lattice holds DualLat L is Submodule of DivisibleMod L
proof end;

theorem ThELEM1: :: ZMODLAT3:36
for L being Z_Lattice
for I being Basis of (EMLat L) holds I is Basis of (EMbedding L)
proof end;

theorem :: ZMODLAT3:37
for L being Z_Lattice
for I being Basis of (EMbedding L) holds I is Basis of (EMLat L)
proof end;

theorem ThDB2: :: ZMODLAT3:38
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for v being Vector of (DivisibleMod L) st v in DualBasis I holds
v is Dual of L
proof end;

theorem ThDLDB: :: ZMODLAT3:39
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L) holds DualBasis I is Basis of (DualLat L)
proof end;

theorem :: ZMODLAT3:40
for L being positive-definite RATional Z_Lattice
for b being OrdBasis of EMLat L
for I being Basis of (EMLat L) st I = rng b holds
(B2DB I) * b is OrdBasis of DualLat L
proof end;

theorem LmEMDetX3: :: ZMODLAT3:41
for L being positive-definite Z_Lattice
for b being OrdBasis of L
for e being OrdBasis of EMLat L st e = (MorphsZQ L) * b holds
GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e)
proof end;

theorem :: ZMODLAT3:42
for L being positive-definite Z_Lattice holds GramDet (InnerProduct L) = GramDet (InnerProduct (EMLat L))
proof end;

theorem ThRankDL: :: ZMODLAT3:43
for L being positive-definite RATional Z_Lattice holds rank L = rank (DualLat L)
proof end;

theorem :: ZMODLAT3:44
for L being INTegral positive-definite Z_Lattice holds EMLat L is Z_Sublattice of DualLat L
proof end;

theorem :: ZMODLAT3:45
for L being Z_Lattice
for b being OrdBasis of L st GramMatrix ((InnerProduct L),b) is Matrix of dim L,INT.Ring holds
L is INTegral
proof end;

theorem ThRatLat1B: :: ZMODLAT3:46
for L being Z_Lattice
for I being finite Subset of L
for u being Vector of L st ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in RAT
proof end;

theorem ThRatLat1A: :: ZMODLAT3:47
for L being Z_Lattice
for I being Basis of L st ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) holds
for v, u being Vector of L holds <;v,u;> in RAT
proof end;

theorem ThRatLat1: :: ZMODLAT3:48
for L being Z_Lattice
for I being Basis of L st ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) holds
L is RATional
proof end;

theorem :: ZMODLAT3:49
for L being Z_Lattice
for b being OrdBasis of L st GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat holds
L is RATional
proof end;

registration
let L be positive-definite RATional Z_Lattice;
cluster DualLat L -> strict RATional ;
correctness
coherence
DualLat L is RATional
;
proof end;
end;

theorem ThSLGM2: :: ZMODLAT3:50
for L being RATional Z_Lattice
for LX being Z_Lattice
for b being OrdBasis of LX st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
GramMatrix ((InnerProduct LX),b) is Matrix of dim LX,F_Rat
proof end;

theorem :: ZMODLAT3:51
for L being positive-definite RATional Z_Lattice
for b being OrdBasis of DualLat L holds GramMatrix ((InnerProduct (DualLat L)),b) is Matrix of dim L,F_Rat
proof end;

theorem ThSLGM3: :: ZMODLAT3:52
for L being positive-definite Z_Lattice
for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
LX is positive-definite
proof end;

registration
let L be positive-definite RATional Z_Lattice;
cluster DualLat L -> strict positive-definite ;
correctness
coherence
DualLat L is positive-definite
;
proof end;
end;

registration
let L be non trivial positive-definite RATional Z_Lattice;
cluster DualLat L -> non trivial strict ;
correctness
coherence
not DualLat L is trivial
;
proof end;
end;