:: Lattice of $\mathbb Z$-module
:: by Yuichi Futa and Yasunari Shidama
::
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem LMEQ: :: ZMODLAT1:1
for D, E being non empty set
for n, m being Nat
for M being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) in E ) holds
M is Matrix of n,m,E
proof end;

definition
let F be 1-sorted ;
attr c2 is strict ;
struct LatticeStr over F -> ModuleStr over F;
aggr LatticeStr(# carrier, addF, ZeroF, lmult, scalar #) -> LatticeStr over F;
sel scalar c2 -> Function of [: the carrier of c2, the carrier of c2:], the carrier of F_Real;
end;

registration
let F be 1-sorted ;
cluster non empty strict for LatticeStr over F;
correctness
existence
ex b1 being LatticeStr over F st
( b1 is strict & not b1 is empty )
;
proof end;
end;

registration
let F be 1-sorted ;
let D be non empty set ;
let Z be Element of D;
let a be BinOp of D;
let m be Function of [: the carrier of F,D:],D;
let s be Function of [:D,D:], the carrier of F_Real;
cluster LatticeStr(# D,a,Z,m,s #) -> non empty ;
coherence
not LatticeStr(# D,a,Z,m,s #) is empty
;
end;

definition
let X be non empty LatticeStr over INT.Ring ;
let x, y be Vector of X;
func <;x,y;> -> Element of F_Real equals :: ZMODLAT1:def 1
the scalar of X . [x,y];
correctness
coherence
the scalar of X . [x,y] is Element of F_Real
;
;
end;

:: deftheorem defines <; ZMODLAT1:def 1 :
for X being non empty LatticeStr over INT.Ring
for x, y being Vector of X holds <;x,y;> = the scalar of X . [x,y];

definition
let X be non empty LatticeStr over INT.Ring ;
let x be Vector of X;
func -> Element of F_Real equals :: ZMODLAT1:def 2
<;x,x;>;
correctness
coherence
<;x,x;> is Element of F_Real
;
;
end;

:: deftheorem defines ||. ZMODLAT1:def 2 :
for X being non empty LatticeStr over INT.Ring
for x being Vector of X holds = <;x,x;>;

definition
let IT be non empty LatticeStr over INT.Ring ;
attr IT is Z_Lattice-like means :defZLattice: :: ZMODLAT1:def 3
( ( for x being Vector of IT st ( for y being Vector of IT holds <;x,y;> = 0 ) holds
x = 0. IT ) & ( for x, y being Vector of IT holds <;x,y;> = <;y,x;> ) & ( for x, y, z being Vector of IT
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) ) );
end;

:: deftheorem defZLattice defines Z_Lattice-like ZMODLAT1:def 3 :
for IT being non empty LatticeStr over INT.Ring holds
( IT is Z_Lattice-like iff ( ( for x being Vector of IT st ( for y being Vector of IT holds <;x,y;> = 0 ) holds
x = 0. IT ) & ( for x, y being Vector of IT holds <;x,y;> = <;y,x;> ) & ( for x, y, z being Vector of IT
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) ) ) );

definition
let V be Z_Module;
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real;
func GenLat (V,sc) -> non empty LatticeStr over INT.Ring equals :: ZMODLAT1:def 4
LatticeStr(# the carrier of V, the addF of V,(0. V), the lmult of V,sc #);
coherence
LatticeStr(# the carrier of V, the addF of V,(0. V), the lmult of V,sc #) is non empty LatticeStr over INT.Ring
;
end;

:: deftheorem defines GenLat ZMODLAT1:def 4 :
for V being Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds GenLat (V,sc) = LatticeStr(# the carrier of V, the addF of V,(0. V), the lmult of V,sc #);

ZMtoZL1: for V being Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds
( GenLat (V,sc) is Abelian & GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )

proof end;

registration
correctness
existence
ex b1 being non empty LatticeStr over INT.Ring st
( b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
;
proof end;
end;

registration
let V be Z_Module;
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real;
correctness
coherence
( GenLat (V,sc) is Abelian & GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
;
by ZMtoZL1;
end;

theorem LmZMtoZL1: :: ZMODLAT1:2
for V being Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds GenLat (V,sc) is Submodule of V
proof end;

theorem :: ZMODLAT1:3
for V being Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds V is Submodule of GenLat (V,sc)
proof end;

ZMtoZL2: for V being free Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds GenLat (V,sc) is free

proof end;

registration
correctness
existence ;
proof end;
end;

registration
let V be free Z_Module;
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real;
cluster GenLat (V,sc) -> non empty free ;
correctness
coherence
GenLat (V,sc) is free
;
by ZMtoZL2;
end;

registration
correctness
existence ;
proof end;
end;

theorem ZMtoZL3: :: ZMODLAT1:4
for V being free finite-rank Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds GenLat (V,sc) is finite-rank
proof end;

registration
correctness
existence ;
proof end;
end;

registration
let V be free finite-rank Z_Module;
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real;
cluster GenLat (V,sc) -> non empty finite-rank ;
correctness
coherence
GenLat (V,sc) is finite-rank
;
by ZMtoZL3;
end;

theorem ThTrivialLat1: :: ZMODLAT1:5
for V being free finite-rank Z_Module
for f being Function of [: the carrier of ((0). V), the carrier of ((0). V):], the carrier of F_Real st f = [: the carrier of ((0). V), the carrier of ((0). V):] --> () holds
GenLat (((0). V),f) is Z_Lattice-like
proof end;

registration
cluster non empty Z_Lattice-like for LatticeStr over INT.Ring ;
existence
ex b1 being non empty LatticeStr over INT.Ring st b1 is Z_Lattice-like
proof end;
end;

registration
existence
proof end;
end;

registration
existence
proof end;
end;

definition end;

theorem ThNonTrivialLat1: :: ZMODLAT1:6
for V being non trivial torsion-free Z_Module
for Z being Submodule of V
for v being non zero Vector of V
for f being Function of [: the carrier of Z, the carrier of Z:], the carrier of F_Real st Z = Lin {v} & ( for v1, v2 being Vector of Z
for a, b being Element of INT.Ring st v1 = a * v & v2 = b * v holds
f . (v1,v2) = a * b ) holds
GenLat (Z,f) is Z_Lattice-like
proof end;

registration
correctness
existence
not for b1 being Z_Lattice holds b1 is trivial
;
proof end;
end;

registration
let V be torsion-free Z_Module;
correctness
coherence
for b1 being non empty ModuleStr over F_Rat st b1 = Z_MQ_VectSp V holds
( b1 is scalar-distributive & b1 is vector-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian )
;
;
end;

theorem ThSc1: :: ZMODLAT1:7
for L being Z_Lattice
for v, u being Vector of L holds
( <;v,(- u);> = - <;v,u;> & <;(- v),u;> = - <;v,u;> )
proof end;

theorem ThSc2: :: ZMODLAT1:8
for L being Z_Lattice
for v, u, w being Vector of L holds <;v,(u + w);> = <;v,u;> + <;v,w;>
proof end;

theorem ThSc3: :: ZMODLAT1:9
for L being Z_Lattice
for v, u being Vector of L
for a being Element of INT.Ring holds <;v,(a * u);> = a * <;v,u;>
proof end;

theorem ThSc4: :: ZMODLAT1:10
for L being Z_Lattice
for v, u, w being Vector of L
for a, b being Element of INT.Ring holds
( <;((a * v) + (b * u)),w;> = (a * <;v,w;>) + (b * <;u,w;>) & <;v,((a * u) + (b * w));> = (a * <;v,u;>) + (b * <;v,w;>) )
proof end;

theorem ThSc5: :: ZMODLAT1:11
for L being Z_Lattice
for v, u, w being Vector of L holds
( <;(v - u),w;> = <;v,w;> - <;u,w;> & <;v,(u - w);> = <;v,u;> - <;v,w;> )
proof end;

theorem ThSc6: :: ZMODLAT1:12
for L being Z_Lattice
for v being Vector of L holds
( <;v,(0. L);> = 0 & <;(0. L),v;> = 0 )
proof end;

:: Integral Lattice
definition
let IT be Z_Lattice;
attr IT is INTegral means :defIntegral: :: ZMODLAT1:def 5
for v, u being Vector of IT holds <;v,u;> in INT ;
end;

:: deftheorem defIntegral defines INTegral ZMODLAT1:def 5 :
for IT being Z_Lattice holds
( IT is INTegral iff for v, u being Vector of IT holds <;v,u;> in INT );

registration
correctness
existence
ex b1 being Z_Lattice st b1 is INTegral
;
proof end;
end;

registration
let L be INTegral Z_Lattice;
let v, u be Vector of L;
cluster <;v,u;> -> integer ;
correctness
coherence
<;v,u;> is integer
;
by ;
end;

registration
let L be INTegral Z_Lattice;
let v be Vector of L;
correctness
coherence ;
;
end;

theorem ThIntLat1B: :: ZMODLAT1:13
for L being Z_Lattice
for I being finite Subset of L
for u being Vector of L st ( for v being Vector of L st v in I holds
<;v,u;> in INT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in INT
proof end;

theorem ThIntLat1A: :: ZMODLAT1:14
for L being Z_Lattice
for I being Basis of L st ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in INT ) holds
for v, u being Vector of L holds <;v,u;> in INT
proof end;

theorem :: ZMODLAT1:15
for L being Z_Lattice
for I being Basis of L st ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in INT ) holds
L is INTegral by ThIntLat1A;

definition
let IT be Z_Lattice;
attr IT is positive-definite means :defPositive: :: ZMODLAT1:def 6
for v being Vector of IT st v <> 0. IT holds
> 0 ;
end;

:: deftheorem defPositive defines positive-definite ZMODLAT1:def 6 :
for IT being Z_Lattice holds
( IT is positive-definite iff for v being Vector of IT st v <> 0. IT holds
> 0 );

registration
correctness
existence
ex b1 being Z_Lattice st
( not b1 is trivial & b1 is INTegral & b1 is positive-definite )
;
proof end;
end;

theorem :: ZMODLAT1:16
for L being positive-definite Z_Lattice
for v being Vector of L holds
( = 0 iff v = 0. L ) by ;

theorem :: ZMODLAT1:17
for L being positive-definite Z_Lattice
for v being Vector of L holds >= 0
proof end;

definition
let IT be INTegral Z_Lattice;
attr IT is even means :: ZMODLAT1:def 7
for v being Vector of IT holds is even ;
end;

:: deftheorem defines even ZMODLAT1:def 7 :
for IT being INTegral Z_Lattice holds
( IT is even iff for v being Vector of IT holds is even );

registration
correctness
existence
ex b1 being INTegral Z_Lattice st b1 is even
;
proof end;
end;

notation
let L be Z_Lattice;
synonym dim L for rank L;
end;

definition
let L be Z_Lattice;
let v, u be Vector of L;
pred v,u are_orthogonal means :: ZMODLAT1:def 8
<;v,u;> = 0 ;
symmetry
for v, u being Vector of L st <;v,u;> = 0 holds
<;u,v;> = 0
by defZLattice;
end;

:: deftheorem defines are_orthogonal ZMODLAT1:def 8 :
for L being Z_Lattice
for v, u being Vector of L holds
( v,u are_orthogonal iff <;v,u;> = 0 );

theorem :: ZMODLAT1:18
for L being Z_Lattice
for v, u being Vector of L st v,u are_orthogonal holds
( v, - u are_orthogonal & - v,u are_orthogonal & - v, - u are_orthogonal )
proof end;

theorem :: ZMODLAT1:19
for L being Z_Lattice
for v, u being Vector of L st v,u are_orthogonal holds
||.(v + u).|| = +
proof end;

theorem :: ZMODLAT1:20
for L being Z_Lattice
for v, u being Vector of L st v,u are_orthogonal holds
||.(v - u).|| = +
proof end;

:: Sublattice
definition
let L be Z_Lattice;
mode Z_Sublattice of L -> Z_Lattice means :defSublattice: :: ZMODLAT1:def 9
( the carrier of it c= the carrier of L & 0. it = 0. L & the addF of it = the addF of L || the carrier of it & the lmult of it = the lmult of L | [: the carrier of INT.Ring, the carrier of it:] & the scalar of it = the scalar of L || the carrier of it );
existence
ex b1 being Z_Lattice st
( the carrier of b1 c= the carrier of L & 0. b1 = 0. L & the addF of b1 = the addF of L || the carrier of b1 & the lmult of b1 = the lmult of L | [: the carrier of INT.Ring, the carrier of b1:] & the scalar of b1 = the scalar of L || the carrier of b1 )
proof end;
end;

:: deftheorem defSublattice defines Z_Sublattice ZMODLAT1:def 9 :
for L, b2 being Z_Lattice holds
( b2 is Z_Sublattice of L iff ( the carrier of b2 c= the carrier of L & 0. b2 = 0. L & the addF of b2 = the addF of L || the carrier of b2 & the lmult of b2 = the lmult of L | [: the carrier of INT.Ring, the carrier of b2:] & the scalar of b2 = the scalar of L || the carrier of b2 ) );

theorem ThSL1: :: ZMODLAT1:21
for L being Z_Lattice
for L1 being Z_Sublattice of L holds L1 is Submodule of L
proof end;

theorem :: ZMODLAT1:22
for x being object
for L being Z_Lattice
for L1, L2 being Z_Sublattice of L st x in L1 & L1 is Z_Sublattice of L2 holds
x in L2
proof end;

theorem :: ZMODLAT1:23
for x being object
for L being Z_Lattice
for L1 being Z_Sublattice of L st x in L1 holds
x in L
proof end;

theorem ThSL4: :: ZMODLAT1:24
for L being Z_Lattice
for L1 being Z_Sublattice of L
for w being Vector of L1 holds w is Vector of L
proof end;

theorem :: ZMODLAT1:25
for L being Z_Lattice
for L1, L2 being Z_Sublattice of L holds 0. L1 = 0. L2
proof end;

theorem :: ZMODLAT1:26
for L being Z_Lattice
for L1 being Z_Sublattice of L
for v1, v2 being Vector of L
for w1, w2 being Vector of L1 st w1 = v1 & w2 = v2 holds
w1 + w2 = v1 + v2
proof end;

theorem :: ZMODLAT1:27
for L being Z_Lattice
for L1 being Z_Sublattice of L
for v being Vector of L
for w being Vector of L1
for a being Element of INT.Ring st w = v holds
a * w = a * v
proof end;

theorem :: ZMODLAT1:28
for L being Z_Lattice
for L1 being Z_Sublattice of L
for v being Vector of L
for w being Vector of L1 st w = v holds
- w = - v
proof end;

theorem :: ZMODLAT1:29
for L being Z_Lattice
for L1 being Z_Sublattice of L
for v1, v2 being Vector of L
for w1, w2 being Vector of L1 st w1 = v1 & w2 = v2 holds
w1 - w2 = v1 - v2
proof end;

theorem :: ZMODLAT1:30
for L being Z_Lattice
for L1 being Z_Sublattice of L holds 0. L in L1
proof end;

theorem :: ZMODLAT1:31
for L being Z_Lattice
for L1, L2 being Z_Sublattice of L holds 0. L1 in L2
proof end;

theorem :: ZMODLAT1:32
for L being Z_Lattice
for L1 being Z_Sublattice of L holds 0. L1 in L
proof end;

theorem :: ZMODLAT1:33
for L being Z_Lattice
for L1 being Z_Sublattice of L
for v1, v2 being Vector of L st v1 in L1 & v2 in L1 holds
v1 + v2 in L1
proof end;

theorem :: ZMODLAT1:34
for L being Z_Lattice
for L1 being Z_Sublattice of L
for v being Vector of L
for a being Element of INT.Ring st v in L1 holds
a * v in L1
proof end;

theorem :: ZMODLAT1:35
for L being Z_Lattice
for L1 being Z_Sublattice of L
for v being Vector of L st v in L1 holds
- v in L1
proof end;

theorem :: ZMODLAT1:36
for L being Z_Lattice
for L1 being Z_Sublattice of L
for v1, v2 being Vector of L st v1 in L1 & v2 in L1 holds
v1 - v2 in L1
proof end;

theorem :: ZMODLAT1:37
for L being positive-definite 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 L & ze = 0. L & ad = the addF of L || A & mu = the lmult of L | [: the carrier of INT.Ring,A:] & sc = the scalar of L || A holds
LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L
proof end;

theorem ThSL18: :: ZMODLAT1:38
for L being Z_Lattice
for L1 being Z_Sublattice of L
for w1, w2 being Vector of L1
for v1, v2 being Vector of L st w1 = v1 & w2 = v2 holds
<;w1,w2;> = <;v1,v2;>
proof end;

registration
let L be INTegral Z_Lattice;
cluster -> INTegral for Z_Sublattice of L;
correctness
coherence
for b1 being Z_Sublattice of L holds b1 is INTegral
;
proof end;
end;

registration
let L be positive-definite Z_Lattice;
cluster -> positive-definite for Z_Sublattice of L;
correctness
coherence
for b1 being Z_Sublattice of L holds b1 is positive-definite
;
proof end;
end;

definition
let V, W be ModuleStr over INT.Ring ;
mode FrForm of V,W is Function of [: the carrier of V, the carrier of W:], the carrier of F_Real;
end;

definition
let V, W be ModuleStr over INT.Ring ;
func NulFrForm (V,W) -> FrForm of V,W equals :: ZMODLAT1:def 10
[: the carrier of V, the carrier of W:] --> ();
coherence
[: the carrier of V, the carrier of W:] --> () is FrForm of V,W
;
end;

:: deftheorem defines NulFrForm ZMODLAT1:def 10 :
for V, W being ModuleStr over INT.Ring holds NulFrForm (V,W) = [: the carrier of V, the carrier of W:] --> ();

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be FrForm of V,W;
func f + g -> FrForm of V,W means :Def2: :: ZMODLAT1:def 11
for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . (v,w)) + (g . (v,w));
existence
ex b1 being FrForm of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w))
proof end;
uniqueness
for b1, b2 being FrForm of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines + ZMODLAT1:def 11 :
for V, W being non empty ModuleStr over INT.Ring
for f, g, b5 being FrForm of V,W holds
( b5 = f + g iff for v being Vector of V
for w being Vector of W holds b5 . (v,w) = (f . (v,w)) + (g . (v,w)) );

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrForm of V,W;
let a be Element of F_Real;
func a * f -> FrForm of V,W means :Def3: :: ZMODLAT1:def 12
for v being Vector of V
for w being Vector of W holds it . (v,w) = a * (f . (v,w));
existence
ex b1 being FrForm of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w))
proof end;
uniqueness
for b1, b2 being FrForm of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = a * (f . (v,w)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines * ZMODLAT1:def 12 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for a being Element of F_Real
for b5 being FrForm of V,W holds
( b5 = a * f iff for v being Vector of V
for w being Vector of W holds b5 . (v,w) = a * (f . (v,w)) );

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrForm of V,W;
func - f -> FrForm of V,W means :Def4: :: ZMODLAT1:def 13
for v being Vector of V
for w being Vector of W holds it . (v,w) = - (f . (v,w));
existence
ex b1 being FrForm of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w))
proof end;
uniqueness
for b1, b2 being FrForm of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = - (f . (v,w)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines - ZMODLAT1:def 13 :
for V, W being non empty ModuleStr over INT.Ring
for f, b4 being FrForm of V,W holds
( b4 = - f iff for v being Vector of V
for w being Vector of W holds b4 . (v,w) = - (f . (v,w)) );

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrForm of V,W;
redefine func - f equals :: ZMODLAT1:def 14
(- ()) * f;
compatibility
for b1 being FrForm of V,W holds
( b1 = - f iff b1 = (- ()) * f )
proof end;
end;

:: deftheorem defines - ZMODLAT1:def 14 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds - f = (- ()) * f;

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be FrForm of V,W;
func f - g -> FrForm of V,W equals :: ZMODLAT1:def 15
f + (- g);
correctness
coherence
f + (- g) is FrForm of V,W
;
;
end;

:: deftheorem defines - ZMODLAT1:def 15 :
for V, W being non empty ModuleStr over INT.Ring
for f, g being FrForm of V,W holds f - g = f + (- g);

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be FrForm of V,W;
redefine func f - g means :Def7: :: ZMODLAT1:def 16
for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . (v,w)) - (g . (v,w));
compatibility
for b1 being FrForm of V,W holds
( b1 = f - g iff for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) - (g . (v,w)) )
proof end;
end;

