:: by Yuichi Futa and Yasunari Shidama

::

:: Received June 27, 2017

:: Copyright (c) 2017-2019 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

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

registration

let L be RATional Z_Lattice;

let r be Element of F_Rat;

correctness

coherence

EMLat (r,L) is RATional ;

end;
let r be Element of F_Rat;

correctness

coherence

EMLat (r,L) is RATional ;

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

ex b_{1} being FinSequence of F_Real st

( len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = <;v,((f . (F /. i)) * (F /. i));> ) )

for b_{1}, b_{2} being FinSequence of F_Real st len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = <;v,((f . (F /. i)) * (F /. i));> ) & len b_{2} = len F & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = <;v,((f . (F /. i)) * (F /. i));> ) holds

b_{1} = b_{2}

end;
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 ( len it = len F & ( for i being Nat st i in dom it holds

it . i = <;v,((f . (F /. i)) * (F /. i));> ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being FinSequence of F_Real holds

( b_{5} = ScFS (v,f,F) iff ( len b_{5} = len F & ( for i being Nat st i in dom b_{5} holds

b_{5} . i = <;v,((f . (F /. i)) * (F /. i));> ) ) );

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 b

( b

b

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

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);>*>

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))

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;

ex b_{1} being Element of F_Real ex F being FinSequence of L st

( F is one-to-one & rng F = Carrier l & b_{1} = Sum (ScFS (v,l,F)) )

for b_{1}, b_{2} being Element of F_Real st ex F being FinSequence of L st

( F is one-to-one & rng F = Carrier l & b_{1} = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of L st

( F is one-to-one & rng F = Carrier l & b_{2} = Sum (ScFS (v,l,F)) ) holds

b_{1} = b_{2}

end;
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 F being FinSequence of L st

( F is one-to-one & rng F = Carrier l & it = Sum (ScFS (v,l,F)) );

ex b

( F is one-to-one & rng F = Carrier l & b

proof end;

uniqueness for b

( F is one-to-one & rng F = Carrier l & b

( F is one-to-one & rng F = Carrier l & b

b

proof 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 b_{4} being Element of F_Real holds

( b_{4} = SumSc (v,l) iff ex F being FinSequence of L st

( F is one-to-one & rng F = Carrier l & b_{4} = Sum (ScFS (v,l,F)) ) );

for L being Z_Lattice

for l being Linear_Combination of L

for v being Vector of L

for b

( b

( F is one-to-one & rng F = Carrier l & b

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

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

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

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))

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)

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

ex b_{1} being FinSequence of F_Real st

( len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) )

for b_{1}, b_{2} being FinSequence of F_Real st len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) & len b_{2} = len F & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) holds

b_{1} = b_{2}

end;
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 ( len it = len F & ( for i being Nat st i in dom it holds

it . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being FinSequence of F_Real holds

( b_{5} = ScFS (v,f,F) iff ( len b_{5} = len F & ( for i being Nat st i in dom b_{5} holds

b_{5} . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) ) );

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 b

( b

b

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))

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)))*>

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))

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

ex b_{1} being Element of F_Real ex F being FinSequence of (DivisibleMod L) st

( F is one-to-one & rng F = Carrier l & b_{1} = Sum (ScFS (v,l,F)) )

for b_{1}, b_{2} being Element of F_Real st ex F being FinSequence of (DivisibleMod L) st

( F is one-to-one & rng F = Carrier l & b_{1} = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of (DivisibleMod L) st

( F is one-to-one & rng F = Carrier l & b_{2} = Sum (ScFS (v,l,F)) ) holds

b_{1} = b_{2}

end;
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 F being FinSequence of (DivisibleMod L) st

( F is one-to-one & rng F = Carrier l & it = Sum (ScFS (v,l,F)) );

ex b

( F is one-to-one & rng F = Carrier l & b

proof end;

uniqueness for b

( F is one-to-one & rng F = Carrier l & b

( F is one-to-one & rng F = Carrier l & b

b

proof 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 b_{4} being Element of F_Real holds

( b_{4} = SumSc (v,l) iff ex F being FinSequence of (DivisibleMod L) st

( F is one-to-one & rng F = Carrier l & b_{4} = Sum (ScFS (v,l,F)) ) );

for L being Z_Lattice

for l being Linear_Combination of DivisibleMod L

for v being Vector of (DivisibleMod L)

for b

( b

( F is one-to-one & rng F = Carrier l & b

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

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

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

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))

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))

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)

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 ~ )

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

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

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 ) )

( 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 )

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 ) )

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;

