ZMODLAT2: Embedded Lattice and Properties of {G}ram Matrix

:: Embedded Lattice and Properties of {G}ram Matrix
:: by Yuichi Futa and Yasunari Shidama
::
:: Received March 17, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

LMBASE2A: for A, B being set
for F, G being FinSequence st F is one-to-one & G is one-to-one & A /\ B = {} & rng F = A & rng G = B holds
( F ^ G is one-to-one & dom (F ^ G) = Seg ((len F) + (len G)) & rng (F ^ G) = (rng F) \/ (rng G) )

proof end;

LMBASE2C: for K being Ring
for V being LeftMod of K
for L being Linear_Combination of V
for F being FinSequence of V st (rng F) /\ (Carrier L) = {} holds
L (#) F = (dom F) --> (0. V)

proof end;

LMBASE2D: for K being Ring
for V being LeftMod of K
for F being FinSequence of V st F = (dom F) --> (0. V) holds
Sum F = 0. V

proof end;

theorem EQSUMLF: :: ZMODLAT2:1

for K being Ring
for V being LeftMod of K
for L being Function of the carrier of V, the carrier of K
for A being Subset of V
for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds
Sum (L (#) F) = Sum (L (#) F1)

proof end;

theorem LMBASE2X: :: ZMODLAT2:2

for K being Ring
for V being LeftMod of K
for A being finite Subset of V holds
( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds
Carrier L = {} )

proof end;

theorem LMBASE2: :: ZMODLAT2:3

for K being Ring
for V being LeftMod of K
for b being FinSequence of V st b is one-to-one holds
( rng b is linearly-independent iff for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) )

proof end;

theorem :: ZMODLAT2:4

for K being Ring
for V being LeftMod of K
for A being finite Subset of V holds
( A is linearly-independent iff ex b being FinSequence of V st
( b is one-to-one & rng b = A & ( for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) ) ) )

proof end;

registration

let V be non trivial free Z_Module;

cluster base -> non empty for Element of bool the carrier of V;

correctness

proof end;

end;

definition

let IT be Z_Lattice;

attr IT is RATional means :defRational: :: ZMODLAT2:def 1
for v, u being Vector of IT holds <;v,u;> in RAT ;

end;

:: deftheorem defRational defines RATional ZMODLAT2:def 1 :

registration

cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() Mult-cancelable free finite-rank finitely-generated Z_Lattice-like positive-definite V259() RATional for LatticeStr over INT.Ring ;

correctness

proof end;

end;

registration

let L be RATional Z_Lattice;
let v, u be Vector of L;

cluster <;v,u;> -> rational ;

correctness by defRational, RAT_1:def 2;

end;

registration

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank Z_Lattice-like INTegral -> INTegral RATional for LatticeStr over INT.Ring ;

correctness by RAT_1:def 2;

end;

LMINTFREAL1: for x being Element of INT
for y being Element of F_Real st x <> 0 & x = y holds
x " = y "

proof end;

definition

let L be Z_Lattice;

func ScProductEM L -> Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real means :defScProductEM: :: ZMODLAT2:def 2
for v, u being Vector of L
for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds
it . (vv,uu) = <;v,u;>;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defScProductEM defines ScProductEM ZMODLAT2:def 2 :

theorem ThSPEM1: :: ZMODLAT2:5

for L being Z_Lattice holds
( ( for x being Vector of (EMbedding L) st ( for y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = 0 ) holds
x = 0. (EMbedding L) ) & ( for x, y being Vector of (EMbedding L) holds (ScProductEM L) . (x,y) = (ScProductEM L) . (y,x) ) & ( for x, y, z being Vector of (EMbedding L)
for a being Element of INT.Ring holds
( (ScProductEM L) . ((x + y),z) = ((ScProductEM L) . (x,z)) + ((ScProductEM L) . (y,z)) & (ScProductEM L) . ((a * x),y) = a * ((ScProductEM L) . (x,y)) ) ) )

proof end;

definition

let L be Z_Lattice;

func ScProductDM L -> Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):], the carrier of F_Real means :defScProductDM: :: ZMODLAT2:def 3
for vv, uu being Vector of (DivisibleMod L)
for v, u being Vector of (EMbedding L)
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
it . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u));

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defScProductDM defines ScProductDM ZMODLAT2:def 3 :

theorem ThSPDM1: :: ZMODLAT2:6

