:: by Yuichi Futa and Yasunari Shidama

::

:: Received March 17, 2017

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

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 = {} )

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

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

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;

correctness

coherence

for b_{1} being Basis of V holds not b_{1} is empty ;

end;
correctness

coherence

for b

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

for IT being Z_Lattice holds

( IT is RATional iff for v, u being Vector of IT holds <;v,u;> in RAT );

registration

existence

ex b_{1} being Z_Lattice st

( not b_{1} is trivial & b_{1} is RATional & b_{1} is positive-definite );

end;

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 V257() RATional for Z_Lattice;

correctness existence

ex b

( not b

proof end;

registration

let L be RATional Z_Lattice;

let v, u be Vector of L;

correctness

coherence

<;v,u;> is rational ;

by defRational, RAT_1:def 2;

end;
let v, u be Vector of L;

correctness

coherence

<;v,u;> is rational ;

by defRational, RAT_1:def 2;

registration

coherence

for b_{1} being INTegral Z_Lattice holds b_{1} is RATional ;

by RAT_1:def 2;

end;

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

correctness coherence

for b

by RAT_1:def 2;

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;

ex b_{1} 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

b_{1} . (vv,uu) = <;v,u;>

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (vv,uu) = <;v,u;> ) holds

b_{1} = b_{2}

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

ex b

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

b

proof end;

uniqueness for b

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

b

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

b

b

proof end;

:: deftheorem defScProductEM defines ScProductEM ZMODLAT2:def 2 :

for L being Z_Lattice

for b_{2} being Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real holds

( b_{2} = 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

b_{2} . (vv,uu) = <;v,u;> );

for L being Z_Lattice

for b

( b

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

b

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

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

ex b_{1} 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

b_{1} . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ) holds

b_{1} = b_{2}

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

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem defScProductDM defines ScProductDM ZMODLAT2:def 3 :

for L being Z_Lattice

for b_{2} being Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):], the carrier of F_Real holds

( b_{2} = 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

b_{2} . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) );

for L being Z_Lattice

for b

( b

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

b

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

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

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)

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

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

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

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

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 )

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

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)

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

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;

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

definition

let L be Z_Lattice;

ex b_{1} being strict Z_Lattice st

( the carrier of b_{1} = rng (MorphsZQ L) & the ZeroF of b_{1} = zeroCoset L & the addF of b_{1} = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b_{1} = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b_{1} = ScProductEM L )

for b_{1}, b_{2} being strict Z_Lattice st the carrier of b_{1} = rng (MorphsZQ L) & the ZeroF of b_{1} = zeroCoset L & the addF of b_{1} = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b_{1} = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b_{1} = ScProductEM L & the carrier of b_{2} = rng (MorphsZQ L) & the ZeroF of b_{2} = zeroCoset L & the addF of b_{2} = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b_{2} = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b_{2} = ScProductEM L holds

b_{1} = b_{2}
;

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defEMLat defines EMLat ZMODLAT2:def 4 :

for L being Z_Lattice

for b_{2} being strict Z_Lattice holds

( b_{2} = EMLat L iff ( the carrier of b_{2} = rng (MorphsZQ L) & the ZeroF of b_{2} = zeroCoset L & the addF of b_{2} = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b_{2} = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b_{2} = ScProductEM L ) );

for L being Z_Lattice

for b

( b

definition

let L be Z_Lattice;

let r be Element of F_Rat;

ex b_{1} being strict Z_Lattice st

( the carrier of b_{1} = r * (rng (MorphsZQ L)) & the ZeroF of b_{1} = zeroCoset L & the addF of b_{1} = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b_{1} = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b_{1} = (ScProductDM L) || (r * (rng (MorphsZQ L))) )

for b_{1}, b_{2} being strict Z_Lattice st the carrier of b_{1} = r * (rng (MorphsZQ L)) & the ZeroF of b_{1} = zeroCoset L & the addF of b_{1} = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b_{1} = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b_{1} = (ScProductDM L) || (r * (rng (MorphsZQ L))) & the carrier of b_{2} = r * (rng (MorphsZQ L)) & the ZeroF of b_{2} = zeroCoset L & the addF of b_{2} = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b_{2} = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b_{2} = (ScProductDM L) || (r * (rng (MorphsZQ L))) holds

b_{1} = b_{2}
;

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defrEMLat defines EMLat ZMODLAT2:def 5 :

for L being Z_Lattice

for r being Element of F_Rat

for b_{3} being strict Z_Lattice holds

( b_{3} = EMLat (r,L) iff ( the carrier of b_{3} = r * (rng (MorphsZQ L)) & the ZeroF of b_{3} = zeroCoset L & the addF of b_{3} = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b_{3} = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b_{3} = (ScProductDM L) || (r * (rng (MorphsZQ L))) ) );

for L being Z_Lattice

for r being Element of F_Rat

for b

( b

registration
end;

registration

let L be non trivial Z_Lattice;

let r be non zero Element of F_Rat;

correctness

coherence

not EMLat (r,L) is trivial ;

end;
let r be non zero Element of F_Rat;

correctness

coherence

not EMLat (r,L) is trivial ;

proof end;

registration
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

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

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

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;

correctness

coherence

EMLat L is positive-definite ;

end;
correctness

coherence

EMLat L is positive-definite ;

proof end;

registration

let L be positive-definite Z_Lattice;

let r be non zero Element of F_Rat;

correctness

coherence

EMLat (r,L) is positive-definite ;

end;
let r be non zero Element of F_Rat;

correctness

coherence

EMLat (r,L) is positive-definite ;

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

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

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;

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

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

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

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

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 )

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

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 )

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

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

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

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 )

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 )

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 )

for b being FinSequence of L holds

( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of 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) )

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

correctness

coherence

(ScProductEM L) . (v,u) is rational ;

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

correctness

coherence

(ScProductEM L) . (v,u) is rational ;

proof end;

registration

let L be RATional Z_Lattice;

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

correctness

coherence

(ScProductDM L) . (v,u) is rational ;

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

correctness

coherence

(ScProductDM L) . (v,u) is rational ;

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

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 ;

correctness

coherence

NulFrForm (V,V) is symmetric ;

end;
correctness

coherence

NulFrForm (V,V) is symmetric ;

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

existence

ex b_{1} being FrForm of V,V st b_{1} is symmetric ;

end;
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 FrForm of ,;

correctness existence

ex b

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

existence

ex b_{1} being bilinear-FrForm of V,V st b_{1} is symmetric ;

end;
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() V250(V,V) V251(V,V) V252(V,V) V253(V,V) symmetric for bilinear-FrForm of ,;

correctness existence

ex b

proof end;

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

correctness

coherence

GramMatrix (f,b) is symmetric ;

end;
let f be symmetric bilinear-FrForm of V,V;

let b be OrdBasis of V;

correctness

coherence

GramMatrix (f,b) is symmetric ;

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

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

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

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

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

F . i in F_Rat ) holds

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

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

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)

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

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

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

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

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

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 )

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

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

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

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

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

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

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

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

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

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

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;

correctness

coherence

GramMatrix b is invertible ;

end;
let b be OrdBasis of L;

correctness

coherence

GramMatrix b is invertible ;

proof end;