:: by Yuichi Futa and Yasunari Shidama

::

:: Received December 30, 2015

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

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 c_{2} is strict ;

struct LatticeStr over F -> ModuleStr over F;

aggr LatticeStr(# carrier, addF, ZeroF, lmult, scalar #) -> LatticeStr over F;

sel scalar c_{2} -> Function of [: the carrier of c_{2}, the carrier of c_{2}:], the carrier of F_Real;

end;
attr c

struct LatticeStr over F -> ModuleStr over F;

aggr LatticeStr(# carrier, addF, ZeroF, lmult, scalar #) -> LatticeStr over F;

sel scalar c

registration

let F be 1-sorted ;

correctness

existence

ex b_{1} being LatticeStr over F st

( b_{1} is strict & not b_{1} is empty );

end;
correctness

existence

ex b

( b

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

coherence

not LatticeStr(# D,a,Z,m,s #) is empty ;

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

coherence

not LatticeStr(# D,a,Z,m,s #) is empty ;

definition

let X be non empty LatticeStr over INT.Ring ;

let x, y be Vector of X;

correctness

coherence

the scalar of X . [x,y] is Element of F_Real;

;

end;
let x, y be Vector of X;

correctness

coherence

the scalar of X . [x,y] is Element of F_Real;

;

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

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;

correctness

coherence

<;x,x;> is Element of F_Real;

;

end;
let x be Vector of X;

correctness

coherence

<;x,x;> is Element of F_Real;

;

:: deftheorem defines ||. ZMODLAT1:def 2 :

for X being non empty LatticeStr over INT.Ring

for x being Vector of X holds ||.x.|| = <;x,x;>;

for X being non empty LatticeStr over INT.Ring

for x being Vector of X holds ||.x.|| = <;x,x;>;

definition

let IT be non empty LatticeStr over INT.Ring ;

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

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

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

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;

LatticeStr(# the carrier of V, the addF of V,(0. V), the lmult of V,sc #) is non empty LatticeStr over INT.Ring ;

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

LatticeStr(# the carrier of V, the addF of V,(0. V), the lmult of V,sc #) is non empty LatticeStr over INT.Ring ;

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

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

existence

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

( b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is strict );

end;

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed strict for LatticeStr over INT.Ring ;

correctness existence

ex b

( b

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

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;
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real;

cluster GenLat (V,sc) -> non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;

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;

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

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)

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

existence

ex b_{1} being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring st b_{1} is free ;

end;

cluster non empty left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() free for LatticeStr over INT.Ring ;

correctness existence

ex b

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

correctness

coherence

GenLat (V,sc) is free ;

by ZMtoZL2;

end;
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real;

correctness

coherence

GenLat (V,sc) is free ;

by ZMtoZL2;

registration

existence

ex b_{1} being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring st b_{1} is torsion-free ;

end;

cluster non empty left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() torsion-free for LatticeStr over INT.Ring ;

correctness existence

ex b

proof 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

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

existence

ex b_{1} being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free LatticeStr over INT.Ring st b_{1} is finite-rank ;

end;

cluster non empty left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() Mult-cancelable torsion-free free finite-rank for LatticeStr over INT.Ring ;

correctness existence

ex b

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

correctness

coherence

GenLat (V,sc) is finite-rank ;

by ZMtoZL3;

end;
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real;

correctness

coherence

GenLat (V,sc) is finite-rank ;

by ZMtoZL3;

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):] --> (0. F_Real) holds

GenLat (((0). V),f) is Z_Lattice-like

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):] --> (0. F_Real) holds

GenLat (((0). V),f) is Z_Lattice-like

proof end;

registration
end;

registration

ex b_{1} being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank LatticeStr over INT.Ring st b_{1} is Z_Lattice-like
end;

cluster non empty left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() Mult-cancelable torsion-free free finite-rank V271() Z_Lattice-like for LatticeStr over INT.Ring ;

existence ex b

proof end;

registration

ex b_{1} being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank Z_Lattice-like LatticeStr over INT.Ring st b_{1} is strict
end;

cluster non empty left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() Mult-cancelable torsion-free free finite-rank V271() strict Z_Lattice-like for LatticeStr over INT.Ring ;

existence ex b

proof end;

definition

mode Z_Lattice is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank Z_Lattice-like LatticeStr over INT.Ring ;

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

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

existence

not for b_{1} being Z_Lattice holds b_{1} is trivial ;

end;

cluster non empty non trivial left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() Mult-cancelable torsion-free free finite-rank V271() Z_Lattice-like for Z_Lattice;

correctness existence

not for b

proof end;

registration

let V be torsion-free Z_Module;

coherence

for b_{1} being non empty ModuleStr over F_Rat st b_{1} = Z_MQ_VectSp V holds

( b_{1} is scalar-distributive & b_{1} is vector-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian );

;

end;
cluster Z_MQ_VectSp V -> non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed for non empty ModuleStr over F_Rat ;

correctness coherence

for b

( b

;

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

for v, u being Vector of L holds

( <;v,(- u);> = - <;v,u;> & <;(- v),u;> = - <;v,u;> )

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

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

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

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;

:: Integral Lattice

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

for IT being Z_Lattice holds

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

registration

existence

ex b_{1} being Z_Lattice st b_{1} is INTegral ;

end;

cluster non empty left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() Mult-cancelable torsion-free free finite-rank V271() Z_Lattice-like INTegral for Z_Lattice;

correctness existence

ex b

proof end;

registration

let L be INTegral Z_Lattice;

let v, u be Vector of L;

correctness

coherence

<;v,u;> is integer ;

by defIntegral, INT_1:def 2;

end;
let v, u be Vector of L;

correctness

coherence

<;v,u;> is integer ;

by defIntegral, INT_1:def 2;

registration
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

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

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

definition

let IT be Z_Lattice;

end;
attr IT is positive-definite means :defPositive: :: ZMODLAT1:def 6

for v being Vector of IT st v <> 0. IT holds

||.v.|| > 0 ;

for v being Vector of IT st v <> 0. IT holds

||.v.|| > 0 ;

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

||.v.|| > 0 );

for IT being Z_Lattice holds

( IT is positive-definite iff for v being Vector of IT st v <> 0. IT holds

||.v.|| > 0 );

registration

existence

ex b_{1} being Z_Lattice st

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

end;

cluster non empty non trivial left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() Mult-cancelable torsion-free free finite-rank V271() Z_Lattice-like INTegral positive-definite for Z_Lattice;

correctness existence

ex b

( not b

proof end;

theorem :: ZMODLAT1:16

:: deftheorem defines even ZMODLAT1:def 7 :

for IT being INTegral Z_Lattice holds

( IT is even iff for v being Vector of IT holds ||.v.|| is even );

for IT being INTegral Z_Lattice holds

( IT is even iff for v being Vector of IT holds ||.v.|| is even );

registration

existence

ex b_{1} being INTegral Z_Lattice st b_{1} is even ;

end;

cluster non empty left_complementable right_complementable complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() Mult-cancelable torsion-free free finite-rank V271() Z_Lattice-like INTegral even for Z_Lattice;

correctness existence

ex b

proof end;

definition

let L be Z_Lattice;

let v, u be Vector of L;

symmetry

for v, u being Vector of L st <;v,u;> = 0 holds

<;u,v;> = 0 by defZLattice;

end;
let v, u be Vector of L;

symmetry

for v, u being Vector of L st <;v,u;> = 0 holds

<;u,v;> = 0 by defZLattice;

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

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 )

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).|| = ||.v.|| + ||.u.||

for v, u being Vector of L st v,u are_orthogonal holds

||.(v + u).|| = ||.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).|| = ||.v.|| + ||.u.||

for v, u being Vector of L st v,u are_orthogonal holds

||.(v - u).|| = ||.v.|| + ||.u.||

proof end;

:: Sublattice

definition

let L be Z_Lattice;

ex b_{1} being Z_Lattice st

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

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

ex b

( the carrier of b

proof end;

:: deftheorem defSublattice defines Z_Sublattice ZMODLAT1:def 9 :

for L, b_{2} being Z_Lattice holds

( b_{2} is Z_Sublattice of L iff ( the carrier of b_{2} c= the carrier of L & 0. b_{2} = 0. L & the addF of b_{2} = the addF of L || the carrier of b_{2} & the lmult of b_{2} = the lmult of L | [: the carrier of INT.Ring, the carrier of b_{2}:] & the scalar of b_{2} = the scalar of L || the carrier of b_{2} ) );

for L, b

( b

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

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

for L1 being Z_Sublattice of L

for w being Vector of L1 holds w is Vector of L

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

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

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

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

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

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

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

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

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

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

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;

correctness

coherence

for b_{1} being Z_Sublattice of L holds b_{1} is INTegral ;

end;
correctness

coherence

for b

proof end;

registration

let L be positive-definite Z_Lattice;

correctness

coherence

for b_{1} being Z_Sublattice of L holds b_{1} is positive-definite ;

end;
correctness

coherence

for b

proof 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;
mode FrForm of V,W is Function of [: the carrier of V, the carrier of W:], the carrier of F_Real;

definition

let V, W be ModuleStr over INT.Ring ;

[: the carrier of V, the carrier of W:] --> (0. F_Real) is FrForm of V,W ;

end;
func NulFrForm (V,W) -> FrForm of V,W equals :: ZMODLAT1:def 10

[: the carrier of V, the carrier of W:] --> (0. F_Real);

coherence [: the carrier of V, the carrier of W:] --> (0. F_Real);

[: the carrier of V, the carrier of W:] --> (0. F_Real) is FrForm of V,W ;

:: 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:] --> (0. F_Real);

for V, W being ModuleStr over INT.Ring holds NulFrForm (V,W) = [: the carrier of V, the carrier of W:] --> (0. F_Real);

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be FrForm of V,W;

ex b_{1} being FrForm of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) + (g . (v,w))

for b_{1}, b_{2} being FrForm of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) + (g . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof end;

:: deftheorem Def2 defines + ZMODLAT1:def 11 :

for V, W being non empty ModuleStr over INT.Ring

for f, g, b_{5} being FrForm of V,W holds

( b_{5} = f + g iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = (f . (v,w)) + (g . (v,w)) );

for V, W being non empty ModuleStr over INT.Ring

for f, g, b

( b

for w being Vector of W holds b

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;

ex b_{1} being FrForm of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = a * (f . (v,w))

for b_{1}, b_{2} being FrForm of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = a * (f . (v,w)) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V

for w being Vector of W holds it . (v,w) = a * (f . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof 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 b_{5} being FrForm of V,W holds

( b_{5} = a * f iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = a * (f . (v,w)) );

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 b

( b

for w being Vector of W holds b

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be FrForm of V,W;

ex b_{1} being FrForm of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = - (f . (v,w))

for b_{1}, b_{2} being FrForm of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = - (f . (v,w)) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V

for w being Vector of W holds it . (v,w) = - (f . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof end;

:: deftheorem Def4 defines - ZMODLAT1:def 13 :

for V, W being non empty ModuleStr over INT.Ring

for f, b_{4} being FrForm of V,W holds

( b_{4} = - f iff for v being Vector of V

for w being Vector of W holds b_{4} . (v,w) = - (f . (v,w)) );

for V, W being non empty ModuleStr over INT.Ring

for f, b

( b

for w being Vector of W holds b

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f be FrForm of V,W;

compatibility

for b_{1} being FrForm of V,W holds

( b_{1} = - f iff b_{1} = (- (1. F_Real)) * f )

end;
let f be FrForm of V,W;

compatibility

for b

( b

proof 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 = (- (1. F_Real)) * f;

for V, W being non empty ModuleStr over INT.Ring

for f being FrForm of V,W holds - f = (- (1. F_Real)) * f;

definition

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be FrForm of V,W;

correctness

coherence

f + (- g) is FrForm of V,W;

;

end;
let f, g be FrForm of V,W;

correctness

coherence

f + (- g) is FrForm of V,W;

;

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

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;

for b_{1} being FrForm of V,W holds

( b_{1} = f - g iff for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) - (g . (v,w)) )

end;
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 v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) - (g . (v,w));

for b

( b

for w being Vector of W holds b

proof end;

:: deftheorem Def7 defines - ZMODLAT1:def 16 :

for V, W being non empty ModuleStr over INT.Ring

for f, g, b_{5} being FrForm of V,W holds

( b_{5} = f - g iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = (f . (v,w)) - (g . (v,w)) );

for V, W being non empty ModuleStr over INT.Ring

for f, g, b

( b

for w being Vector of W holds b

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

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

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

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)

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)

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)

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)

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)

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 (1. F_Real) * f = f

for f being FrForm of V,W holds (1. F_Real) * 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;
mode FrFunctional of V is Function of the carrier of V, the carrier of F_Real;

definition

let V be non empty ModuleStr over INT.Ring ;

let f, g be FrFunctional of V;

ex b_{1} being FrFunctional of V st

for x being Element of V holds b_{1} . x = (f . x) + (g . x)

for b_{1}, b_{2} being FrFunctional of V st ( for x being Element of V holds b_{1} . x = (f . x) + (g . x) ) & ( for x being Element of V holds b_{2} . x = (f . x) + (g . x) ) holds

b_{1} = b_{2}

end;
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 for x being Element of V holds it . x = (f . x) + (g . x);

ex b

for x being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem HDef3 defines + ZMODLAT1:def 17 :

for V being non empty ModuleStr over INT.Ring

for f, g, b_{4} being FrFunctional of V holds

( b_{4} = f + g iff for x being Element of V holds b_{4} . x = (f . x) + (g . x) );

for V being non empty ModuleStr over INT.Ring

for f, g, b

( b

definition

let V be non empty ModuleStr over INT.Ring ;

let f be FrFunctional of V;

ex b_{1} being FrFunctional of V st

for x being Element of V holds b_{1} . x = - (f . x)

for b_{1}, b_{2} being FrFunctional of V st ( for x being Element of V holds b_{1} . x = - (f . x) ) & ( for x being Element of V holds b_{2} . x = - (f . x) ) holds

b_{1} = b_{2}

end;
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 for x being Element of V holds it . x = - (f . x);

ex b

for x being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem HDef4 defines - ZMODLAT1:def 18 :

for V being non empty ModuleStr over INT.Ring

for f, b_{3} being FrFunctional of V holds

( b_{3} = - f iff for x being Element of V holds b_{3} . x = - (f . x) );

for V being non empty ModuleStr over INT.Ring

for f, b

( b

definition

let V be non empty ModuleStr over INT.Ring ;

let f, g be FrFunctional of V;

coherence

f + (- g) is FrFunctional of V ;

end;
let f, g be FrFunctional of V;

coherence

f + (- g) is FrFunctional of V ;

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

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;

ex b_{1} being FrFunctional of V st

for x being Element of V holds b_{1} . x = v * (f . x)

for b_{1}, b_{2} being FrFunctional of V st ( for x being Element of V holds b_{1} . x = v * (f . x) ) & ( for x being Element of V holds b_{2} . x = v * (f . x) ) holds

b_{1} = b_{2}

end;
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 for x being Element of V holds it . x = v * (f . x);

ex b

for x being Element of V holds b

proof end;

uniqueness for b

b

proof 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, b_{4} being FrFunctional of V holds

( b_{4} = v * f iff for x being Element of V holds b_{4} . x = v * (f . x) );

for V being non empty ModuleStr over INT.Ring

for v being Element of F_Real

for f, b

( b

definition
end;

:: deftheorem defines 0FrFunctional ZMODLAT1:def 21 :

for V being ModuleStr over INT.Ring holds 0FrFunctional V = ([#] V) --> (0. F_Real);

for V being ModuleStr over INT.Ring holds 0FrFunctional V = ([#] V) --> (0. F_Real);

definition

let V be non empty ModuleStr over INT.Ring ;

let F be FrFunctional of V;

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

for x being Vector of V

for r being Scalar of holds F . (r * x) = r * (F . x);

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

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

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

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;

for b_{1} being FrFunctional of V st b_{1} is homogeneous holds

b_{1} is 0-preserving

end;
cluster Function-like V18( the carrier of V, the carrier of F_Real) homogeneous -> 0-preserving for FrFunctional of ;

coherence for b

b

proof end;

registration
end;

registration
end;

registration

let V be non empty ModuleStr over INT.Ring ;

coherence

0FrFunctional V is 0-preserving by FUNCOP_1:7;

end;
coherence

0FrFunctional V is 0-preserving by FUNCOP_1:7;

registration

let V be non empty ModuleStr over INT.Ring ;

ex b_{1} being FrFunctional of V st

( b_{1} is additive & b_{1} is homogeneous & b_{1} is 0-preserving )

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

existence ex b

( b

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)

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 (0FrFunctional V) . x = 0. F_Real by FUNCOP_1:7;

for x being Element of V holds (0FrFunctional V) . 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 + (0FrFunctional V) = f

for f being FrFunctional of V holds f + (0FrFunctional V) = 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

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)

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)

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)

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 (1. F_Real) * f = f

for f being FrFunctional of V holds (1. F_Real) * f = f

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

let f, g be additive FrFunctional of V;

coherence

f + g is additive

end;
let f, g be additive FrFunctional of V;

coherence

f + g is additive

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

let f be additive FrFunctional of V;

coherence

- f is additive

end;
let f be additive FrFunctional of V;

coherence

- f is additive

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

coherence

v * f is additive

end;
let v be Element of F_Real;

let f be additive FrFunctional of V;

coherence

v * f is additive

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

let f, g be homogeneous FrFunctional of V;

coherence

f + g is homogeneous

end;
let f, g be homogeneous FrFunctional of V;

coherence

f + g is homogeneous

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

let f be homogeneous FrFunctional of V;

coherence

- f is homogeneous

end;
let f be homogeneous FrFunctional of V;

coherence

- f is homogeneous

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

coherence

v * f is homogeneous

end;
let v be Element of F_Real;

let f be homogeneous FrFunctional of V;

coherence

v * f is homogeneous

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

correctness

coherence

(curry f) . v is FrFunctional of W;

;

end;
let f be FrForm of V,W;

let v be Vector of V;

correctness

coherence

(curry f) . v is FrFunctional of W;

;

:: 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) = (curry f) . v;

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) = (curry f) . 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;

correctness

coherence

(curry' f) . w is FrFunctional of V;

;

end;
let f be FrForm of V,W;

let w be Vector of W;

correctness

coherence

(curry' f) . w is FrFunctional of V;

;

:: 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) = (curry' f) . w;

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) = (curry' f) . 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) ) )

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

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 (0FrFunctional V) . x = 0. F_Real by FUNCOP_1:7;

for x being Element of V holds (0FrFunctional V) . 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

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

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

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

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

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

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

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

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

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

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;

ex b_{1} being FrForm of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . v) * (g . w)

for b_{1}, b_{2} being FrForm of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . v) * (g . w) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = (f . v) * (g . w) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . v) * (g . w);

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof 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 b_{5} being FrForm of V,W holds

( b_{5} = FrFormFunctional (f,g) iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = (f . v) * (g . w) );

for V, W being non empty ModuleStr over INT.Ring

for f being FrFunctional of V

for g being FrFunctional of W

for b

( b

for w being Vector of W holds b

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,(0FrFunctional W))) . (v,w) = 0. INT.Ring

for f being FrFunctional of V

for v being Vector of V

for w being Vector of W holds (FrFormFunctional (f,(0FrFunctional W))) . (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 ((0FrFunctional V),g)) . (v,w) = 0. INT.Ring

for g being FrFunctional of W

for v being Vector of V

for w being Vector of W holds (FrFormFunctional ((0FrFunctional V),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,(0FrFunctional W)) = NulFrForm (V,W)

for f being FrFunctional of V holds FrFormFunctional (f,(0FrFunctional W)) = 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 ((0FrFunctional V),g) = NulFrForm (V,W)

for g being FrFunctional of W holds FrFormFunctional ((0FrFunctional V),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

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

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;

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

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 ;

for w being Vector of W holds FrFunctionalSAF (f,w) is additive ;

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

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

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;

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

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 ;

for w being Vector of W holds FrFunctionalSAF (f,w) is homogeneous ;

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

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

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 ;

coherence

NulFrForm (V,W) is additiveFAF

NulFrForm (V,W) is additiveSAF

end;
coherence

NulFrForm (V,W) is additiveFAF

proof end;

coherence NulFrForm (V,W) is additiveSAF

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

ex b_{1} being FrForm of V,W st

( b_{1} is additiveFAF & b_{1} is additiveSAF )

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

existence ex b

( b

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

coherence

NulFrForm (V,W) is homogeneousFAF

NulFrForm (V,W) is homogeneousSAF

end;
coherence

NulFrForm (V,W) is homogeneousFAF

proof end;

coherence NulFrForm (V,W) is homogeneousSAF

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

ex b_{1} being FrForm of V,W st

( b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

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

existence ex b

( b

proof end;

definition

let V, W be non empty ModuleStr over INT.Ring ;

mode bilinear-FrForm of V,W is additiveFAF additiveSAF homogeneousFAF homogeneousSAF FrForm of V,W;

end;
mode bilinear-FrForm of V,W is additiveFAF additiveSAF homogeneousFAF homogeneousSAF FrForm of V,W;

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;

coherence

FrFunctionalFAF (f,v) is additive by HDef11;

end;
let f be additiveFAF FrForm of V,W;

let v be Vector of V;

coherence

FrFunctionalFAF (f,v) is additive by HDef11;

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;

coherence

FrFunctionalSAF (f,w) is additive by HDef12;

end;
let f be additiveSAF FrForm of V,W;

let w be Vector of W;

coherence

FrFunctionalSAF (f,w) is additive by HDef12;

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;
let f be homogeneousFAF FrForm of V,W;

let v be Vector of V;

coherence

FrFunctionalFAF (f,v) is homogeneous by HDef13;

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;
let f be homogeneousSAF FrForm of V,W;

let w be Vector of W;

coherence

FrFunctionalSAF (f,w) is homogeneous by HDef14;

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

FrFormFunctional (f,g) is additiveFAF

end;
let f be FrFunctional of V;

let g be additive FrFunctional of W;

coherence

FrFormFunctional (f,g) is additiveFAF

proof 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

FrFormFunctional (f,g) is additiveSAF

end;
let f be additive FrFunctional of V;

let g be FrFunctional of W;

coherence

FrFormFunctional (f,g) is additiveSAF

proof 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

end;
let f be FrFunctional of V;

let g be homogeneous FrFunctional of W;

coherence

FrFormFunctional (f,g) is homogeneousFAF

proof 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

end;
let f be homogeneous FrFunctional of V;

let g be FrFunctional of W;

coherence

FrFormFunctional (f,g) is homogeneousSAF

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

coherence

not FrFormFunctional (f,g) is trivial

end;
let W be non empty ModuleStr over INT.Ring ;

let f be FrFunctional of V;

let g be FrFunctional of W;

coherence

not FrFormFunctional (f,g) is trivial

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

coherence

not FrFormFunctional (f,g) is trivial

end;
let W be non trivial ModuleStr over INT.Ring ;

let f be FrFunctional of V;

let g be FrFunctional of W;

coherence

not FrFormFunctional (f,g) is trivial

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

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;

for b_{1} being FrFunctional of V st b_{1} is homogeneous holds

b_{1} is 0-preserving

end;
cluster Function-like V18( the carrier of V, the carrier of F_Real) homogeneous -> 0-preserving for FrFunctional of ;

coherence for b

b

proof end;

registration

let V be non empty ModuleStr over INT.Ring ;

coherence

0FrFunctional V is 0-preserving by FUNCOP_1:7;

end;
coherence

0FrFunctional V is 0-preserving by FUNCOP_1:7;

registration

let V be non empty ModuleStr over INT.Ring ;

ex b_{1} being FrFunctional of V st

( b_{1} is additive & b_{1} is homogeneous & b_{1} is 0-preserving )

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

existence ex b

( b

proof end;

registration

let V be non trivial free Z_Module;

ex b_{1} being FrFunctional of V st

( b_{1} is additive & b_{1} is homogeneous & not b_{1} is constant & not b_{1} is trivial )

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

existence ex b

( b

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

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;

coherence

not FrFormFunctional (f,g) is constant

end;
let f be non constant 0-preserving FrFunctional of V;

let g be non constant 0-preserving FrFunctional of W;

coherence

not FrFormFunctional (f,g) is constant

proof end;

definition

let V be non empty ModuleStr over INT.Ring ;

mode linear-FrFunctional of V is additive homogeneous FrFunctional of V;

end;
mode linear-FrFunctional of V is additive homogeneous FrFunctional of V;

registration

let V, W be non trivial free Z_Module;

ex b_{1} being FrForm of V,W st

( not b_{1} is trivial & not b_{1} is constant & b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

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

existence ex b

( not b

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be additiveSAF FrForm of V,W;

correctness

coherence

f + g is additiveSAF ;

end;
let f, g be additiveSAF FrForm of V,W;

correctness

coherence

f + g is additiveSAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be additiveFAF FrForm of V,W;

correctness

coherence

f + g is additiveFAF ;

end;
let f, g be additiveFAF FrForm of V,W;

correctness

coherence

f + g is additiveFAF ;

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

correctness

coherence

a * f is additiveSAF ;

end;
let f be additiveSAF FrForm of V,W;

let a be Element of F_Real;

correctness

coherence

a * f is additiveSAF ;

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

correctness

coherence

a * f is additiveFAF ;

end;
let f be additiveFAF FrForm of V,W;

let a be Element of F_Real;

correctness

coherence

a * f is additiveFAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additiveSAF FrForm of V,W;

correctness

coherence

- f is additiveSAF ;

;

end;
let f be additiveSAF FrForm of V,W;

correctness

coherence

- f is additiveSAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be additiveFAF FrForm of V,W;

correctness

coherence

- f is additiveFAF ;

;

end;
let f be additiveFAF FrForm of V,W;

correctness

coherence

- f is additiveFAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be additiveSAF FrForm of V,W;

correctness

coherence

f - g is additiveSAF ;

;

end;
let f, g be additiveSAF FrForm of V,W;

correctness

coherence

f - g is additiveSAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f, g be additiveFAF FrForm of V,W;

correctness

coherence

f - g is additiveFAF ;

;

end;
let f, g be additiveFAF FrForm of V,W;

correctness

coherence

f - g is additiveFAF ;

;

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;
let f, g be homogeneousSAF FrForm of V,W;

correctness

coherence

f + g is homogeneousSAF ;

proof 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;
let f, g be homogeneousFAF FrForm of V,W;

correctness

coherence

f + g is homogeneousFAF ;

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

end;
let f be homogeneousSAF FrForm of V,W;

let a be Element of F_Real;

correctness

coherence

a * f is homogeneousSAF ;

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

end;
let f be homogeneousFAF FrForm of V,W;

let a be Element of F_Real;

correctness

coherence

a * f is homogeneousFAF ;

proof end;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneousSAF FrForm of V,W;

correctness

coherence

- f is homogeneousSAF ;

;

end;
let f be homogeneousSAF FrForm of V,W;

correctness

coherence

- f is homogeneousSAF ;

;

registration

let V, W be non empty ModuleStr over INT.Ring ;

let f be homogeneousFAF FrForm of V,W;

correctness

coherence

- f is homogeneousFAF ;

;

end;
let f be homogeneousFAF FrForm of V,W;

correctness

coherence

- f is homogeneousFAF ;

;

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;
let f, g be homogeneousSAF FrForm of V,W;

correctness

coherence

f - g is homogeneousSAF ;

;

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;
let f, g be homogeneousFAF FrForm of V,W;

correctness

coherence

f - g is homogeneousFAF ;

;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 )

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;

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

b_{1} * (i,j) = f . ((b1 /. i),(b2 /. j))

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

b_{1} * (i,j) = f . ((b1 /. i),(b2 /. j)) ) & ( for i, j being Nat st i in dom b1 & j in dom b2 holds

b_{2} * (i,j) = f . ((b1 /. i),(b2 /. j)) ) holds

b_{1} = b_{2}

end;
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 for i, j being Nat st i in dom b1 & j in dom b2 holds

it * (i,j) = f . ((b1 /. i),(b2 /. j));

ex b

for i, j being Nat st i in dom b1 & j in dom b2 holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{6} being Matrix of len b1, len b2,F_Real holds

( b_{6} = BilinearM (f,b1,b2) iff for i, j being Nat st i in dom b1 & j in dom b2 holds

b_{6} * (i,j) = f . ((b1 /. i),(b2 /. j)) );

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 b

( b

b

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

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)

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)

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;

definition
end;

:: deftheorem defines inttorealM ZMODLAT1:def 33 :

for M being Matrix of INT.Ring holds inttorealM M = M;

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;

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

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;

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

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

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

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

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

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

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

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

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

definition

let V be free finite-rank Z_Module;

let f be bilinear-FrForm of V,V;

let b be OrdBasis of V;

correctness

coherence

BilinearM (f,b,b) is Matrix of rank V,F_Real;

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

let b be OrdBasis of V;

correctness

coherence

BilinearM (f,b,b) is Matrix of rank V,F_Real;

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

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;

ex b_{1} being Element of F_Real st

for b being OrdBasis of V holds b_{1} = Det (GramMatrix (f,b))

for b_{1}, b_{2} being Element of F_Real st ( for b being OrdBasis of V holds b_{1} = Det (GramMatrix (f,b)) ) & ( for b being OrdBasis of V holds b_{2} = Det (GramMatrix (f,b)) ) holds

b_{1} = b_{2}

end;
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 for b being OrdBasis of V holds it = Det (GramMatrix (f,b));

ex b

for b being OrdBasis of V holds b

proof end;

uniqueness for b

b

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

( b_{3} = GramDet f iff for b being OrdBasis of V holds b_{3} = Det (GramMatrix (f,b)) );

for V being free finite-rank Z_Module

for f being bilinear-FrForm of V,V

for b

( b

:: deftheorem defines InnerProduct ZMODLAT1:def 36 :

for L being Z_Lattice holds InnerProduct L = the scalar of L;

for L being Z_Lattice holds InnerProduct L = the scalar of L;

registration

let L be Z_Lattice;

correctness

coherence

( InnerProduct L is additiveSAF & InnerProduct L is homogeneousSAF & InnerProduct L is additiveFAF & InnerProduct L is homogeneousFAF );

end;
correctness

coherence

( InnerProduct L is additiveSAF & InnerProduct L is homogeneousSAF & InnerProduct L is additiveFAF & InnerProduct L is homogeneousFAF );

proof end;

definition

let L be Z_Lattice;

let b be OrdBasis of L;

coherence

GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Real;

;

end;
let b be OrdBasis of L;

func GramMatrix b -> Matrix of dim L,F_Real equals :: ZMODLAT1:def 37

GramMatrix ((InnerProduct L),b);

correctness GramMatrix ((InnerProduct L),b);

coherence

GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Real;

;

:: deftheorem defines GramMatrix ZMODLAT1:def 37 :

for L being Z_Lattice

for b being OrdBasis of L holds GramMatrix b = GramMatrix ((InnerProduct L),b);

for L being Z_Lattice

for b being OrdBasis of L holds GramMatrix b = GramMatrix ((InnerProduct L),b);

definition
end;

:: deftheorem defines GramDet ZMODLAT1:def 38 :

for L being Z_Lattice holds GramDet L = GramDet (InnerProduct L);

for L being Z_Lattice holds GramDet L = GramDet (InnerProduct L);

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

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