:: 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
coherence
for b1 being Basis of V holds not b1 is empty
;
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 :
for IT being Z_Lattice holds
( IT is RATional iff for v, u being Vector of IT holds <;v,u;> in RAT );

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
existence
ex b1 being Z_Lattice st
( not b1 is trivial & b1 is RATional & b1 is positive-definite )
;
proof end;
end;

registration
let L be RATional Z_Lattice;
let v, u be Vector of L;
cluster <;v,u;> -> rational ;
correctness
coherence
<;v,u;> is rational
;
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
coherence
for b1 being INTegral Z_Lattice holds b1 is RATional
;
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
ex b1 being Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real st
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
b1 . (vv,uu) = <;v,u;>
proof end;
uniqueness
for b1, b2 being Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real st ( 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
b1 . (vv,uu) = <;v,u;> ) & ( 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
b2 . (vv,uu) = <;v,u;> ) holds
b1 = b2
proof end;
end;

:: deftheorem defScProductEM defines ScProductEM ZMODLAT2:def 2 :
for L being Z_Lattice
for b2 being Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real holds
( b2 = ScProductEM L iff 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
b2 . (vv,uu) = <;v,u;> );

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
ex b1 being Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):], the carrier of F_Real st
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
b1 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u))
proof end;
uniqueness
for b1, b2 being Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):], the carrier of F_Real st ( 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
b1 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ) & ( 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
b2 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defScProductDM defines ScProductDM ZMODLAT2:def 3 :
for L being Z_Lattice
for b2 being Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):], the carrier of F_Real holds
( b2 = ScProductDM L iff 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
b2 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) );

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
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
v = 0. (DivisibleMod L)
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
ex b1 being strict Z_Lattice st
( the carrier of b1 = rng (MorphsZQ L) & the ZeroF of b1 = zeroCoset L & the addF of b1 = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b1 = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b1 = ScProductEM L )
proof end;
uniqueness
for b1, b2 being strict Z_Lattice st the carrier of b1 = rng (MorphsZQ L) & the ZeroF of b1 = zeroCoset L & the addF of b1 = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b1 = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b1 = ScProductEM L & the carrier of b2 = rng (MorphsZQ L) & the ZeroF of b2 = zeroCoset L & the addF of b2 = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b2 = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b2 = ScProductEM L holds
b1 = b2
;
end;

:: deftheorem defEMLat defines EMLat ZMODLAT2:def 4 :
for L being Z_Lattice
for b2 being strict Z_Lattice holds
( b2 = EMLat L iff ( the carrier of b2 = rng (MorphsZQ L) & the ZeroF of b2 = zeroCoset L & the addF of b2 = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b2 = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b2 = ScProductEM L ) );

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
ex b1 being strict Z_Lattice st
( the carrier of b1 = r * (rng (MorphsZQ L)) & the ZeroF of b1 = zeroCoset L & the addF of b1 = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b1 = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b1 = (ScProductDM L) || (r * (rng (MorphsZQ L))) )
proof end;
uniqueness
for b1, b2 being strict Z_Lattice st the carrier of b1 = r * (rng (MorphsZQ L)) & the ZeroF of b1 = zeroCoset L & the addF of b1 = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b1 = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b1 = (ScProductDM L) || (r * (rng (MorphsZQ L))) & the carrier of b2 = r * (rng (MorphsZQ L)) & the ZeroF of b2 = zeroCoset L & the addF of b2 = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b2 = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b2 = (ScProductDM L) || (r * (rng (MorphsZQ L))) holds
b1 = b2
;
end;

:: deftheorem defrEMLat defines EMLat ZMODLAT2:def 5 :
for L being Z_Lattice
for r being Element of F_Rat
for b3 being strict Z_Lattice holds
( b3 = EMLat (r,L) iff ( the carrier of b3 = r * (rng (MorphsZQ L)) & the ZeroF of b3 = zeroCoset L & the addF of b3 = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b3 = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b3 = (ScProductDM L) || (r * (rng (MorphsZQ L))) ) );

registration
let L be non trivial Z_Lattice;
cluster EMLat L -> non trivial strict ;
correctness
coherence
not EMLat L is trivial
;
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
coherence
not EMLat (r,L) is trivial
;
proof end;
end;

registration
let L be INTegral Z_Lattice;
cluster EMLat L -> strict INTegral ;
correctness
coherence
EMLat L is INTegral
;
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
coherence
EMLat L is positive-definite
;
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
coherence
EMLat (r,L) is positive-definite
;
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
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
Sum K = Sum H
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
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
Lin I = Lin J
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
coherence
(ScProductEM L) . (v,u) is rational
;
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
coherence
(ScProductDM L) . (v,u) is rational
;
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 :
for V being ModuleStr over INT.Ring
for f being FrForm of V,V holds
( f is symmetric iff for v, w being Vector of V holds f . (v,w) = f . (w,v) );

registration
let V be non empty ModuleStr over INT.Ring ;
cluster NulFrForm (V,V) -> symmetric ;
correctness
coherence
NulFrForm (V,V) is symmetric
;
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
existence
ex b1 being FrForm of V,V st b1 is symmetric
;
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
existence
ex b1 being bilinear-FrForm of V,V st b1 is symmetric
;
proof end;
end;

registration
let L be Z_Lattice;
cluster InnerProduct L -> symmetric ;
correctness
coherence
InnerProduct L is symmetric
;
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
coherence
GramMatrix (f,b) is symmetric
;
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
coherence
GramMatrix b is invertible
;
proof end;
end;