:: Lattice of $\mathbb Z$-module
:: by Yuichi Futa and Yasunari Shidama
::
:: Received December 30, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GAUSSINT, NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0,
FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3,
ORDINAL4, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1,
NAT_1, FINSET_1, FUNCOP_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, INT_1,
ZMODUL01, ZMODUL03, FINSEQ_4, RLVECT_3, RMOD_2, RANKNULL, UNIALG_1,
FUNCT_7, GROUP_1, INT_3, COMPLEX1, VECTSP_1, MESFUNC1, XCMPLX_0,
REALSET1, MATRLIN, ZMODUL02, RLVECT_5, ZMODUL06, NORMSP_1, BHSP_1, ABIAN,
RVSUM_1, MATRIX_1, MATRIX_3, MOD_3, ZMATRLIN, FUNCT_5, ZMODLAT1, TREES_1,
MFOLD_2, BILINEAR, HAHNBAN, FVSUM_1, INCSP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1,
FINSET_1, CARD_1, FUNCT_5, XCMPLX_0, XXREAL_0, INT_1, RAT_1, COMPLEX1,
FINSEQ_1, ABIAN, MATRIX_0, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1,
VECTSP_1, VECTSP_4, VECTSP_7, MATRIX_1, FVSUM_1, MATRIX_3, HAHNBAN1,
INT_3, BILINEAR, ZMODUL01, ZMODUL03, GAUSSINT, ZMODUL04, ZMODUL06,
ZMATRLIN;
constructors BINOP_2, UPROOTS, ZMODUL01, REALSET1, EUCLID, FVSUM_1, FUNCT_3,
ALGSTR_1, EC_PF_1, MATRIX_3, ZMODUL04, ZMODUL06, ABIAN, ZMATRLIN,
ZMODUL07, RELSET_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, RLVECT_1, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1,
ZMODUL01, XBOOLE_0, BINOP_2, ORDINAL1, XXREAL_0, NAT_1, ALGSTR_0, INT_3,
REALSET1, RELAT_1, VECTSP_1, VECTSP_2, FUNCT_3, XCMPLX_0, ZMODUL03,
ZMODUL04, ZMODUL05, ZMODUL06, ABIAN, MATRIX_0, ZMATRLIN;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions RLVECT_1, ALGSTR_0, VECTSP_1;
equalities BINOP_1, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, VECTSP_4, REALSET1,
FVSUM_1, FUNCOP_1, FINSEQ_1, MATRIX_0, ZMATRLIN;
expansions TARSKI, STRUCT_0, VECTSP_1, BINOP_1, FINSEQ_1, HAHNBAN1, ZMATRLIN;
theorems BINOP_1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, INT_1,
NAT_1, RLVECT_1, TARSKI, ZMODUL01, ZFMISC_1, GAUSSINT, XTUPLE_0,
ZMODUL03, HAHNBAN1, XBOOLE_0, XBOOLE_1, FUNCOP_1, XREAL_1, XXREAL_0,
STRUCT_0, PARTFUN1, VECTSP_1, ALGSTR_0, EC_PF_1, ZMODUL02, VECTSP_7,
NUMBERS, VECTSP_4, ABSVALUE, MATRIX_0, ZMODUL06, MATRIXR2, MATRIX_3,
ZMATRLIN, FUNCT_5, VECTSP10, FVSUM_1, DOMAIN_1, MATRIX_4, MATRIX11,
MATRIX_7, MATRIX_1, RELAT_1;
schemes BINOP_1, FUNCT_2, NAT_1, MATRIX_0, FINSEQ_2;
begin :: 1. Definition of lattices of $\mathbb Z$-module
theorem LMEQ:
for D, E being non empty set, n, m being Nat, 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
let D, E be non empty set, n, m be Nat, M be Matrix of n,m,D;
assume for i, j being Nat st [i, j] in Indices M
holds M*(i,j) in E;
then reconsider G = M as Matrix of E by ZMATRLIN:5;
per cases;
suppose not n > 0; then
X1: n = 0;
then G = {} by MATRIX_0:22;
hence thesis by X1,MATRIX_0:13;
end;
suppose X1: n > 0;
then len G = n & width G = m by MATRIX_0:23;
hence thesis by X1,MATRIX_0:20;
end;
end;
definition
let F be 1-sorted;
struct (ModuleStr over F) LatticeStr over F
(# carrier -> set,
addF -> BinOp of the carrier,
ZeroF -> Element of the carrier,
lmult -> Function of [: the carrier of F, the carrier :], the carrier,
scalar -> Function of [: the carrier, the carrier :],
the carrier of F_Real #);
end;
registration
let F be 1-sorted;
cluster strict non empty for LatticeStr over F;
correctness
proof
set D = the non empty set, Z = the Element of D,
a = the BinOp of D,
m = the Function of [:the carrier of F, D:],
D,s = the Function of [: D,D:],the carrier of F_Real;
take LatticeStr(#D,a,Z,m,s#);
thus thesis;
end;
end;
registration
let F be 1-sorted;
let D be non empty set, Z be Element of D, a be BinOp of D,m be Function of
[:the carrier of F, D:], D, s be Function of [: D,D:],the carrier of F_Real;
cluster LatticeStr(#D,a,Z,m,s#) -> non empty;
coherence;
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
(the scalar of X).[x, y];
correctness;
end;
definition
let X be non empty LatticeStr over INT.Ring;
let x be Vector of X;
func ||. x .|| -> Element of F_Real equals
<; x, x ;>;
correctness;
end;
definition
let IT be non empty LatticeStr over INT.Ring;
attr IT is Z_Lattice-like means
:defZLattice:
(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, a being Element of INT.Ring
holds <; x+y, z ;> = <; x, z ;> + <; y, z ;>
& <; a*x, y ;> = a * <; x, y ;>);
end;
definition
let V be Z_Module,
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
LatticeStr (# the carrier of V, the addF of V, 0.V, the lmult of V, sc #);
coherence;
end;
ZMtoZL1:
for V being Z_Module,
sc being Function of [: the carrier of V, the carrier of V :],
the carrier of F_Real holds
GenLat (V,sc) is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
proof
let V be Z_Module,
sc be Function of [: the carrier of V, the carrier of V :],
the carrier of F_Real;
set L = GenLat (V,sc);
A1: for x,y be Vector of L for x9, y9 be Vector of V
st x = x9 & y = y9
holds x + y = x9 + y9 & for a being Element of INT.Ring holds
a * x = a * x9;
thus for v, w being Vector of L holds v + w = w + v
proof
let v, w be Vector of L;
reconsider v9 = v, w9 = w as Vector of V;
thus v + w = w9+ v9 by A1
.= w + v;
end;
thus for u, v, w being Vector of L holds (u + v) + w = u + (v + w)
proof
let u, v, w be Vector of L;
reconsider u9 = u, v9 = v, w9 = w as Vector of V;
thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w);
end;
thus for v being Vector of L holds v + 0.L = v
proof
let v be Vector of L;
reconsider v9 = v as Vector of V;
thus v + 0.L = v9+ 0.V .= v;
end;
thus L is right_complementable
proof
let v be Vector of L;
reconsider v9 = v as Vector of V;
consider w9 be Vector of V such that
A2: v9 + w9 = 0.V by ALGSTR_0:def 11;
reconsider w = w9 as Vector of L;
take w;
thus thesis by A2;
end;
thus for a, b being Element of INT.Ring, v being Vector of L
holds (a + b) * v = a * v + b * v
proof
let a, b be Element of INT.Ring, v be Vector of L;
reconsider v9 = v as Vector of V;
thus (a + b) * v = (a + b) * v9 .= a * v9 + b * v9 by VECTSP_1:def 15
.= a * v + b * v;
end;
thus for a being Element of INT.Ring, v, w being Vector of L
holds a * (v + w) = a * v + a * w
proof
let a be Element of INT.Ring, v, w be Vector of L;
reconsider v9 = v, w9 = w as Vector of V;
thus a * (v + w) = a *(v9 + w9) .= a * v9 + a * w9 by VECTSP_1:def 14
.= a * v + a * w;
end;
thus for a, b being Element of INT.Ring, v being Vector of L
holds (a * b) * v = a * (b * v)
proof
let a, b be Element of INT.Ring, v be Vector of L;
reconsider v9 = v as Vector of V;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by VECTSP_1:def 16
.= a * (b * v);
end;
thus for v being Vector of L holds 1.(INT.Ring) * v = v
proof
let v be Vector of L;
reconsider v9 = v as Vector of V;
thus 1.(INT.Ring) * v = 1.(INT.Ring) * v9 .= v;
end;
end;
registration
cluster vector-distributive scalar-distributive scalar-associative
scalar-unital Abelian add-associative right_zeroed right_complementable
strict for non empty LatticeStr over INT.Ring;
correctness
proof
set V0 = the Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat ((0).V0, nilfunc);
take X0;
thus X0 is vector-distributive scalar-distributive scalar-associative
scalar-unital Abelian add-associative right_zeroed right_complementable
strict by ZMtoZL1;
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;
cluster GenLat (V, sc) -> Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital;
correctness by ZMtoZL1;
end;
theorem LmZMtoZL1:
for V being Z_Module,
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
let V be Z_Module,
sc be Function of [: the carrier of V, the carrier of V :],
the carrier of F_Real;
set L = GenLat (V,sc);
A2: 0.L = 0.V;
A3: the addF of L = (the addF of V) || the carrier of L;
the lmult of L = (the lmult of V) |
[:the carrier of INT.Ring, the carrier of L:];
hence thesis by A2,A3,VECTSP_4:def 2;
end;
theorem
for V being Z_Module,
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
let V be Z_Module,
sc be Function of [: the carrier of V, the carrier of V :],
the carrier of F_Real;
set L = GenLat (V,sc);
A2: 0.V = 0.L;
A3: the addF of V = (the addF of L) || the carrier of V;
the lmult of V = (the lmult of L) |
[:the carrier of INT.Ring, the carrier of V:];
hence thesis by A2,A3,VECTSP_4:def 2;
end;
ZMtoZL2:
for V being free Z_Module,
sc being Function of [: the carrier of V, the carrier of V :],
the carrier of F_Real holds
GenLat (V,sc) is free
proof
let V be free Z_Module,
sc be Function of [: the carrier of V, the carrier of V :],
the carrier of F_Real;
set L = GenLat (V,sc);
consider A be Subset of V such that
AX2: A is base by VECTSP_7:def 4;
reconsider AA = A as Subset of L;
A4: L is Submodule of V by LmZMtoZL1;
A5: AA is linearly-independent by AX2,A4,VECTSP_7:def 3,ZMODUL03:16;
Lin(AA) = Lin(A) by A4,ZMODUL03:20
.= (Omega).L by AX2,VECTSP_7:def 3;
hence thesis by A5,VECTSP_7:def 3,VECTSP_7:def 4;
end;
registration
cluster free for Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
correctness
proof
set V0 = the free Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat ((0).V0, nilfunc);
reconsider X0 as Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
take X0;
thus X0 is free by ZMtoZL2;
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) -> free;
correctness by ZMtoZL2;
end;
registration
cluster torsion-free for Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
correctness
proof
set V0 = the free Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat ((0).V0, nilfunc);
reconsider X0 as Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
take X0;
thus X0 is torsion-free;
end;
end;
theorem ZMtoZL3:
for V being finite-rank free Z_Module,
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
let V be finite-rank free Z_Module,
sc be Function of [: the carrier of V, the carrier of V :],
the carrier of F_Real;
set L = GenLat (V,sc);
L is Submodule of V by LmZMtoZL1;
hence thesis;
end;
registration
cluster finite-rank for free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
correctness
proof
set V0 = the finite-rank free Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat ((0).V0,nilfunc);
reconsider X0 as Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
reconsider X0 as free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
take X0;
thus X0 is finite-rank by ZMtoZL3;
end;
end;
registration
let V be finite-rank 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) -> finite-rank;
correctness by ZMtoZL3;
end;
theorem ThTrivialLat1:
for V being finite-rank free Z_Module, 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
let V be finite-rank free Z_Module,
f be Function of [:the carrier of (0).V, the carrier of (0).V:],
the carrier of F_Real such that
P1: f = [:the carrier of (0).V, the carrier of (0).V:] --> 0.F_Real;
set X = GenLat ((0).V,f);
reconsider X as Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
reconsider X as free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
reconsider X as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
P2: for x being Vector of X
st for y being Vector of X holds <; x, y ;> = 0
holds x = 0.X
proof
let x be Vector of X such that
for y being Vector of X holds <; x, y ;> = 0;
x in the carrier of (0).V;
then x in {0.V} by VECTSP_4:def 3;
hence x = 0.V by TARSKI:def 1
.= 0.X by ZMODUL01:26;
end;
for x, y, z being Vector of X, a being Element of INT.Ring holds
<; x, y ;> = <; y, x ;>
& <; x+y, z ;> = <; x, z ;> + <; y, z ;>
& <; a*x, y ;> = a * <; x, y ;>
proof
let x, y, z be Vector of X;
let a be Element of INT.Ring;
A1: the carrier of (0).V = {0.V} by VECTSP_4:def 3;
then A3: 0.V in the carrier of (0).V by TARSKI:def 1;
thus <; x, y ;> = <; y, x ;>
proof
x = 0.V & y = 0.V by A1,TARSKI:def 1;
hence thesis;
end;
A4: f.[0.V, 0.V] = 0 by A3,P1,FUNCOP_1:7,ZFMISC_1:87;
thus <; x+y, z ;> = <; x, z ;> + <; y, z ;>
proof
reconsider u = x, v = y, w = z as Vector of (0).V;
B2: w = 0.V by A1,TARSKI:def 1;
u = 0.V & v = 0.V by A1,TARSKI:def 1;
hence thesis by A1,A4,B2,TARSKI:def 1;
end;
thus <; a*x, y ;> = a * <; x, y ;>
proof
reconsider u = x, v = y as Vector of (0).V;
u = 0.V & v = 0.V by A1,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 1;
end;
end;
hence thesis by P2;
end;
registration
cluster Z_Lattice-like for non empty LatticeStr over INT.Ring;
existence
proof
set V0 = the finite-rank free Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0.F_Real
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real;
set X0 = GenLat ((0).V0,nilfunc);
reconsider X0 as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
take X0;
thus thesis by ThTrivialLat1;
end;
end;
registration
cluster Z_Lattice-like for finite-rank free Abelian add-associative
right_zeroed right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
existence
proof
set V0 = the finite-rank free Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat ((0).V0,nilfunc);
reconsider X0 as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
take X0;
thus thesis by ThTrivialLat1;
end;
end;
registration
cluster strict for finite-rank free
Z_Lattice-like Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
existence
proof
set V0 = the finite-rank free Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat ((0).V0,nilfunc);
reconsider X0 as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
reconsider X0 as Z_Lattice-like finite-rank free Abelian add-associative
right_zeroed right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring by ThTrivialLat1;
take X0;
thus X0 is strict;
end;
end;
definition
mode Z_Lattice is finite-rank free
Z_Lattice-like Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
end;
theorem ThNonTrivialLat1:
for V being non trivial torsion-free Z_Module,
Z being Submodule of V, v being non zero Vector of V,
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, 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
let V be non trivial torsion-free Z_Module,
Z be Submodule of V, v be non zero Vector of V,
f be Function of [:the carrier of Z, the carrier of Z:],
the carrier of F_Real such that
A1: Z = Lin{v} and
A2: (for v1, v2 being Vector of Z, a, b being Element of INT.Ring
st v1 = a*v & v2 = b*v holds f.(v1, v2) = a*b);
set L = GenLat (Z,f);
reconsider L as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring by A1;
L is Z_Lattice-like
proof
thus for x being Vector of L st for y being Vector of L holds
<; x, y ;> = 0
holds x = 0.L
proof
let x be Vector of L such that
C1: for y being Vector of L holds <; x, y ;> = 0;
assume x <> 0.L;
then C2: x <> 0.V by ZMODUL01:26;
x in Lin{v} by A1;
then consider ix be Element of INT.Ring such that
C3: x = ix * v by ZMODUL06:19;
reconsider xx = x as Vector of Z;
C4: ix <> 0 by C2,C3,ZMODUL01:1;
<; x, x ;> = f.(x, x)
.= ix * ix by A2,C3;
hence contradiction by C1,C4;
end;
thus for x, y being Vector of L holds <; x, y ;> = <; y, x ;>
proof
let x, y be Vector of L;
C1: x in Lin{v} & y in Lin{v} by A1;
then consider ix be Element of INT.Ring such that
C2: x = ix * v by ZMODUL06:19;
consider iy be Element of INT.Ring such that
C3: y = iy * v by C1,ZMODUL06:19;
thus <; x, y ;> = f.(x, y)
.= ix * iy by A2,C2,C3
.= f.(y, x) by A2,C2,C3
.= <; y, x ;>;
end;
thus for x, y, z being Vector of L, a being Element of INT.Ring
holds <; x+y, z ;> = <; x, z ;> + <; y, z ;> &
<; a*x, y ;> = a * <; x, y ;>
proof
let x, y, z be Vector of L, a be Element of INT.Ring;
C1: x in Lin{v} & y in Lin{v} & z in Lin{v} by A1;
then consider ix be Element of INT.Ring such that
C2: x = ix * v by ZMODUL06:19;
consider iy be Element of INT.Ring such that
C3: y = iy * v by C1,ZMODUL06:19;
consider iz be Element of INT.Ring such that
C4: z = iz * v by C1,ZMODUL06:19;
ix * v in Lin{v} by ZMODUL06:21;
then reconsider iixv = ix * v as Vector of Z by A1;
reconsider ixv = ix * v as Vector of V;
iy * v in Lin{v} by ZMODUL06:21;
then reconsider iiyv = iy * v as Vector of Z by A1;
reconsider iyv = iy * v as Vector of V;
C5: x + y = iixv + iiyv by C2,C3
.= ixv + iyv by ZMODUL01:28
.= (ix + iy) * v by VECTSP_1:def 15;
C6: a*x = a*iixv by C2
.= a*ixv by ZMODUL01:29
.= (a*ix) * v by VECTSP_1:def 16;
thus <; x+y, z ;> = f.(x+y, z)
.= (ix + iy)*iz by A2,C4,C5
.= ix*iz + iy*iz
.= f.(x, z) + iy*iz by A2,C2,C4
.= f.[x, z] + f.(y, z) by A2,C3,C4
.= <; x, z ;> + <; y, z ;>;
thus <; a*x, y ;> = f.(a*x, y)
.= (a*ix)*iy by A2,C3,C6
.= a*(ix*iy)
.= a * f.(x, y) by A2,C2,C3
.= a * <; x, y ;>;
end;
end;
hence thesis;
end;
registration
cluster non trivial for Z_Lattice;
correctness
proof
set V = the non trivial torsion-free Z_Module;
set v = the non zero Vector of V;
set Z = Lin{v};
defpred P[object, object] means
ex a, b being Element of INT.Ring st $1 = [a*v, b*v] & $2 = a*b;
A1: for x being Element of [:the carrier of Z, the carrier of Z:]
ex y being Element of the carrier of F_Real st P[x, y]
proof
let x be Element of [:the carrier of Z, the carrier of Z:];
consider x1, x2 be object such that
B1: x1 in the carrier of Z & x2 in the carrier of Z & x = [x1, x2]
by ZFMISC_1:def 2;
reconsider x1, x2 as Vector of Z by B1;
x1 in Lin{v};
then consider i1 be Element of INT.Ring such that
B2: x1 = i1*v by ZMODUL06:19;
x2 in Lin{v};
then consider i2 be Element of INT.Ring such that
B3: x2 = i2*v by ZMODUL06:19;
reconsider i12 = i1*i2 as Element of INT;
INT c= the carrier of F_Real by NUMBERS:5,XBOOLE_0:def 8;
then reconsider i12 as Element of the carrier of F_Real;
take i12;
thus thesis by B1,B2,B3;
end;
consider f be Function of [:the carrier of Z, the carrier of Z:],
the carrier of F_Real such that
A2: for x being Element of [:the carrier of Z, the carrier of Z:]
holds P[x, f.x] from FUNCT_2:sch 3(A1);
A3: for v1, v2 being Vector of Z, a, b being Element of INT.Ring
st v1 = a*v & v2 = b*v holds f.(v1, v2) = a*b
proof
let v1, v2 be Vector of Z, a, b be Element of INT.Ring such that
B0: v1 = a*v & v2 = b*v;
consider a0, b0 be Element of INT.Ring such that
B1: [v1, v2] = [a0*v, b0*v] & f.[v1, v2] = a0*b0 by A2;
B2: v <> 0.V;
v1 = a0*v by B1,XTUPLE_0:1;
then B3: a = a0 by B0,B2,ZMODUL01:11;
v2 = b0*v by B1,XTUPLE_0:1;
hence thesis by B0,B1,B2,B3,ZMODUL01:11;
end;
set L = GenLat (Z,f);
reconsider L as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
reconsider L as strict Z_Lattice by A3,ThNonTrivialLat1;
take L;
L is non trivial
proof
assume B1: L is trivial;
v in Lin{v} by ZMODUL06:20;
then B2: v = 0.L by B1;
v <> 0.V;
hence contradiction by B2,ZMODUL01:26;
end;
hence thesis;
end;
end;
registration
let V be torsion-free Z_Module;
cluster Z_MQ_VectSp(V) -> scalar-distributive vector-distributive
scalar-associative scalar-unital add-associative right_zeroed
right_complementable Abelian for non empty ModuleStr over F_Rat;
correctness;
end;
theorem ThSc1:
for L being Z_Lattice, v, u being Vector of L holds
<; v, -u ;> = - <; v, u ;> & <; -v, u ;> = - <; v, u ;>
proof
let L be Z_Lattice, v, u be Vector of L;
thus <; v, -u ;> = <; v, (-1.(INT.Ring))*u ;> by ZMODUL01:2
.= <; (-1.(INT.Ring))*u, v ;> by defZLattice
.= (-1) * <; u, v ;> by defZLattice
.= - <; u, v ;>
.= - <; v, u ;> by defZLattice;
thus <; -v, u ;> = <; (-1.(INT.Ring))*v, u ;> by ZMODUL01:2
.= (-1.(INT.Ring)) * <; v, u ;> by defZLattice
.= - <; v, u ;>;
end;
theorem ThSc2:
for L being Z_Lattice, v, u, w being Vector of L holds
<; v, u + w ;> = <; v, u ;> + <; v, w ;>
proof
let L be Z_Lattice, v, u, w be Vector of L;
thus <; v, u+w ;> = <; u+w, v ;> by defZLattice
.= <; u, v ;> + <; w, v ;> by defZLattice
.= <; v, u ;> + <; w, v ;> by defZLattice
.= <; v, u ;> + <; v, w ;> by defZLattice;
end;
theorem ThSc3:
for L being Z_Lattice, v, u being Vector of L, a being Element of INT.Ring
holds <; v, a*u ;> = a * <; v, u ;>
proof
let L be Z_Lattice, v, u be Vector of L, a be Element of INT.Ring;
thus <; v, a*u ;> = <; a*u, v ;> by defZLattice
.= a * <; u, v ;> by defZLattice
.= a * <; v, u ;> by defZLattice;
end;
theorem ThSc4:
for L being Z_Lattice, v, u, w being Vector of L,
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
let L be Z_Lattice, v, u, w be Vector of L, a, b be Element of INT.Ring;
thus <; a*v + b*u, w ;> = <; a*v, w ;> + <; b*u, w ;> by defZLattice
.= a * <; v, w ;> + <; b*u, w ;> by defZLattice
.= a * <; v, w ;> + b * <; u, w ;> by defZLattice;
thus <; v, a*u + b*w ;> = <; v, a*u ;> + <; v, b*w ;> by ThSc2
.= a * <; v, u ;> + <; v, b*w ;> by ThSc3
.= a * <; v, u ;> + b * <; v, w ;> by ThSc3;
end;
theorem ThSc5:
for L being Z_Lattice, v, u, w being Vector of L holds
<; v-u, w ;> = <; v, w ;> - <; u, w ;> &
<; v, u-w ;> = <; v, u ;> - <; v, w ;>
proof
let L be Z_Lattice, v, u, w be Vector of L;
thus <; v-u, w ;> = <; v+(-1.(INT.Ring))*u, w ;> by ZMODUL01:2
.= <; v, w ;> + <; (-1.(INT.Ring))*u, w ;> by defZLattice
.= <; v, w ;> + (-1.(INT.Ring)) * <; u, w ;> by defZLattice
.= <; v, w ;> - <; u, w ;>;
thus <; v, u-w ;> = <; v, u+(-1.(INT.Ring))*w ;> by ZMODUL01:2
.= <; v, u ;> + <; v, (-1.(INT.Ring))*w ;> by ThSc2
.= <; v, u ;> + (-1.(INT.Ring)) * <; v, w ;> by ThSc3
.= <; v, u ;> - <; v, w ;>;
end;
theorem ThSc6:
for L being Z_Lattice, v being Vector of L holds
<; v, 0.L ;> = 0 & <; 0.L, v ;> = 0
proof
let L be Z_Lattice, v be Vector of L;
thus <; v, 0.L ;> = <; v, v - v ;> by RLVECT_1:15
.= <; v, v ;> - <; v, v ;> by ThSc5
.= 0;
thus <; 0.L, v ;> = <; v - v, v ;> by RLVECT_1:15
.= <; v, v ;> - <; v, v ;> by ThSc5
.= 0;
end;
:: Integral Lattice
definition
let IT be Z_Lattice;
attr IT is INTegral means
:defIntegral:
for v, u being Vector of IT holds <; v, u ;> in INT;
end;
registration
cluster INTegral for Z_Lattice;
correctness
proof
set V0 = the finite-rank free Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat ((0).V0,nilfunc);
reconsider X0 as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
reconsider X0 as Z_Lattice by ThTrivialLat1;
take X0;
thus thesis by INT_1:def 2;
end;
end;
registration
let L be INTegral Z_Lattice;
let v, u be Vector of L;
cluster <; v, u ;> -> integer;
correctness by defIntegral,INT_1:def 2;
end;
registration
let L be INTegral Z_Lattice;
let v be Vector of L;
cluster ||. v .|| -> integer;
correctness;
end;
theorem ThIntLat1B:
for L being Z_Lattice, I being finite Subset of L, 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
let L be Z_Lattice, I be finite Subset of L, u be Vector of L;
assume AS: for v being Vector of L st v in I holds <; v, u ;> in INT;
defpred P[Nat] means
for I be finite Subset of L
st card(I) = $1 &
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;
P1: P[0]
proof
let I be finite Subset of L;
assume card(I) = 0 &
for v being Vector of L st v in I holds <; v, u ;> in INT;
then I = {}(the carrier of L); then
A2: Lin(I) = (0).L by ZMODUL02:67;
let v be Vector of L;
assume v in Lin(I);
then v in {0.L} by A2,VECTSP_4:def 3;
then v = 0.L by TARSKI:def 1;
then <; v, u ;> = 0 by ThSc6;
hence <; v, u ;> in INT;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A0: P[n];
thus P[n+1]
proof
let I be finite Subset of L;
assume A1: card(I) = n+1 &
for v being Vector of L st v in I holds <; v, u ;> in INT;
then I <> {};
then consider v be object such that
A3: v in I by XBOOLE_0:def 1;
reconsider v as Vector of L by A3;
(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A3,ZFMISC_1:40; then
A4: Lin(I) = Lin(I \ {v}) + Lin{v} by ZMODUL02:72;
A5: card(I \ {v}) = card(I) - card{v} by A3,CARD_2:44,ZFMISC_1:31
.= card(I) - 1 by CARD_1:30
.= n by A1;
reconsider J = I \ {v} as finite Subset of L;
B8: for x being Vector of L st x in J holds <; x, u ;> in INT
proof
let x be Vector of L;
assume x in J;
then x in I by XBOOLE_1:36,TARSKI:def 3;
hence <; x, u ;> in INT by A1;
end;
thus for x being Vector of L st x in Lin(I) holds <; x, u ;> in INT
proof
let x be Vector of L;
assume x in Lin(I);
then consider xu1, xu2 be Vector of L such that
A10: xu1 in Lin(I \ {v}) & xu2 in Lin{v} & x = xu1 + xu2
by A4,ZMODUL01:92;
consider ixu2 be Element of INT.Ring such that
A12: xu2 = ixu2 * v by A10,ZMODUL06:19;
B11: x = (1.(INT.Ring))*xu1 + ixu2*v by A10,A12;
set i1 = 1.(INT.Ring);
B13: <; x,u ;> = i1*<; xu1,u ;> + ixu2* <; v,u ;> by B11,ThSc4;
B14: <; xu1,u ;> in INT by A0,A5,B8,A10;
<; v,u ;> in INT by A1,A3;
hence <; x, u ;> in INT by B13,B14,INT_1:def 2;
end;
end;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
card (I) is Nat;
hence thesis by X1,AS;
end;
theorem ThIntLat1A:
for L being Z_Lattice, 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
let L be Z_Lattice;
defpred P[Nat] means
for I be finite Subset of L
st card(I) = $1 &
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 st v in Lin(I) & u in Lin(I)
holds <; v, u ;> in INT;
P1: P[0]
proof
let I be finite Subset of L;
assume card(I) = 0 &
for v, u being Vector of L st v in I & u in I holds <; v, u ;> in INT;
then I = {}(the carrier of L);
then
A2: Lin(I) = (0).L by ZMODUL02:67;
let v, u be Vector of L;
assume v in Lin(I) & u in Lin(I);
then v in {0.L} & u in {0.L} by A2,VECTSP_4:def 3;
then v = 0.L & u = 0.L by TARSKI:def 1;
then <; v, u ;> = 0 by ThSc6;
hence <; v, u ;> in INT;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A0: P[n];
thus P[n+1]
proof
let I be finite Subset of L;
assume A1: card(I) = n+1 &
for v, u being Vector of L st v in I & u in I holds <; v, u ;> in INT;
then I <> {};
then consider v be object such that
A3: v in I by XBOOLE_0:def 1;
reconsider v as Vector of L by A3;
(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A3,ZFMISC_1:40;
then
A4: Lin(I) = Lin(I \ {v}) + Lin{v} by ZMODUL02:72;
A5: card(I \ {v}) = card(I) - card{v} by A3,CARD_2:44,ZFMISC_1:31
.= card(I) - 1 by CARD_1:30
.= n by A1;
reconsider J = I \ {v} as finite Subset of L;
B8: for x, y being Vector of L st x in J & y in J holds
<; x, y ;> in INT
proof
let x, y be Vector of L;
assume x in J & y in J;
then x in I & y in I by XBOOLE_1:36,TARSKI:def 3;
hence <; x, y ;> in INT by A1;
end;
A6X: for x being Vector of L st x in J holds <; x, v ;> in INT
proof
let x be Vector of L;
assume x in J;
then x in I & v in I by A3,XBOOLE_1:36,TARSKI:def 3;
hence <; x, v ;> in INT by A1;
end;
thus for x, y being Vector of L st x in Lin(I) & y in Lin(I) holds
<; x, y ;> in INT
proof
let x, y be Vector of L;
assume A9: x in Lin(I) & y in Lin(I);
then consider xu1, xu2 be Vector of L such that
A10: xu1 in Lin(I \ {v}) & xu2 in Lin{v} & x = xu1 + xu2
by A4,ZMODUL01:92;
consider yu1, yu2 be Vector of L such that
A11: yu1 in Lin(I \ {v}) & yu2 in Lin{v} & y = yu1 + yu2
by A9,A4,ZMODUL01:92;
consider ixu2 be Element of INT.Ring such that
A12: xu2 = ixu2 * v by A10,ZMODUL06:19;
consider iyu2 be Element of INT.Ring such that
A13: yu2 = iyu2 * v by A11,ZMODUL06:19;
B11: x = (1.(INT.Ring))*xu1 + ixu2*v by A10,A12;
set i1 = 1.(INT.Ring);
B13: <; x, y ;>
= <; i1*xu1+ixu2*v, yu1 ;> + <; i1*xu1+ixu2*v, iyu2*v ;>
by A11,A13,B11,ThSc2
.= i1 * <; xu1, yu1 ;> + ixu2 * <; v, yu1 ;>
+ <; i1*xu1 + ixu2*v, iyu2*v ;> by ThSc4
.= i1 * <; xu1, yu1 ;> + ixu2 * <; v, yu1;>
+ (i1 * <; xu1, iyu2*v ;> + ixu2 * <; v, iyu2*v ;>) by ThSc4
.= <; xu1, yu1 ;> + ixu2 * <; v, yu1 ;>
+ <; xu1, iyu2*v ;> + ixu2 * <; v, iyu2*v ;>
.= <; xu1,yu1 ;> + ixu2 * <; v,yu1 ;>
+ <; xu1, iyu2*v ;> + ixu2 * (iyu2 * <; v, v ;>) by ThSc3
.= <; xu1, yu1 ;> + ixu2 * <;v,yu1;>
+ iyu2 * <; xu1, v ;> + (ixu2 * iyu2) * <; v, v ;> by ThSc3;
B14: <; xu1, yu1 ;> in INT by A0,A5,B8,A10,A11;
<; yu1, v ;> in INT by A11,A6X,ThIntLat1B;
then B15: <; v, yu1 ;> in INT by defZLattice;
B16: <; xu1, v ;> in INT by A10,A6X,ThIntLat1B;
<; v, v ;> in INT by A3,A1;
hence <; x, y ;> in INT by B13,B14,B15,B16,INT_1:def 2;
end;
end;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
let I being Basis of L;
assume
X2: for v, u being Vector of L st v in I & u in I holds
<; v, u ;> in INT;
X3: I is linearly-independent &
Lin (I) = the ModuleStr of L by VECTSP_7:def 3;
X4: card (I) is Nat;
let v, u be Vector of L;
v in Lin(I) & u in Lin(I) by X3;
hence <; v, u ;> in INT by X1,X2,X4;
end;
theorem
for L being Z_Lattice, 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:
for v being Vector of IT st v <> 0.IT holds ||. v .|| > 0;
end;
registration
cluster non trivial INTegral positive-definite for Z_Lattice;
correctness
proof
set V = the non trivial torsion-free Z_Module;
set v = the non zero Vector of V;
set Z = Lin{v};
defpred P[object, object] means
ex a, b being Element of INT.Ring st $1 = [a*v, b*v] & $2 = a*b;
A1: for x being Element of [:the carrier of Z, the carrier of Z:]
ex y being Element of the carrier of F_Real st P[x, y]
proof
let x be Element of [:the carrier of Z, the carrier of Z:];
consider x1, x2 be object such that
B1: x1 in the carrier of Z & x2 in the carrier of Z & x = [x1, x2]
by ZFMISC_1:def 2;
reconsider x1, x2 as Vector of Z by B1;
x1 in Lin{v};
then consider i1 be Element of INT.Ring such that
B2: x1 = i1*v by ZMODUL06:19;
x2 in Lin{v};
then consider i2 be Element of INT.Ring such that
B3: x2 = i2*v by ZMODUL06:19;
reconsider i12 = i1*i2 as Element of INT;
INT c= the carrier of F_Real by NUMBERS:5,XBOOLE_0:def 8;
then reconsider i12 as Element of F_Real;
take i12;
thus thesis by B1,B2,B3;
end;
consider f be Function of [:the carrier of Z, the carrier of Z:],
the carrier of F_Real such that
A2: for x being Element of [:the carrier of Z, the carrier of Z:]
holds P[x, f.x] from FUNCT_2:sch 3(A1);
A3: for a, b being Element of INT.Ring holds f.[a*v, b*v] = a*b
proof
let a, b be Element of INT.Ring;
a*v in Lin{v} & b*v in Lin{v} by ZMODUL06:21;
then [a*v, b*v] in [:the carrier of Z, the carrier of Z:] by ZFMISC_1:87;
then consider a0, b0 be Element of INT.Ring such that
B1: [a*v, b*v] = [a0*v, b0*v] & f.[a*v, b*v] = a0*b0 by A2;
B2: v <> 0.V;
a*v = a0*v by B1,XTUPLE_0:1;
then B3: a = a0 by B2,ZMODUL01:11;
b*v = b0*v by B1,XTUPLE_0:1;
hence thesis by B1,B2,B3,ZMODUL01:11;
end;
set L = GenLat (Z,f);
reconsider L as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring;
L is Z_Lattice-like
proof
thus for x being Vector of L st for y being Vector of L holds
<; x, y ;> = 0
holds x = 0.L
proof
let x be Vector of L such that
C1: for y being Vector of L holds <; x, y ;> = 0;
assume x <> 0.L;
then C2: x <> 0.V by ZMODUL01:26;
x in Lin{v};
then consider ix be Element of INT.Ring such that
C3: x = ix * v by ZMODUL06:19;
C4: ix <> 0 by C2,C3,ZMODUL01:1;
<; x, x ;> = ix * ix by A3,C3;
hence contradiction by C1,C4;
end;
thus for x, y being Vector of L holds <; x, y ;> = <; y, x ;>
proof
let x, y be Vector of L;
C1: x in Lin{v} & y in Lin{v};
then consider ix be Element of INT.Ring such that
C2: x = ix * v by ZMODUL06:19;
consider iy be Element of INT.Ring such that
C3: y = iy * v by C1,ZMODUL06:19;
thus <; x, y ;> = ix * iy by A3,C2,C3
.= <; y, x ;> by A3,C2,C3;
end;
thus for x, y, z being Vector of L, a being Element of INT.Ring
holds <; x+y, z ;> = <; x, z ;> + <; y, z ;> &
<; a*x, y ;> = a * <; x, y ;>
proof
let x, y, z be Vector of L, a be Element of INT.Ring;
C1: x in Lin{v} & y in Lin{v} & z in Lin{v};
then consider ix be Element of INT.Ring such that
C2: x = ix * v by ZMODUL06:19;
consider iy be Element of INT.Ring such that
C3: y = iy * v by C1,ZMODUL06:19;
consider iz be Element of INT.Ring such that
C4: z = iz * v by C1,ZMODUL06:19;
ix * v in Lin{v} by ZMODUL06:21;
then reconsider iixv = ix * v as Vector of Z;
reconsider ixv = ix * v as Vector of V;
iy * v in Lin{v} by ZMODUL06:21;
then reconsider iiyv = iy * v as Vector of Z;
reconsider iyv = iy * v as Vector of V;
C5: x + y = iixv + iiyv by C2,C3
.= ixv + iyv by ZMODUL01:28
.= (ix + iy) * v by VECTSP_1:def 15;
C6: a*x = a*iixv by C2
.= a*ixv by ZMODUL01:29
.= (a*ix) * v by VECTSP_1:def 16;
thus <; x+y, z ;> = (ix + iy)*iz by A3,C4,C5
.= ix*iz + iy*iz
.= f.[x, z] + iy*iz by A3,C2,C4
.= <; x, z ;> + <; y, z ;> by A3,C3,C4;
thus <; a*x, y ;> = (a*ix)*iy by A3,C3,C6
.= a*(ix*iy)
.= a * <; x, y ;> by A3,C2,C3;
end;
end;
then reconsider L as Z_Lattice;
A4: for u being Vector of L st u <> 0.L holds ||. u .|| > 0
proof
let u be Vector of L such that
B1: u <> 0.L;
B2: u <> 0.V by B1,ZMODUL01:26;
u in Lin{v};
then consider iu be Element of INT.Ring such that
B4: u = iu * v by ZMODUL06:19;
B5: iu <> 0 by B2,B4,ZMODUL01:1;
||. u .|| = iu * iu by A3,B4;
hence thesis by B5,XREAL_1:63;
end;
take L;
A5: L is non trivial
proof
assume B1: L is trivial;
v in Lin{v} by ZMODUL06:20;
then B2: v = 0.L by B1;
v <> 0.V;
hence contradiction by B2,ZMODUL01:26;
end;
for w, u being Vector of L holds <; w, u ;> in INT
proof
let w, u be Vector of L;
w in Lin{v};
then consider iw be Element of INT.Ring such that
B1: w = iw * v by ZMODUL06:19;
u in Lin{v};
then consider iu be Element of INT.Ring such that
B2: u = iu * v by ZMODUL06:19;
<; w, u ;> = iw * iu by A3,B1,B2;
hence thesis;
end;
hence thesis by A4,A5;
end;
end;
theorem
for L being positive-definite Z_Lattice, v being Vector of L holds
||. v .|| = 0 iff v = 0.L by ThSc6,defPositive;
theorem
for L being positive-definite Z_Lattice, v being Vector of L holds
||. v .|| >= 0
proof
let L be positive-definite Z_Lattice, v be Vector of L;
per cases;
suppose v = 0.L;
hence thesis by ThSc6;
end;
suppose v <> 0.L;
hence thesis by defPositive;
end;
end;
definition
let IT be INTegral Z_Lattice;
attr IT is even means
for v being Vector of IT holds ||. v .|| is even;
end;
registration
cluster even for INTegral Z_Lattice;
correctness
proof
set V0 = the finite-rank free Z_Module;
reconsider nilfunc = [: the carrier of (0).V0,
the carrier of (0).V0 :] --> 0
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :],
the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat ((0).V0,nilfunc);
reconsider X0 as finite-rank free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
reconsider X0 as Z_Lattice by ThTrivialLat1;
X0 is INTegral by INT_1:def 2;
then reconsider X0 as INTegral Z_Lattice;
take X0;
thus thesis by FUNCOP_1:7;
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
<; v, u ;> = 0;
symmetry by defZLattice;
end;
theorem
for L being Z_Lattice, v, u being Vector of L holds
v, u are_orthogonal implies v, -u are_orthogonal & -v, u are_orthogonal &
-v, -u are_orthogonal
proof
let L be Z_Lattice, v, u be Vector of L;
assume A1: v, u are_orthogonal;
<; v, -u ;> = - <; v, u ;> by ThSc1
.= 0 by A1;
hence v, -u are_orthogonal;
A2: <; -v, u ;> = - <; v, u ;> by ThSc1
.= 0 by A1;
hence -v, u are_orthogonal;
<; -v, -u ;> = - <; -v, u ;> by ThSc1
.= 0 by A2;
hence -v, -u are_orthogonal;
end;
theorem
for L being Z_Lattice, v, u being Vector of L holds
v, u are_orthogonal implies ||. v + u .|| = ||. v .|| + ||. u .||
proof
let L be Z_Lattice, v, u be Vector of L;
assume A1: v, u are_orthogonal;
thus ||. v + u .|| = <; v, v+u ;> + <; u, v+u ;> by defZLattice
.= <; v, v ;> + <; v, u ;> + <; u, v+u ;> by ThSc2
.= <; v, v ;> + 0 + (<; u, v ;> + <; u, u ;>) by A1,ThSc2
.= <; v, v ;> + (0 + <; u, u ;>) by A1,defZLattice
.= ||. v .|| + ||. u .||;
end;
theorem
for L being Z_Lattice, v, u being Vector of L holds
v, u are_orthogonal implies ||. v - u .|| = ||. v .|| + ||. u .||
proof
let L be Z_Lattice, v, u be Vector of L;
assume A1: v, u are_orthogonal;
thus ||. v - u .|| = <; v, v-u ;> - <; u, v-u ;> by ThSc5
.= <; v, v ;> - <; v, u ;> - <; u, v-u ;> by ThSc5
.= <; v, v ;> - 0 - (<; u, v ;> - <; u, u ;>) by A1,ThSc5
.= <; v, v ;> - (0 - <; u, u ;>) by A1,defZLattice
.= ||. v .|| + ||. u .||;
end;
:: Sublattice
definition
let L be Z_Lattice;
mode Z_Sublattice of L -> Z_Lattice means
:defSublattice:
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
proof
take L;
thus thesis;
end;
end;
theorem ThSL1:
for L being Z_Lattice, L1 being Z_Sublattice of L holds
L1 is Submodule of L
proof
let L be Z_Lattice, L1 be Z_Sublattice of L;
A1: the carrier of L1 c= the carrier of L by defSublattice;
A2: the addF of L1 = (the addF of L) || the carrier of L1 by defSublattice;
A3: 0.L1 = 0.L by defSublattice;
the lmult of L1 = (the lmult of L) |
[:the carrier of INT.Ring, the carrier of L1:] by defSublattice;
hence thesis by A1,A2,A3,VECTSP_4:def 2;
end;
theorem
for x being object, L being Z_Lattice, L1, L2 being Z_Sublattice of L holds
x in L1 & L1 is Z_Sublattice of L2 implies x in L2
proof
let x be object, L be Z_Lattice, L1, L2 be Z_Sublattice of L;
assume AS: x in L1 & L1 is Z_Sublattice of L2;
then A1: L1 is Submodule of L2 by ThSL1;
L1 is Submodule of L & L2 is Submodule of L by ThSL1;
hence thesis by AS,A1,ZMODUL01:23;
end;
theorem
for x being object, L being Z_Lattice, L1 being Z_Sublattice of L holds
x in L1 implies x in L
proof
let x be object, L be Z_Lattice, L1 be Z_Sublattice of L;
A1: L1 is Submodule of L by ThSL1;
assume x in L1;
hence thesis by A1,ZMODUL01:24;
end;
theorem ThSL4:
for L being Z_Lattice, L1 being Z_Sublattice of L, w being Vector of L1 holds
w is Vector of L
proof
let L be Z_Lattice, L1 be Z_Sublattice of L, w be Vector of L1;
L1 is Submodule of L by ThSL1;
hence thesis by ZMODUL01:25;
end;
theorem
for L being Z_Lattice, L1, L2 being Z_Sublattice of L holds
0.L1 = 0.L2
proof
let L be Z_Lattice, L1, L2 be Z_Sublattice of L;
thus 0.L1 = 0.L by defSublattice
.= 0.L2 by defSublattice;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L,
v1, v2 being Vector of L, w1, w2 being Vector of L1 holds
w1 = v1 & w2 = v2 implies w1 + w2 = v1 + v2
proof
let L be Z_Lattice, L1 be Z_Sublattice of L,
v1, v2 be Vector of L, w1, w2 be Vector of L1;
assume AS: w1 = v1 & w2 = v2;
L1 is Submodule of L by ThSL1;
hence thesis by AS,ZMODUL01:28;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L,
v being Vector of L, w being Vector of L1, a being Element of INT.Ring holds
w = v implies a * w = a * v
proof
let L be Z_Lattice, L1 be Z_Sublattice of L,
v be Vector of L, w be Vector of L1, a be Element of INT.Ring;
assume AS: w = v;
L1 is Submodule of L by ThSL1;
hence thesis by AS,ZMODUL01:29;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L,
v being Vector of L, w being Vector of L1 holds
w = v implies -w = -v
proof
let L be Z_Lattice, L1 be Z_Sublattice of L,
v be Vector of L, w be Vector of L1;
assume AS: w = v;
L1 is Submodule of L by ThSL1;
hence thesis by AS,ZMODUL01:30;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L,
v1, v2 being Vector of L, w1, w2 being Vector of L1 holds
w1 = v1 & w2 = v2 implies w1 - w2 = v1 - v2
proof
let L be Z_Lattice, L1 be Z_Sublattice of L,
v1, v2 be Vector of L, w1, w2 be Vector of L1;
assume AS: w1 = v1 & w2 = v2;
L1 is Submodule of L by ThSL1;
hence thesis by AS,ZMODUL01:31;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L holds
0.L in L1
proof
let L be Z_Lattice, L1 be Z_Sublattice of L;
L1 is Submodule of L by ThSL1;
hence thesis by ZMODUL01:33;
end;
theorem
for L being Z_Lattice, L1, L2 being Z_Sublattice of L holds
0.L1 in L2
proof
let L be Z_Lattice, L1, L2 be Z_Sublattice of L;
L1 is Submodule of L & L2 is Submodule of L by ThSL1;
hence thesis by ZMODUL01:34;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L holds
0.L1 in L
proof
let L be Z_Lattice, L1 be Z_Sublattice of L;
L1 is Submodule of L by ThSL1;
hence thesis by ZMODUL01:35;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L,
v1, v2 being Vector of L holds
v1 in L1 & v2 in L1 implies v1 + v2 in L1
proof
let L be Z_Lattice, L1 be Z_Sublattice of L,
v1, v2 be Vector of L;
assume AS: v1 in L1 & v2 in L1;
L1 is Submodule of L by ThSL1;
hence thesis by AS,ZMODUL01:36;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L,
v being Vector of L, a being Element of INT.Ring holds
v in L1 implies a * v in L1
proof
let L be Z_Lattice, L1 be Z_Sublattice of L,
v be Vector of L, a be Element of INT.Ring;
assume AS: v in L1;
L1 is Submodule of L by ThSL1;
hence thesis by AS,ZMODUL01:37;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L,
v being Vector of L holds
v in L1 implies -v in L1
proof
let L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L;
assume AS: v in L1;
L1 is Submodule of L by ThSL1;
hence thesis by AS,ZMODUL01:38;
end;
theorem
for L being Z_Lattice, L1 being Z_Sublattice of L,
v1, v2 being Vector of L holds
v1 in L1 & v2 in L1 implies v1 - v2 in L1
proof
let L be Z_Lattice, L1 be Z_Sublattice of L, v1, v2 be Vector of L;
assume AS: v1 in L1 & v2 in L1;
L1 is Submodule of L by ThSL1;
hence thesis by AS,ZMODUL01:39;
end;
theorem
for L being positive-definite Z_Lattice, A being non empty set,
ze being Element of A,
ad being BinOp of A, mu being Function of [:the carrier of INT.Ring, A:],A,
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
let L be positive-definite Z_Lattice, A be non empty set,
ze be Element of A,
ad be BinOp of A, mu be Function of [:the carrier of INT.Ring, A:],A,
sc be Function of [:A, A:],the carrier of F_Real such that
A1: 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;
set L1 = LatticeStr (# A, ad, ze, mu, sc #);
set V1 = ModuleStr (# A, ad, ze, mu #);
reconsider V1 as Submodule of L by A1,ZMODUL01:40;
AY3: A = the carrier of V1 & ze = 0.V1 & ad = the addF of V1 &
mu = the lmult of V1;
reconsider scc = sc
as Function of [:the carrier of V1, the carrier of V1:],
the carrier of F_Real;
AA: L1 = GenLat (V1,scc);
then A3: L1 is Submodule of V1 by LmZMtoZL1;
reconsider L1 as Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring by AA;
reconsider L1 as free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty LatticeStr over INT.Ring by AA;
AX3: L1 is Submodule of L by A3,ZMODUL01:42;
L1 is Z_Lattice-like
proof
thus for x being Vector of L1
st for y being Vector of L1 holds <; x, y ;> = 0 holds x = 0.L1
proof
let x be Vector of L1 such that
B1: for y being Vector of L1 holds <; x, y ;> = 0;
reconsider xx = x as Vector of L by AY3,ZMODUL01:25;
assume x <> 0.L1;
then ||. xx .|| <> 0 by A1,defPositive;
then <; x, x ;> <> 0 by A1,FUNCT_1:49;
hence contradiction by B1;
end;
thus for x, y being Vector of L1 holds <; x, y ;> = <; y, x ;>
proof
let x, y be Vector of L1;
reconsider xx = x, yy = y as Vector of L by AY3,ZMODUL01:25;
thus <; x, y ;> = <; xx, yy ;> by A1,FUNCT_1:49
.= <; yy, xx ;> by defZLattice
.= <; y, x ;> by A1,FUNCT_1:49;
end;
thus for x, y, z being Vector of L1, a being Element of INT.Ring
holds <; x+y, z ;> = <; x, z ;> + <; y, z ;>
& <; a*x, y ;> = a * <; x, y ;>
proof
let x, y, z be Vector of L1, a be Element of INT.Ring;
reconsider xx = x, yy = y, zz = z as Vector of L by AY3,ZMODUL01:25;
xx + yy = x + y by AX3,ZMODUL01:28;
hence <; x + y, z ;> = <; xx + yy, zz ;> by A1,FUNCT_1:49
.= <; xx, zz ;> + <; yy, zz ;> by defZLattice
.= <; x, z ;> + <; yy, zz ;> by A1,FUNCT_1:49
.= <; x, z ;> + <; y, z ;> by A1,FUNCT_1:49;
a * xx = a * x by AX3,ZMODUL01:29;
hence <; a*x, y ;> = <; a*xx, yy ;> by A1,FUNCT_1:49
.= a * <; xx, yy ;> by defZLattice
.= a * <; x, y ;> by A1,FUNCT_1:49;
end;
end;
hence thesis by A1,defSublattice,AA;
end;
theorem ThSL18:
for L being Z_Lattice, L1 being Z_Sublattice of L,
w1, w2 being Vector of L1, v1, v2 being Vector of L
st w1 = v1 & w2 = v2 holds <; w1, w2 ;> = <; v1, v2 ;>
proof
let L be Z_Lattice, L1 be Z_Sublattice of L,
w1, w2 be Vector of L1, v1, v2 be Vector of L such that
B1: w1 = v1 & w2 = v2;
B2: [w1, w2] in [:the carrier of L1, the carrier of L1:];
thus <; w1, w2 ;> = ((the scalar of L) || the carrier of L1).(w1, w2)
by defSublattice
.= <; v1, v2 ;> by B1,B2,FUNCT_1:49;
end;
registration
let L be INTegral Z_Lattice;
cluster -> INTegral for Z_Sublattice of L;
correctness
proof
let L1 be Z_Sublattice of L;
thus for w1, w2 being Vector of L1 holds <; w1, w2 ;> in INT
proof
let w1, w2 be Vector of L1;
reconsider v1 = w1, v2 = w2 as Vector of L by ThSL4;
<; w1, w2 ;> = <; v1, v2 ;> by ThSL18;
hence thesis by defIntegral;
end;
end;
end;
registration
let L be positive-definite Z_Lattice;
cluster -> positive-definite for Z_Sublattice of L;
correctness
proof
let L1 be Z_Sublattice of L;
thus for w being Vector of L1 st w <> 0.L1 holds ||. w .|| > 0
proof
let w be Vector of L1 such that
A1: w <> 0.L1;
reconsider v = w as Vector of L by ThSL4;
v <> 0.L by A1,defSublattice;
then ||. v .|| > 0 by defPositive;
hence thesis by ThSL18;
end;
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
[:the carrier of V,the carrier of W:] --> 0.F_Real;
coherence;
end;
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:
for v being Vector of V, w being Vector of W holds
it.(v,w) = f.(v,w)+g.(v,w);
existence
proof
set K = F_Real;
set X = the carrier of V, Y = the carrier of W, Z = the carrier of F_Real;
deffunc F(Element of X, Element of Y) = f.($1,$2)+g.($1,$2);
consider ff be Function of [:X,Y:],Z such that
A1: for x being Element of X, y being Element of Y holds ff.(x,y) = F(x,y)
from BINOP_1:sch 4;
reconsider ff as FrForm of V,W;
take ff;
thus thesis by A1;
end;
uniqueness
proof
let F, G be FrForm of V, W such that
A2: for v being Vector of V, w be Vector of W holds
F.(v,w) = f.(v,w)+g.( v,w) and
A3: for v being Vector of V, w being Vector of W holds
G.(v,w) = f.(v,w)+g.( v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = f.(v,w)+g.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
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:
for v being Vector of V, w being Vector of W holds it.(v,w) = a*f.(v,w);
existence
proof
set K = F_Real;
set X = the carrier of V, Y = the carrier of W, Z = the carrier of F_Real;
deffunc F(Element of X, Element of Y) =
In(a,the carrier of F_Real) * f.($1,$2);
consider ff be Function of [:X,Y:],Z such that
A1: for x being Element of X, y being Element of Y holds ff.(x,y) = F(x,y)
from BINOP_1:sch 4;
reconsider ff as FrForm of V,W;
take ff;
thus for v being Vector of V, w being Vector of W holds
ff.(v,w) = a*f.(v,w) by A1;
end;
uniqueness
proof
let F, G be FrForm of V, W such that
A2: for v being Vector of V, w being Vector of W holds
F.(v,w) = a*f.(v,w) and
A3: for v being Vector of V, w being Vector of W holds G.(v,w) = a*f.(v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = a*f.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
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:
for v being Vector of V, w being Vector of W holds it.(v,w) = -f.(v,w);
existence
proof
set K = F_Real;
set X = the carrier of V, Y = the carrier of W, Z = the carrier of K;
deffunc F(Element of X,Element of Y) = -f.($1,$2);
consider ff be Function of [:X,Y:],Z such that
A1: for x being Element of X, y being Element of Y holds ff.(x,y) = F(x,y)
from BINOP_1:sch 4;
reconsider ff as FrForm of V,W;
take ff;
thus thesis by A1;
end;
uniqueness
proof
let F, G be FrForm of V, W such that
A2: for v being Vector of V, w being Vector of W holds
F.(v,w) = -f.(v,w) and
A3: for v being Vector of V, w being Vector of W holds G.(v,w) = -f.(v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = -f.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be FrForm of V,W;
redefine func -f equals :: redefines - (ZMODLAT1, definition)
(- 1.F_Real) *f;
compatibility
proof
let g be FrForm of V,W;
thus g = -f implies g = (- 1.F_Real) *f
proof
assume A1: g = -f;
now
let v be Vector of V, w be Vector of W;
thus g.(v,w)= -f.(v,w) by A1,Def4
.= (-1.F_Real)* f.(v,w)
.= ((- 1.F_Real) *f).(v,w) by Def3;
end;
hence thesis;
end;
assume A2: g = (- 1.F_Real) *f;
now
let v be Vector of V, w be Vector of W;
thus g.(v,w)= (-1.F_Real)* f.(v,w) by A2,Def3
.= - f.(v,w)
.= (-f).(v,w) by Def4;
end;
hence thesis;
end;
end;
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
f + -g;
correctness;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f, g be FrForm of V,W;
redefine func f - g means :: redefines - (ZMODLAT1, definition)
:Def7:
for v being Vector of V, w being Vector of W holds
it.(v,w) = f.(v,w) - g.(v,w);
compatibility
proof
let h be FrForm of V,W;
thus h = f - g implies
for v being Vector of V, w being Vector of W holds
h.(v,w) = f.(v,w) - g.(v,w)
proof
assume
A1: h = f-g;
let v be Vector of V, w be Vector of W;
thus h.(v,w) = f.(v,w) + (-g).(v,w) by A1,Def2
.= f.(v,w) -g.(v,w) by Def4;
end;
assume
A2: for v being Vector of V, w being Vector of W holds
h.(v,w) = f.(v,w) - g .(v,w);
now
let v be Vector of V, w be Vector of W;
thus h.(v,w) = f.(v,w) - g.(v,w) by A2
.= f.(v,w) + (-g).(v,w) by Def4
.= (f-g).(v,w) by Def2;
end;
hence thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f, g be FrForm of V,W;
redefine func f+g; :: redefines + (ZMODLAT1, definition)
commutativity
proof
let f, g be FrForm of V,W;
now
let v be Vector of V,w be Vector of W;
thus (f+g).(v,w) = f.(v,w) + g.(v,w) by Def2
.= (g+f).(v,w) by Def2;
end;
hence f+g=g+f;
end;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W
holds f + NulFrForm(V,W) = f
proof
let V, W be non empty ModuleStr over INT.Ring, f be FrForm of V,W;
set g = NulFrForm(V,W);
now
let v be Vector of V, w be Vector of W;
thus (f+g).(v,w) = f.(v,w) + g.(v,w) by Def2
.= f.(v,w) + 0.INT.Ring by FUNCOP_1:70
.= f.(v,w);
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f, g, h being FrForm of V,W
holds f+g+h = f+(g+h)
proof
let V, W be non empty ModuleStr over INT.Ring, f, g, h be FrForm of V,W;
now
let v be Vector of V, w be Vector of W;
thus (f+g+h).(v,w) = (f+g).(v,w) + h.(v,w) by Def2
.= f.(v,w) + g.(v,w)+ h.(v,w) by Def2
.= f.(v,w) + (g.(v,w)+ h.(v,w))
.= f.(v,w) + (g+h).(v,w) by Def2
.= (f+ (g+h)).(v,w) by Def2;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W
holds f - f = NulFrForm(V,W)
proof
let V, W be non empty ModuleStr over INT.Ring, f be FrForm of V,W;
now
let v be Vector of V, w be Vector of W;
thus (f-f).(v,w) = f.(v,w) - f.(v,w) by Def7
.= (NulFrForm(V,W)).(v,w) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, a being Element of F_Real,
f, g being FrForm of V,W holds
a*(f+g) = a*f+a*g
proof
let V, W be non empty ModuleStr over INT.Ring,
r be Element of F_Real, f,g be FrForm of V,W;
now
let v be Vector of V, w be Vector of W;
thus (r*(f+g)).(v,w) = r * (f+g).(v,w) by Def3
.= r*(f.(v,w) + g.(v,w)) by Def2
.= r*f.(v,w) + r*g.(v,w)
.= (r*f).(v,w) + r*g.(v,w) by Def3
.= (r*f).(v,w) + (r*g).(v,w) by Def3
.= (r*f + r*g).(v,w) by Def2;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring,
a, b being Element of F_Real, f being FrForm of V,W holds
(a+b)*f = a*f+b*f
proof
let V, W be non empty ModuleStr over INT.Ring,
r, s be Element of F_Real, f be FrForm of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((r+s)*f).(v,w) = (r+s) * f.(v,w) by Def3
.= r*f.(v,w) + s*f.(v,w)
.= (r*f).(v,w) + s*f.(v,w) by Def3
.= (r*f).(v,w) + (s*f).(v,w) by Def3
.= (r*f + s*f).(v,w) by Def2;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring,
a, b being Element of F_Real, f being FrForm of V,W holds
(a*b)*f = a*(b*f)
proof
let V, W be non empty ModuleStr over INT.Ring,
r, s be Element of F_Real, f be FrForm of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((r*s)*f).(v,w) = (r*s) * f.(v,w) by Def3
.= r*(s*f.(v,w))
.= r*(s*f).(v,w) by Def3
.= (r*(s*f)).(v,w) by Def3;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W
holds (1.F_Real)*f = f
proof
let V, W be non empty ModuleStr over INT.Ring, f be FrForm of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((1.F_Real)*f).(v,w) = (1.F_Real) * f.(v,w) by Def3
.= f.(v,w);
end;
hence thesis;
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:
for x being Element of V holds it.x = f.x + g.x;
existence
proof
deffunc G(Element of V) = f.$1 + g.$1;
consider F be Function of the carrier of V,the carrier of F_Real such that
A1: for x being Element of V holds F.x = G(x) from FUNCT_2:sch 4;
reconsider F as FrFunctional of V;
take F;
thus thesis by A1;
end;
uniqueness
proof
let a, b be FrFunctional of V such that
A2: for x being Element of V holds a.x = f.x + g.x and
A3: for x being Element of V holds b.x = f.x + g.x;
now
let x be Element of V;
thus a.x = f.x + g.x by A2
.= b.x by A3;
end;
hence a = b by FUNCT_2:63;
end;
end;
definition
let V be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V;
func -f -> FrFunctional of V means
:HDef4:
for x being Element of V holds it.x = - (f.x);
existence
proof
deffunc G(Element of V) = -(f.$1);
consider F be Function of the carrier of V,the carrier of F_Real such that
A1: for x being Element of V holds F.x = G(x) from FUNCT_2:sch 4;
reconsider F as FrFunctional of V;
take F;
thus thesis by A1;
end;
uniqueness
proof
let a, b be FrFunctional of V such that
A2: for x being Element of V holds a.x = -(f.x) and
A3: for x being Element of V holds b.x = -(f.x);
now
let x be Element of V;
thus a.x = -(f.x) by A2
.= b.x by A3;
end;
hence a = b by FUNCT_2:63;
end;
end;
definition
let V be non empty ModuleStr over INT.Ring;
let f, g be FrFunctional of V;
func f-g -> FrFunctional of V equals
f+-g;
coherence;
end;
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:
for x being Element of V holds it.x = v*(f.x);
existence
proof
deffunc G(Element of V) = v *(f.$1);
consider F be Function of the carrier of V,the carrier of F_Real such that
A1: for x being Element of V holds F.x = G(x) from FUNCT_2:sch 4;
reconsider F as FrFunctional of V;
take F;
thus thesis by A1;
end;
uniqueness
proof
let a, b be FrFunctional of V such that
A2: for x being Element of V holds a.x = v*(f.x) and
A3: for x being Element of V holds b.x = v*(f.x);
now
let x be Element of V;
thus a.x = v*(f.x) by A2
.= b.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let V be ModuleStr over INT.Ring;
func 0FrFunctional(V) -> FrFunctional of V equals
[#]V --> 0.F_Real;
coherence;
end;
definition
let V be non empty ModuleStr over INT.Ring;
let F be FrFunctional of V;
attr F is homogeneous means
:HDef8:
for x being Vector of V, r being Scalar of V holds F.(r*x) = r*F.x;
end;
definition
let V be non empty ModuleStr over INT.Ring;
let F be FrFunctional of V;
attr F is 0-preserving means
F.(0.V) = 0.F_Real;
end;
registration
let V be Z_Module;
cluster homogeneous -> 0-preserving for FrFunctional of V;
coherence
proof
let F be FrFunctional of V;
assume
A1: F is homogeneous;
thus F.(0.V) = F.(0.INT.Ring * 0.V) by ZMODUL01:1
.= 0.INT.Ring * F.(0.V) by A1
.= 0.F_Real;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster 0FrFunctional(V) -> additive;
coherence
proof
let x,y be Vector of V;
A1: (0FrFunctional(V)).x = 0.F_Real
& (0FrFunctional(V)).y = 0.F_Real by FUNCOP_1:7;
thus (0FrFunctional(V)).(x+y)
= (0FrFunctional(V)).x + (0FrFunctional(V)).y by A1,FUNCOP_1:7;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster 0FrFunctional(V) -> homogeneous;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
A1: (0FrFunctional(V)).x = 0.F_Real by FUNCOP_1:7;
thus (0FrFunctional(V)).(r*x)
= r*(0FrFunctional(V)).x by A1,FUNCOP_1:7;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster 0FrFunctional(V) -> 0-preserving;
coherence by FUNCOP_1:7;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster additive homogeneous
0-preserving for FrFunctional of V;
existence
proof
take 0FrFunctional(V);
thus thesis;
end;
end;
theorem
for V be non empty ModuleStr over INT.Ring, f, g be FrFunctional of V holds
f+g = g+f
proof
let V be non empty ModuleStr over INT.Ring;
let f, g be FrFunctional of V;
now
let x be Element of V;
thus (f+g).x = f.x + g.x by HDef3
.= (g+f).x by HDef3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V being non empty ModuleStr over INT.Ring,
f, g, h being FrFunctional of V holds f+g+h = f+(g+h)
proof
let V be non empty ModuleStr over INT.Ring;
let f, g, h be FrFunctional of V;
now
let x be Element of V;
thus (f+g+h).x = (f+g).x + h.x by HDef3
.= f.x + g.x + h.x by HDef3
.= f.x + (g.x + h.x)
.= f.x + ((g+h).x) by HDef3
.= (f+(g+h)).x by HDef3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V being non empty ModuleStr over INT.Ring,
x being Element of V holds (0FrFunctional(V)).x = 0.F_Real by FUNCOP_1:7;
theorem
for V being non empty ModuleStr over INT.Ring, f being FrFunctional of V
holds f + 0FrFunctional(V) = f
proof
let V be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V;
now
let x be Element of V;
thus (f+0FrFunctional(V)).x = f.x+(0FrFunctional(V)).x by HDef3
.= f.x+0.F_Real by FUNCOP_1:7
.= f.x;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V being non empty ModuleStr over INT.Ring, f being FrFunctional of V
holds f-f = 0FrFunctional(V)
proof
let V be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V;
now
let x be Element of V;
thus (f-f).x = f.x+(-f).x by HDef3
.= f.x+-f.x by HDef4
.= (0FrFunctional(V)).x by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V being non empty ModuleStr over INT.Ring, r being Element of F_Real,
f, g being FrFunctional of V holds r*(f+g) = r*f+r*g
proof
let V be non empty ModuleStr over INT.Ring;
let r be Element of F_Real;
let f, g be FrFunctional of V;
now
let x be Element of V;
thus (r*(f+g)).x = r*(f+g).x by HDef6
.= r*(f.x+g.x) by HDef3
.= r*f.x+r*g.x
.= (r*f).x+r*g.x by HDef6
.= (r*f).x+(r*g).x by HDef6
.= (r*f+r*g).x by HDef3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V being non empty ModuleStr over INT.Ring, r, s being Element of F_Real,
f being FrFunctional of V holds (r+s)*f = r*f+s*f
proof
let V be non empty ModuleStr over INT.Ring;
let r, s be Element of F_Real;
let f be FrFunctional of V;
now
let x be Element of V;
thus ((r+s)*f).x = (r+s)*f.x by HDef6
.= r*f.x+s*f.x
.= (r*f).x+s*f.x by HDef6
.= (r*f).x+(s*f).x by HDef6
.= (r*f+s*f).x by HDef3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V being non empty ModuleStr over INT.Ring, r, s being Element of F_Real,
f being FrFunctional of V holds (r*s)*f = r*(s*f)
proof
let V be non empty ModuleStr over INT.Ring;
let r, s be Element of F_Real;
let f be FrFunctional of V;
now
let x be Element of V;
thus ((r*s)*f).x = (r*s)*f.x by HDef6
.= r*(s*f.x)
.= r*(s*f).x by HDef6
.= (r*(s*f)).x by HDef6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V being non empty ModuleStr over INT.Ring, f being FrFunctional of V
holds (1.F_Real)*f = f
proof
let V be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V;
now
let x be Element of V;
thus ((1.F_Real)*f).x = (1.F_Real)*f.x by HDef6
.= f.x;
end;
hence thesis by FUNCT_2:63;
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
let x,y be Vector of V;
thus (f+g).(x+y) = f.(x+y)+g.(x+y) by HDef3
.= f.x+f.y+g.(x+y) by VECTSP_1:def 20
.= f.x+f.y+(g.x+g.y) by VECTSP_1:def 20
.= f.x+g.x+(f.y+g.y)
.= (f+g).x+(f.y+g.y) by HDef3
.= (f+g).x+(f+g).y by HDef3;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
let f be additive FrFunctional of V;
cluster -f -> additive;
coherence
proof
let x, y be Vector of V;
thus (-f).(x+y) = -f.(x+y) by HDef4
.= -(f.x + f.y) by VECTSP_1:def 20
.= -f.x+-f.y
.= (-f).x+-f.y by HDef4
.= (-f).x+(-f).y by HDef4;
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
let x,y be Vector of V;
thus (v*f).(x+y) = v*f.(x+y) by HDef6
.= v*(f.x + f.y) by VECTSP_1:def 20
.= v*f.x+v*f.y
.= (v*f).x+v*f.y by HDef6
.= (v*f).x+(v*f).y by HDef6;
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
proof
let x be Vector of V;
let r be Scalar of V;
thus (f+g).(r*x) = f.(r*x) + g.(r*x) by HDef3
.= r*f.x + g.(r*x) by HDef8
.= r*f.x + r*g.x by HDef8
.= r*(f.x + g.x)
.= r*(f+g).x by HDef3;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
let f be homogeneous FrFunctional of V;
cluster -f -> homogeneous;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
thus (-f).(r*x) = -f.(r*x) by HDef4
.= -r*f.x by HDef8
.= r* (-f.x)
.= r*(-f).x by HDef4;
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
proof
let x be Vector of V;
let r be Scalar of V;
thus (v*f).(r*x) = v*f.(r*x) by HDef6
.= v*(r*f.x) by HDef8
.= r*(v*f.x)
.= r*(v*f).x by HDef6;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be FrForm of V,W, v be Vector of V;
func FrFunctionalFAF(f,v) -> FrFunctional of W equals
(curry f).v;
correctness;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be FrForm of V,W, w be Vector of W;
func FrFunctionalSAF(f,w) -> FrFunctional of V equals
(curry' f).w;
correctness;
end;
theorem HTh8:
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W,
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
let V, W be non empty ModuleStr over INT.Ring;
let f be FrForm of V,W, v be Vector of V;
set F = FrFunctionalFAF(f,v);
dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
then
A1: ex g being Function st (curry f).v = g
& dom g = the carrier of W & rng g c= rng f &
for y being object st y in the carrier of W holds g.y = f.( v,y)
by FUNCT_5:29;
hence dom F = the carrier of W & rng F c= the carrier of F_Real;
let y be Vector of W;
thus thesis by A1;
end;
theorem HTh9:
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W,
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
let V, W be non empty ModuleStr over INT.Ring, f be FrForm of V,W,
w be Vector of W;
set F = FrFunctionalSAF(f,w);
dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
then
A1: ex g being Function st (curry' f).w = g
& dom g = the carrier of V & rng g c= rng f &
for y being object st y in the carrier of V holds g .y = f.(y,w)
by FUNCT_5:32;
hence dom F = the carrier of V & rng F c= the carrier of F_Real;
let v be Vector of V;
thus thesis by A1;
end;
theorem
for V being non empty ModuleStr over INT.Ring, x being Element of V
holds (0FrFunctional(V)).x = 0.F_Real by FUNCOP_1:7;
theorem HTh10:
for V, W being non empty ModuleStr over INT.Ring, v being Vector of V holds
FrFunctionalFAF(NulFrForm(V,W),v) = 0FrFunctional(W)
proof
let V, W be non empty ModuleStr over INT.Ring, v be Vector of V;
set N = NulFrForm(V,W);
now
let y be Vector of W;
thus FrFunctionalFAF(N,v).y = N.(v,y) by HTh8
.= 0.F_Real by FUNCOP_1:70
.= (0FrFunctional(W)).y by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem HTh11:
for V, W being non empty ModuleStr over INT.Ring, w being Vector of W holds
FrFunctionalSAF(NulFrForm(V,W),w) = 0FrFunctional(V)
proof
let V, W be non empty ModuleStr over INT.Ring, y be Vector of W;
set N = NulFrForm(V,W);
now
let v be Vector of V;
thus FrFunctionalSAF(N,y).v = N.(v,y) by HTh9
.= 0.INT.Ring by FUNCOP_1:70
.= (0FrFunctional(V)).v by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem HTh12:
for V, W being non empty ModuleStr over INT.Ring, f, g being FrForm of V,W,
w being Vector of W holds
FrFunctionalSAF(f+g,w) = FrFunctionalSAF(f,w) + FrFunctionalSAF(g,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f,g be FrForm of V,W,
w be Vector of W;
now
let v be Vector of V;
thus (FrFunctionalSAF(f+g,w)).v = (f+g).(v,w) by HTh9
.= f.(v,w) + g.(v,w) by Def2
.= (FrFunctionalSAF(f,w)).v + g.(v,w) by HTh9
.= (FrFunctionalSAF(f,w)).v + (FrFunctionalSAF(g,w)).v by HTh9
.= (FrFunctionalSAF(f,w) +FrFunctionalSAF(g,w)).v by HDef3;
end;
hence thesis by FUNCT_2:63;
end;
theorem HTh13:
for V, W being non empty ModuleStr over INT.Ring, f, g being FrForm of V,W,
v being Vector of V holds
FrFunctionalFAF(f+g,v) = FrFunctionalFAF(f,v) + FrFunctionalFAF(g,v)
proof
let V, W be non empty ModuleStr over INT.Ring, f,g be FrForm of V,W,
w be Vector of V;
now
let v be Vector of W;
thus (FrFunctionalFAF(f+g,w)).v = (f+g).(w,v) by HTh8
.= f.(w,v) + g.(w,v) by Def2
.= (FrFunctionalFAF(f,w)).v + g.(w,v) by HTh8
.= (FrFunctionalFAF(f,w)).v + (FrFunctionalFAF(g,w)).v by HTh8
.= (FrFunctionalFAF(f,w) + FrFunctionalFAF(g,w)).v by HDef3;
end;
hence thesis by FUNCT_2:63;
end;
theorem HTh14:
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W,
a being Element of F_Real, w being Vector of W holds
FrFunctionalSAF(a*f,w) = a*FrFunctionalSAF(f,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f be FrForm of V,W,
a be Element of F_Real, w be Vector of W;
now
let v be Vector of V;
thus (FrFunctionalSAF(a*f,w)).v = (a*f).(v,w) by HTh9
.= a*f.(v,w) by Def3
.= a*(FrFunctionalSAF(f,w)).v by HTh9
.= (a*(FrFunctionalSAF(f,w))).v by HDef6;
end;
hence thesis by FUNCT_2:63;
end;
theorem HTh15:
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W,
a being Element of F_Real, v being Vector of V holds
FrFunctionalFAF(a*f,v) = a*FrFunctionalFAF(f,v)
proof
let V, W be non empty ModuleStr over INT.Ring, f be FrForm of V,W,
a be Element of F_Real, w be Vector of V;
now
let v be Vector of W;
thus (FrFunctionalFAF(a*f,w)).v = (a*f).(w,v) by HTh8
.= a*f.(w,v) by Def3
.= a*(FrFunctionalFAF(f,w)).v by HTh8
.= (a* FrFunctionalFAF(f,w)).v by HDef6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W,
w being Vector of W holds
FrFunctionalSAF(-f,w) = -FrFunctionalSAF(f,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f be FrForm of V,W,
w be Vector of W;
now
let v be Vector of V;
thus (FrFunctionalSAF(-f,w)).v = (-f).(v,w) by HTh9
.= -f.(v,w) by Def4
.= -(FrFunctionalSAF(f,w)).v by HTh9
.= (- FrFunctionalSAF(f,w)).v by HDef4;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being FrForm of V,W,
v being Vector of V holds
FrFunctionalFAF(-f,v) = -FrFunctionalFAF(f,v)
proof
let V, W be non empty ModuleStr over INT.Ring, f be FrForm of V,W,
w be Vector of V;
now
let v be Vector of W;
thus (FrFunctionalFAF(-f,w)).v = (-f).(w,v) by HTh8
.= -f.(w,v) by Def4
.= -(FrFunctionalFAF(f,w)).v by HTh8
.= (- FrFunctionalFAF(f,w)).v by HDef4;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f, g being FrForm of V,W,
w being Vector of W holds
FrFunctionalSAF(f-g,w) = FrFunctionalSAF(f,w) - FrFunctionalSAF(g,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f, g be FrForm of V,W,
w be Vector of W;
now
let v be Vector of V;
thus (FrFunctionalSAF(f-g,w)).v = (f-g).(v,w) by HTh9
.= f.(v,w) - g.(v,w) by Def7
.= (FrFunctionalSAF(f,w)).v - g.(v,w) by HTh9
.= (FrFunctionalSAF(f,w)).v - (FrFunctionalSAF(g,w)).v by HTh9
.= (FrFunctionalSAF(f,w)).v + (-FrFunctionalSAF(g,w)).v by HDef4
.= (FrFunctionalSAF(f,w) -FrFunctionalSAF(g,w)).v by HDef3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f, g being FrForm of V,W,
v being Vector of V holds
FrFunctionalFAF(f-g,v) = FrFunctionalFAF(f,v) - FrFunctionalFAF(g,v)
proof
let V, W be non empty ModuleStr over INT.Ring, f, g be FrForm of V,W,
w be Vector of V;
now
let v be Vector of W;
thus (FrFunctionalFAF(f-g,w)).v = (f-g).(w,v) by HTh8
.= f.(w,v) - g.(w,v) by Def7
.= (FrFunctionalFAF(f,w)).v - g.(w,v) by HTh8
.= (FrFunctionalFAF(f,w)).v - (FrFunctionalFAF(g,w)).v by HTh8
.= (FrFunctionalFAF(f,w)).v + (-FrFunctionalFAF(g,w)).v by HDef4
.= (FrFunctionalFAF(f,w) -FrFunctionalFAF(g,w)).v by HDef3;
end;
hence thesis by FUNCT_2:63;
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:
for v being Vector of V, w being Vector of W holds it.(v,w)= f.v * g.w;
existence
proof
deffunc F(Vector of V, Vector of W) = (f.$1) * (g.$2);
set c1 = the carrier of V, c2 = the carrier of W,
k = the carrier of F_Real;
consider i be Function of [:c1,c2:],k such that
A1: for x being Element of c1, y being Element of c2 holds i.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider i as FrForm of V,W;
take i;
thus thesis by A1;
end;
uniqueness
proof
let F1, F2 be FrForm of V,W such that
A2: for v being Vector of V, y being Vector of W holds F1.(v,y)= f.v * g.y
and
A3: for v being Vector of V, y being Vector of W holds F2.(v,y)= f.v * g.y;
now
let v be Vector of V, y be Vector of W;
thus F1.(v,y) = f.v * g.y by A2
.= F2.(v,y) by A3;
end;
hence thesis;
end;
end;
theorem HTh20:
for V, W being non empty ModuleStr over INT.Ring, f being FrFunctional of V,
v being Vector of V, w being Vector of W holds
FrFormFunctional(f,0FrFunctional(W)).(v,w) = 0.INT.Ring
proof
let V, W be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V, v be Vector of V, y be Vector of W;
set 0F = 0FrFunctional(W), F = FrFormFunctional(f,0F);
thus F.(v,y) = f.v * 0F.y by HDef10
.= f.v * 0.INT.Ring by FUNCOP_1:7
.= 0.INT.Ring;
end;
theorem HTh21:
for V, W being non empty ModuleStr over INT.Ring, g being FrFunctional of W,
v being Vector of V, w being Vector of W holds
FrFormFunctional(0FrFunctional(V),g).(v,w) = 0.INT.Ring
proof
let V, W be non empty ModuleStr over INT.Ring;
let h be FrFunctional of W, v be Vector of V, y be Vector of W;
set 0F = 0FrFunctional(V), F = FrFormFunctional(0F,h);
thus F.(v,y) = 0F.v * h.y by HDef10
.= 0.INT.Ring * h.y by FUNCOP_1:7
.= 0.INT.Ring;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being FrFunctional of V
holds FrFormFunctional(f,0FrFunctional(W)) = NulFrForm(V,W)
proof
let V, W be non empty ModuleStr over INT.Ring, f be FrFunctional of V;
now
let v be Vector of V, y be Vector of W;
thus FrFormFunctional(f,0FrFunctional(W)).(v,y) = 0.INT.Ring by HTh20
.= NulFrForm(V,W).(v,y) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, g being FrFunctional of W
holds FrFormFunctional(0FrFunctional(V),g) = NulFrForm(V,W)
proof
let V, W be non empty ModuleStr over INT.Ring, h be FrFunctional of W;
now
let v be Vector of V, y be Vector of W;
thus FrFormFunctional(0FrFunctional(V),h).(v,y) = 0.INT.Ring by HTh21
.= NulFrForm(V,W).(v,y) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem HTh24:
for V, W being non empty ModuleStr over INT.Ring, f being FrFunctional of V,
g being FrFunctional of W, v being Vector of V holds
FrFunctionalFAF(FrFormFunctional(f,g),v) = f.v * g
proof
let V, W be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V, h be FrFunctional of W, v be Vector of V;
set F = FrFormFunctional(f,h), FF = FrFunctionalFAF(F,v);
now
let y be Vector of W;
thus FF.y = F.(v,y) by HTh8
.= f.v * h.y by HDef10
.= (f.v * h).y by HDef6;
end;
hence thesis by FUNCT_2:63;
end;
theorem HTh25:
for V, W being non empty ModuleStr over INT.Ring, f being FrFunctional of V,
g being FrFunctional of W, w being Vector of W holds
FrFunctionalSAF(FrFormFunctional(f,g),w) = g.w * f
proof
let V, W be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V,h be FrFunctional of W, y be Vector of W;
set F = FrFormFunctional(f,h), FF = FrFunctionalSAF(F,y);
now
let v be Vector of V;
thus FF.v = F.(v,y) by HTh9
.= f.v * h.y by HDef10
.= (h.y * f).v by HDef6;
end;
hence thesis by FUNCT_2:63;
end;
begin :: 2. Bilinear forms over real number field $\mathbb R$, and their properties
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be FrForm of V,W;
attr f is additiveFAF means
:HDef11:
for v being Vector of V holds FrFunctionalFAF (f,v) is additive;
attr f is additiveSAF means
:HDef12:
for w being Vector of W holds FrFunctionalSAF (f,w) is additive;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be FrForm of V,W;
attr f is homogeneousFAF means
:HDef13:
for v being Vector of V holds FrFunctionalFAF(f,v) is homogeneous;
attr f is homogeneousSAF means
:HDef14:
for w being Vector of W holds FrFunctionalSAF(f,w) is homogeneous;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
cluster NulFrForm(V,W) -> additiveFAF;
coherence
proof
let v be Vector of V;
FrFunctionalFAF(NulFrForm(V,W),v)= 0FrFunctional(W) by HTh10;
hence thesis;
end;
cluster NulFrForm(V,W) -> additiveSAF;
coherence
proof
let y be Vector of W;
FrFunctionalSAF(NulFrForm(V,W),y)= 0FrFunctional(V) by HTh11;
hence thesis;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
cluster additiveFAF additiveSAF for FrForm of V,W;
existence
proof
take NulFrForm(V,W);
thus thesis;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
cluster NulFrForm(V,W) -> homogeneousFAF;
coherence
proof
let v be Vector of V;
FrFunctionalFAF(NulFrForm(V,W),v)= 0FrFunctional(W) by HTh10;
hence thesis;
end;
cluster NulFrForm(V,W) -> homogeneousSAF;
coherence
proof
let y be Vector of W;
FrFunctionalSAF(NulFrForm(V,W),y)= 0FrFunctional(V) by HTh11;
hence thesis;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF
for FrForm of V,W;
existence
proof
take NulFrForm(V,W);
thus thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
mode bilinear-FrForm of V,W is additiveSAF homogeneousSAF additiveFAF
homogeneousFAF FrForm of V,W;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveFAF FrForm of V,W, 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, 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, v be Vector of V;
cluster FrFunctionalFAF(f,v) -> homogeneous;
coherence by HDef13;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousSAF FrForm of V,W, w be Vector of W;
cluster FrFunctionalSAF(f,w) -> homogeneous;
coherence by HDef14;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V, g be additive FrFunctional of W;
cluster FrFormFunctional(f,g) -> additiveFAF;
coherence
proof
let v be Vector of V;
set fg = FrFormFunctional(f,g), F = FrFunctionalFAF(fg,v);
let y,y9 be Vector of W;
A1: F = f.v * g by HTh24;
hence F.(y+y9) = f.v * g.(y+y9) by HDef6
.= f.v *(g.y +g.y9) by VECTSP_1:def 20
.= f.v * g.y + f.v * g.y9
.= f.v * g.y + F.y9 by A1,HDef6
.= F.y + F.y9 by A1,HDef6;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additive FrFunctional of V, g be FrFunctional of W;
cluster FrFormFunctional(f,g) -> additiveSAF;
coherence
proof
let y be Vector of W;
set fg = FrFormFunctional(f,g), F = FrFunctionalSAF(fg,y);
F = g.y * f by HTh25;
hence thesis;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be FrFunctional of V, g be homogeneous FrFunctional of W;
cluster FrFormFunctional(f,g) -> homogeneousFAF;
coherence
proof
let v be Vector of V;
set fg = FrFormFunctional(f,g), F = FrFunctionalFAF(fg,v);
let y be Vector of W,r be Scalar of W;
A1: F = f.v * g by HTh24;
hence F.(r* y) = f.v * g.(r*y) by HDef6
.= f.v *(r*g.y) by HDef8
.= r*(f.v * g.y)
.= r *F.y by A1,HDef6;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneous FrFunctional of V, g be FrFunctional of W;
cluster FrFormFunctional(f,g) -> homogeneousSAF;
coherence
proof
let y be Vector of W;
set fg = FrFormFunctional(f,g);
set F = FrFunctionalSAF(fg,y);
let v be Vector of V,r be Scalar of V;
A1: F = g.y * f by HTh25;
hence F.(r* v) = g.y * f.(r*v) by HDef6
.= g.y *(r*f.v) by HDef8
.= r*(g.y * f.v)
.= r *F.v by A1,HDef6;
end;
end;
registration
let V be non trivial ModuleStr over INT.Ring, W be non empty ModuleStr
over INT.Ring;
let f be FrFunctional of V, g be FrFunctional of W;
cluster FrFormFunctional(f,g) -> non trivial;
coherence
proof
set fg = FrFormFunctional(f,g);
set w = the Vector of W;
consider v be Vector of V such that
A1: v <> 0.V by STRUCT_0:def 18;
A2: [0.V,0.W] <> [v,w] by A1,XTUPLE_0:1;
dom fg = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then
A3: [[0.V,0.W],fg.(0.V,0.W)] in fg & [[v,w],fg.(v,w)] in fg by FUNCT_1:1;
assume
A4: fg is trivial;
per cases by A4,ZFMISC_1:131;
suppose
fg = {};
hence contradiction;
end;
suppose
ex x being object st fg = {x};
then consider x be object such that
A5: fg = {x};
[[0.V,0.W],fg.(0.V,0.W)] = x & x=[[v,w],fg.(v,w)]
by A3,A5,TARSKI:def 1;
hence contradiction by A2,XTUPLE_0:1;
end;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring,
W be non trivial ModuleStr over INT.Ring;
let f be FrFunctional of V, g be FrFunctional of W;
cluster FrFormFunctional(f,g) -> non trivial;
coherence
proof
set fg = FrFormFunctional(f,g);
set v = the Vector of V;
consider w be Vector of W such that
A1: w <> 0.W by STRUCT_0:def 18;
A2: [0.V,0.W] <> [v,w] by A1,XTUPLE_0:1;
dom fg = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then
A3: [[0.V,0.W],fg.(0.V,0.W)] in fg & [[v,w],fg.(v,w)] in fg by FUNCT_1:1;
assume
A4: fg is trivial;
per cases by A4,ZFMISC_1:131;
suppose
fg = {};
hence contradiction;
end;
suppose
ex x being object st fg = {x};
then consider x be object such that
A5: fg = {x};
[[0.V,0.W],fg.(0.V,0.W)] = x & x=[[v,w],fg.(v,w)]
by A3,A5,TARSKI:def 1;
hence contradiction by A2,XTUPLE_0:1;
end;
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:
F.(0.V) = 0.F_Real;
end;
registration
let V be Z_Module;
cluster homogeneous -> 0-preserving for FrFunctional of V;
coherence
proof
let F be FrFunctional of V;
assume
A1: F is homogeneous;
thus F.(0.V) = F.(0.INT.Ring * 0.V) by VECTSP_1:14
.= 0.INT.Ring * F.(0.V) by A1
.= 0.F_Real;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster 0FrFunctional(V) -> 0-preserving;
coherence by FUNCOP_1:7;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster additive homogeneous 0-preserving for FrFunctional of V;
existence
proof
take 0FrFunctional(V);
thus thesis;
end;
end;
registration
let V be non trivial free Z_Module;
cluster additive homogeneous non constant non trivial
for FrFunctional of V;
existence
proof
set f = the additive homogeneous non constant non trivial Functional of V;
reconsider g = f as FrFunctional of V by FUNCT_2:7,NUMBERS:15;
take g;
for x, y being Vector of V holds g.(x+y) = g.x +g.y
proof
let x, y be Vector of V;
thus g.(x+y) = f.x +f.y by VECTSP_1:def 20
.= g.x +g.y;
end;
hence g is additive;
for x being Vector of V, r being Element of INT.Ring
holds g.(r*x) = r*g.x
proof
let x be Vector of V,r be Element of INT.Ring;
thus g.(r*x) = r*f.x by HAHNBAN1:def 8
.= r*g.x;
end;
hence g is homogeneous;
thus g is non constant non trivial;
end;
end;
theorem VS10Th28:
for V being non trivial free Z_Module,
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
let V be non trivial free Z_Module,
f be non constant 0-preserving FrFunctional of V;
A1: f.(0.V) = 0.F_Real by HDef9;
assume
A2: for v being Vector of V st v <> 0.V holds f.v = 0.F_Real;
now
let x, y be object;
assume x in dom f & y in dom f;
then reconsider v = x, w = y as Vector of V;
thus f.x = f.v
.= 0 by A2,A1
.= f.w by A2,A1
.= f.y;
end;
hence contradiction by FUNCT_1:def 10;
end;
registration
let V, W be non trivial free Z_Module;
let f be non constant 0-preserving FrFunctional of V,
g be non constant 0-preserving FrFunctional of W;
cluster FrFormFunctional(f,g) -> non constant;
coherence
proof
set fg = FrFormFunctional(f,g);
consider v be Vector of V such that
v <> 0.V and
A1: f.v <> 0.F_Real by VS10Th28;
consider w be Vector of W such that
w <> 0.W and
A2: g.w <> 0.F_Real by VS10Th28;
fg.(v,w) = f.v * g.w by HDef10;
then
A3: dom fg = [:the carrier of V, the carrier of W:]
& fg.(v,w) <> 0.F_Real by A1,A2,FUNCT_2:def 1;
fg.(0.V,0.W) = f.(0.V)*g.(0.W) by HDef10
.= 0.INT.Ring * g.(0.W) by HDef9
.= 0.F_Real;
hence thesis by A3,BINOP_1:19;
end;
end;
definition
let V be non empty ModuleStr over INT.Ring;
mode linear-FrFunctional of V is additive homogeneous FrFunctional of V;
end;
registration
let V, W be non trivial free Z_Module;
cluster non trivial non constant additiveFAF homogeneousFAF additiveSAF
homogeneousSAF for FrForm of V,W;
existence
proof
set f = the non constant non trivial linear-FrFunctional of V,
g = the non constant non trivial linear-FrFunctional of W;
take FrFormFunctional(f,g);
thus thesis;
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
proof
let w be Vector of W;
set Ffg = FrFunctionalSAF(f+g,w), Ff = FrFunctionalSAF(f,w);
set Fg = FrFunctionalSAF(g,w);
let v,y be Vector of V;
A1: Ff is additive;
A2: Fg is additive;
thus Ffg.(v+y) = (Ff+Fg).(v+y) by HTh12
.= Ff.(v+y) + Fg.(v+y) by HDef3
.= Ff.v+Ff.y + Fg.(v+y) by A1
.= Ff.v+Ff.y + (Fg.v+Fg.y) by A2
.= Ff.v+Fg.v + Ff.y+Fg.y
.= (Ff+Fg).v + Ff.y+Fg.y by HDef3
.= (Ff+Fg).v + (Ff.y+Fg.y)
.= (Ff+Fg).v + (Ff+Fg).y by HDef3
.= Ffg.v + (Ff+Fg).y by HTh12
.= Ffg.v + Ffg.y by HTh12;
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
proof
let w be Vector of V;
set Ffg = FrFunctionalFAF(f+g,w), Ff = FrFunctionalFAF(f,w);
set Fg = FrFunctionalFAF(g,w);
let v, y be Vector of W;
A1: Ff is additive;
A2: Fg is additive;
thus Ffg.(v+y) = (Ff+Fg).(v+y) by HTh13
.= Ff.(v+y) + Fg.(v+y) by HDef3
.= Ff.v+Ff.y + Fg.(v+y) by A1
.= Ff.v+Ff.y + (Fg.v+Fg.y) by A2
.= Ff.v+Fg.v + Ff.y+Fg.y
.= (Ff+Fg).v + Ff.y+Fg.y by HDef3
.= (Ff+Fg).v + (Ff.y+Fg.y)
.= (Ff+Fg).v + (Ff+Fg).y by HDef3
.= Ffg.v + (Ff+Fg).y by HTh13
.= Ffg.v + Ffg.y by HTh13;
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
proof
let w be Vector of W;
set Ffg = FrFunctionalSAF(a*f,w), Ff = FrFunctionalSAF(f,w);
let v, y be Vector of V;
A1: Ff is additive;
thus Ffg.(v+y) = (a*Ff).(v+y) by HTh14
.= a*Ff.(v+y) by HDef6
.= a*(Ff.v + Ff.y) by A1
.= a* Ff.v + a*Ff.y
.= (a*Ff).v +a* Ff.y by HDef6
.= (a*Ff).v + (a*Ff).y by HDef6
.= Ffg.v + (a*Ff).y by HTh14
.= Ffg.v + Ffg.y by HTh14;
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
proof
let w be Vector of V;
set Ffg = FrFunctionalFAF(a*f,w), Ff = FrFunctionalFAF(f,w);
let v, y be Vector of W;
A1: Ff is additive;
thus Ffg.(v+y) = (a*Ff).(v+y) by HTh15
.= a*Ff.(v+y) by HDef6
.= a*(Ff.v + Ff.y) by A1
.= a* Ff.v +a* Ff.y
.= (a*Ff).v +a* Ff.y by HDef6
.= (a*Ff).v + (a*Ff).y by HDef6
.= Ffg.v + (a*Ff).y by HTh15
.= Ffg.v + Ffg.y by HTh15;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveSAF FrForm of V,W;
cluster -f -> additiveSAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveFAF FrForm of V,W;
cluster -f -> additiveFAF;
correctness;
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;
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;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f, g be homogeneousSAF FrForm of V,W;
cluster f+g -> homogeneousSAF;
correctness
proof
let w be Vector of W;
set Ffg = FrFunctionalSAF(f+g,w), Ff = FrFunctionalSAF(f,w);
set Fg = FrFunctionalSAF(g,w);
let v be Vector of V, a be Scalar of V;
thus Ffg.(a*v) = (Ff+Fg).(a*v) by HTh12
.= Ff.(a*v) + Fg.(a*v) by HDef3
.= a*Ff.v + Fg.(a*v) by HDef8
.= a*Ff.v + a*Fg.v by HDef8
.= a*(Ff.v + Fg.v)
.= a*(Ff + Fg).v by HDef3
.= a* Ffg.v by HTh12;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f, g be homogeneousFAF FrForm of V,W;
cluster f+g -> homogeneousFAF;
correctness
proof
let w be Vector of V;
set Ffg = FrFunctionalFAF(f+g,w), Ff = FrFunctionalFAF(f,w);
set Fg = FrFunctionalFAF(g,w);
let v be Vector of W, a be Scalar of V;
thus Ffg.(a*v) = (Ff+Fg).(a*v) by HTh13
.= Ff.(a*v) + Fg.(a*v) by HDef3
.= a*Ff.v + Fg.(a*v) by HDef8
.= a*Ff.v + a*Fg.v by HDef8
.= a*(Ff.v + Fg.v)
.= a*(Ff + Fg).v by HDef3
.= a* Ffg.v by HTh13;
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;
cluster a*f -> homogeneousSAF;
correctness
proof
let w be Vector of W;
set Ffg = FrFunctionalSAF(a*f,w), Ff = FrFunctionalSAF(f,w);
let v be Vector of V, b be Scalar of V;
thus Ffg.(b*v) = (a*Ff).(b*v) by HTh14
.= a*Ff.(b*v) by HDef6
.= a*(b*Ff.v) by HDef8
.= b*(a*Ff.v)
.= b*(a*Ff).v by HDef6
.= b* Ffg.v by HTh14;
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;
cluster a*f -> homogeneousFAF;
correctness
proof
let w be Vector of V;
set Ffg = FrFunctionalFAF(a*f,w), Ff = FrFunctionalFAF(f,w);
let v be Vector of W, b be Scalar of V;
thus Ffg.(b*v) = (a*Ff).(b*v) by HTh15
.= a*Ff.(b*v) by HDef6
.= a*(b*Ff.v) by HDef8
.= b*(a*Ff.v)
.= b*(a*Ff).v by HDef6
.= b* Ffg.v by HTh15;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousSAF FrForm of V,W;
cluster -f -> homogeneousSAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousFAF FrForm of V,W;
cluster -f -> homogeneousFAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f, g be homogeneousSAF FrForm of V,W;
cluster f-g -> homogeneousSAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f, g be homogeneousFAF FrForm of V,W;
cluster f-g -> homogeneousFAF;
correctness;
end;
theorem HTh26:
for V, W being non empty ModuleStr over INT.Ring, v, u being Vector of V,
w being Vector of W, f being FrForm of V,W st f is additiveSAF
holds f.(v+u,w) = f.(v,w) + f.(u,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let v, w be Vector of V, y be Vector of W, f be FrForm of V,W;
set F=FrFunctionalSAF(f,y);
assume f is additiveSAF;
then
A1: F is additive;
thus f.(v+w,y) = F.(v+w) by HTh9
.= F.v+F.w by A1
.= f.(v,y) + F.w by HTh9
.= f.(v,y) + f.(w,y) by HTh9;
end;
theorem HTh27:
for V,W being non empty ModuleStr over INT.Ring, v being Vector of V,
u, w being Vector of W, f being FrForm of V,W st f is additiveFAF
holds f.(v,u+w) = f.(v,u) + f.(v,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let v be Vector of V, y,z be Vector of W, f be FrForm of V,W;
set F = FrFunctionalFAF(f,v);
assume f is additiveFAF;
then
A1: F is additive;
thus f.(v,y+z) = F.(y+z) by HTh8
.= F.y+F.z by A1
.= f.(v,y) + F.z by HTh8
.= f.(v,y) + f.(v,z) by HTh8;
end;
theorem HTh28:
for V,W being non empty ModuleStr over INT.Ring, v, u being Vector of V,
w, t being Vector of W, f being additiveSAF additiveFAF FrForm of V,W
holds f.(v+u,w+t) = f.(v,w) + f.(v,t) + (f.(u,w) + f.(u,t))
proof
let V, W be non empty ModuleStr over INT.Ring;
let v, w be Vector of V, y, z be Vector of W,
f be additiveSAF additiveFAF FrForm of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v+w,y+z) = f.(v,y+z) + f.(w,y+z) by HTh26
.= (v1 + v3) + f.(w,y+z) by HTh27
.= v1 +v3 + (v4 + v5) by HTh27;
end;
theorem HTh29:
for V, W being right_zeroed non empty ModuleStr over INT.Ring,
f being additiveFAF FrForm of V,W, v being Vector of V holds
f.(v,0.W) = 0.INT.Ring
proof
let V, W be right_zeroed non empty ModuleStr over INT.Ring;
let f be additiveFAF FrForm of V,W, v be Vector of V;
f.(v,0.W) = f.(v,0.W+0.W) by RLVECT_1:def 4
.= f.(v,0.W) + f.(v,0.W) by HTh27;
hence thesis;
end;
theorem HTh30:
for V, W being right_zeroed non empty ModuleStr over INT.Ring,
f being additiveSAF FrForm of V,W, w being Vector of W holds
f.(0.V,w) = 0.INT.Ring
proof
let V, W be right_zeroed non empty ModuleStr over INT.Ring;
let f be additiveSAF FrForm of V,W, v be Vector of W;
f.(0.V,v) = f.(0.V+0.V,v) by RLVECT_1:def 4
.= f.(0.V,v) + f.(0.V,v) by HTh26;
hence thesis;
end;
theorem HTh31:
for V, W being non empty ModuleStr over INT.Ring, v being Vector of V,
w being Vector of W, a being Element of INT.Ring, f being FrForm of V,W
st f is homogeneousSAF holds f.(a*v,w) = a*f.(v,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let v be Vector of V, y be Vector of W,
r be Element of INT.Ring, f be FrForm of V,W;
set F = FrFunctionalSAF(f,y);
assume f is homogeneousSAF;
then
A1: F is homogeneous;
thus f.(r*v,y) = F.(r*v) by HTh9
.= r*F.v by A1
.= r*f.(v,y) by HTh9;
end;
theorem HTh32:
for V, W being non empty ModuleStr over INT.Ring, v being Vector of V,
w being Vector of W, a being Element of INT.Ring, f being FrForm of V,W
st f is homogeneousFAF holds f.(v,a*w) = a*f.(v,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let v be Vector of V, y be Vector of W,
r be Element of INT.Ring, f be FrForm of V,W;
set F = FrFunctionalFAF(f,v);
assume f is homogeneousFAF;
then
A1: F is homogeneous;
thus f.(v,r*y) = F.(r*y) by HTh8
.= r*F.y by A1
.= r*f.(v,y) by HTh8;
end;
theorem
for V, W being add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring, f being homogeneousSAF FrForm of V,W,
w being Vector of W holds f.(0.V,w) = 0.F_Real
proof
let V, W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring;
let f be homogeneousSAF FrForm of V,W, v be Vector of W;
thus f.(0.V,v) = f.((0.INT.Ring)*(0.V),v) by VECTSP10:1
.= 0.INT.Ring *f.(0.V,v) by HTh31
.= 0.F_Real;
end;
theorem
for V, W being add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring, f being homogeneousFAF FrForm of V,W,
v being Vector of V holds f.(v,0.W) = 0.F_Real
proof
let V, W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring;
let f be homogeneousFAF FrForm of V,W, v be Vector of V;
thus f.(v,0.W) = f.(v,(0.INT.Ring)*(0.W)) by VECTSP10:1
.= 0.INT.Ring * f.(v,0.W) by HTh32
.= 0.F_Real;
end;
theorem HTh35:
for V, W being Z_Module, v, u being Vector of V, w being Vector of W,
f being additiveSAF homogeneousSAF FrForm of V,W holds
f.(v-u,w) = f.(v,w) - f.(u,w)
proof
let V, W be Z_Module, v,w be Vector of V, y be Vector of W;
let f be additiveSAF homogeneousSAF FrForm of V,W;
thus f.(v-w,y) = f.(v,y) +f.(-w,y) by HTh26
.= f.(v,y) +f.((-1.INT.Ring)* w,y) by VECTSP_1:14
.= f.(v,y) +(-1.INT.Ring)*f.(w,y) by HTh31
.= f.(v,y) - f.( w,y);
end;
theorem HTh36:
for V, W being Z_Module, v being Vector of V, w, t being Vector of W,
f being additiveFAF homogeneousFAF FrForm of V,W holds
f.(v,w-t) = f.(v,w) - f.(v,t)
proof
let V, W be Z_Module, v be Vector of V, y,z be Vector of W,
f be additiveFAF homogeneousFAF FrForm of V,W;
thus f.(v,y-z) = f.(v,y) + f.(v,-z) by HTh27
.= f.(v,y) + f.(v,(-1.INT.Ring)* z) by VECTSP_1:14
.= f.(v,y) + (-1.INT.Ring)*f.(v,z) by HTh32
.= f.(v,y) - f.(v,z);
end;
theorem HTh37:
for V, W being Z_Module, v, u being Vector of V, w, t being Vector of W,
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
let V, W be Z_Module;
let v, w be Vector of V, y, z be Vector of W, f be bilinear-FrForm of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v-w,y-z) = f.(v,y-z) - f.(w,y-z) by HTh35
.= v1 - v3 - f.(w,y-z) by HTh36
.= v1 - v3 - (v4 - v5) by HTh36;
end;
theorem
for V,W being add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring, v, u being Vector of V,
w, t being Vector of W, a, b being Element of INT.Ring,
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
let V, W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring,
v, w be Vector of V, y, z be Vector of W, a, b be Element of INT.Ring;
let f be bilinear-FrForm of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v+a*w,y+b*z) = v1 +f.(v,b*z) + (f.(a*w,y) +f.(a*w,b*z)) by HTh28
.= v1 +b*v3 + (f.(a*w,y) +f.(a*w,b*z)) by HTh32
.= v1 + b*v3 + (a*v4 + f.(a*w,b*z)) by HTh31
.= v1 + b*v3 + (a*v4 + a*f.(w,b*z)) by HTh31
.= v1 + b*v3 + (a*v4 + a*(b*v5)) by HTh32;
end;
theorem
for V, W being Z_Module, v, u being Vector of V, w, t being Vector of W,
a, b being Element of INT.Ring, 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
let V, W be Z_Module, v, w be Vector of V, y, z be Vector of W,
a, b be Element of INT.Ring, f be bilinear-FrForm of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v-a*w,y-b*z) = v1 -f.(v,b*z) - (f.(a*w,y) -f.(a*w,b*z)) by HTh37
.= v1 -b*v3 - (f.(a*w,y) -f.(a*w,b*z)) by HTh32
.= v1 - b*v3 - (a*v4 - f.(a*w,b*z)) by HTh31
.= v1 - b*v3 - (a*v4 - a*f.(w,b*z)) by HTh31
.= v1 - b*v3 - (a*v4 - a*(b*v5)) by HTh32;
end;
theorem
for V, W being right_zeroed non empty ModuleStr over INT.Ring,
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, w being Vector of W holds f.(v,w) = 0.INT.Ring
proof
let V, W be right_zeroed non empty ModuleStr over INT.Ring,
f be FrForm of V,W;
A1: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
assume
A2: f is additiveFAF or f is additiveSAF;
hereby
assume
A3: f is constant;
let v be Vector of V, w be Vector of W;
per cases by A2;
suppose
A4: f is additiveFAF;
thus f.(v,w) = f.(v,0.W) by A1,A3,BINOP_1:19
.= 0.INT.Ring by A4,HTh29;
end;
suppose
A5: f is additiveSAF;
thus f.(v,w) = f.(0.V,w) by A1,A3,BINOP_1:19
.= 0.INT.Ring by A5,HTh30;
end;
end;
hereby
assume
A6: for v being Vector of V, w being Vector of W holds
f.(v,w) = 0.INT.Ring;
now
let x, y be object such that
A7: x in dom f and
A8: y in dom f;
consider v be Vector of V, w be Vector of W such that
A9: x = [v,w] by A7,DOMAIN_1:1;
consider s be Vector of V, t be Vector of W such that
A10: y = [s,t] by A8,DOMAIN_1:1;
thus f.x = f.(v,w) by A9
.= 0.INT.Ring by A6
.= f.(s,t) by A6
.= f.y by A10;
end;
hence f is constant by FUNCT_1:def 10;
end;
end;
begin :: 3. Matrices of bilinear form over real number field $\mathbb R$
definition
let V1, V2 be finite-rank free Z_Module;
let b1 be OrdBasis of V1, 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:
for i, j being Nat st i in dom b1 & j in dom b2
holds it*(i,j) = f.(b1/.i, b2/.j);
existence
proof
deffunc F(Nat,Nat) = In(f.(b1/.$1, b2/.$2), the carrier of F_Real);
consider M be Matrix of len b1, len b2, F_Real such that
A20: for i, j being Nat st [i,j] in Indices M holds M*(i,j) = F(i,j)
from MATRIX_0:sch 1;
take M;
thus for i, j being Nat st i in dom b1 & j in dom b2
holds M*(i,j) = f.(b1/.i, b2/.j)
proof
let i, j be Nat;
assume A21: i in dom b1 & j in dom b2;
len b1 <> 0
proof
assume len b1 = 0;
then Seg len b1 = {};
hence contradiction by A21,FINSEQ_1:def 3;
end;
then Indices M = [:Seg len b1, Seg len b2:] by MATRIX_0:23
.= [: dom b1, Seg len b2:] by FINSEQ_1:def 3
.= [: dom b1, dom b2:] by FINSEQ_1:def 3;
then [i, j] in Indices M by A21,ZFMISC_1:87;
then M*(i,j) = F(i,j) by A20;
hence M*(i,j) = f.(b1/.i, b2/.j);
end;
end;
uniqueness
proof
let M1, M2 be Matrix of len b1, len b2, F_Real;
assume that
A22: for i, j being Nat st i in dom b1 & j in dom b2
holds M1*(i,j) = f.(b1/.i, b2/.j) and
A23: for i, j being Nat st i in dom b1 & j in dom b2
holds M2*(i,j) = f.(b1/.i, b2/.j);
now
let i, j be Nat;
assume
A25: [i,j] in Indices M1;
then len b1 <> 0 by MATRIX_0:22;
then Indices M1 = [:Seg len b1, Seg len b2:] by MATRIX_0:23
.= [: dom b1, Seg len b2:] by FINSEQ_1:def 3
.= [: dom b1, dom b2:] by FINSEQ_1:def 3;
then
A26: i in dom b1 & j in dom b2 by A25,ZFMISC_1:87;
thus M1*(i,j) = f.(b1/.i, b2/.j) by A22,A26
.= M2*(i,j) by A26,A23;
end;
hence thesis by MATRIX_0:27;
end;
end;
theorem LMThMBF1X0:
for V being finite-rank free Z_Module,
F being linear-FrFunctional of V,
y being FinSequence of V,
x being FinSequence of INT.Ring,
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
let V be finite-rank free Z_Module,
F be linear-FrFunctional of V;
defpred P[FinSequence of V] means
for x being FinSequence of INT.Ring,
X, Y being FinSequence of F_Real
st X = x & len $1 = len x & len X = len Y &
(for k being Nat st k in Seg len x holds Y.k = F.($1/.k))
holds X "*" Y = F.(Sum lmlt (x,$1));
A2: for y being FinSequence of V
for w being Element of V st P[y] holds P[y^<*w*>]
proof
let y be FinSequence of V;
let w be Element of V such that
P1: for x being FinSequence of INT.Ring,
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));
thus for x being FinSequence of INT.Ring,
X, Y being FinSequence of F_Real
st X = x & len (y^<*w*>) = len x & len X = len Y &
(for k being Nat st k in Seg len x holds Y.k = F.((y^<*w*>)/.k))
holds X "*" Y = F.(Sum lmlt (x,y^<*w*>))
proof
let x be FinSequence of INT.Ring,
X, Y be FinSequence of F_Real;
assume that
R1: X = x and
R2: len (y^<*w*>) = len x and
R3: len X = len Y and
R4: for k being Nat st k in Seg len x holds Y.k = F.((y^<*w*>)/.k);
X1: F is additive;
X2: F is homogeneous;
set n = len y;
set X0 = X | n;
set Y0 = Y | n;
set x0 = x | n;
Q0: len (y^<*w*>) = len y + len <*w*> by FINSEQ_1:22
.= n + 1 by FINSEQ_1:39;
LN4: len x0 = n by Q0,R2,FINSEQ_1:59,NAT_1:11;
LN5: len X0 = n by Q0,R1,R2,FINSEQ_1:59,NAT_1:11;
LN6: len Y0 = n by Q0,R1,R2,R3,FINSEQ_1:59,NAT_1:11;
LN7: n+1 in Seg (n+1) by FINSEQ_1:4;
Q2: len y = len x0 by Q0,R2,FINSEQ_1:59,NAT_1:11;
Q3: len X0 = len Y0 by LN5,Q0,R1,R2,R3,FINSEQ_1:59,NAT_1:11;
for k being Nat st k in Seg len x0 holds Y0.k = F.(y/.k)
proof
let k be Nat;
assume Q31: k in Seg len x0;
then
Q34: k in dom y by LN4,FINSEQ_1:def 3;
Q32: Seg len x0 c= Seg len x by FINSEQ_3:18,Q0,R2,LN4;
then k in Seg len x by Q31;
then
Q33: k in dom (y^<*w*>) by R2,FINSEQ_1:def 3;
Q35: (y^<*w*>)/.k = (y^<*w*>).k by Q33,PARTFUN1:def 6
.= y.k by FINSEQ_1:def 7,Q34
.= y/.k by Q34,PARTFUN1:def 6;
thus Y0.k = Y.k by LN4,Q31,FUNCT_1:49
.= F.(y/.k) by R4,Q31,Q32,Q35;
end;
then
Q4: X0 "*" Y0 = F.(Sum lmlt (x0,y)) by R1,Q2,Q3,P1;
Q51: n+1 in dom X by LN7,Q0,R1,R2,FINSEQ_1:def 3;
Q61: n+1 in dom Y by LN7,Q0,R1,R2,R3,FINSEQ_1:def 3;
Q71: n+1 in dom x by LN7,Q0,R2,FINSEQ_1:def 3;
Q9: X/.(n+1) = X.(n+1) by Q51,PARTFUN1:def 6
.= x/.(n+1) by R1,Q71,PARTFUN1:def 6;
Q103: n+1 in dom (y^<*w*>) by LN7,Q0,FINSEQ_1:def 3;
Q102: (y^<*w*>)/.(n+1) = (y^<*w*>).(n+1) by Q103,PARTFUN1:def 6
.= w by FINSEQ_1:42;
Y/.(n+1) = Y.(n+1) by Q61,PARTFUN1:def 6
.= F.w by Q0,Q102,R2,R4,FINSEQ_1:4;
then
Q11: X/.(n+1)* Y/.(n+1) = F.((x/.(n+1))*w) by Q9,X2;
len mlt (X,Y) = n+1 by Q0,R1,R2,R3,MATRIX_3:6;
then
Q85: dom (mlt (X,Y)) = Seg (n+1) by FINSEQ_1:def 3;
Q82: len mlt (X0,Y0) = n by LN5,LN6,MATRIX_3:6;
len ((mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *> )
= len (mlt (X0,Y0)) + len ( <* X/.(n+1)* Y/.(n+1) *> ) by FINSEQ_1:22
.= n+1 by Q82,FINSEQ_1:39;
then
DM1: dom (mlt (X,Y)) = dom ((mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *> )
by Q85,FINSEQ_1:def 3;
for k being Nat st k in dom (mlt (X,Y))
holds (mlt (X,Y)).k = ((mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *>).k
proof
let k be Nat;
assume V1: k in dom mlt (X,Y); then
V2: 1<=k & k <= n + 1 by Q85,FINSEQ_1:1;
set f=((mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *>);
per cases;
suppose k <= n; then
V3: k in Seg n by V2;
then
V4: k in dom (mlt (X0,Y0)) by Q82,FINSEQ_1:def 3;
V5: k in dom X0 by LN5,V3,FINSEQ_1:def 3;
V6: k in dom Y0 by LN6,V3,FINSEQ_1:def 3;
X0.k in rng X0 by V5,FUNCT_1:3;
then reconsider X0k = X0.k as Element of F_Real;
Y0.k in rng Y0 by V6,FUNCT_1:3;
then reconsider Y0k = Y0.k as Element of F_Real;
k in dom X by V1,Q0,Q85,R1,R2,FINSEQ_1:def 3;
then X.k in rng X by FUNCT_1:3;
then reconsider Xk = X.k as Element of F_Real;
k in dom Y by V1,Q0,Q85,R1,R2,R3,FINSEQ_1:def 3;
then Y.k in rng Y by FUNCT_1:3;
then reconsider Yk = Y.k as Element of F_Real;
f.k = (mlt (X0,Y0)).k by V4,FINSEQ_1:def 7
.= X0k*Y0k by V4,FVSUM_1:60
.= (X.k)*(Y0.k) by V5,FUNCT_1:47
.= Xk*Yk by V6,FUNCT_1:47
.= (mlt (X,Y)).k by V1,FVSUM_1:60;
hence thesis;
end;
suppose not k <= n;
then n+1 <= k by NAT_1:13;
then V8: k=n+1 by XXREAL_0:1,V2;
Seg 1 = dom (<* X/.(n+1)* Y/.(n+1) *>) by FINSEQ_1:38;
then
V10: 1 in dom (<* X/.(n+1)* Y/.(n+1) *>);
Q9: X/.(n+1) = X.(n+1) by Q51,PARTFUN1:def 6;
then reconsider Xn = X.(n+1) as Element of F_Real;
Q10: Y/.(n+1) = Y.(n+1) by Q61,PARTFUN1:def 6;
then reconsider Yn = Y.(n+1) as Element of F_Real;
f.k = (<* X/.(n+1)* Y/.(n+1) *>).1
by Q82,FINSEQ_1:def 7,V8,V10
.= X/.(n+1)* Y/.(n+1)
.= (mlt (X,Y)).k by Q9,Q10,V1,V8,FVSUM_1:60;
hence thesis;
end;
end;
then
Q8: mlt (X,Y) =(mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *>
by DM1,FINSEQ_1:13;
QX121: dom x = Seg (n+1) by Q0,R2,FINSEQ_1:def 3
.= dom (y^<*w*>) by Q0,FINSEQ_1:def 3;
then
Q121: dom (lmlt (x,y^<*w*>)) = dom x by ZMATRLIN:13;
dom x0 = Seg n by FINSEQ_1:def 3,LN4
.= dom y by FINSEQ_1:def 3;
then
dom (lmlt (x0,y)) = dom x0 by ZMATRLIN:13;
then
Q124: dom (lmlt (x0,y)) = Seg n by LN4,FINSEQ_1:def 3;
then
Q125: len lmlt (x0,y) = n by FINSEQ_1:def 3;
len ((lmlt (x0,y)) ^ <* (x/.(n+1))*w *> )
= len (lmlt (x0,y)) + len ( <* (x/.(n+1))*w *> ) by FINSEQ_1:22
.= n+1 by Q125,FINSEQ_1:39;
then dom ((lmlt (x0,y)) ^ <* (x/.(n+1))*w *> )
= Seg (n+1) by FINSEQ_1:def 3;
then
DM1: dom (lmlt (x,y^<*w*>))
= dom ((lmlt (x0,y)) ^ <* (x/.(n+1))*w *> )
by Q0,Q121,R2,FINSEQ_1:def 3;
for k being Nat st k in dom (lmlt (x,y^<*w*>)) holds
(lmlt (x,y^<*w*> )).k = ((lmlt (x0,y)) ^ <* (x/.(n+1))*w *> ).k
proof
let k be Nat;
assume V1: k in dom (lmlt (x,y^<*w*>));
then
V0: k in Seg (n+1) by Q121,Q0,R2,FINSEQ_1:def 3;
then
V2: 1<=k & k <= n + 1 by FINSEQ_1:1;
set f = (lmlt (x0,y)) ^<* (x/.(n+1))*w *>;
per cases;
suppose VX3: k <= n;
then V3: k in Seg n by V2;
V5: k in dom x0 by V3,LN4,FINSEQ_1:def 3;
V6: k in dom y by V3,FINSEQ_1:def 3;
rng x0 c= the carrier of INT.Ring by RELAT_1:def 19;
then reconsider x0k = x0.k as Element of INT.Ring by V5,FUNCT_1:3;
y.k in rng y by V6,FUNCT_1:3;
then reconsider y0k = y.k as Element of V;
XX2: k in dom x by V1,QX121,ZMATRLIN:13;
rng x c= the carrier of INT.Ring;
then reconsider xk = x.k as Element of INT.Ring by XX2,FUNCT_1:3;
k in dom (y^<*w*>) by V0,Q0,FINSEQ_1:def 3;
then (y^<*w*>).k in rng (y^<*w*>) by FUNCT_1:3;
then reconsider yk = (y^<*w*>).k as Element of V;
W: y0k = yk by V6,FINSEQ_1:def 7;
f.k = (lmlt (x0,y)).k by V3,Q124,FINSEQ_1:def 7
.= x0k*y0k by V2,VX3,Q124,FUNCOP_1:22,FINSEQ_1:1
.= (xk)*y0k by V5,FUNCT_1:47
.= (lmlt (x,y^<*w*>)).k by W,V1,FUNCOP_1:22;
hence thesis;
end;
suppose not k <= n;
then n+1 <= k by NAT_1:13;
then V8: k = n+1 by XXREAL_0:1,V2;
Seg 1 = dom (<* (x/.(n+1))*w *>) by FINSEQ_1:38;
then V10: 1 in dom (<* (x/.(n+1))*w *>);
Seg 1 = dom ( <*w*> ) by FINSEQ_1:38;
then V11: 1 in dom ( <*w*> );
Q9: x/.(n+1) = x.(n+1) by Q71,PARTFUN1:def 6;
then reconsider xn = x.(n+1) as Element of INT.Ring;
(y^<*w*>)/.(n+1) = (y^<*w*>).(n+1) by Q103,PARTFUN1:def 6;
then reconsider yn = (y^<*w*>).(n+1) as Element of V;
Q11: (y^<*w*>).(n+1) = (<*w*>).1 by V11,FINSEQ_1:def 7
.= w;
f.k = (<* (x/.(n+1))*w *>).1 by Q125,V8,V10,FINSEQ_1:def 7
.= xn*w by Q9
.= (lmlt (x,y^<*w*>)).k by Q11,V1,V8,FUNCOP_1:22;
hence thesis;
end;
end;
then
Q12: lmlt (x,y^<*w*>) = (lmlt (x0,y)) ^ <* (x/.(n+1))*w *>
by DM1,FINSEQ_1:13;
thus X "*" Y = Sum (mlt (X0,Y0)) + X/.(n+1)* Y/.(n+1) by FVSUM_1:71,Q8
.= F.(Sum lmlt (x0,y) + (x/.(n+1))*w) by Q4,Q11,X1
.= F.(Sum lmlt (x,y^<*w*>)) by FVSUM_1:71,Q12;
end;
end;
A4: P[<*>(the carrier of V)]
proof
let x be FinSequence of INT.Ring,
X, Y be FinSequence of F_Real;
assume that
R1: X = x and
R2: len (<*>(the carrier of V)) = len x and
len X = len Y and
for k being Nat st k in Seg len x
holds Y.k = F.((<*>(the carrier of V))/.k);
set y = <*>(the carrier of V);
Q2: X = <*>(the carrier of F_Real) by R1,R2;
Q4: mlt (X,Y) = <*>(the carrier of F_Real) by Q2;
reconsider I0 = 0 as Element of INT.Ring;
X1: F is additive;
X2: F.(0.V) = F.(0.V+0.V)
.= F.(0.V) + F.(0.V) by X1;
thus X "*" Y = 0.F_Real by Q4,RLVECT_1:43
.= F.(Sum lmlt (x,y)) by X2,RLVECT_1:43;
end;
for p being FinSequence of V holds P[p] from FINSEQ_2:sch 2(A4,A2);
hence thesis;
end;
theorem LMThMBF1X:
for V1, V2 being finite-rank free Z_Module,
b2 being OrdBasis of V2, b3 being OrdBasis of V2,
f being bilinear-FrForm of V1, V2,
v1 being Vector of V1,
v2 being Vector of V2,
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
let V1, V2 be finite-rank free Z_Module,
b2 be OrdBasis of V2, b3 be OrdBasis of V2,
f be bilinear-FrForm of V1, V2,
v1 be Vector of V1,
v2 be Vector of V2,
X, Y be FinSequence of F_Real;
assume that
A1: len X = len b2 and
A2: len Y = len b2 and
A3:( for k being Nat st k in Seg len b2 holds Y.k = f.(v1, b2/.k)) and
A4: X = (v2|-- b2);
set x = (v2|-- b2);
P2: for k being Nat st k in Seg len x
holds Y.k = (FrFunctionalFAF(f,v1)).(b2/.k)
proof
let k be Nat;
assume k in Seg len x;
then Y.k = f.(v1, b2/.k) by A1,A3,A4;
hence Y.k = (FrFunctionalFAF(f,v1)).(b2/.k) by HTh8;
end;
thus Y "*" X = X "*" Y by FVSUM_1:90
.= (FrFunctionalFAF(f,v1)).(Sum lmlt(v2|--b2,b2))
by LMThMBF1X0,A1,A2,A4,P2
.= f.(v1, Sum lmlt(v2|--b2,b2)) by HTh8
.= f.(v1, v2) by ZMATRLIN:30;
end;
theorem LMThMBF1Y:
for V1, V2 being finite-rank free Z_Module,
b1 being OrdBasis of V1,
f being bilinear-FrForm of V1, V2,
v1 being Vector of V1,
v2 being Vector of V2,
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
let V1, V2 be finite-rank free Z_Module,
b1 be OrdBasis of V1,
f be bilinear-FrForm of V1, V2,
v1 be Vector of V1,
v2 be Vector of V2,
X,Y be FinSequence of F_Real;
assume that
A1: len X = len b1 and
A2: len Y = len b1 and
A3: for k being Nat st k in Seg len b1 holds Y.k = f.(b1/.k, v2) and
A4: X = v1|-- b1;
set x = v1|-- b1;
P2: for k being Nat st k in Seg len x
holds Y.k = (FrFunctionalSAF(f,v2)).(b1/.k)
proof
let k be Nat;
assume k in Seg len x;
then Y.k = f.(b1/.k,v2) by A1,A3,A4;
hence Y.k = (FrFunctionalSAF(f,v2)).(b1/.k) by HTh9;
end;
thus X "*" Y = (FrFunctionalSAF(f,v2)).(Sum lmlt(v1|--b1,b1))
by LMThMBF1X0,A1,A2,A4,P2
.= f.(Sum lmlt(v1|--b1,b1),v2) by HTh9
.= f.(v1, v2) by ZMATRLIN:30;
end;
theorem INTTOREAL:
for M being Matrix of INT.Ring
holds M is Matrix of F_Real
proof
let M be Matrix of INT.Ring;
(the carrier of INT.Ring)* c= (the carrier of F_Real)*
by NUMBERS:15,FINSEQ_1:62;
then rng M c= (the carrier of F_Real)*;
hence thesis by FINSEQ_1:def 4;
end;
definition
let M be Matrix of INT.Ring;
func inttorealM(M) -> Matrix of F_Real equals
M;
correctness by INTTOREAL;
end;
definition
let n, m be Nat;
let M be Matrix of n,m,INT.Ring;
redefine func inttorealM(M) -> Matrix of n,m,F_Real; :: redefines inttorealM (ZMODLAT1, definition)
correctness
proof
B2: len M = n by MATRIX_0:25;
per cases;
suppose X11: not 0 < n;
then X1: n = 0;
M = {} by X11,MATRIX_0:25;
hence inttorealM(M) is Matrix of n,m,F_Real by X1,MATRIX_0:13;
end;
suppose X2: 0 < n;
then width M = m by B2,MATRIX_0:20;
hence inttorealM(M) is Matrix of n, m, F_Real by X2,B2,MATRIX_0:20;
end;
end;
end;
definition
let n be Nat;
let M be Matrix of n,INT.Ring;
redefine func inttorealM(M) -> Matrix of n,F_Real; :: redefines inttorealM (ZMODLAT1, definition)
correctness
proof
inttorealM(M) is Matrix of n,n,F_Real;
hence thesis;
end;
end;
theorem MLT1:
for m, l, n being Nat
for S being Matrix of l,m,INT.Ring,
T being Matrix of m,n,INT.Ring,
S1 being Matrix of l,m,F_Real,
T1 being Matrix of m,n,F_Real
st S = S1 & T = T1 & 0 < l & 0 < m
holds S*T = S1*T1
proof
let m, l, n be Nat;
let S be Matrix of l,m,INT.Ring, T be Matrix of m,n,INT.Ring,
S1 be Matrix of l,m,F_Real, T1 be Matrix of m,n,F_Real;
assume AS: S = S1 & T = T1 & 0 < l & 0 < m;
P1: len S = l & width S = m & Indices S = [:Seg l, Seg m:]
by MATRIX_0:23,AS;
Q1: len S1 = l & width S1 = m & Indices S1 = [:Seg l, Seg m:]
by MATRIX_0:23,AS;
P2: len T = m & width T = n & Indices T = [:Seg m, Seg n:]
by MATRIX_0:23,AS;
Q2: len T1 = m & width T1 = n & Indices T1 = [:Seg m, Seg n:]
by MATRIX_0:23,AS;
P3: len (S*T)=len S & width (S*T)=width T by P1,P2,MATRIX_3:def 4;
Q3: len (S1*T1)=len S1 & width (S1*T1)=width T1
by Q1,Q2,MATRIX_3:def 4;
reconsider ST = S*T as Matrix of l,n,INT.Ring
by P3,AS,P1,P2,MATRIX_0:20;
reconsider S1T1 = S1*T1 as Matrix of l,n,F_Real
by Q3,AS,Q1,Q2,MATRIX_0:20;
for i, j being Nat st [i,j] in Indices ST
holds ST*(i,j) = S1T1*(i,j)
proof
let i, j be Nat;
assume A1: [i,j] in Indices ST;
A2: Indices ST = [:Seg len ST,Seg width ST:] by FINSEQ_1:def 3
.= Indices S1T1 by AS,P3,Q3,FINSEQ_1:def 3;
i in dom ST by A1,ZFMISC_1:87;
then i in Seg len ST by FINSEQ_1:def 3;
then i in dom S by FINSEQ_1:def 3,P3;
then
X1: Line(S,i) = Line(S1,i) by ZMATRLIN:2,AS;
j in Seg width T by A1,P3,ZFMISC_1:87;
then
X2: Col(T,j) = Col(T1,j) by ZMATRLIN:3,AS;
thus ST*(i,j) = Line(S,i) "*" Col(T,j) by A1,P1,P2,MATRIX_3:def 4
.= Line(S1,i) "*" Col(T1,j) by X1,X2,ZMATRLIN:37
.= S1T1*(i,j) by A1,A2,Q1,Q2,MATRIX_3:def 4;
end;
hence thesis by AS,P3,Q3,ZMATRLIN:4;
end;
theorem MLT2:
for n being Nat holds 1.(INT.Ring,n) = 1.(F_Real,n)
proof
let n be Nat;
set M = 1.(INT.Ring,n);
set L = 1.(F_Real,n);
P1: len M = n & width M = n & Indices M = [:Seg n, Seg n:] by MATRIX_0:24;
P2: len L = n & width L = n & Indices L = [:Seg n, Seg n:] by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices M holds M*(i,j) = L*(i,j)
proof
let i, j be Nat;
assume AS: [i,j] in Indices M;
per cases;
suppose Q1: i = j;
hence M*(i,j) = 1.INT.Ring by MATRIX_1:def 3,AS
.= 1.F_Real
.= L*(i,j) by Q1,MATRIX_1:def 3,P1,P2,AS;
end;
suppose Q2: i <> j;
hence M*(i,j) = 0.INT.Ring by MATRIX_1:def 3,AS
.= 0.F_Real
.= L*(i,j) by Q2,MATRIX_1:def 3,P1,P2,AS;
end;
end;
hence thesis by P1,P2,ZMATRLIN:4;
end;
theorem ThMBF1:
for V1, V2 being finite-rank free Z_Module,
b1 being OrdBasis of V1, b2 being OrdBasis of V2, b3 being OrdBasis of V2,
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
let V1, V2 be finite-rank free Z_Module,
b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V2,
f be bilinear-FrForm of V1,V2;
set I = inttorealM(AutMt(id(V2), b3, b2));
assume AS: 0 < rank V1;
set n = len b2;
A2: len b2 = rank V2 by ZMATRLIN:49;
A3: len b3 = rank V2 by ZMATRLIN:49;
reconsider IM1 = AutMt(id(V2), b3, b2) as Matrix of n,INT.Ring
by ZMATRLIN:50,A2;
reconsider M1 = inttorealM(IM1@) as Matrix of n,F_Real;
set M2 = BilinearM(f, b1, b2) * M1;
B1: len M1 = n & width M1 = n
& Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
F1: len IM1 = n & width IM1 = n
& Indices IM1 = [:Seg n, Seg n:] by MATRIX_0:24;
B2: 0 < len b1 by AS,ZMATRLIN:49;
then B3: len BilinearM(f, b1, b2) = len b1
& width BilinearM(f, b1, b2) = len b2 by MATRIX_0:23;
C1: width BilinearM(f, b1, b2) = len M1 by B1,B2,MATRIX_0:23;
X0:len M2 = len b1 & width M2 = n by B1,B3,MATRIX_3:def 4;
then reconsider M2 as Matrix of len b1,n,F_Real by B2,MATRIX_0:20;
set FM1 = M1;
set FBM = BilinearM(f, b1, b2);
X1: len BilinearM(f, b1, b3) = len M2
& width BilinearM(f, b1, b3) = width M2 by A2,A3,B2,X0,MATRIX_0:23;
X2: M1 = I@ by ZMATRLIN:6;
for i, j being Nat st [i,j] in Indices BilinearM(f, b1, b3)
holds BilinearM(f, b1, b3)*(i,j) = M2*(i,j)
proof
let i, j be Nat;
assume [i,j] in Indices BilinearM(f, b1, b3);
then B6: [i,j] in [:Seg len b1,Seg len b3 :] by B2,MATRIX_0:23;
then B7: i in Seg len b1 & j in Seg len b3 by ZFMISC_1:87;
then B8: i in dom b1 & j in dom b3 by FINSEQ_1:def 3;
then B9: (BilinearM(f, b1, b3))*(i,j) = f.(b1/.i, b3/.j) by defBilinearM;
[i,j] in Indices M2 by B2,B6,A2,A3,MATRIX_0:23;
then B11: M2*(i,j) = Line(FBM,i) "*" Col(FM1,j) by C1,MATRIX_3:def 4;
B12: len Line(FBM,i) = len b2 by B3,MATRIX_0:def 7;
B13:
now
let k be Nat;
assume B131: k in Seg len b2;
then B132: k in Seg width FBM by B2,MATRIX_0:23;
B81: k in dom b2 by FINSEQ_1:def 3,B131;
thus Line(FBM,i).k = FBM*(i,k) by B132,MATRIX_0:def 7
.= f.(b1/.i, b2/.k) by B8,B81,defBilinearM;
end;
B14: len Col(FM1,j) = len b2 by B1,MATRIX_0:def 8;
B135: j in Seg n by B6,A2,A3,ZFMISC_1:87;
B15:
now
let k be Nat;
assume 1 <= k & k <= len Col(FM1,j);
then B131:k in Seg len b2 by B14;
then B132: k in dom FM1 by B1,FINSEQ_1:def 3;
B132A: j in dom IM1 by B135,F1,FINSEQ_1:def 3;
Y1: [j,k] in Indices IM1 by F1,B131,B135,ZFMISC_1:87;
then consider p be FinSequence of INT such that
B133: p = IM1.j & IM1*(j,k) = p.k by MATRIX_0:def 5;
B81A: j in dom b3 by B7,FINSEQ_1:def 3;
Y2: [k,j] in Indices IM1@ by Y1,MATRIX_0:def 6;
X0: Col(FM1,j).k = FM1*(k,j) by B132,MATRIX_0:def 8
.= (IM1@)*(k,j) by Y2,ZMATRLIN:1
.= (AutMt(id(V2),b3,b2))*(j,k) by Y1,MATRIX_0:def 6;
IM1.j = (AutMt(id(V2), b3, b2)) /.j by B132A,PARTFUN1:def 6
.= (id(V2)).(b3/.j) |-- b2 by B81A,ZMATRLIN:def 8;
hence Col(FM1,j).k = ((b3/.j) |-- b2).k by B133,X0;
end;
len Col(FM1,j) = len ((b3/.j) |-- b2) by B14,ZMATRLIN:def 7;
hence thesis by B9,B11,B12,B13,B14,B15,LMThMBF1X,FINSEQ_1:def 18;
end;
hence thesis by ZMATRLIN:4,X1,X2;
end;
theorem ThMBF2:
for V1, V2 being finite-rank free Z_Module,
b1 being OrdBasis of V1, b2 being OrdBasis of V2, b3 being OrdBasis of V1,
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
let V1, V2 be finite-rank free Z_Module,
b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V1,
f be bilinear-FrForm of V1, V2;
assume AS: 0 < rank V1;
set I = inttorealM(AutMt(id(V1), b3, b1));
set n = len b3;
A1: len b1 = rank V1 by ZMATRLIN:49;
A3: len b3 = rank V1 by ZMATRLIN:49;
reconsider IM1 = AutMt(id(V1), b3, b1) as Matrix of n,INT.Ring
by ZMATRLIN:50,A3;
reconsider M1 = inttorealM(IM1) as Matrix of n,F_Real;
set M2 = M1 * BilinearM(f, b1, b2);
B1: len M1 = n & width M1 = n
& Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
0 < len b1 by AS,ZMATRLIN:49; then
B3: len BilinearM(f, b1, b2) = len b1
& width BilinearM(f, b1, b2) = len b2 by MATRIX_0:23;
then
X0:len M2 = n & width M2 = len b2 by A1,A3,B1,MATRIX_3:def 4;
then reconsider M2 as Matrix of n,len b2, F_Real by A3,AS,MATRIX_0:20;
set FM1 = M1;
set FBM = BilinearM(f, b1, b2);
X1: len BilinearM(f, b3, b2) = len M2
& width BilinearM(f, b3, b2) = width M2 by AS,A3,X0,MATRIX_0:23;
for i, j being Nat st [i,j] in Indices BilinearM(f, b3, b2)
holds BilinearM(f, b3, b2)*(i,j) = M2*(i,j)
proof
let i, j be Nat;
assume [i,j] in Indices BilinearM(f, b3, b2);
then B6: [i,j] in [:Seg len b3,Seg len b2 :] by AS,A3,MATRIX_0:23;
then i in Seg len b3 & j in Seg len b2 by ZFMISC_1:87;
then B8: i in dom b3 & j in dom b2 by FINSEQ_1:def 3;
then B9: (BilinearM(f, b3, b2))*(i,j) = f.(b3/.i, b2/.j) by defBilinearM;
[i,j] in Indices M2 by AS,A3,B6,MATRIX_0:23;
then B11: M2*(i,j) = Line(FM1,i) "*" Col(FBM,j)
by A1,A3,B1,B3,MATRIX_3:def 4;
B12: len Line(FM1,i) = len b3 by B1,MATRIX_0:def 7;
B14: len Col(FBM,j) = len b3 by B3,A1,A3,MATRIX_0:def 8;
B13:
now
let k be Nat;
assume B131: k in Seg len b1;
then B132: k in dom FBM by B3,FINSEQ_1:def 3;
B81: k in dom b1 by FINSEQ_1:def 3,B131;
thus Col(FBM,j).k = FBM*(k,j) by B132,MATRIX_0:def 8
.= f.(b1/.k, b2/.j) by B8,B81,defBilinearM;
end;
B135: i in Seg n by B6,ZFMISC_1:87;
then B135A: i in dom M1 by B1,FINSEQ_1:def 3;
B136: i in dom b3 by B135,FINSEQ_1:def 3;
B15:
now
let k be Nat;
assume BX131: 1 <= k & k <= len Line(FM1,i);
then B131: k in Seg len b1 by B12,A1,A3;
XX1: [i,k] in Indices M1 by A1,A3,B1,B131,B135,ZFMISC_1:87;
X0: Line(FM1,i).k = FM1*(i,k)
by B1,B12,BX131,FINSEQ_1:1,MATRIX_0:def 7
.= (AutMt(id(V1),b3,b1))*(i,k) by XX1,ZMATRLIN:1;
[i,k] in Indices IM1 by A1,A3,B1,B131,B135,ZFMISC_1:87;
then XX3: ex p being FinSequence of INT.Ring
st p = IM1.i & IM1*(i,k) = p.k by MATRIX_0:def 5;
IM1.i = AutMt(id(V1), b3, b1)/.i by B135A,PARTFUN1:def 6
.= (id(V1)).(b3/.i) |-- b1 by B136,ZMATRLIN:def 8
.= (b3/.i) |-- b1;
hence Line(FM1,i).k = ((b3/.i) |-- b1).k by X0,XX3;
end;
len Line(FM1,i) = len ((b3/.i) |-- b1) by A1,A3,B12,ZMATRLIN:def 7;
hence thesis by A1,A3,B9,B11,B12,B13,B14,B15,LMThMBF1Y,FINSEQ_1:def 18;
end;
hence thesis by X1,ZMATRLIN:4;
end;
theorem ThMBF3:
for V being finite-rank free Z_Module,
b1, b2 being OrdBasis of V, 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
let V be finite-rank free Z_Module,
b1, b2 be OrdBasis of V, f be bilinear-FrForm of V,V;
set I = inttorealM( AutMt(id(V), b2, b1));
assume AS: 0 < rank V;
set n = len b1;
A1: len b1 = rank V by ZMATRLIN:49;
reconsider IM1 = AutMt(id(V), b2, b1) as Matrix of
n,INT.Ring by ZMATRLIN:50,A1;
reconsider IM2 = AutMt(id(V), b2, b1) as Matrix of n,INT.Ring
by ZMATRLIN:50,A1;
reconsider M1 = IM1@ as Matrix of n,INT.Ring;
reconsider M2 = IM2 as Matrix of n,INT.Ring;
Y1: width IM1=n by MATRIX_0:24;
Yb: width BilinearM(f, b1, b1)=len b1 by MATRIX_0:24;
width (AutMt(id(V), b2, b1))=len BilinearM(f, b1, b1) &
width BilinearM(f, b1, b1)=len (AutMt(id(V), b2, b1)@)
by MATRIX_0:def 2,Y1,Yb;
then
X1: width I=len BilinearM(f, b1, b1) &
width BilinearM(f, b1, b1)=len (I@) by ZMATRLIN:6;
thus BilinearM(f, b2, b2)
= I* BilinearM(f, b1, b2) by ThMBF2,AS
.= I* ( BilinearM(f, b1, b1) * (I@)) by ThMBF1,AS
.= I * BilinearM(f, b1, b1) *(I@) by MATRIX_3:33,X1;
end;
theorem ThSign2:
for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V,
M being Matrix of rank(V),F_Real st M = AutMt(id(V), b1, b2)
holds ( Det M = 1 & Det M@ = 1) or ( Det M = -1 & Det M@ = -1)
proof
let V be finite-rank free Z_Module, b1, b2 be OrdBasis of V,
M be Matrix of rank(V),F_Real;
assume AS1: M = AutMt(id(V), b1, b2);
set n = rank(V);
per cases;
suppose AS1: rank(V) = 0;
then A1: Det M = 1.F_Real by MATRIXR2:41
.= 1;
Det M@ = 1.F_Real by AS1,MATRIXR2:41
.= 1;
hence thesis by A1;
end;
suppose AS2: rank(V) > 0;
B0: len b1 = rank(V) by ZMATRLIN:49;
B1: len AutMt(id(V), b2, b1) = len b2 by ZMATRLIN:def 8
.= rank(V) by ZMATRLIN:49;
len b2 = rank(V) by ZMATRLIN:49;
then width AutMt(id(V), b2, b1) = len b1 by AS2,ZMATRLIN:34;
then reconsider M2 = AutMt(id(V), b2, b1) as Matrix of rank(V),INT.Ring
by AS2,B0,B1,MATRIX_0:20;
AutMt(id(V), b1, b2) is Matrix of n,INT.Ring &
AutMt(id(V), b2, b1) is Matrix of n,INT.Ring by ZMATRLIN:50;
then
A1: M*inttorealM(M2) = AutMt(id(V), b1, b2) * AutMt(id(V), b2, b1)
by AS1,AS2,MLT1
.= 1.(INT.Ring,rank(V)) by ZMATRLIN:54,AS2
.= 1.(F_Real,rank(V)) by MLT2;
then reconsider MM2 = M*inttorealM(M2) as Matrix of rank(V),F_Real;
A2: (Det M) * (Det inttorealM(M2))
= Det (MM2) by MATRIXR2:45
.= 1_(F_Real) by AS2,A1,NAT_1:14,MATRIX_7:16
.= 1;
reconsider i = Det M as Integer by AS1,ZMATRLIN:51,INT_1:def 2;
Det inttorealM(M2) in INT by ZMATRLIN:51;
then reconsider j = Det inttorealM(M2) as Integer;
i * j = 1 by A2;
then Det M = 1 or Det M = -1 by INT_1:9;
hence thesis by AS2,MATRIX_7:37,NAT_1:14;
end;
end;
theorem
for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V,
M being Matrix of rank(V),F_Real st M = AutMt(id(V), b1, b2)
holds |. Det M .| = 1
proof
let V be finite-rank free Z_Module, b1, b2 be OrdBasis of V,
M be Matrix of rank(V),F_Real;
assume M = AutMt(id(V), b1, b2);
then Det M = 1 or Det M = -1 by ThSign2;
then |. Det M .| = 1 or |. Det M .| = -(-1) by ABSVALUE:def 1;
hence thesis;
end;
theorem ThMBFY:
for V being finite-rank free Z_Module,
b1, b2 being OrdBasis of V, f being bilinear-FrForm of V, V
holds Det BilinearM(f, b2, b2) = Det BilinearM(f, b1, b1)
proof
let V be finite-rank free Z_Module,
b1, b2 be OrdBasis of V, f be bilinear-FrForm of V, V;
set n = len b1;
A1: len b1 = rank V by ZMATRLIN:49;
A2: len b2 = rank V by ZMATRLIN:49;
reconsider B1 = BilinearM(f, b1, b1) as Matrix of n,F_Real;
reconsider B2 = BilinearM(f, b2, b2) as Matrix of n,F_Real by A1,A2;
reconsider I1 = AutMt(id(V), b2, b1) as Matrix of n,INT.Ring
by A1,ZMATRLIN:50;
set I = inttorealM(I1);
per cases;
suppose rank V = 0;
hence Det BilinearM(f, b2, b2) = Det BilinearM(f, b1, b1)
by A1,A2,MATRIX_0:45;
end;
suppose ZZ: rank V > 0;
then B2: BilinearM(f, b2, b2) = I * (BilinearM(f, b1, b1)) * (I@)
by ThMBF3;
set M1 = I@;
set M2 = I;
width M2 = n & len M2 = n &
width B1 = n & len B1 = n by MATRIX_0:24;
then width M2 = len B1 & len M2 > 0 & len B1> 0 by ZZ,ZMATRLIN:49;
then reconsider M2B1 = M2 * B1 as Matrix of n, F_Real by MATRIX_4:64;
X2: (Det M2 = 1 & Det M1 = 1) or (Det M2 = -1 & Det M1 = -1)
by A1,ThSign2;
thus Det BilinearM(f, b2, b2) = Det B2 by A1,ZMATRLIN:49
.= (Det(M2B1)) * (Det M1) by A1,B2,ZZ,MATRIX11:62
.= ((Det M2) * (Det B1)) * (Det M1) by ZZ,A1,MATRIX11:62
.= Det BilinearM(f, b1, b1) by X2;
end;
end;
theorem
for V being finite-rank free Z_Module,
b1, b2 being OrdBasis of V, f being bilinear-FrForm of V, V
holds |. Det BilinearM(f, b2, b2) .| = |. Det BilinearM(f, b1, b1) .|
by ThMBFY;
definition
let V be finite-rank free 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
BilinearM(f, b, b);
correctness
proof
len b = rank V by ZMATRLIN:49;
hence thesis;
end;
end;
definition
let V be finite-rank free Z_Module;
let f be bilinear-FrForm of V, V;
func GramDet(f) -> Element of F_Real means
:defGramDet:
for b being OrdBasis of V holds
it = Det GramMatrix(f, b);
existence
proof
set b1 = the OrdBasis of V;
for b being OrdBasis of V holds
Det GramMatrix(f, b) = Det GramMatrix(f, b1)
proof
let b be OrdBasis of V;
thus Det GramMatrix(f, b) = Det BilinearM(f, b, b) by ZMATRLIN:49
.= Det BilinearM(f, b1, b1) by ThMBFY
.= Det GramMatrix(f, b1) by ZMATRLIN:49;
end;
hence thesis;
end;
uniqueness
proof
let n, m be Element of F_Real;
assume that
A1: for b being OrdBasis of V holds Det GramMatrix(f, b) = n and
A2: for b being OrdBasis of V holds Det GramMatrix(f, b) = m;
set b1 = the OrdBasis of V;
Det GramMatrix(f, b1) = n by A1;
hence thesis by A2;
end;
end;
definition
let L be Z_Lattice;
func InnerProduct(L) -> FrForm of L,L equals
the scalar of L;
correctness;
end;
registration
let L be Z_Lattice;
cluster InnerProduct(L) -> additiveSAF homogeneousSAF additiveFAF
homogeneousFAF;
correctness
proof
set f = InnerProduct(L);
for v being Vector of L holds (curry' f).v is additive
proof
let v be Vector of L;
set g = (curry' f).v;
for w1, w2 being Vector of L holds g.(w1+w2) = g.w1 + g.w2
proof
let w1, w2 be Vector of L;
thus g.(w1+w2) = f.(w1+w2, v) by FUNCT_5:70
.= <; w1+w2, v ;>
.= <; v, w1+w2 ;> by defZLattice
.= <; v, w1 ;> + <; v, w2 ;> by ThSc2
.= <; w1, v ;> + <; v, w2 ;> by defZLattice
.= <; w1, v ;> + <; w2, v ;> by defZLattice
.= f.(w1, v) + f.(w2, v)
.= g.w1 + f.(w2, v) by FUNCT_5:70
.= g.w1 + g.w2 by FUNCT_5:70;
end;
hence thesis;
end;
hence f is additiveSAF;
for v being Vector of L holds (curry' f).v is homogeneous
proof
let v be Vector of L;
set g = (curry' f).v;
for w being Vector of L, i being Element of INT.Ring holds
g.(i*w) = i*g.w
proof
let w be Vector of L, i be Element of INT.Ring;
thus g.(i*w) = f.(i*w, v) by FUNCT_5:70
.= <; i*w, v ;>
.= <; v, i*w ;> by defZLattice
.= i * <; v, w ;> by ThSc3
.= i * <; w, v ;> by defZLattice
.= i* f.(w, v)
.= i * g.w by FUNCT_5:70;
end;
hence thesis;
end;
hence f is homogeneousSAF;
for v being Vector of L holds (curry f).v is additive
proof
let v be Vector of L;
set g = (curry f).v;
for w1, w2 being Vector of L holds g.(w1+w2) = g.w1 + g.w2
proof
let w1, w2 be Vector of L;
thus g.(w1+w2) = f.(v, w1+w2) by FUNCT_5:69
.= <; v, w1+w2 ;>
.= <; v, w1 ;> + <; v, w2 ;> by ThSc2
.= f.(v, w1) + f.(v, w2)
.= g.w1 + f.(v, w2) by FUNCT_5:69
.= g.w1 + g.w2 by FUNCT_5:69;
end;
hence thesis;
end;
hence f is additiveFAF;
for v being Vector of L holds (curry f).v is homogeneous
proof
let v be Vector of L;
set g = (curry f).v;
for w being Vector of L, i being Element of INT.Ring holds
g.(i*w) = i * g.w
proof
let w be Vector of L, i be Element of INT.Ring;
thus g.(i*w) = f.(v, i*w) by FUNCT_5:69
.= <; v, i*w ;>
.= i * <; v, w ;> by ThSc3
.= i* f.(v, w)
.= i * g.w by FUNCT_5:69;
end;
hence thesis;
end;
hence f is homogeneousFAF;
end;
end;
definition
let L be Z_Lattice;
let b be OrdBasis of L;
func GramMatrix(b) -> Matrix of dim(L),F_Real equals
GramMatrix(InnerProduct(L),b);
correctness;
end;
definition
let L be Z_Lattice;
func GramDet(L) -> Element of F_Real equals
GramDet(InnerProduct(L));
correctness;
end;
theorem
for L being INTegral Z_Lattice holds
InnerProduct(L) is bilinear-Form of L,L
proof
let L be INTegral Z_Lattice;
X1: dom InnerProduct(L) =
[:the carrier of L,the carrier of L:] by FUNCT_2:def 1;
for z be object st z in [:the carrier of L,the carrier of L:]
holds (InnerProduct(L)).z in the carrier of INT.Ring
proof
let z be object;
assume z in [:the carrier of L,the carrier of L:];
then consider x1, x2 be object such that
B1: x1 in the carrier of L & x2 in the carrier of L
& z = [x1, x2] by ZFMISC_1:def 2;
reconsider x1, x2 as Vector of L by B1;
(InnerProduct(L)).z = <; x1, x2 ;> by B1;
hence (InnerProduct(L)).z in the carrier of INT.Ring by defIntegral;
end;
then reconsider f = InnerProduct(L) as Form of L,L by X1,FUNCT_2:3;
for v being Vector of L holds FunctionalSAF(f,v) is additive
proof
let v be Vector of L;
for x, y being Vector of L holds
(FunctionalSAF(f,v)).(x+y)
= (FunctionalSAF(f,v)).x +(FunctionalSAF(f,v)).y
proof
let x, y be Vector of L;
thus (FunctionalSAF(f,v)).(x+y) = f.(x+y,v) by FUNCT_5:70
.= <; x+y,v ;>
.= <; v,x+y ;> by defZLattice
.= <; v, x ;> + <; v, y ;> by ThSc2
.= <; x, v ;> + <; v, y ;> by defZLattice
.= <; x, v ;> + <; y, v ;> by defZLattice
.= f.(x,v) + f.(y,v)
.= ((curry' f).v).x + f.(y,v) by FUNCT_5:70
.= (FunctionalSAF(f,v)).x + (FunctionalSAF(f,v)).y by FUNCT_5:70;
end;
hence FunctionalSAF(f,v) is additive;
end;
then
X1: f is additiveSAF;
for v being Vector of L holds FunctionalSAF (f,v) is homogeneous
proof
let v be Vector of L;
for x being Vector of L, i being Element of INT.Ring holds
(FunctionalSAF(f,v)).(i*x)
= i*(FunctionalSAF(f,v)).x
proof
let x be Vector of L, i be Element of INT.Ring;
thus (FunctionalSAF(f,v)).(i*x) = f.(i*x,v) by FUNCT_5:70
.= <; i*x,v ;>
.= <; v,i*x ;> by defZLattice
.= i*<; v, x ;> by ThSc3
.= i*<; x, v ;> by defZLattice
.= i*f.(x,v)
.= i*(FunctionalSAF(f,v)).x by FUNCT_5:70;
end;
hence FunctionalSAF(f,v) is homogeneous;
end;
then
X2: f is homogeneousSAF;
for v being Vector of L holds FunctionalFAF (f,v) is additive
proof
let v be Vector of L;
for x, y being Vector of L holds
(FunctionalFAF(f,v)).(x+y)
= (FunctionalFAF(f,v)).x +(FunctionalFAF(f,v)).y
proof
let x, y be Vector of L;
thus (FunctionalFAF(f,v)).(x+y) = f.(v,x+y) by FUNCT_5:69
.= <; v,x+y ;>
.= <; v, x ;> + <; v, y ;> by ThSc2
.= f.(v,x) + f.(v,y)
.= ((curry f).v).x + f.(v,y) by FUNCT_5:69
.= (FunctionalFAF(f,v)).x + (FunctionalFAF(f,v)).y by FUNCT_5:69;
end;
hence FunctionalFAF(f,v) is additive;
end;
then
X3: f is additiveFAF;
for v being Vector of L holds FunctionalFAF (f,v) is homogeneous
proof
let v be Vector of L;
for x being Vector of L, i being Element of INT.Ring holds
(FunctionalFAF(f,v)).(i*x) = i*(FunctionalFAF(f,v)).x
proof
let x be Vector of L, i be Element of INT.Ring;
thus (FunctionalFAF(f,v)).(i*x) = f.(v,i*x) by FUNCT_5:69
.= <; v,i*x ;>
.= i*<; v, x ;> by ThSc3
.= i*f.(v,x)
.= i*(FunctionalFAF(f,v)).x by FUNCT_5:69;
end;
hence FunctionalFAF(f,v) is homogeneous;
end;
then f is homogeneousFAF;
hence thesis by X1,X2,X3;
end;
theorem ThIntLatY:
for L being INTegral Z_Lattice, b being OrdBasis of L holds
GramMatrix(b) is Matrix of dim(L),INT.Ring
proof
let L be INTegral Z_Lattice, b be OrdBasis of L;
X1: len GramMatrix(b) = dim L & width GramMatrix(b) = dim L
& Indices GramMatrix(b) = [:Seg dim L, Seg dim L:] by MATRIX_0:24;
X3: len b = dim L by ZMATRLIN:49;
for i, j being Nat st [i, j] in Indices GramMatrix(b)
holds (GramMatrix(b))*(i,j) in the carrier of INT.Ring
proof
let i, j be Nat;
assume [i, j] in Indices GramMatrix(b);
then i in Seg dim L & j in Seg dim L by X1,ZFMISC_1:87;
then
D1: i in dom b & j in dom b by X3,FINSEQ_1:def 3;
(GramMatrix(b))*(i,j) = (InnerProduct(L)).(b/.i, b/.j)
by defBilinearM,D1
.= <; b/.i, b/.j ;>;
hence (GramMatrix(b))*(i,j) in the carrier of INT.Ring by defIntegral;
end;
hence GramMatrix(b) is Matrix of dim(L),INT.Ring by LMEQ;
end;
ThIntLatZ:
for L being INTegral Z_Lattice holds GramDet(L) is Integer
proof
let L be INTegral Z_Lattice;
set b = the OrdBasis of L;
GramMatrix(b) is Matrix of dim(L),INT.Ring by ThIntLatY;
then Det GramMatrix(b) in INT by ZMATRLIN:47;
hence thesis by defGramDet;
end;
registration
let L be INTegral Z_Lattice;
cluster GramDet(L) -> integer;
correctness by ThIntLatZ;
end;