:: deftheorem Def7 defines - ZMODLAT1:def 16 :
for V, W being non empty ModuleStr over INT.Ring
for f, g, b5 being FrForm of V,W holds
( b5 = f - g iff for v being Vector of V
for w being Vector of W holds b5 . (v,w) = (f . (v,w)) - (g . (v,w)) );

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be FrForm of V,W;
:: original: +
redefine func f + g -> FrForm of V,W;
commutativity
for f, g being FrForm of V,W holds f + g = g + f
proof end;
end;

theorem :: ZMODLAT1:39
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds f + (NulFrForm (V,W)) = f
proof end;

theorem :: ZMODLAT1:40
for V, W being non empty ModuleStr over INT.Ring
for f, g, h being FrForm of V,W holds (f + g) + h = f + (g + h)
proof end;

theorem :: ZMODLAT1:41
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds f - f = NulFrForm (V,W)
proof end;

theorem :: ZMODLAT1:42
for V, W being non empty ModuleStr over INT.Ring
for a being Element of F_Real
for f, g being FrForm of V,W holds a * (f + g) = (a * f) + (a * g)
proof end;

theorem :: ZMODLAT1:43
for V, W being non empty ModuleStr over INT.Ring
for a, b being Element of F_Real
for f being FrForm of V,W holds (a + b) * f = (a * f) + (b * f)
proof end;