for L being Z_Lattice holds
( ( for x being Vector of (DivisibleMod L) st ( for y being Vector of (DivisibleMod L) holds (ScProductDM L) . (x,y) = 0 ) holds
x = 0. (DivisibleMod L) ) & ( for x, y being Vector of (DivisibleMod L) holds (ScProductDM L) . (x,y) = (ScProductDM L) . (y,x) ) & ( for x, y, z being Vector of (DivisibleMod L)
for a being Element of INT.Ring holds
( (ScProductDM L) . ((x + y),z) = ((ScProductDM L) . (x,z)) + ((ScProductDM L) . (y,z)) & (ScProductDM L) . ((a * x),y) = a * ((ScProductDM L) . (x,y)) ) ) )

proof end;

theorem ThSPEM2: :: ZMODLAT2:7

for L being Z_Lattice holds ScProductEM L = (ScProductDM L) || (rng (MorphsZQ L))

proof end;

theorem ThSPEM3: :: ZMODLAT2:8

for L being Z_Lattice
for v1, v2 being Vector of (DivisibleMod L)
for u1, u2 being Vector of (EMbedding L) st v1 = u1 & v2 = u2 holds
(ScProductEM L) . (u1,u2) = (ScProductDM L) . (v1,v2)

proof end;

theorem ThSPrEM1: :: ZMODLAT2:9

for L being Z_Lattice
for r being Element of F_Rat
for v, u being Vector of (EMbedding (r,L)) holds ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,u) = (ScProductDM L) . (v,u)

proof end;

theorem :: ZMODLAT2:10

for L being Z_Lattice
for A being non empty set
for ze being Element of A
for ad being BinOp of A
for mu being Function of [: the carrier of INT.Ring,A:],A
for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds
LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

proof end;

theorem ThScDM1: :: ZMODLAT2:11

for L being Z_Lattice
for v, u being Vector of (DivisibleMod L) holds
( (ScProductDM L) . ((- v),u) = - ((ScProductDM L) . (v,u)) & (ScProductDM L) . (u,(- v)) = - ((ScProductDM L) . (u,v)) )

proof end;

theorem :: ZMODLAT2:12

for L being Z_Lattice
for v, u, w being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(u + w)) = ((ScProductDM L) . (v,u)) + ((ScProductDM L) . (v,w))

proof end;

theorem :: ZMODLAT2:13

for L being Z_Lattice
for v, u being Vector of (DivisibleMod L)
for a being Element of INT.Ring holds (ScProductDM L) . (v,(a * u)) = a * ((ScProductDM L) . (v,u))

proof end;

theorem ThScDM6: :: ZMODLAT2:14

for L being Z_Lattice
for v being Vector of (DivisibleMod L) holds
( (ScProductDM L) . ((0. (DivisibleMod L)),v) = 0 & (ScProductDM L) . (v,(0. (DivisibleMod L))) = 0 )

proof end;

theorem LmDE22: :: ZMODLAT2:15

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) = 0 ) holds
for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0

proof end;

theorem :: ZMODLAT2:16

proof end;

theorem :: ZMODLAT2:17

for R being Ring
for V being LeftMod of R
for v being Vector of V
for u being object st u in Lin {v} holds
ex i being Element of R st u = i * v

proof end;

theorem ThLin2: :: ZMODLAT2:18

for R being Ring
for V being LeftMod of R
for v being Vector of V holds v in Lin {v} by VECTSP_7:8, ZFMISC_1:31;

theorem :: ZMODLAT2:19

for R being Ring
for V being LeftMod of R
for v being Vector of V
for i being Element of R holds i * v in Lin {v} by ThLin2, VECTSP_4:21;

definition

let L be Z_Lattice;

func EMLat L -> strict Z_Lattice means :defEMLat: :: ZMODLAT2:def 4
( the carrier of it = rng (MorphsZQ L) & the ZeroF of it = zeroCoset L & the addF of it = (addCoset L) || (rng (MorphsZQ L)) & the lmult of it = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of it = ScProductEM L );

existence

proof end;

uniqueness ;

end;

:: deftheorem defEMLat defines EMLat ZMODLAT2:def 4 :

definition

let L be Z_Lattice;
let r be Element of F_Rat;

func EMLat (r,L) -> strict Z_Lattice means :defrEMLat: :: ZMODLAT2:def 5
( the carrier of it = r * (rng (MorphsZQ L)) & the ZeroF of it = zeroCoset L & the addF of it = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of it = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of it = (ScProductDM L) || (r * (rng (MorphsZQ L))) );

existence

proof end;

uniqueness ;

end;

:: deftheorem defrEMLat defines EMLat ZMODLAT2:def 5 :

registration

let L be non trivial Z_Lattice;

cluster EMLat L -> non trivial strict ;

correctness

proof end;

end;

registration

let L be non trivial Z_Lattice;
let r be non zero Element of F_Rat;