ex b_{1} being Vector of (DivisibleMod L) st

for v being Vector of (DivisibleMod L) st v in EMbedding L holds

(ScProductDM L) . (b_{1},v) in INT.Ring

end;
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 for v being Vector of (DivisibleMod L) st v in EMbedding L holds

(ScProductDM L) . (it,v) in INT.Ring ;

ex b

for v being Vector of (DivisibleMod L) st v in EMbedding L holds

(ScProductDM L) . (b

proof end;

:: deftheorem defDualElement defines Dual ZMODLAT3:def 5 :

for L being Z_Lattice

for b_{2} being Vector of (DivisibleMod L) holds

( b_{2} is Dual of L iff for v being Vector of (DivisibleMod L) st v in EMbedding L holds

(ScProductDM L) . (b_{2},v) in INT.Ring );

for L being Z_Lattice

for b

( b

(ScProductDM L) . (b

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

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;

coherence

{ v where v is Dual of L : verum } is non empty Subset of (DivisibleMod L);

end;
func DualSet L -> non empty Subset of (DivisibleMod L) equals :: ZMODLAT3:def 6

{ v where v is Dual of L : verum } ;

correctness { v where v is Dual of L : verum } ;

coherence

{ v where v is Dual of L : verum } is non empty Subset of (DivisibleMod L);

proof end;

:: deftheorem defines DualSet ZMODLAT3:def 6 :

for L being Z_Lattice holds DualSet L = { v where v is Dual of L : verum } ;

for L being Z_Lattice holds DualSet L = { v where v is Dual of L : verum } ;

definition

let L be Z_Lattice;

ex b_{1} being non empty strict LatticeStr over INT.Ring st

( the carrier of b_{1} = DualSet L & the addF of b_{1} = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b_{1} = 0. (DivisibleMod L) & the lmult of b_{1} = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b_{1} = (ScProductDM L) | [:(DualSet L),(DualSet L):] )

for b_{1}, b_{2} being non empty strict LatticeStr over INT.Ring st the carrier of b_{1} = DualSet L & the addF of b_{1} = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b_{1} = 0. (DivisibleMod L) & the lmult of b_{1} = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b_{1} = (ScProductDM L) | [:(DualSet L),(DualSet L):] & the carrier of b_{2} = DualSet L & the addF of b_{2} = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b_{2} = 0. (DivisibleMod L) & the lmult of b_{2} = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b_{2} = (ScProductDM L) | [:(DualSet L),(DualSet L):] holds

b_{1} = b_{2}
;

end;
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 ( 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):] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defDualMod defines DualLatMod ZMODLAT3:def 7 :

for L being Z_Lattice

for b_{2} being non empty strict LatticeStr over INT.Ring holds

( b_{2} = DualLatMod L iff ( the carrier of b_{2} = DualSet L & the addF of b_{2} = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b_{2} = 0. (DivisibleMod L) & the lmult of b_{2} = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b_{2} = (ScProductDM L) | [:(DualSet L),(DualSet L):] ) );

for L being Z_Lattice

for b

( b

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

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

ex b_{1} being Subset of (DivisibleMod L) st

for v being Vector of (DivisibleMod L) holds

( v in b_{1} 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 b_{1}, b_{2} being Subset of (DivisibleMod L) st ( for v being Vector of (DivisibleMod L) holds

( v in b_{1} 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 b_{2} 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

b_{1} = b_{2}

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

ex b

for v being Vector of (DivisibleMod L) holds

( v in b

( 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 b

( v in b

( 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 b

( 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

b

proof end;

:: deftheorem defDualBasis defines DualBasis ZMODLAT3:def 8 :

for L being positive-definite RATional Z_Lattice

for I being Basis of (EMLat L)

for b_{3} being Subset of (DivisibleMod L) holds

( b_{3} = DualBasis I iff for v being Vector of (DivisibleMod L) holds

( v in b_{3} 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 L being positive-definite RATional Z_Lattice

for I being Basis of (EMLat L)

for b

( b

( v in b

( 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);

ex b_{1} being Function of I,(DualBasis I) st

( dom b_{1} = I & rng b_{1} = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

( (ScProductDM L) . (v,(b_{1} . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds

(ScProductDM L) . (w,(b_{1} . v)) = 0 ) ) ) )

for b_{1}, b_{2} being Function of I,(DualBasis I) st dom b_{1} = I & rng b_{1} = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

( (ScProductDM L) . (v,(b_{1} . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds

(ScProductDM L) . (w,(b_{1} . v)) = 0 ) ) ) & dom b_{2} = I & rng b_{2} = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

( (ScProductDM L) . (v,(b_{2} . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds

(ScProductDM L) . (w,(b_{2} . v)) = 0 ) ) ) holds

b_{1} = b_{2}

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

ex b

( dom b

( (ScProductDM L) . (v,(b

(ScProductDM L) . (w,(b

proof end;

uniqueness for b

( (ScProductDM L) . (v,(b

(ScProductDM L) . (w,(b

( (ScProductDM L) . (v,(b

(ScProductDM L) . (w,(b

b

proof end;

:: deftheorem defB2DB defines B2DB ZMODLAT3:def 9 :

for L being positive-definite RATional Z_Lattice

for I being Basis of (EMLat L)

for b_{3} being Function of I,(DualBasis I) holds

( b_{3} = B2DB I iff ( dom b_{3} = I & rng b_{3} = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds

( (ScProductDM L) . (v,(b_{3} . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds

(ScProductDM L) . (w,(b_{3} . v)) = 0 ) ) ) ) );

for L being positive-definite RATional Z_Lattice

for I being Basis of (EMLat L)

for b

( b

( (ScProductDM L) . (v,(b

(ScProductDM L) . (w,(b

registration

let L be positive-definite RATional Z_Lattice;

let I be Basis of (EMLat L);

correctness

coherence

( B2DB I is onto & B2DB I is one-to-one );

end;
let I be Basis of (EMLat L);

correctness

coherence

( B2DB I is onto & B2DB I is one-to-one );

proof 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)

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

correctness

coherence

DualBasis I is finite ;

end;
let I be Basis of (EMLat L);

correctness

coherence

DualBasis I is finite ;

proof end;

registration

let L be non trivial positive-definite RATional Z_Lattice;

let I be Basis of (EMLat L);

correctness

coherence

not DualBasis I is empty ;

end;
let I be Basis of (EMLat L);

correctness

coherence

not DualBasis I is empty ;

proof 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)

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)

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

correctness

coherence

DualBasis I is linearly-independent ;

end;
let I be Basis of (EMLat L);

correctness

coherence

DualBasis I is linearly-independent ;

proof end;

definition

let L be positive-definite RATional Z_Lattice;

ex b_{1} being strict Z_Lattice st

( the carrier of b_{1} = DualSet L & 0. b_{1} = 0. (DivisibleMod L) & the addF of b_{1} = the addF of (DivisibleMod L) || the carrier of b_{1} & the lmult of b_{1} = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b_{1}:] & the scalar of b_{1} = (ScProductDM L) || the carrier of b_{1} )

for b_{1}, b_{2} being strict Z_Lattice st the carrier of b_{1} = DualSet L & 0. b_{1} = 0. (DivisibleMod L) & the addF of b_{1} = the addF of (DivisibleMod L) || the carrier of b_{1} & the lmult of b_{1} = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b_{1}:] & the scalar of b_{1} = (ScProductDM L) || the carrier of b_{1} & the carrier of b_{2} = DualSet L & 0. b_{2} = 0. (DivisibleMod L) & the addF of b_{2} = the addF of (DivisibleMod L) || the carrier of b_{2} & the lmult of b_{2} = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b_{2}:] & the scalar of b_{2} = (ScProductDM L) || the carrier of b_{2} holds

b_{1} = b_{2}
;

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defDualLat defines DualLat ZMODLAT3:def 10 :

for L being positive-definite RATional Z_Lattice

for b_{2} being strict Z_Lattice holds

( b_{2} = DualLat L iff ( the carrier of b_{2} = DualSet L & 0. b_{2} = 0. (DivisibleMod L) & the addF of b_{2} = the addF of (DivisibleMod L) || the carrier of b_{2} & the lmult of b_{2} = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b_{2}:] & the scalar of b_{2} = (ScProductDM L) || the carrier of b_{2} ) );

for L being positive-definite RATional Z_Lattice

for b

( b

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 )

for v being Vector of (DivisibleMod L) holds

( v in DualLat L iff v is Dual of 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

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)

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

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)

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 :: 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

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

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

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

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

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;

correctness

coherence

DualLat L is RATional ;

end;
correctness

coherence

DualLat L is RATional ;

proof 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

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

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

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;

correctness

coherence

DualLat L is positive-definite ;

end;
correctness

coherence

DualLat L is positive-definite ;

proof end;

registration

let L be non trivial positive-definite RATional Z_Lattice;

correctness

coherence

not DualLat L is trivial ;

end;
correctness

coherence

not DualLat L is trivial ;

proof end;