theorem :: ZMODLAT1:44
for V, W being non empty ModuleStr over INT.Ring
for a, b being Element of F_Real
for f being FrForm of V,W holds (a * b) * f = a * (b * f)
proof end;

theorem :: ZMODLAT1:45
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds () * f = f
proof end;

definition
let V be ModuleStr over INT.Ring ;
mode FrFunctional of V is Function of the carrier of V, the carrier of F_Real;
end;

definition
let V be non empty ModuleStr over INT.Ring ;
let f, g be FrFunctional of V;
func f + g -> FrFunctional of V means :HDef3: :: ZMODLAT1:def 17
for x being Element of V holds it . x = (f . x) + (g . x);
existence
ex b1 being FrFunctional of V st
for x being Element of V holds b1 . x = (f . x) + (g . x)
proof end;
uniqueness
for b1, b2 being FrFunctional of V st ( for x being Element of V holds b1 . x = (f . x) + (g . x) ) & ( for x being Element of V holds b2 . x = (f . x) + (g . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem HDef3 defines + ZMODLAT1:def 17 :
for V being non empty ModuleStr over INT.Ring
for f, g, b4 being FrFunctional of V holds
( b4 = f + g iff for x being Element of V holds b4 . x = (f . x) + (g . x) );

definition
let V be non empty ModuleStr over INT.Ring ;
let f be FrFunctional of V;
func - f -> FrFunctional of V means :HDef4: :: ZMODLAT1:def 18
for x being Element of V holds it . x = - (f . x);
existence
ex b1 being FrFunctional of V st
for x being Element of V holds b1 . x = - (f . x)
proof end;
uniqueness
for b1, b2 being FrFunctional of V st ( for x being Element of V holds b1 . x = - (f . x) ) & ( for x being Element of V holds b2 . x = - (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem HDef4 defines - ZMODLAT1:def 18 :
for V being non empty ModuleStr over INT.Ring
for f, b3 being FrFunctional of V holds
( b3 = - f iff for x being Element of V holds b3 . x = - (f . x) );

definition
let V be non empty ModuleStr over INT.Ring ;
let f, g be FrFunctional of V;
func f - g -> FrFunctional of V equals :: ZMODLAT1:def 19
f + (- g);
coherence
f + (- g) is FrFunctional of V
;
end;

:: deftheorem defines - ZMODLAT1:def 19 :
for V being non empty ModuleStr over INT.Ring
for f, g being FrFunctional of V holds f - g = f + (- g);

definition
let V be non empty ModuleStr over INT.Ring ;
let v be Element of F_Real;
let f be FrFunctional of V;
func v * f -> FrFunctional of V means :HDef6: :: ZMODLAT1:def 20
for x being Element of V holds it . x = v * (f . x);
existence
ex b1 being FrFunctional of V st
for x being Element of V holds b1 . x = v * (f . x)
proof end;
uniqueness
for b1, b2 being FrFunctional of V st ( for x being Element of V holds b1 . x = v * (f . x) ) & ( for x being Element of V holds b2 . x = v * (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem HDef6 defines * ZMODLAT1:def 20 :
for V being non empty ModuleStr over INT.Ring
for v being Element of F_Real
for f, b4 being FrFunctional of V holds
( b4 = v * f iff for x being Element of V holds b4 . x = v * (f . x) );

definition
let V be ModuleStr over INT.Ring ;
func 0FrFunctional V -> FrFunctional of V equals :: ZMODLAT1:def 21
([#] V) --> ();
coherence
([#] V) --> () is FrFunctional of V
;
end;

:: deftheorem defines 0FrFunctional ZMODLAT1:def 21 :
for V being ModuleStr over INT.Ring holds 0FrFunctional V = ([#] V) --> ();

definition
let V be non empty ModuleStr over INT.Ring ;
let F be FrFunctional of V;
attr F is homogeneous means :HDef8: :: ZMODLAT1:def 22
for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x);
end;

:: deftheorem HDef8 defines homogeneous ZMODLAT1:def 22 :
for V being non empty ModuleStr over INT.Ring
for F being FrFunctional of V holds
( F is homogeneous iff for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x) );

definition
let V be non empty ModuleStr over INT.Ring ;
let F be FrFunctional of V;
attr F is 0-preserving means :: ZMODLAT1:def 23
F . (0. V) = 0. F_Real;
end;

:: deftheorem defines 0-preserving ZMODLAT1:def 23 :
for V being non empty ModuleStr over INT.Ring
for F being FrFunctional of V holds
( F is 0-preserving iff F . (0. V) = 0. F_Real );

registration
let V be Z_Module;
cluster Function-like V18( the carrier of V, the carrier of F_Real) homogeneous -> 0-preserving for Element of bool [: the carrier of V, the carrier of F_Real:];
coherence
for b1 being FrFunctional of V st b1 is homogeneous holds
b1 is 0-preserving
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
coherence
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
coherence
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
coherence by FUNCOP_1:7;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
cluster Relation-like the carrier of V -defined the carrier of F_Real -valued Function-like non empty total V18( the carrier of V, the carrier of F_Real) V71() V72() V73() additive homogeneous 0-preserving for Element of bool [: the carrier of V, the carrier of F_Real:];
existence
ex b1 being FrFunctional of V st
( b1 is additive & b1 is homogeneous & b1 is 0-preserving )
proof end;
end;

theorem :: ZMODLAT1:46
for V being non empty ModuleStr over INT.Ring
for f, g being FrFunctional of V holds f + g = g + f
proof end;

theorem :: ZMODLAT1:47
for V being non empty ModuleStr over INT.Ring
for f, g, h being FrFunctional of V holds (f + g) + h = f + (g + h)
proof end;

theorem :: ZMODLAT1:48
for V being non empty ModuleStr over INT.Ring
for x being Element of V holds () . x = 0. F_Real by FUNCOP_1:7;

theorem :: ZMODLAT1:49
for V being non empty ModuleStr over INT.Ring
for f being FrFunctional of V holds f + () = f
proof end;

theorem :: ZMODLAT1:50
for V being non empty ModuleStr over INT.Ring
for f being FrFunctional of V holds f - f = 0FrFunctional V
proof end;

theorem :: ZMODLAT1:51
for V being non empty ModuleStr over INT.Ring
for r being Element of F_Real
for f, g being FrFunctional of V holds r * (f + g) = (r * f) + (r * g)
proof end;

theorem :: ZMODLAT1:52
for V being non empty ModuleStr over INT.Ring
for r, s being Element of F_Real
for f being FrFunctional of V holds (r + s) * f = (r * f) + (s * f)
proof end;

theorem :: ZMODLAT1:53
for V being non empty ModuleStr over INT.Ring
for r, s being Element of F_Real
for f being FrFunctional of V holds (r * s) * f = r * (s * f)
proof end;

theorem :: ZMODLAT1:54
for V being non empty ModuleStr over INT.Ring
for f being FrFunctional of V holds () * f = f
proof end;

registration
let V be non empty ModuleStr over INT.Ring ;
let f, g be additive FrFunctional of V;
cluster f + g -> additive ;
coherence
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
let f be additive FrFunctional of V;
cluster - f -> additive ;
coherence
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
let v be Element of F_Real;
let f be additive FrFunctional of V;
cluster v * f -> additive ;
coherence
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
let f, g be homogeneous FrFunctional of V;
cluster f + g -> homogeneous ;
coherence
f + g is homogeneous
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
let f be homogeneous FrFunctional of V;
coherence
- f is homogeneous
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
let v be Element of F_Real;
let f be homogeneous FrFunctional of V;
cluster v * f -> homogeneous ;
coherence
v * f is homogeneous
proof end;
end;

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrForm of V,W;
let v be Vector of V;
func FrFunctionalFAF (f,v) -> FrFunctional of W equals :: ZMODLAT1:def 24
() . v;
correctness
coherence
() . v is FrFunctional of W
;
;
end;

:: deftheorem defines FrFunctionalFAF ZMODLAT1:def 24 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for v being Vector of V holds FrFunctionalFAF (f,v) = () . v;

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrForm of V,W;
let w be Vector of W;
func FrFunctionalSAF (f,w) -> FrFunctional of V equals :: ZMODLAT1:def 25
() . w;
correctness
coherence
() . w is FrFunctional of V
;
;
end;

:: deftheorem defines FrFunctionalSAF ZMODLAT1:def 25 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for w being Vector of W holds FrFunctionalSAF (f,w) = () . w;

theorem HTh8: :: ZMODLAT1:55
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for v being Vector of V holds
( dom (FrFunctionalFAF (f,v)) = the carrier of W & rng (FrFunctionalFAF (f,v)) c= the carrier of F_Real & ( for w being Vector of W holds (FrFunctionalFAF (f,v)) . w = f . (v,w) ) )
proof end;

theorem HTh9: :: ZMODLAT1:56
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for w being Vector of W holds
( dom (FrFunctionalSAF (f,w)) = the carrier of V & rng (FrFunctionalSAF (f,w)) c= the carrier of F_Real & ( for v being Vector of V holds (FrFunctionalSAF (f,w)) . v = f . (v,w) ) )
proof end;

theorem :: ZMODLAT1:57
for V being non empty ModuleStr over INT.Ring
for x being Element of V holds () . x = 0. F_Real by FUNCOP_1:7;

theorem HTh10: :: ZMODLAT1:58
for V, W being non empty ModuleStr over INT.Ring
for v being Vector of V holds FrFunctionalFAF ((NulFrForm (V,W)),v) = 0FrFunctional W
proof end;

theorem HTh11: :: ZMODLAT1:59
for V, W being non empty ModuleStr over INT.Ring
for w being Vector of W holds FrFunctionalSAF ((NulFrForm (V,W)),w) = 0FrFunctional V
proof end;

theorem HTh12: :: ZMODLAT1:60
for V, W being non empty ModuleStr over INT.Ring
for f, g being FrForm of V,W
for w being Vector of W holds FrFunctionalSAF ((f + g),w) = (FrFunctionalSAF (f,w)) + (FrFunctionalSAF (g,w))
proof end;

theorem HTh13: :: ZMODLAT1:61
for V, W being non empty ModuleStr over INT.Ring
for f, g being FrForm of V,W
for v being Vector of V holds FrFunctionalFAF ((f + g),v) = (FrFunctionalFAF (f,v)) + (FrFunctionalFAF (g,v))
proof end;

theorem HTh14: :: ZMODLAT1:62
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for a being Element of F_Real
for w being Vector of W holds FrFunctionalSAF ((a * f),w) = a * (FrFunctionalSAF (f,w))
proof end;

theorem HTh15: :: ZMODLAT1:63
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for a being Element of F_Real
for v being Vector of V holds FrFunctionalFAF ((a * f),v) = a * (FrFunctionalFAF (f,v))
proof end;

theorem :: ZMODLAT1:64
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for w being Vector of W holds FrFunctionalSAF ((- f),w) = - (FrFunctionalSAF (f,w))
proof end;

theorem :: ZMODLAT1:65
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for v being Vector of V holds FrFunctionalFAF ((- f),v) = - (FrFunctionalFAF (f,v))
proof end;

theorem :: ZMODLAT1:66
for V, W being non empty ModuleStr over INT.Ring
for f, g being FrForm of V,W
for w being Vector of W holds FrFunctionalSAF ((f - g),w) = (FrFunctionalSAF (f,w)) - (FrFunctionalSAF (g,w))
proof end;

theorem :: ZMODLAT1:67
for V, W being non empty ModuleStr over INT.Ring
for f, g being FrForm of V,W
for v being Vector of V holds FrFunctionalFAF ((f - g),v) = (FrFunctionalFAF (f,v)) - (FrFunctionalFAF (g,v))
proof end;

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrFunctional of V;
let g be FrFunctional of W;
func FrFormFunctional (f,g) -> FrForm of V,W means :HDef10: :: ZMODLAT1:def 26
for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . v) * (g . w);
existence
ex b1 being FrForm of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . v) * (g . w)
proof end;
uniqueness
for b1, b2 being FrForm of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . v) * (g . w) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . v) * (g . w) ) holds
b1 = b2
proof end;
end;

:: deftheorem HDef10 defines FrFormFunctional ZMODLAT1:def 26 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrFunctional of V
for g being FrFunctional of W
for b5 being FrForm of V,W holds
( b5 = FrFormFunctional (f,g) iff for v being Vector of V
for w being Vector of W holds b5 . (v,w) = (f . v) * (g . w) );

theorem HTh20: :: ZMODLAT1:68
for V, W being non empty ModuleStr over INT.Ring
for f being FrFunctional of V
for v being Vector of V
for w being Vector of W holds (FrFormFunctional (f,())) . (v,w) = 0. INT.Ring
proof end;

theorem HTh21: :: ZMODLAT1:69
for V, W being non empty ModuleStr over INT.Ring
for g being FrFunctional of W
for v being Vector of V
for w being Vector of W holds (FrFormFunctional ((),g)) . (v,w) = 0. INT.Ring
proof end;

theorem :: ZMODLAT1:70
for V, W being non empty ModuleStr over INT.Ring
for f being FrFunctional of V holds FrFormFunctional (f,()) = NulFrForm (V,W)
proof end;

theorem :: ZMODLAT1:71
for V, W being non empty ModuleStr over INT.Ring
for g being FrFunctional of W holds FrFormFunctional ((),g) = NulFrForm (V,W)
proof end;

theorem HTh24: :: ZMODLAT1:72
for V, W being non empty ModuleStr over INT.Ring
for f being FrFunctional of V
for g being FrFunctional of W
for v being Vector of V holds FrFunctionalFAF ((FrFormFunctional (f,g)),v) = (f . v) * g
proof end;

theorem HTh25: :: ZMODLAT1:73
for V, W being non empty ModuleStr over INT.Ring
for f being FrFunctional of V
for g being FrFunctional of W
for w being Vector of W holds FrFunctionalSAF ((FrFormFunctional (f,g)),w) = (g . w) * f
proof end;

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrForm of V,W;
attr f is additiveFAF means :HDef11: :: ZMODLAT1:def 27
for v being Vector of V holds FrFunctionalFAF (f,v) is additive ;
attr f is additiveSAF means :HDef12: :: ZMODLAT1:def 28
for w being Vector of W holds FrFunctionalSAF (f,w) is additive ;
end;

:: deftheorem HDef11 defines additiveFAF ZMODLAT1:def 27 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds
( f is additiveFAF iff for v being Vector of V holds FrFunctionalFAF (f,v) is additive );

:: deftheorem HDef12 defines additiveSAF ZMODLAT1:def 28 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds
( f is additiveSAF iff for w being Vector of W holds FrFunctionalSAF (f,w) is additive );

definition
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrForm of V,W;
attr f is homogeneousFAF means :HDef13: :: ZMODLAT1:def 29
for v being Vector of V holds FrFunctionalFAF (f,v) is homogeneous ;
attr f is homogeneousSAF means :HDef14: :: ZMODLAT1:def 30
for w being Vector of W holds FrFunctionalSAF (f,w) is homogeneous ;
end;

:: deftheorem HDef13 defines homogeneousFAF ZMODLAT1:def 29 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds
( f is homogeneousFAF iff for v being Vector of V holds FrFunctionalFAF (f,v) is homogeneous );

:: deftheorem HDef14 defines homogeneousSAF ZMODLAT1:def 30 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds
( f is homogeneousSAF iff for w being Vector of W holds FrFunctionalSAF (f,w) is homogeneous );

registration
let V, W be non empty ModuleStr over INT.Ring ;
cluster NulFrForm (V,W) -> additiveFAF ;
coherence
proof end;
cluster NulFrForm (V,W) -> additiveSAF ;
coherence
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
cluster Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of F_Real -valued Function-like non empty total V18([: the carrier of V, the carrier of W:], the carrier of F_Real) V71() V72() V73() additiveFAF additiveSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of F_Real:];
existence
ex b1 being FrForm of V,W st
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
cluster NulFrForm (V,W) -> homogeneousFAF ;
coherence
NulFrForm (V,W) is homogeneousFAF
proof end;
cluster NulFrForm (V,W) -> homogeneousSAF ;
coherence
NulFrForm (V,W) is homogeneousSAF
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
cluster Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of F_Real -valued Function-like non empty total V18([: the carrier of V, the carrier of W:], the carrier of F_Real) V71() V72() V73() additiveFAF additiveSAF homogeneousFAF homogeneousSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of F_Real:];
existence
ex b1 being FrForm of V,W st
( b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof end;
end;

definition end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be additiveFAF FrForm of V,W;
let v be Vector of V;
cluster FrFunctionalFAF (f,v) -> additive ;
coherence
by HDef11;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be additiveSAF FrForm of V,W;
let w be Vector of W;
cluster FrFunctionalSAF (f,w) -> additive ;
coherence
by HDef12;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be homogeneousFAF FrForm of V,W;
let v be Vector of V;
coherence
FrFunctionalFAF (f,v) is homogeneous
by HDef13;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be homogeneousSAF FrForm of V,W;
let w be Vector of W;
coherence
FrFunctionalSAF (f,w) is homogeneous
by HDef14;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrFunctional of V;
let g be additive FrFunctional of W;
coherence
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be additive FrFunctional of V;
let g be FrFunctional of W;
coherence
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be FrFunctional of V;
let g be homogeneous FrFunctional of W;
coherence
FrFormFunctional (f,g) is homogeneousFAF
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be homogeneous FrFunctional of V;
let g be FrFunctional of W;
coherence
FrFormFunctional (f,g) is homogeneousSAF
proof end;
end;

registration
let V be non trivial ModuleStr over INT.Ring ;
let W be non empty ModuleStr over INT.Ring ;
let f be FrFunctional of V;
let g be FrFunctional of W;
cluster FrFormFunctional (f,g) -> non trivial ;
coherence
not FrFormFunctional (f,g) is trivial
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
let W be non trivial ModuleStr over INT.Ring ;
let f be FrFunctional of V;
let g be FrFunctional of W;
cluster FrFormFunctional (f,g) -> non trivial ;
coherence
not FrFormFunctional (f,g) is trivial
proof end;
end;

definition
let V be non empty ModuleStr over INT.Ring ;
let F be FrFunctional of V;
attr F is 0-preserving means :HDef9: :: ZMODLAT1:def 31
F . (0. V) = 0. F_Real;
end;

:: deftheorem HDef9 defines 0-preserving ZMODLAT1:def 31 :
for V being non empty ModuleStr over INT.Ring
for F being FrFunctional of V holds
( F is 0-preserving iff F . (0. V) = 0. F_Real );

registration
let V be Z_Module;
cluster Function-like V18( the carrier of V, the carrier of F_Real) homogeneous -> 0-preserving for Element of bool [: the carrier of V, the carrier of F_Real:];
coherence
for b1 being FrFunctional of V st b1 is homogeneous holds
b1 is 0-preserving
proof end;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
coherence by FUNCOP_1:7;
end;

registration
let V be non empty ModuleStr over INT.Ring ;
cluster Relation-like the carrier of V -defined the carrier of F_Real -valued Function-like non empty total V18( the carrier of V, the carrier of F_Real) V71() V72() V73() additive homogeneous 0-preserving for Element of bool [: the carrier of V, the carrier of F_Real:];
existence
ex b1 being FrFunctional of V st
( b1 is additive & b1 is homogeneous & b1 is 0-preserving )
proof end;
end;

registration
let V be non trivial free Z_Module;
cluster Relation-like the carrier of V -defined the carrier of F_Real -valued Function-like non constant non empty non trivial total V18( the carrier of V, the carrier of F_Real) V71() V72() V73() additive homogeneous for Element of bool [: the carrier of V, the carrier of F_Real:];
existence
ex b1 being FrFunctional of V st
( b1 is additive & b1 is homogeneous & not b1 is constant & not b1 is trivial )
proof end;
end;

theorem VS10Th28: :: ZMODLAT1:74
for V being non trivial free Z_Module
for f being non constant 0-preserving FrFunctional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. F_Real )
proof end;

registration
let V, W be non trivial free Z_Module;
let f be non constant 0-preserving FrFunctional of V;
let g be non constant 0-preserving FrFunctional of W;
cluster FrFormFunctional (f,g) -> non constant ;
coherence
not FrFormFunctional (f,g) is constant
proof end;
end;

definition end;

registration
let V, W be non trivial free Z_Module;
cluster Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of F_Real -valued Function-like non constant non empty non trivial total V18([: the carrier of V, the carrier of W:], the carrier of F_Real) V71() V72() V73() additiveFAF additiveSAF homogeneousFAF homogeneousSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of F_Real:];
existence
ex b1 being FrForm of V,W st
( not b1 is trivial & not b1 is constant & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be additiveSAF FrForm of V,W;
cluster f + g -> additiveSAF ;
correctness
coherence
;
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be additiveFAF FrForm of V,W;
cluster f + g -> additiveFAF ;
correctness
coherence
;
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be additiveSAF FrForm of V,W;
let a be Element of F_Real;
cluster a * f -> additiveSAF ;
correctness
coherence
;
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be additiveFAF FrForm of V,W;
let a be Element of F_Real;
cluster a * f -> additiveFAF ;
correctness
coherence
;
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be additiveSAF FrForm of V,W;
correctness
coherence
;
;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be additiveFAF FrForm of V,W;
correctness
coherence
;
;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be additiveSAF FrForm of V,W;
cluster f - g -> additiveSAF ;
correctness
coherence
;
;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be additiveFAF FrForm of V,W;
cluster f - g -> additiveFAF ;
correctness
coherence
;
;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be homogeneousSAF FrForm of V,W;
correctness
coherence
f + g is homogeneousSAF
;
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be homogeneousFAF FrForm of V,W;
correctness
coherence
f + g is homogeneousFAF
;
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be homogeneousSAF FrForm of V,W;
let a be Element of F_Real;
correctness
coherence
a * f is homogeneousSAF
;
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be homogeneousFAF FrForm of V,W;
let a be Element of F_Real;
correctness
coherence
a * f is homogeneousFAF
;
proof end;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be homogeneousSAF FrForm of V,W;
correctness
coherence ;
;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f be homogeneousFAF FrForm of V,W;
correctness
coherence ;
;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be homogeneousSAF FrForm of V,W;
correctness
coherence
f - g is homogeneousSAF
;
;
end;

registration
let V, W be non empty ModuleStr over INT.Ring ;
let f, g be homogeneousFAF FrForm of V,W;
correctness
coherence
f - g is homogeneousFAF
;
;
end;

theorem HTh26: :: ZMODLAT1:75
for V, W being non empty ModuleStr over INT.Ring
for v, u being Vector of V
for w being Vector of W
for f being FrForm of V,W st f is additiveSAF holds
f . ((v + u),w) = (f . (v,w)) + (f . (u,w))
proof end;

theorem HTh27: :: ZMODLAT1:76
for V, W being non empty ModuleStr over INT.Ring
for v being Vector of V
for u, w being Vector of W
for f being FrForm of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))
proof end;

theorem HTh28: :: ZMODLAT1:77
for V, W being non empty ModuleStr over INT.Ring
for v, u being Vector of V
for w, t being Vector of W
for f being additiveFAF additiveSAF FrForm of V,W holds f . ((v + u),(w + t)) = ((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t)))
proof end;