cluster EMLat (r,L) -> non trivial strict ;

correctness

proof end;

end;

registration

let L be INTegral Z_Lattice;

cluster EMLat L -> strict INTegral ;

correctness

proof end;

end;

theorem ThDivisibleL1: :: ZMODLAT2:20

for L being Z_Lattice holds EMLat L is Submodule of DivisibleMod L

proof end;

theorem ThDivisibleL2: :: ZMODLAT2:21

for L being Z_Lattice
for r being Element of F_Rat holds EMLat (r,L) is Submodule of DivisibleMod L

proof end;

theorem ThrEMLat1: :: ZMODLAT2:22

for L being Z_Lattice
for r being non zero Element of F_Rat
for m, n being Element of INT.Ring
for m1, n1 being Element of INT
for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of (EMLat L) st n * v = m * x

proof end;

theorem ThrEMLat2: :: ZMODLAT2:23

for L being Z_Lattice
for r being Element of F_Rat
for v, u being Vector of (EMLat (r,L))
for x, y being Vector of (EMLat L) st v = x & u = y holds
<;v,u;> = <;x,y;>

proof end;

theorem :: ZMODLAT2:24

for L being INTegral Z_Lattice
for r being non zero Element of F_Rat
for a being Rational
for v, u being Vector of (EMLat (r,L)) st r = a holds
((a ") * (a ")) * <;v,u;> in INT

proof end;

registration

let L be positive-definite Z_Lattice;

cluster EMLat L -> strict positive-definite ;

correctness

proof end;

end;

registration

let L be positive-definite Z_Lattice;
let r be non zero Element of F_Rat;

cluster EMLat (r,L) -> strict positive-definite ;

correctness

proof end;

end;

theorem ThSPDM2: :: ZMODLAT2:25

for L being positive-definite Z_Lattice
for v being Vector of (DivisibleMod L) holds
( (ScProductDM L) . (v,v) = 0 iff v = 0. (DivisibleMod L) )

proof end;

theorem ThSLX2: :: ZMODLAT2:26

for L being positive-definite Z_Lattice
for Z being non empty LatticeStr over INT.Ring st Z is Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z holds
Z is Z_Lattice-like

proof end;

theorem :: ZMODLAT2:27

for L being positive-definite Z_Lattice
for Z being non empty LatticeStr over INT.Ring st Z is finitely-generated Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z holds
Z is Z_Lattice by ThSLX2;

theorem LmEMDetX0: :: ZMODLAT2:28

for L being Z_Lattice holds ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = EMbedding L

proof end;

theorem LmEMDetX53: :: ZMODLAT2:29

for L, E being Z_Module st ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
L is Submodule of E

proof end;

theorem LmEMDetX541: :: ZMODLAT2:30

for E, L being Z_Module
for I being Subset of L
for J being Subset of E
for K being Linear_Combination of J st I = J & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
K is Linear_Combination of I

proof end;

theorem :: ZMODLAT2:31

for E, L being Z_Module
for K being Linear_Combination of E
for H being Linear_Combination of L st K = H & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
Carrier K = Carrier H ;

theorem LmEMDetX543: :: ZMODLAT2:32

proof end;

theorem LmEMDetX51: :: ZMODLAT2:33

for L, E being Z_Module
for I being Subset of L
for J being Subset of E st ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) & I = J holds
( I is linearly-independent iff J is linearly-independent )

proof end;

theorem LmEMDetX52: :: ZMODLAT2:34

proof end;

theorem LmEMDetX5: :: ZMODLAT2:35

for L, E being free Z_Module
for I being Subset of L
for J being Subset of E st ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) & I = J holds
( I is Basis of L iff J is Basis of E )

proof end;

theorem LmEMDetX4: :: ZMODLAT2:36

for L, E being free finite-rank Z_Module st ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
rank L = rank E

proof end;

theorem LmEMDetX6: :: ZMODLAT2:37

for L being Z_Lattice
for I being Subset of L holds
( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) )

proof end;

theorem :: ZMODLAT2:38

for L being Z_Lattice
for I being Subset of L holds
( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMLat L) )

proof end;

theorem LmEMDetX8: :: ZMODLAT2:39

for L being Z_Lattice
for b being FinSequence of L holds
( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L )

proof end;

theorem LmEMDetX9: :: ZMODLAT2:40

for L being Z_Lattice
for E being free finite-rank Z_Module
for I being FinSequence of L
for J being FinSequence of E st ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) & I = J holds
( I is OrdBasis of L iff J is OrdBasis of E )

proof end;

theorem :: ZMODLAT2:41

for L being Z_Lattice
for b being FinSequence of L holds
( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMLat L )

proof end;

theorem :: ZMODLAT2:42

for L being Z_Lattice holds rank L = rank (EMLat L)

proof end;

theorem ThEME1: :: ZMODLAT2:43

for L being Z_Lattice
for x being object holds
( x is Vector of (EMLat L) iff x is Vector of (EMbedding L) )

proof end;

registration

let L be RATional Z_Lattice;
let v, u be Vector of (EMLat L);

cluster (ScProductEM L) . (v,u) -> rational ;

correctness

proof end;

end;

registration

let L be RATional Z_Lattice;
let v, u be Vector of (DivisibleMod L);

cluster (ScProductDM L) . (v,u) -> rational ;

correctness

proof end;

end;

definition

let V be ModuleStr over INT.Ring ;
let f be FrForm of V,V;

attr f is symmetric means :defSymForm: :: ZMODLAT2:def 6
for v, w being Vector of V holds f . (v,w) = f . (w,v);

end;

:: deftheorem defSymForm defines symmetric ZMODLAT2:def 6 :

registration

let V be non empty ModuleStr over INT.Ring ;

cluster NulFrForm (V,V) -> symmetric ;

correctness

proof end;

end;

registration

let V be non empty ModuleStr over INT.Ring ;

cluster Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of F_Real -valued Function-like non empty total quasi_total V71() V72() V73() symmetric for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Real:];

correctness

proof end;

end;

registration

let V be non empty ModuleStr over INT.Ring ;

cluster Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of F_Real -valued Function-like non empty total quasi_total V71() V72() V73() V252(V,V) V253(V,V) V254(V,V) V255(V,V) symmetric for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Real:];

correctness

proof end;

end;

registration

let L be Z_Lattice;

cluster InnerProduct L -> symmetric ;

correctness

proof end;

end;

registration

let V be free finite-rank Z_Module;
let f be symmetric bilinear-FrForm of V,V;
let b be OrdBasis of V;

cluster GramMatrix (f,b) -> symmetric ;

correctness

proof end;

end;

theorem :: ZMODLAT2:44

for L being RATional Z_Lattice
for v, u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) in F_Rat by RAT_1:def 2;

theorem ThGM1: :: ZMODLAT2:45

for L being RATional Z_Lattice
for b being OrdBasis of L holds GramMatrix b is Matrix of dim L,F_Rat

proof end;

theorem ZMATRLIN42: :: ZMODLAT2:46

for F being FinSequence of F_Real
for G being FinSequence of F_Rat st F = G holds
Sum F = Sum G

proof end;

theorem ZMATRLIN43: :: ZMODLAT2:47

for i being Nat
for j being Element of F_Real
for k being Element of F_Rat st j = k holds
((power F_Real) . ((- (1_ F_Real)),i)) * j = ((power F_Rat) . ((- (1_ F_Rat)),i)) * k

proof end;

theorem LmSign1C: :: ZMODLAT2:48

for F being FinSequence of F_Real st ( for i being Nat st i in dom F holds
F . i in F_Rat ) holds
Sum F in F_Rat

proof end;

theorem LmSign1D: :: ZMODLAT2:49

for i being Nat holds (power F_Real) . ((- (1_ F_Real)),i) in F_Rat

proof end;

theorem LmSign1F: :: ZMODLAT2:50

for n, i, j, k, m being Nat
for M being Matrix of n + 1,F_Real
for L being Matrix of n + 1,F_Rat st 0 < n & M = L & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds
(Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)

proof end;

theorem :: ZMODLAT2:51

for n, i, j, k, m being Nat
for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,F_Rat & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds
(Delete (M,i,j)) * (k,m) is Element of F_Rat

proof end;

theorem LmSign1E: :: ZMODLAT2:52

for n, i, j being Nat
for M being Matrix of n + 1,F_Real
for L being Matrix of n + 1,F_Rat st 0 < n & M = L & [i,j] in Indices M holds
Delete (M,i,j) = Delete (L,i,j)

proof end;

theorem LmSign1EX: :: ZMODLAT2:53

for n, i, j being Nat
for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,F_Rat & [i,j] in Indices M holds
Delete (M,i,j) is Matrix of n,F_Rat

proof end;

theorem LmSign1A: :: ZMODLAT2:54

for n being Nat
for M being Matrix of n,F_Real
for H being Matrix of n,F_Rat st M = H holds
Det M = Det H

proof end;

theorem LmGM11: :: ZMODLAT2:55

for n being Nat
for M being Matrix of n,F_Real st M is Matrix of n,F_Rat holds
Det M in F_Rat