theorem HTh29: :: ZMODLAT1:78
for V, W being non empty right_zeroed ModuleStr over INT.Ring
for f being additiveFAF FrForm of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. INT.Ring
proof end;

theorem HTh30: :: ZMODLAT1:79
for V, W being non empty right_zeroed ModuleStr over INT.Ring
for f being additiveSAF FrForm of V,W
for w being Vector of W holds f . ((0. V),w) = 0. INT.Ring
proof end;

theorem HTh31: :: ZMODLAT1:80
for V, W being non empty ModuleStr over INT.Ring
for v being Vector of V
for w being Vector of W
for a being Element of INT.Ring
for f being FrForm of V,W st f is homogeneousSAF holds
f . ((a * v),w) = a * (f . (v,w))
proof end;

theorem HTh32: :: ZMODLAT1:81
for V, W being non empty ModuleStr over INT.Ring
for v being Vector of V
for w being Vector of W
for a being Element of INT.Ring
for f being FrForm of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
proof end;

theorem :: ZMODLAT1:82
for V, W being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over INT.Ring
for f being homogeneousSAF FrForm of V,W
for w being Vector of W holds f . ((0. V),w) = 0. F_Real
proof end;

theorem :: ZMODLAT1:83
for V, W being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over INT.Ring
for f being homogeneousFAF FrForm of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. F_Real
proof end;

theorem HTh35: :: ZMODLAT1:84
for V, W being Z_Module
for v, u being Vector of V
for w being Vector of W
for f being additiveSAF homogeneousSAF FrForm of V,W holds f . ((v - u),w) = (f . (v,w)) - (f . (u,w))
proof end;

theorem HTh36: :: ZMODLAT1:85
for V, W being Z_Module
for v being Vector of V
for w, t being Vector of W
for f being additiveFAF homogeneousFAF FrForm of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
proof end;

theorem HTh37: :: ZMODLAT1:86
for V, W being Z_Module
for v, u being Vector of V
for w, t being Vector of W
for f being bilinear-FrForm of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))
proof end;

theorem :: ZMODLAT1:87
for V, W being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over INT.Ring
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of INT.Ring
for f being bilinear-FrForm of V,W holds f . ((v + (a * u)),(w + (b * t))) = ((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (u,w))) + (a * (b * (f . (u,t)))))
proof end;

theorem :: ZMODLAT1:88
for V, W being Z_Module
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of INT.Ring
for f being bilinear-FrForm of V,W holds f . ((v - (a * u)),(w - (b * t))) = ((f . (v,w)) - (b * (f . (v,t)))) - ((a * (f . (u,w))) - (a * (b * (f . (u,t)))))
proof end;