proof end;

theorem :: ZMODLAT2:56

for n, i, j being Nat
for M being Matrix of n + 1,F_Real st M is Matrix of n + 1,F_Rat & [i,j] in Indices M holds
Cofactor (M,i,j) in F_Rat

proof end;

theorem :: ZMODLAT2:57

for L being RATional Z_Lattice
for b being OrdBasis of L holds Det (GramMatrix b) in F_Rat

proof end;

theorem ZL2LmSc1: :: ZMODLAT2:58

for L being positive-definite Z_Lattice
for I being Basis of L
for v, w being Vector of L st ( for u being Vector of L st u in I holds
<;u,v;> = <;u,w;> ) holds
for u being Vector of L holds <;u,v;> = <;u,w;>

proof end;

theorem ZL2ThSc1: :: ZMODLAT2:59

for L being positive-definite Z_Lattice
for b being OrdBasis of L
for v, w being Vector of L st ( for n being Nat st n in dom b holds
<;(b /. n),v;> = <;(b /. n),w;> ) holds
v = w

proof end;

theorem :: ZMODLAT2:60

for n being Nat
for M being Matrix of n,F_Rat st M is without_repeated_line holds
( Det M <> 0. F_Rat iff lines M is linearly-independent )

proof end;

theorem :: ZMODLAT2:61

for L being positive-definite Z_Lattice
for I being Basis of L
for v, w being Vector of L st ( for u being Vector of L st u in I holds
<;v,u;> = <;w,u;> ) holds
for u being Vector of L holds <;v,u;> = <;w,u;>

proof end;

theorem ZL2ThSc1X: :: ZMODLAT2:62

for L being positive-definite Z_Lattice
for b being OrdBasis of L
for v, w being Vector of L st ( for n being Nat st n in dom b holds
<;v,(b /. n);> = <;w,(b /. n);> ) holds
v = w

proof end;

theorem ZL2ThSc1D: :: ZMODLAT2:63

for L being positive-definite Z_Lattice
for b being OrdBasis of EMLat L
for v, w being Vector of (DivisibleMod L) st ( for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) ) holds
v = w

proof end;

theorem :: ZMODLAT2:64

for L being positive-definite Z_Lattice
for b being OrdBasis of EMLat L
for v, w being Vector of (DivisibleMod L) st ( for n being Nat st n in dom b holds
(ScProductDM L) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n)) ) holds
v = w

proof end;

theorem LMThGM21: :: ZMODLAT2:65

for L being non trivial positive-definite RATional Z_Lattice
for v being Element of L
for b being FinSequence of L
for sbv being FinSequence of F_Rat st len b = len sbv & ( for n being Nat st n in dom sbv holds
sbv . n = <;(b /. n),v;> ) holds
<;(Sum b),v;> = Sum sbv

proof end;

LMThGM2311: for r being Element of F_Rat ex K being Integer st
( K <> 0 & K * r in INT )

proof end;

LMThGM231: for n being Nat
for r being FinSequence of F_Rat st len r = n holds
ex K being Integer st
( K <> 0 & ( for i being Nat st i in Seg n holds
K * (r /. i) in INT ) )

proof end;

theorem LMThGM23: :: ZMODLAT2:66

for n being Nat
for r being FinSequence of F_Rat st len r = n holds
ex K being Integer ex Kr being FinSequence of INT.Ring st
( K <> 0 & len Kr = n & ( for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) ) )

proof end;

theorem LMThGM24: :: ZMODLAT2:67

for i, j being Nat
for K being Field
for a, aj being Element of K
for R being Element of (i -VectSp_over K) st j in Seg i & aj = R . j holds
(a * R) . j = a * aj

proof end;

theorem LMThGM25: :: ZMODLAT2:68

for i, j being Nat
for K being Field
for aj, bj being Element of K
for A, B being Element of (i -VectSp_over K) st j in Seg i & aj = A . j & bj = B . j holds
(A + B) . j = aj + bj

proof end;

theorem LMSUM1: :: ZMODLAT2:69

for K being Field
for n, i being Nat st i in Seg n holds
for s being FinSequence of (n -VectSp_over K) ex si being FinSequence of K st
( len si = len s & (Sum s) . i = Sum si & ( for k being Nat st k in dom si holds
si . k = (s /. k) . i ) )

proof end;

theorem ThGM2: :: ZMODLAT2:70

for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L holds Det (GramMatrix b) <> 0. F_Real

proof end;

registration

let L be non trivial positive-definite RATional Z_Lattice;
let b be OrdBasis of L;

cluster GramMatrix b -> invertible ;

correctness

proof end;

end;