theorem :: ZMODLAT1:89
for V, W being non empty right_zeroed ModuleStr over INT.Ring
for f being FrForm of V,W st ( f is additiveFAF or f is additiveSAF ) holds
( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. INT.Ring )
proof end;

definition
let V1, V2 be free finite-rank Z_Module;
let b1 be OrdBasis of V1;
let b2 be OrdBasis of V2;
let f be bilinear-FrForm of V1,V2;
func BilinearM (f,b1,b2) -> Matrix of len b1, len b2,F_Real means :defBilinearM: :: ZMODLAT1:def 32
for i, j being Nat st i in dom b1 & j in dom b2 holds
it * (i,j) = f . ((b1 /. i),(b2 /. j));
existence
ex b1 being Matrix of len b1, len b2,F_Real st
for i, j being Nat st i in dom b1 & j in dom b2 holds
b1 * (i,j) = f . ((b1 /. i),(b2 /. j))
proof end;
uniqueness
for b1, b2 being Matrix of len b1, len b2,F_Real st ( for i, j being Nat st i in dom b1 & j in dom b2 holds
b1 * (i,j) = f . ((b1 /. i),(b2 /. j)) ) & ( for i, j being Nat st i in dom b1 & j in dom b2 holds
b2 * (i,j) = f . ((b1 /. i),(b2 /. j)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defBilinearM defines BilinearM ZMODLAT1:def 32 :
for V1, V2 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being bilinear-FrForm of V1,V2
for b6 being Matrix of len b1, len b2,F_Real holds
( b6 = BilinearM (f,b1,b2) iff for i, j being Nat st i in dom b1 & j in dom b2 holds
b6 * (i,j) = f . ((b1 /. i),(b2 /. j)) );

theorem LMThMBF1X0: :: ZMODLAT1:90
for V being free finite-rank Z_Module
for F being linear-FrFunctional of V
for y being FinSequence of V
for x being FinSequence of INT.Ring
for X, Y being FinSequence of F_Real st X = x & len y = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds
Y . k = F . (y /. k) ) holds
X "*" Y = F . (Sum (lmlt (x,y)))
proof end;

theorem LMThMBF1X: :: ZMODLAT1:91
for V1, V2 being free finite-rank Z_Module
for b2, b3 being OrdBasis of V2
for f being bilinear-FrForm of V1,V2
for v1 being Vector of V1
for v2 being Vector of V2
for X, Y being FinSequence of F_Real st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds
Y "*" X = f . (v1,v2)
proof end;

theorem LMThMBF1Y: :: ZMODLAT1:92
for V1, V2 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for f being bilinear-FrForm of V1,V2
for v1 being Vector of V1
for v2 being Vector of V2
for X, Y being FinSequence of F_Real st len X = len b1 & len Y = len b1 & ( for k being Nat st k in Seg (len b1) holds
Y . k = f . ((b1 /. k),v2) ) & X = v1 |-- b1 holds
X "*" Y = f . (v1,v2)
proof end;

theorem INTTOREAL: :: ZMODLAT1:93
for M being Matrix of INT.Ring holds M is Matrix of F_Real
proof end;

definition
let M be Matrix of INT.Ring;
func inttorealM M -> Matrix of F_Real equals :: ZMODLAT1:def 33
M;
correctness
coherence
M is Matrix of F_Real
;
by INTTOREAL;
end;

:: deftheorem defines inttorealM ZMODLAT1:def 33 :
for M being Matrix of INT.Ring holds inttorealM M = M;

definition
let n, m be Nat;
let M be Matrix of n,m,INT.Ring;
:: original: inttorealM
redefine func inttorealM M -> Matrix of n,m,F_Real;
correctness
coherence
inttorealM M is Matrix of n,m,F_Real
;
proof end;
end;

definition
let n be Nat;
let M be Matrix of n,INT.Ring;
:: original: inttorealM
redefine func inttorealM M -> Matrix of n,F_Real;
correctness
coherence
inttorealM M is Matrix of n,F_Real
;
proof end;
end;

theorem MLT1: :: ZMODLAT1:94
for m, l, n being Nat
for S being Matrix of l,m,INT.Ring
for T being Matrix of m,n,INT.Ring
for S1 being Matrix of l,m,F_Real
for T1 being Matrix of m,n,F_Real st S = S1 & T = T1 & 0 < l & 0 < m holds
S * T = S1 * T1
proof end;

theorem MLT2: :: ZMODLAT1:95
for n being Nat holds 1. (INT.Ring,n) = 1. (F_Real,n)
proof end;

theorem ThMBF1: :: ZMODLAT1:96
for V1, V2 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for b2, b3 being OrdBasis of V2
for f being bilinear-FrForm of V1,V2 st 0 < rank V1 holds
BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((inttorealM (AutMt ((id V2),b3,b2))) @)
proof end;

theorem ThMBF2: :: ZMODLAT1:97
for V1, V2 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V1
for f being bilinear-FrForm of V1,V2 st 0 < rank V1 holds
BilinearM (f,b3,b2) = (inttorealM (AutMt ((id V1),b3,b1))) * (BilinearM (f,b1,b2))
proof end;

theorem ThMBF3: :: ZMODLAT1:98
for V being free finite-rank Z_Module
for b1, b2 being OrdBasis of V
for f being bilinear-FrForm of V,V st 0 < rank V holds
BilinearM (f,b2,b2) = ((inttorealM (AutMt ((id V),b2,b1))) * (BilinearM (f,b1,b1))) * ((inttorealM (AutMt ((id V),b2,b1))) @)
proof end;

theorem ThSign2: :: ZMODLAT1:99
for V being free finite-rank Z_Module
for b1, b2 being OrdBasis of V
for M being Matrix of rank V,F_Real holds
( not M = AutMt ((id V),b1,b2) or ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )
proof end;

theorem :: ZMODLAT1:100
for V being free finite-rank Z_Module
for b1, b2 being OrdBasis of V
for M being Matrix of rank V,F_Real st M = AutMt ((id V),b1,b2) holds
|.(Det M).| = 1
proof end;

theorem ThMBFY: :: ZMODLAT1:101
for V being free finite-rank Z_Module
for b1, b2 being OrdBasis of V
for f being bilinear-FrForm of V,V holds Det (BilinearM (f,b2,b2)) = Det (BilinearM (f,b1,b1))
proof end;

theorem :: ZMODLAT1:102
for V being free finite-rank Z_Module
for b1, b2 being OrdBasis of V
for f being bilinear-FrForm of V,V holds |.(Det (BilinearM (f,b2,b2))).| = |.(Det (BilinearM (f,b1,b1))).| by ThMBFY;

definition
let V be free finite-rank Z_Module;
let f be bilinear-FrForm of V,V;
let b be OrdBasis of V;
func GramMatrix (f,b) -> Matrix of rank V,F_Real equals :: ZMODLAT1:def 34
BilinearM (f,b,b);
correctness
coherence
BilinearM (f,b,b) is Matrix of rank V,F_Real
;
proof end;
end;

:: deftheorem defines GramMatrix ZMODLAT1:def 34 :
for V being free finite-rank Z_Module
for f being bilinear-FrForm of V,V
for b being OrdBasis of V holds GramMatrix (f,b) = BilinearM (f,b,b);

definition
let V be free finite-rank Z_Module;
let f be bilinear-FrForm of V,V;
func GramDet f -> Element of F_Real means :defGramDet: :: ZMODLAT1:def 35
for b being OrdBasis of V holds it = Det (GramMatrix (f,b));
existence
ex b1 being Element of F_Real st
for b being OrdBasis of V holds b1 = Det (GramMatrix (f,b))
proof end;
uniqueness
for b1, b2 being Element of F_Real st ( for b being OrdBasis of V holds b1 = Det (GramMatrix (f,b)) ) & ( for b being OrdBasis of V holds b2 = Det (GramMatrix (f,b)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defGramDet defines GramDet ZMODLAT1:def 35 :
for V being free finite-rank Z_Module
for f being bilinear-FrForm of V,V
for b3 being Element of F_Real holds
( b3 = GramDet f iff for b being OrdBasis of V holds b3 = Det (GramMatrix (f,b)) );

definition
let L be Z_Lattice;
func InnerProduct L -> FrForm of L,L equals :: ZMODLAT1:def 36
the scalar of L;
correctness
coherence
the scalar of L is FrForm of L,L
;
;
end;

:: deftheorem defines InnerProduct ZMODLAT1:def 36 :
for L being Z_Lattice holds InnerProduct L = the scalar of L;

registration
let L be Z_Lattice;
correctness
coherence ;
proof end;
end;

definition
let L be Z_Lattice;
let b be OrdBasis of L;
func GramMatrix b -> Matrix of dim L,F_Real equals :: ZMODLAT1:def 37
GramMatrix ((),b);
correctness
coherence
GramMatrix ((),b) is Matrix of dim L,F_Real
;
;
end;

:: deftheorem defines GramMatrix ZMODLAT1:def 37 :
for L being Z_Lattice
for b being OrdBasis of L holds GramMatrix b = GramMatrix ((),b);

definition
let L be Z_Lattice;
func GramDet L -> Element of F_Real equals :: ZMODLAT1:def 38
GramDet ();
correctness
coherence
GramDet () is Element of F_Real
;
;
end;

:: deftheorem defines GramDet ZMODLAT1:def 38 :
for L being Z_Lattice holds GramDet L = GramDet ();

theorem :: ZMODLAT1:103
for L being INTegral Z_Lattice holds InnerProduct L is bilinear-Form of L,L
proof end;

theorem ThIntLatY: :: ZMODLAT1:104
for L being INTegral Z_Lattice
for b being OrdBasis of L holds GramMatrix b is Matrix of dim L,INT.Ring
proof end;

ThIntLatZ: for L being INTegral Z_Lattice holds GramDet L is Integer
proof end;

registration
let L be INTegral Z_Lattice;
correctness
coherence ;
by ThIntLatZ;
end;