:: Dual Lattice of $\mathbb Z$-module Lattice
:: by Yuichi Futa and Yasunari Shidama
::
:: Received June 27, 2017
:: Copyright (c) 2017-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, XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3,
ORDINAL4, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1,
NAT_1, FINSET_1, FUNCOP_1, RLSUB_1, BINOP_1, ZFMISC_1, INT_1,
RLVECT_2, ZMODUL03, FINSEQ_4, RLVECT_3, RMOD_2, RANKNULL, UPROOTS,
GROUP_1, INT_3, VECTSP_1, MESFUNC1, REALSET1, MATRLIN, RLVECT_5,
NORMSP_1, BHSP_1, RVSUM_1, MATRIX_1, MATRIX_3, ZMATRLIN, ZMODLAT1,
TREES_1, MFOLD_2, FVSUM_1, INCSP_1, ZMODUL04, ZMODUL08, FUNCT_2,
ZMODLAT2, VECTSP10, MATRIX_6, LAPLACE, ZMODLAT3, XCMPLX_0, VECTSP_2;
notations GCD_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1,
FUNCOP_1, REALSET1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, INT_1, FINSEQ_1, MATRIX_0, STRUCT_0, ALGSTR_0, RLVECT_1,
GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_6, VECTSP_7, MATRIX_1,
FVSUM_1, MATRIX_3, INT_3, ZMODUL01, ZMODUL03, GAUSSINT, ZMODUL04,
ZMATRLIN, ZMODLAT1, ZMODUL08, MATRIX_6, LAPLACE, MATRIX13,
FINSEQ_4, ZMODLAT2;
constructors VECTSP_2, GCD_1, BINOP_2, UPROOTS, RELSET_1, REALSET1,
ORDERS_1, VECTSP_9, ZMODUL02, ZMODUL01, EUCLID, FVSUM_1, EC_PF_1,
ZMODUL04, ZMODUL07, ZMODUL05, MATRIX_6, LAPLACE, MATRIX13,
FINSEQ_4, ZMODLAT2, MATRIX_3;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1,
XBOOLE_0, BINOP_2, ORDINAL1, XXREAL_0, NAT_1, INT_3, REALSET1,
RELAT_1, VECTSP_1, GAUSSINT, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04,
ZMODUL06, ZMODLAT1, ZMODUL08, FINSEQ_2, ZMODLAT2, MATRIX_3,
RING_2, GCD_1, VECTSP_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities XCMPLX_0, BINOP_1, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, VECTSP_4,
REALSET1, FVSUM_1, FINSEQ_1, MATRIX_0, ZMODLAT1, LAPLACE, GAUSSINT,
VECTSP_6;
expansions TARSKI, STRUCT_0, FINSEQ_1, FUNCT_2, ZMODLAT1, XBOOLE_0, RELAT_1,
FUNCT_1;
theorems CARD_1, CARD_2, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, INT_1, NAT_1,
RLVECT_1, TARSKI, ZMODUL01, ZFMISC_1, GAUSSINT, SUBSET_1, ZMODUL05,
RELAT_1, ZMODUL03, XBOOLE_0, XBOOLE_1, FUNCOP_1, XREAL_1, PARTFUN1,
VECTSP_1, ZMODUL02, VECTSP_7, NUMBERS, VECTSP_4, MATRIX_0, ZMODUL06,
MATRIX_3, ZMATRLIN, FVSUM_1, MATRIX_1, ZMODLAT1, ZMODUL04, ZMODUL08,
XCMPLX_1, ZMODUL07, VECTSP_6, RAT_1, XREAL_0, FINSEQ_2, MATRIX_6,
LAPLACE, RLVECT_2, WELLORD2, FINSEQ_4, MATRIX15, ZMODLAT2, STRUCT_0;
schemes FINSEQ_1, FUNCT_2, NAT_1, FUNCT_1, SUBSET_1, FRAENKEL;
begin :: 1. Summation of inner products
theorem ThSLGM1:
for L being RATional Z_Lattice, LX being Z_Lattice
st LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX
holds LX is RATional
proof
let L be RATional Z_Lattice, LX be Z_Lattice such that
A1: LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX;
for v, u being Vector of LX holds <; v, u ;> in RAT
proof
let v, u be Vector of LX;
reconsider vv = v, uu = u as Vector of DivisibleMod(L) by A1,ZMODUL01:25;
<; v, u ;> = (ScProductDM(L)).(vv, uu) by A1,FUNCT_1:49;
hence thesis by RAT_1:def 2;
end;
hence thesis by ZMODLAT2:def 1;
end;
registration
let L be RATional Z_Lattice;
cluster EMLat(L) -> RATional;
correctness
proof
A1: the scalar of EMLat(L) = ScProductEM(L) by ZMODLAT2:def 4
.= (ScProductDM(L)) || (rng MorphsZQ(L)) by ZMODLAT2:7
.= (ScProductDM(L)) || the carrier of EMLat(L) by ZMODLAT2:def 4;
EMLat(L) is Submodule of DivisibleMod(L) by ZMODLAT2:20;
hence thesis by A1,ThSLGM1;
end;
end;
registration
let L be RATional Z_Lattice;
let r be Element of F_Rat;
cluster EMLat(r, L) -> RATional;
correctness
proof
A1: the scalar of EMLat(r, L) = (ScProductDM(L)) || (r * (rng MorphsZQ(L)))
by ZMODLAT2:def 5
.= (ScProductDM(L)) || the carrier of EMLat(r, L) by ZMODLAT2:def 5;
EMLat(r, L) is Submodule of DivisibleMod(L) by ZMODLAT2:21;
hence thesis by A1,ThSLGM1;
end;
end;
definition
let L be Z_Lattice;
let F be FinSequence of L;
let f be Function of L, INT.Ring;
let v be Vector of L;
func ScFS(v, f, F) -> FinSequence of F_Real means :defScFS:
len it = len F & for i being Nat st i in dom it
holds it.i = <; v, f.(F/.i) * F/.i ;>;
existence
proof
deffunc X(object) = <; v, f.(F/.$1) * F/.$1 ;>;
consider G be FinSequence such that
A1: len G = len F & for i being Nat st i in dom G
holds G.i = X(i) from FINSEQ_1:sch 2;
rng G c= the carrier of F_Real
proof
let x be object such that
B1: x in rng G;
consider z be object such that
B2: z in dom G & x = G.z by B1,FUNCT_1:def 3;
x = <; v, f.(F/.z) * F/.z ;> by A1,B2;
hence thesis;
end;
then reconsider G as FinSequence of F_Real by FINSEQ_1:def 4;
take G;
thus thesis by A1;
end;
uniqueness
proof
let f1, f2 be FinSequence of F_Real;
assume AS1: len f1 = len F & for i being Nat st i in dom f1
holds f1.i = <; v, f.(F/.i) * F/.i ;>;
assume AS2: len f2 = len F & for i being Nat st i in dom f2
holds f2.i = <; v, f.(F/.i) * F/.i ;>;
A2: dom f1 = dom f2 by AS1,AS2,FINSEQ_3:29;
for k being Nat st k in dom f1 holds f1.k = f2.k
proof
let k be Nat;
assume
B1: k in dom f1;
hence f1.k = <; v, f.(F/.k) * F/.k ;> by AS1
.= f2.k by AS2,A2,B1;
end;
hence thesis by AS1,AS2,FINSEQ_3:29;
end;
end;
theorem ThScFS1:
for L being Z_Lattice, f being Function of L, INT.Ring,
F being FinSequence of L,
v, u being Vector of L, i being Nat
st i in dom F & u = F.i
holds (ScFS(v, f, F)).i = <; v, f.u * u ;>
proof
let L be Z_Lattice, f be Function of L, INT.Ring,
F be FinSequence of L,
v, u be Vector of L, i be Nat such that
A1: i in dom F & u = F.i;
A2: F/.i = F.i by A1,PARTFUN1:def 6;
len(ScFS(v, f, F)) = len F by defScFS;
then i in dom(ScFS(v, f, F)) by A1,FINSEQ_3:29;
hence thesis by A1,A2,defScFS;
end;
theorem ThScFS3:
for L being Z_Lattice, f being Function of L, INT.Ring,
v, u being Vector of L holds
ScFS(v, f, <* u *>) = <* <; v, f.u * u ;> *>
proof
let L be Z_Lattice, f be Function of L, INT.Ring;
let v, u be Vector of L;
A1: 1 in {1} by TARSKI:def 1;
A2: len ScFS(v, f, <* u *>) = len <* u *> by defScFS
.= 1 by FINSEQ_1:40;
then dom(ScFS(v, f, <* u *>)) = {1} by FINSEQ_1:2,FINSEQ_1:def 3;
then (ScFS(v, f, <* u *>)).1 = <; v, f.(<* u *>/.1) * <* u *>/.1 ;>
by A1,defScFS
.= <; v, f.(<* u *>/.1) * u ;> by FINSEQ_4:16
.= <; v, f.u * u ;> by FINSEQ_4:16;
hence thesis by A2,FINSEQ_1:40;
end;
theorem ThScFS6:
for L being Z_Lattice, f being Function of L, INT.Ring,
F, G being FinSequence of L,
v being Vector of L holds
ScFS(v, f, F ^ G) = ScFS(v, f, F) ^ ScFS(v, f, G)
proof
let L be Z_Lattice, f be Function of L, INT.Ring,
F, G be FinSequence of L,
v be Vector of L;
set H = ScFS(v, f, F) ^ ScFS(v, f, G);
set I = F ^ G;
A1: len F = len(ScFS(v, f, F)) by defScFS;
A2: len H = len(ScFS(v, f, F)) + len(ScFS(v, f, G)) by FINSEQ_1:22
.= len F + len(ScFS(v, f, G)) by defScFS
.= len F + len G by defScFS
.= len I by FINSEQ_1:22;
A3: len G = len(ScFS(v, f, G)) by defScFS;
now
let k be Nat;
assume
A4: k in dom H;
per cases by A4,FINSEQ_1:25;
suppose
A5: k in dom(ScFS(v, f, F)); then
A6: k in dom F by A1,FINSEQ_3:29; then
A7: k in dom(F ^ G) by FINSEQ_3:22;
A8: F/.k = F.k by A6,PARTFUN1:def 6
.= (F ^ G).k by A6,FINSEQ_1:def 7
.= (F ^ G)/.k by A7,PARTFUN1:def 6;
thus H.k = (ScFS(v, f, F)).k by A5,FINSEQ_1:def 7
.= <; v, f.(I/.k) * I/.k ;> by A5,A8,defScFS;
end;
suppose
A9: ex n being Nat st n in dom(ScFS(v, f, G))
& k = len(ScFS(v, f, F)) + n;
A10: k in dom I by A2,A4,FINSEQ_3:29;
consider n be Nat such that
A11: n in dom(ScFS(v, f, G)) and
A12: k = len(ScFS(v, f, F)) + n by A9;
A13: n in dom G by A3,A11,FINSEQ_3:29; then
A14: G/.n = G.n by PARTFUN1:def 6
.= (F ^ G).k by A1,A12,A13,FINSEQ_1:def 7
.= (F ^ G)/.k by A10,PARTFUN1:def 6;
thus H.k = (ScFS(v, f, G)).n by A11,A12,FINSEQ_1:def 7
.= <; v, f.(I/.k) * I/.k ;> by A11,A14,defScFS;
end;
end;
hence thesis by A2,defScFS;
end;
definition
let L be Z_Lattice;
let l be Linear_Combination of L;
let v be Vector of L;
func SumSc(v, l) -> Element of F_Real means :defSumSc:
ex F being FinSequence of L st
F is one-to-one & rng F = Carrier(l) & it = Sum(ScFS(v, l, F));
existence
proof
consider F be FinSequence such that
A1: rng F = Carrier(l) & F is one-to-one by FINSEQ_4:58;
reconsider F as FinSequence of L by A1,FINSEQ_1:def 4;
take Sum(ScFS(v, l, F)), F;
thus thesis by A1;
end;
uniqueness
proof
let r1, r2 be Element of F_Real;
given F1 be FinSequence of L such that
A1: F1 is one-to-one and
A2: rng F1 = Carrier(l) and
A3: r1 = Sum(ScFS(v, l, F1));
given F2 be FinSequence of L such that
A4: F2 is one-to-one and
A5: rng F2 = Carrier(l) and
A6: r2 = Sum(ScFS(v, l, F2));
deffunc F(object) = F1".(F2.$1);
A7: len F1 = len F2 by A1,A2,A4,A5,FINSEQ_1:48; then
A8: dom F1 = dom F2 by FINSEQ_3:29;
A9: for x being object st x in dom F1 holds F(x) in dom F1
proof
let x be object;
assume x in dom F1;
then F2.x in rng F1 by A2,A5,A8,FUNCT_1:3;
then F2.x in dom(F1") by A1,FUNCT_1:33;
then F1".(F2.x) in rng(F1") by FUNCT_1:3;
hence thesis by A1,FUNCT_1:33;
end;
consider f be Function of dom F1, dom F1 such that
A10: for x being object st x in dom F1 holds f.x = F(x)
from FUNCT_2:sch 2(A9);
for x1, x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1, x2 be object;
assume
B1: x1 in dom f & x2 in dom f & f.x1 = f.x2; then
F2.x1 in rng F1 by A2,A5,A8,FUNCT_1:3;
then B4: F2.x1 in dom(F1") by A1,FUNCT_1:33;
F2.x2 in rng F1 by A2,A5,A8,B1,FUNCT_1:3;
then B7: F2.x2 in dom(F1") by A1,FUNCT_1:33;
F1".(F2.x1) = f.x1 by A10,B1
.= F1".(F2.x2) by A10,B1;
then F2.x1 = F2.x2 by A1,B4,B7,FUNCT_1:def 4;
hence thesis by A4,A8,B1;
end;
then A11: f is one-to-one;
dom F1 c= rng f
proof
let y be object;
assume
B1: y in dom F1; then
F1.y in rng F2 by A2,A5,FUNCT_1:3;
then consider x be object such that
B2: x in dom F2 & F2.x = F1.y by FUNCT_1:def 3;
B3: f.x = F1".(F2.x) by A8,A10,B2
.= y by A1,B1,B2,FUNCT_1:34;
x in dom f by A8,B2,FUNCT_2:def 1;
hence thesis by B3,FUNCT_1:3;
end;
then A12: rng f = dom F1;
then reconsider f as Permutation of dom F1 by A11,FUNCT_2:57;
reconsider G1 = ScFS(v, l, F1) as FinSequence of F_Real;
set G2 = ScFS(v, l, F2);
A14: len G2 = len F2 by defScFS;
len F1 = len G1 by defScFS; then
A15: dom F1 = dom G1 by FINSEQ_3:29;
then reconsider f as Permutation of dom G1;
A16: len G1 = len F2 by A7,defScFS
.= len G2 by defScFS;
for i being Nat st i in dom G2 holds G2.i = G1.(f.i)
proof
let i be Nat such that
B1: i in dom G2;
B2: G2.i = <; v, l.(F2/.i) * F2/.i ;> by B1,defScFS;
B3: i in dom F2 by A14,B1,FINSEQ_3:29;
then reconsider u = F2.i as Element of L by FINSEQ_2:11;
B4: i in dom f by A8,B3,FUNCT_2:def 1;
then f.i in dom F1 by A12,FUNCT_1:3;
then reconsider m = f.i as Element of NAT;
reconsider w = F1.m as Element of L by A12,B4,FINSEQ_2:11,FUNCT_1:3;
B5: F2.i in rng F1 by A2,A5,B3,FUNCT_1:3;
B6: F1.(f.i) = F1.(F1".(F2.i)) by A8,A10,B3
.= F2.i by A1,B5,FUNCT_1:35;
F1.m = F1/.m & F2.i = F2/.i by A12,B3,B4,FUNCT_1:3,PARTFUN1:def 6;
hence G2.i = G1.(f.i) by A12,A15,B2,B4,B6,defScFS,FUNCT_1:3;
end;
hence thesis by A3,A6,A16,RLVECT_2:6;
end;
end;
theorem LmSumSc11:
for L being Z_Lattice, v being Vector of L holds
SumSc(v, ZeroLC(L)) = 0.F_Real
proof
let L be Z_Lattice, v be Vector of L;
consider F be FinSequence of L such that
A1: F is one-to-one & rng F = Carrier(ZeroLC(L)) &
SumSc(v,ZeroLC(L)) = Sum(ScFS(v, ZeroLC(L),F)) by defSumSc;
F = {} by A1,VECTSP_6:def 3;
then len(ScFS(v, ZeroLC(L),F)) = 0 by defScFS;
hence thesis by A1,RLVECT_1:75;
end;
theorem
for L being Z_Lattice, v being Vector of L,
l being Linear_Combination of {}(the carrier of L)
holds SumSc(v, l) = 0.F_Real
proof
let L be Z_Lattice, v be Vector of L,
l be Linear_Combination of {}(the carrier of L);
l = ZeroLC(L) by VECTSP_6:6;
hence thesis by LmSumSc11;
end;
theorem LmSumSc13:
for L being Z_Lattice, v being Vector of L,
l being Linear_Combination of L
st Carrier l = {}
holds SumSc(v, l) = 0.F_Real
proof
let L be Z_Lattice, v be Vector of L,
l be Linear_Combination of L;
assume Carrier l = {}; then
l = ZeroLC(L) by VECTSP_6:def 3;
hence thesis by LmSumSc11;
end;
theorem LmSumSc14:
for L being Z_Lattice, v, u being Vector of L,
l being Linear_Combination of {u}
holds SumSc(v, l) = <; v, l.u * u ;>
proof
let L be Z_Lattice, v, u be Vector of L,
l be Linear_Combination of {u};
per cases by VECTSP_6:def 4,ZFMISC_1:33;
suppose Carrier(l) = {};
then A2: l = ZeroLC(L) by VECTSP_6:def 3;
hence SumSc(v, l) = 0.F_Real by LmSumSc11
.= <; v, 0.L ;> by ZMODLAT1:12
.= <; v, 0.INT.Ring * u ;> by VECTSP_1:14
.= <; v, l.u * u ;> by A2,VECTSP_6:3;
end;
suppose Carrier(l) = {u};
then consider F be FinSequence of L such that
A3: F is one-to-one & rng F = {u} & SumSc(v, l) = Sum(ScFS(v, l, F))
by defSumSc;
F = <* u *> by A3,FINSEQ_3:97;
then ScFS(v, l, F) = <* <; v, l.u * u ;> *> by ThScFS3;
hence thesis by A3,RLVECT_1:44;
end;
end;
theorem LmSumSc1X:
for L being Z_Lattice, v being Vector of L,
l1, l2 being Linear_Combination of L
holds SumSc(v, l1+l2) = SumSc(v, l1) + SumSc(v, l2)
proof
let L be Z_Lattice, w be Vector of L,
l1, l2 be Linear_Combination of L;
set A = Carrier(l1 + l2) \/ Carrier(l1) \/ Carrier(l2);
set C1 = A \ Carrier(l1);
consider p be FinSequence such that
A1: rng p = C1 and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of L by A1,FINSEQ_1:def 4;
A3: A = Carrier(l1) \/ (Carrier(l1 + l2) \/ Carrier(l2)) by XBOOLE_1:4;
set C3 = A \ Carrier(l1 + l2);
consider r be FinSequence such that
A4: rng r = C3 and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r as FinSequence of L by A4,FINSEQ_1:def 4;
A6: A = Carrier(l1 + l2) \/ (Carrier(l1) \/ Carrier(l2)) by XBOOLE_1:4;
set C2 = A \ Carrier(l2);
consider q be FinSequence such that
A7: rng q = C2 and
A8: q is one-to-one by FINSEQ_4:58;
reconsider q as FinSequence of L by A7,FINSEQ_1:def 4;
consider F be FinSequence of L such that
A9: F is one-to-one and
A10: rng F = Carrier(l1 + l2) and
A11: SumSc(w, l1 + l2) = Sum(ScFS(w, l1 + l2, F)) by defSumSc;
set FF = F ^ r;
consider G be FinSequence of L such that
A12: G is one-to-one and
A13: rng G = Carrier(l1) and
A14: SumSc(w, l1) = Sum(ScFS(w, l1, G)) by defSumSc;
rng FF = rng F \/ rng r by FINSEQ_1:31;
then rng FF = Carrier(l1 + l2) \/ A by A10,A4,XBOOLE_1:39;
then
A15: rng FF = A by A6,XBOOLE_1:7,12;
set GG = G ^ p;
rng GG = rng G \/ rng p by FINSEQ_1:31;
then rng GG = Carrier(l1) \/ A by A13,A1,XBOOLE_1:39;
then
A16: rng GG = A by A3,XBOOLE_1:7,12;
rng F misses rng r
proof
set x = the Element of rng F /\ rng r;
assume not thesis;
then x in Carrier(l1 + l2) & x in C3 by A10,A4,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A17: FF is one-to-one by A9,A5,FINSEQ_3:91;
rng G misses rng p
proof
set x = the Element of rng G /\ rng p;
assume not thesis;
then x in Carrier(l1) & x in C1 by A13,A1,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end; then
A18: GG is one-to-one by A12,A2,FINSEQ_3:91; then
A19: len GG = len FF by A17,A16,A15,FINSEQ_1:48;
deffunc F(Nat) = FF <- (GG.$1);
consider P be FinSequence such that
A20: len P = len FF and
A21: for k be Nat st k in dom P holds P.k = F(k) from FINSEQ_1:sch 2;
A22: dom P = dom FF by A20,FINSEQ_3:29;
a22: dom FF = dom GG by A19,FINSEQ_3:29;
A23:
now
let x be object;
assume
A24: x in dom GG;
then reconsider n = x as Element of NAT;
GG.n in rng FF by A16,A15,A24,FUNCT_1:def 3; then
A25: FF just_once_values GG.n by A17,FINSEQ_4:8;
FF.(P.n) = FF.(FF <- (GG.n)) by A21,A22,a22,A24
.= GG.n by A25,FINSEQ_4:def 3;
hence GG.x = FF.(P.x);
end;
A26: rng P c= dom FF
proof
let x be object;
assume x in rng P;
then consider y be object such that
A27: y in dom P and
A28: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A27;
y in dom GG by A19,A20,A27,FINSEQ_3:29;
then GG.y in rng FF by A16,A15,FUNCT_1:def 3;
then
A29: FF just_once_values GG.y by A17,FINSEQ_4:8;
P.y = FF <- (GG.y) by A21,A27;
hence thesis by A28,A29,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom P & P.x in dom FF
proof
assume x in dom GG;
hence x in dom P by A20,FINSEQ_3:29,A19;
then P.x in rng P by FUNCT_1:def 3;
hence thesis by A26;
end;
assume x in dom P & P.x in dom FF;
hence x in dom GG by A20,FINSEQ_3:29,A19;
end;
then
A31: GG = FF * P by A23,FUNCT_1:10;
dom FF c= rng P
proof
set f = FF" * GG;
let x be object;
assume
A32: x in dom FF;
dom(FF") = rng GG by A17,A16,A15,FUNCT_1:33; then
A33: rng f = rng(FF") by RELAT_1:28
.= dom FF by A17,FUNCT_1:33;
f = FF " * FF * P by A31,RELAT_1:36
.= id(dom FF) * P by A17,FUNCT_1:39
.= P by A26,RELAT_1:53;
hence thesis by A32,A33;
end;
then
A34: dom FF = rng P by A26;
A35: len r = len(ScFS(w, l1 + l2, r)) by defScFS; then
B1: dom r = dom(ScFS(w, l1 + l2, r)) by FINSEQ_3:29;
now
let k be Nat;
assume
A36: k in dom(ScFS(w, l1 + l2, r));
then r/.k = r.k by B1,PARTFUN1:def 6;
then r/.k in C3 by A4,A36,B1,FUNCT_1:def 3;
then
A37: not r/.k in Carrier((l1 + l2)) by XBOOLE_0:def 5;
(ScFS(w, l1 + l2, r)).k = <; w, (l1 + l2).(r/.k) * r/.k ;>
by A36,defScFS;
then (ScFS(w, l1 + l2, r)).k = <; w, 0.INT.Ring * r/.k ;> by A37
.= <; w, 0.L ;> by VECTSP_1:14
.= 0.F_Real by ZMODLAT1:12;
hence (ScFS(w, l1 + l2, r)).k = - (ScFS(w, l1 + l2, r)).k
.= - (ScFS(w, l1 + l2, r))/.k by A36,PARTFUN1:def 6;
end;
then A38: Sum(ScFS(w, l1 + l2, r)) = - Sum(ScFS(w, l1 + l2, r))
by A35,RLVECT_2:4;
A39: len p = len(ScFS(w, l1, p)) by defScFS; then
B1: dom p = dom(ScFS(w, l1, p)) by FINSEQ_3:29;
now
let k be Nat;
assume
A40: k in dom(ScFS(w, l1, p));
then p/.k = p.k by B1,PARTFUN1:def 6;
then p/.k in C1 by A1,A40,B1,FUNCT_1:def 3;
then
A41: not p/.k in Carrier(l1) by XBOOLE_0:def 5;
(ScFS(w, l1, p)).k = <; w, l1.(p/.k) * p/.k ;> by A40,defScFS;
then (ScFS(w, l1, p)).k = <; w, 0.INT.Ring * p/.k ;> by A41
.= <; w, 0.L ;> by VECTSP_1:14
.= 0.F_Real by ZMODLAT1:12;
hence (ScFS(w, l1, p)).k = - (ScFS(w, l1, p)).k
.= - (ScFS(w, l1, p))/.k by A40,PARTFUN1:def 6;
end;
then A42: Sum(ScFS(w, l1, p)) = -Sum(ScFS(w, l1, p)) by A39,RLVECT_2:4;
A43: len q = len(ScFS(w, l2, q)) by defScFS; then
B1: dom q = dom(ScFS(w, l2, q)) by FINSEQ_3:29;
now
let k be Nat;
assume
A44: k in dom(ScFS(w, l2, q));
then q/.k = q.k by B1,PARTFUN1:def 6;
then q/.k in C2 by A7,A44,B1,FUNCT_1:def 3;
then
A45: not q/.k in Carrier(l2) by XBOOLE_0:def 5;
(ScFS(w, l2, q)).k = <; w, l2.(q/.k) * q/.k ;> by A44,defScFS;
then (ScFS(w, l2, q)).k = <; w, 0.INT.Ring * q/.k ;> by A45
.= <; w, 0.L ;> by VECTSP_1:14
.= 0.F_Real by ZMODLAT1:12;
hence (ScFS(w, l2, q)).k = -(ScFS(w, l2, q)).k
.= -(ScFS(w, l2, q))/.k by A44,PARTFUN1:def 6;
end;
then A46: Sum(ScFS(w, l2, q)) = - Sum(ScFS(w, l2, q)) by A43,RLVECT_2:4;
set g = ScFS(w, l1, GG);
A47: len g = len GG by defScFS; then
A48: dom GG = dom g by FINSEQ_3:29;
set f = ScFS(w, l1 + l2, FF);
consider H be FinSequence of L such that
A49: H is one-to-one and
A50: rng H = Carrier(l2) and
A51: Sum(ScFS(w, l2, H)) = SumSc(w, l2) by defSumSc;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of rng H /\ rng q;
assume not thesis;
then x in Carrier(l2) & x in C2 by A50,A7,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A52: HH is one-to-one by A49,A8,FINSEQ_3:91;
rng HH = rng H \/ rng q by FINSEQ_1:31;
then rng HH = Carrier(l2) \/ A by A50,A7,XBOOLE_1:39; then
A53: rng HH = A by XBOOLE_1:7,12; then
A54: len GG = len HH by A52,A18,A16,FINSEQ_1:48; then
a54: dom GG = dom HH by FINSEQ_3:29;
deffunc F(Nat) = HH <- (GG.$1);
consider R be FinSequence such that
A55: len R = len HH and
A56: for k being Nat st k in dom R holds R.k = F(k) from FINSEQ_1:sch 2;
A57: dom R = dom HH by A55,FINSEQ_3:29;
A58:
now
let x be object;
assume
A59: x in dom GG;
then reconsider n = x as Element of NAT;
GG.n in rng HH by A16,A53,A59,FUNCT_1:def 3; then
A60: HH just_once_values GG.n by A52,FINSEQ_4:8;
HH.(R.n) = HH.(HH <- (GG.n)) by A56,A57,A59,a54
.= GG.n by A60,FINSEQ_4:def 3;
hence GG.x = HH.(R.x);
end;
A61: rng R c= dom HH
proof
let x be object;
assume x in rng R;
then consider y be object such that
A62: y in dom R and
A63: R.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A62;
y in dom GG by A54,A55,A62,FINSEQ_3:29;
then GG.y in rng HH by A16,A53,FUNCT_1:def 3;
then
A64: HH just_once_values GG.y by A52,FINSEQ_4:8;
R.y = HH <- (GG.y) by A56,A62;
hence thesis by A63,A64,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom R & R.x in dom HH
proof
assume x in dom GG;
hence x in dom R by A55,FINSEQ_3:29,A54;
then R.x in rng R by FUNCT_1:def 3;
hence thesis by A61;
end;
assume x in dom R & R.x in dom HH;
hence x in dom GG by A54,A55,FINSEQ_3:29;
end; then
A66: GG = HH * R by A58,FUNCT_1:10;
dom HH c= rng R
proof
set f = HH" * GG;
let x be object;
assume
A67: x in dom HH;
dom(HH") = rng GG by A52,A16,A53,FUNCT_1:33; then
A68: rng f = rng(HH") by RELAT_1:28
.= dom HH by A52,FUNCT_1:33;
f = HH " * HH * R by A66,RELAT_1:36
.= id(dom HH) * R by A52,FUNCT_1:39
.= R by A61,RELAT_1:53;
hence thesis by A67,A68;
end; then
A69: dom HH = rng R by A61;
set h = ScFS(w, l2, HH);
A70: Sum(h) = Sum(ScFS(w, l2, H) ^ ScFS(w, l2, q)) by ThScFS6
.= Sum(ScFS(w, l2, H)) + 0.F_Real by A46,RLVECT_1:41
.= Sum(ScFS(w, l2, H));
A71: Sum(g) = Sum(ScFS(w, l1, G) ^ ScFS(w, l1, p)) by ThScFS6
.= Sum(ScFS(w, l1, G)) + 0.F_Real by A42,RLVECT_1:41
.= Sum(ScFS(w, l1, G));
A72: dom P = dom FF by A20,FINSEQ_3:29;
A73: P is one-to-one by A20,A34,FINSEQ_3:29,FINSEQ_4:60;
A74: dom R = dom HH by A55,FINSEQ_3:29;
A75: R is one-to-one by A55,A69,FINSEQ_3:29,FINSEQ_4:60;
R is Function of dom HH, dom HH by A61,A74,FUNCT_2:2; then
reconsider R as Permutation of dom HH by A69,A75,FUNCT_2:57;
A76: len h = len HH by defScFS;
then dom h = dom HH by FINSEQ_3:29;
then reconsider R as Permutation of dom h;
reconsider Hp = h * R as FinSequence of F_Real by FINSEQ_2:47;
A77: len Hp = len GG by A54,A76,FINSEQ_2:44;
P is Function of dom FF, dom FF by A26,A72,FUNCT_2:2; then
reconsider P as Permutation of dom FF by A34,A73,FUNCT_2:57;
A78: len f = len FF by defScFS;
then dom f = dom FF by FINSEQ_3:29;
then reconsider P as Permutation of dom f;
reconsider Fp = f * P as FinSequence of F_Real by FINSEQ_2:47;
A79: Sum(f) = Sum(ScFS(w, l1 + l2, F) ^ ScFS(w, l1 + l2, r)) by ThScFS6
.= Sum(ScFS(w, l1 + l2, F)) + 0.F_Real by A38,RLVECT_1:41
.= Sum(ScFS(w, l1 + l2, F));
deffunc F(Nat) = g/.$1 + Hp/.$1;
consider I be FinSequence such that
A80: len I = len GG and
A81: for k being Nat st k in dom I holds I.k = F(k) from FINSEQ_1:sch 2;
A83: dom I = dom GG by A80,FINSEQ_3:29;
rng I c= the carrier of F_Real
proof
let x be object;
assume x in rng I;
then consider y be object such that
A84: y in dom I and
A85: I.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A84;
I.y = g/.y + Hp/.y by A81,A84;
hence thesis by A85;
end;
then reconsider I as FinSequence of F_Real by FINSEQ_1:def 4;
A86: len Fp = len I by A19,A78,A80,FINSEQ_2:44;
then X1: dom I = Seg(len I) & dom Fp = Seg(len I) by FINSEQ_1:def 3;
X2: dom Hp = Seg(len Hp) by FINSEQ_1:def 3
.= dom I by A54,A76,A80,FINSEQ_1:def 3,FINSEQ_2:44;
X3: dom HH = Seg(len HH) by FINSEQ_1:def 3
.= dom I by A18,A16,A52,A53,A80,FINSEQ_1:48,FINSEQ_1:def 3;
X5: dom g = Seg(len g) by FINSEQ_1:def 3
.= dom I by A80,defScFS,FINSEQ_1:def 3;
A87:
now
let k be Nat;
assume
A88: k in dom I; then
A90: Hp/.k = (h * R).k by X2,PARTFUN1:def 6
.= h.(R.k) by A88,X2,FUNCT_1:12;
set v = GG/.k;
A91: Fp.k = f.(P.k) by A88,X1,FUNCT_1:12;
R.k in dom R by A69,A74,A88,X3,FUNCT_1:def 3;
then reconsider j = R.k as Element of NAT by FINSEQ_3:23;
A94: HH.j = GG.k by A58,A88,X3,a54
.= GG/.k by A88,X3,PARTFUN1:def 6,a54;
A95: dom FF = dom GG by A19,FINSEQ_3:29;
then P.k in dom P by A34,A72,A88,X3,FUNCT_1:def 3,a54;
then reconsider l = P.k as Element of NAT by FINSEQ_3:23;
A96: FF.l = GG.k by A23,A88,X3,a54
.= GG/.k by A88,X3,a54,PARTFUN1:def 6;
R.k in dom HH by A69,A74,A88,X3,FUNCT_1:def 3; then
A97: h.j = <; w, l2.v * v ;> by A94,ThScFS1;
P.k in dom FF by A34,A72,A88,A95,X3,a54,FUNCT_1:def 3; then
A98: f.l = <; w, (l1 + l2).v * v ;> by A96,ThScFS1
.= <; w, (l1.v + l2.v) * v ;> by VECTSP_6:22
.= <; w, l1.v * v + l2.v * v ;> by VECTSP_1:def 15
.= <; w, l1.v * v ;> + <; w, l2.v * v ;> by ZMODLAT1:8;
g/.k = g.k by A88,X5,PARTFUN1:def 6
.= <; w, l1.v * v ;> by A88,X5,defScFS;
hence I.k = Fp.k by A81,A88,A90,A97,A91,A98;
end;
dom I = Seg(len I) & dom Fp = Seg(len I) by A86,FINSEQ_1:def 3;
then A100: I = Fp by A87;
Sum(Fp) = Sum(f) & Sum(Hp) = Sum(h) by RLVECT_2:7;
hence thesis
by A11,A14,A51,A71,A70,A79,A80,A81,A83,A77,A47,A100,A48,RLVECT_2:2;
end;
theorem ThSumSc1:
for L being Z_Lattice, l being Linear_Combination of L,
v being Vector of L holds
<; v, Sum(l) ;> = SumSc(v, l)
proof
defpred P[Nat] means
for L being Z_Lattice, l being Linear_Combination of L,
v being Vector of L st card(Carrier l) = $1 holds
<; v, Sum(l) ;> = SumSc(v, l);
A1: P[0]
proof
let L be Z_Lattice, l be Linear_Combination of L,
v be Vector of L such that
B1: card(Carrier l) = 0;
B2: Carrier l = {} by B1;
then Sum(l) = 0.L by VECTSP_6:19;
then <; v, Sum(l) ;> = 0.F_Real by ZMODLAT1:12;
hence thesis by B2,LmSumSc13;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let L be Z_Lattice, l be Linear_Combination of L,
v be Vector of L such that
B2: card(Carrier l) = n+1;
Carrier l <> {} by B2;
then consider u be object such that
B3: u in Carrier l by XBOOLE_0:def 1;
reconsider u as Element of L by B3;
B4: card(Carrier(l) \ {u}) = card(Carrier l) - card{u}
by B3,CARD_2:44,ZFMISC_1:31
.= n+1 - 1 by B2,CARD_2:42
.= n;
B5: Carrier(l) = (Carrier(l) \ {u}) \/ {u}
by B3,XBOOLE_1:45,ZFMISC_1:31;
B6: (Carrier(l) \ {u}) /\ {u} = {} by XBOOLE_0:def 7,XBOOLE_1:79;
l is Linear_Combination of Carrier(l) by VECTSP_6:7;
then consider l1 be Linear_Combination of (Carrier (l) \ {u}),
l2 be Linear_Combination of {u} such that
B7: l = l1 + l2 by B5,B6,ZMODUL04:26;
Sum(l) = Sum(l1) + Sum(l2) by B7,ZMODUL02:52;
then B8: <; v, Sum(l) ;> = <; v, Sum(l1) ;> + <; v, Sum(l2) ;>
by ZMODLAT1:8;
B9: SumSc(v, l) = SumSc(v, l1) + SumSc(v, l2) by B7,LmSumSc1X;
for x being Vector of L st x in (Carrier(l) \ {u}) holds x in Carrier(l1)
proof
let x be Vector of L such that
C1: x in (Carrier(l) \ {u});
x in Carrier(l) by C1,XBOOLE_0:def 5;
then C2: l.x <> 0.INT.Ring by VECTSP_6:2;
C3: Carrier(l2) c= {u} by VECTSP_6:def 4;
C4: l.x = l1.x + l2.x by B7,VECTSP_6:22;
not x in Carrier(l2) by C1,C3,XBOOLE_0:def 5;
then l1.x <> 0.INT.Ring by C2,C4;
hence thesis;
end;
then (Carrier(l) \ {u}) c= Carrier(l1);
then B10: Carrier(l1) = (Carrier(l) \ {u}) by VECTSP_6:def 4;
SumSc(v, l2) = <; v, l2.u * u ;> by LmSumSc14
.= <; v, Sum(l2) ;> by VECTSP_6:17;
hence thesis by B1,B4,B8,B9,B10;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let L be Z_Lattice, l be Linear_Combination of L,
v be Vector of L;
reconsider n = card (Carrier l) as Nat;
P[n] by A3;
hence thesis;
end;
definition
let L be Z_Lattice;
let F be FinSequence of DivisibleMod(L);
let f be Function of DivisibleMod(L), INT.Ring;
let v be Vector of DivisibleMod(L);
func ScFS(v, f, F) -> FinSequence of F_Real means :defScFSDM:
len it = len F & for i being Nat st i in dom it
holds it.i = (ScProductDM(L)).(v, f.(F/.i) * F/.i);
existence
proof
deffunc X(object) = (ScProductDM(L)).(v, f.(F/.$1) * F/.$1);
consider G be FinSequence such that
A1: len G = len F & for i being Nat st i in dom G
holds G.i = X(i) from FINSEQ_1:sch 2;
rng G c= the carrier of F_Real
proof
let x be object such that
B1: x in rng G;
consider z be object such that
B2: z in dom G & x = G.z by B1,FUNCT_1:def 3;
x = (ScProductDM(L)).(v, f.(F/.z) * F/.z) by A1,B2;
hence thesis;
end;
then reconsider G as FinSequence of F_Real by FINSEQ_1:def 4;
take G;
thus thesis by A1;
end;
uniqueness
proof
let f1, f2 be FinSequence of F_Real;
assume AS1: len f1 = len F & for i being Nat st i in dom f1
holds f1.i = (ScProductDM(L)).(v, f.(F/.i) * F/.i);
assume AS2: len f2 = len F & for i being Nat st i in dom f2
holds f2.i = (ScProductDM(L)).(v, f.(F/.i) * F/.i);
A2: dom f1 = dom f2 by AS1,AS2,FINSEQ_3:29;
for k being Nat st k in dom f1 holds f1.k = f2.k
proof
let k be Nat;
assume
B1: k in dom f1;
hence f1.k = (ScProductDM(L)).(v, f.(F/.k) * F/.k) by AS1
.= f2.k by AS2,A2,B1;
end;
hence thesis by AS1,AS2,FINSEQ_3:29;
end;
end;
theorem ThScFSDM1:
for L being Z_Lattice, f being Function of DivisibleMod(L), INT.Ring,
F being FinSequence of DivisibleMod(L),
v, u being Vector of DivisibleMod(L), i being Nat
st i in dom F & u = F.i
holds (ScFS(v, f, F)).i = (ScProductDM(L)).(v, f.u * u)
proof
let L be Z_Lattice, f be Function of DivisibleMod(L), INT.Ring,
F be FinSequence of DivisibleMod(L),
v, u be Vector of DivisibleMod(L), i be Nat such that
A1: i in dom F & u = F.i;
A2: F/.i = F.i by A1,PARTFUN1:def 6;
len(ScFS(v, f, F)) = len F by defScFSDM;
then i in dom(ScFS(v, f, F)) by A1,FINSEQ_3:29;
hence thesis by A1,A2,defScFSDM;
end;
theorem ThScFSDM3:
for L being Z_Lattice, f being Function of DivisibleMod(L), INT.Ring,
v, u being Vector of DivisibleMod(L) holds
ScFS(v, f, <* u *>) = <* (ScProductDM(L)).(v, f.u * u) *>
proof
let L be Z_Lattice, f be Function of DivisibleMod(L), INT.Ring;
let v, u be Vector of DivisibleMod(L);
A1: 1 in {1} by TARSKI:def 1;
A2: len ScFS(v, f, <* u *>) = len <* u *> by defScFSDM
.= 1 by FINSEQ_1:40;
then dom(ScFS(v, f, <* u *>)) = {1} by FINSEQ_1:2,FINSEQ_1:def 3;
then (ScFS(v, f, <* u *>)).1
= (ScProductDM(L)).(v, f.(<* u *>/.1) * <* u *>/.1) by A1,defScFSDM
.= (ScProductDM(L)).(v, f.(<* u *>/.1) * u) by FINSEQ_4:16
.= (ScProductDM(L)).(v, f.u * u) by FINSEQ_4:16;
hence thesis by A2,FINSEQ_1:40;
end;
theorem ThScFSDM6:
for L being Z_Lattice, f being Function of DivisibleMod(L), INT.Ring,
F, G being FinSequence of DivisibleMod(L),
v being Vector of DivisibleMod(L) holds
ScFS(v, f, F ^ G) = ScFS(v, f, F) ^ ScFS(v, f, G)
proof
let L be Z_Lattice, f be Function of DivisibleMod(L), INT.Ring,
F, G be FinSequence of DivisibleMod(L),
v be Vector of DivisibleMod(L);
set H = ScFS(v, f, F) ^ ScFS(v, f, G);
set I = F ^ G;
A1: len F = len(ScFS(v, f, F)) by defScFSDM;
A2: len H = len(ScFS(v, f, F)) + len(ScFS(v, f, G)) by FINSEQ_1:22
.= len F + len(ScFS(v, f, G)) by defScFSDM
.= len F + len G by defScFSDM
.= len I by FINSEQ_1:22;
A3: len G = len(ScFS(v, f, G)) by defScFSDM;
now
let k be Nat;
assume
A4: k in dom H; then
per cases by FINSEQ_1:25;
suppose
A5: k in dom(ScFS(v, f, F)); then
A6: k in dom F by A1,FINSEQ_3:29; then
A7: k in dom(F ^ G) by FINSEQ_3:22;
A8: F/.k = F.k by A6,PARTFUN1:def 6
.= (F ^ G).k by A6,FINSEQ_1:def 7
.= (F ^ G)/.k by A7,PARTFUN1:def 6;
thus H.k = (ScFS(v, f, F)).k by A5,FINSEQ_1:def 7
.= (ScProductDM(L)).(v, f.(I/.k) * I/.k) by A5,A8,defScFSDM;
end;
suppose
A9: ex n being Nat st n in dom(ScFS(v, f, G))
& k = len(ScFS(v, f, F)) + n;
A10: k in dom I by A2,A4,FINSEQ_3:29;
consider n be Nat such that
A11: n in dom(ScFS(v, f, G)) and
A12: k = len(ScFS(v, f, F)) + n by A9;
A13: n in dom G by A3,A11,FINSEQ_3:29; then
A14: G/.n = G.n by PARTFUN1:def 6
.= (F ^ G).k by A1,A12,A13,FINSEQ_1:def 7
.= (F ^ G)/.k by A10,PARTFUN1:def 6;
thus H.k = (ScFS(v, f, G)).n by A11,A12,FINSEQ_1:def 7
.= (ScProductDM(L)).(v, f.(I/.k) * I/.k) by A11,A14,defScFSDM;
end;
end;
hence thesis by A2,defScFSDM;
end;
definition
let L be Z_Lattice;
let l be Linear_Combination of DivisibleMod(L);
let v be Vector of DivisibleMod(L);
func SumSc(v, l) -> Element of F_Real means :defSumScDM:
ex F being FinSequence of DivisibleMod(L) st
F is one-to-one & rng F = Carrier(l) & it = Sum(ScFS(v, l, F));
existence
proof
consider F be FinSequence such that
A1: rng F = Carrier(l) & F is one-to-one by FINSEQ_4:58;
reconsider F as FinSequence of DivisibleMod(L) by A1,FINSEQ_1:def 4;
take Sum(ScFS(v, l, F)), F;
thus thesis by A1;
end;
uniqueness
proof
let r1, r2 be Element of F_Real;
given F1 be FinSequence of DivisibleMod(L) such that
A1: F1 is one-to-one and
A2: rng F1 = Carrier(l) and
A3: r1 = Sum(ScFS(v, l, F1));
given F2 be FinSequence of DivisibleMod(L) such that
A4: F2 is one-to-one and
A5: rng F2 = Carrier(l) and
A6: r2 = Sum(ScFS(v, l, F2));
deffunc F(object) = F1".(F2.$1);
A7: len F1 = len F2 by A1,A2,A4,A5,FINSEQ_1:48; then
A8: dom F1 = dom F2 by FINSEQ_3:29;
A9: for x being object st x in dom F1 holds F(x) in dom F1
proof
let x be object;
assume x in dom F1;
then F2.x in rng F1 by A2,A5,A8,FUNCT_1:3;
then F2.x in dom(F1") by A1,FUNCT_1:33;
then F1".(F2.x) in rng(F1") by FUNCT_1:3;
hence thesis by A1,FUNCT_1:33;
end;
consider f be Function of dom F1, dom F1 such that
A10: for x being object st x in dom F1 holds f.x = F(x)
from FUNCT_2:sch 2(A9);
for x1, x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1, x2 be object such that
B1: x1 in dom f & x2 in dom f & f.x1 = f.x2;
F2.x1 in rng F1 by A2,A5,A8,B1,FUNCT_1:3;
then B4: F2.x1 in dom(F1") by A1,FUNCT_1:33;
F2.x2 in rng F1 by A2,A5,A8,B1,FUNCT_1:3;
then B7: F2.x2 in dom(F1") by A1,FUNCT_1:33;
F1".(F2.x1) = f.x1 by A10,B1
.= F1".(F2.x2) by A10,B1;
then F2.x1 = F2.x2 by A1,B4,B7,FUNCT_1:def 4;
hence thesis by A4,A8,B1;
end;
then A11: f is one-to-one;
dom F1 c= rng f
proof
let y be object such that
B1: y in dom F1;
F1.y in rng F2 by A2,A5,B1,FUNCT_1:3;
then consider x be object such that
B2: x in dom F2 & F2.x = F1.y by FUNCT_1:def 3;
B3: f.x = F1".(F2.x) by A8,A10,B2
.= y by A1,B1,B2,FUNCT_1:34;
x in dom f by A8,B2,FUNCT_2:def 1;
hence thesis by B3,FUNCT_1:3;
end;
then A12: rng f = dom F1;
then reconsider f as Permutation of dom F1 by A11,FUNCT_2:57;
reconsider G1 = ScFS(v, l, F1) as FinSequence of F_Real;
set G2 = ScFS(v, l, F2);
A14: len G2 = len F2 by defScFSDM;
A15: dom F1 = Seg(len F1) by FINSEQ_1:def 3
.= Seg(len G1) by defScFSDM
.= dom G1 by FINSEQ_1:def 3;
then reconsider f as Permutation of dom G1;
A16: len G1 = len F2 by A7,defScFSDM
.= len G2 by defScFSDM;
for i being Nat st i in dom G2 holds G2.i = G1.(f.i)
proof
let i be Nat such that
B1: i in dom G2;
B2: G2.i = (ScProductDM(L)).(v, l.(F2/.i) * F2/.i) by B1,defScFSDM;
B3: i in dom F2 by A14,B1,FINSEQ_3:29;
then reconsider u = F2.i as Element of DivisibleMod(L) by FINSEQ_2:11;
B4: i in dom f by A8,B3,FUNCT_2:def 1;
then f.i in dom F1 by A12,FUNCT_1:3;
then reconsider m = f.i as Element of NAT;
reconsider w = F1.m as Element of DivisibleMod(L)
by A12,B4,FINSEQ_2:11,FUNCT_1:3;
B5: F2.i in rng F1 by A2,A5,B3,FUNCT_1:3;
B6: F1.(f.i) = F1.(F1".(F2.i)) by A8,A10,B3
.= F2.i by A1,B5,FUNCT_1:35;
F1.m = F1/.m & F2.i = F2/.i by A12,B3,B4,FUNCT_1:3,PARTFUN1:def 6;
hence G2.i = G1.(f.i) by A12,A15,B2,B4,B6,defScFSDM,FUNCT_1:3;
end;
hence thesis by A3,A6,A16,RLVECT_2:6;
end;
end;
theorem LmSumScDM11:
for L being Z_Lattice, v being Vector of DivisibleMod(L) holds
SumSc(v, ZeroLC(DivisibleMod(L))) = 0.F_Real
proof
let L be Z_Lattice, v be Vector of DivisibleMod(L);
consider F be FinSequence of DivisibleMod(L) such that
A1: F is one-to-one & rng F = Carrier(ZeroLC(DivisibleMod(L))) &
SumSc(v,ZeroLC(DivisibleMod(L)))
= Sum(ScFS(v, ZeroLC(DivisibleMod(L)),F)) by defSumScDM;
F = {} by A1,VECTSP_6:def 3;
then len(ScFS(v, ZeroLC(DivisibleMod(L)),F)) = 0 by defScFSDM;
hence thesis by A1,RLVECT_1:75;
end;
theorem
for L being Z_Lattice, v being Vector of DivisibleMod(L),
l being Linear_Combination of {}(the carrier of DivisibleMod(L))
holds SumSc(v, l) = 0.F_Real
proof
let L be Z_Lattice, v be Vector of DivisibleMod(L),
l be Linear_Combination of {}(the carrier of DivisibleMod(L));
l = ZeroLC(DivisibleMod(L)) by VECTSP_6:6;
hence thesis by LmSumScDM11;
end;
theorem LmSumScDM13:
for L being Z_Lattice, v being Vector of DivisibleMod(L),
l being Linear_Combination of DivisibleMod(L)
st Carrier l = {}
holds SumSc(v, l) = 0.F_Real
proof
let L be Z_Lattice, v be Vector of DivisibleMod(L),
l be Linear_Combination of DivisibleMod(L) such that
A1: Carrier l = {};
l = ZeroLC(DivisibleMod(L)) by A1,VECTSP_6:def 3;
hence thesis by LmSumScDM11;
end;
theorem LmSumScDM14:
for L being Z_Lattice, v, u being Vector of DivisibleMod(L),
l being Linear_Combination of {u}
holds SumSc(v, l) = (ScProductDM(L)).(v, l.u * u)
proof
let L be Z_Lattice, v, u be Vector of DivisibleMod(L),
l be Linear_Combination of {u};
per cases by ZFMISC_1:33,VECTSP_6:def 4;
suppose Carrier(l) = {};
then A2: l = ZeroLC(DivisibleMod(L)) by VECTSP_6:def 3;
hence SumSc(v, l) = 0.F_Real by LmSumScDM11
.= (ScProductDM(L)).(v, 0.DivisibleMod(L)) by ZMODLAT2:14
.= (ScProductDM(L)).(v, 0.INT.Ring * u) by VECTSP_1:14
.= (ScProductDM(L)).(v, l.u * u) by A2,VECTSP_6:3;
end;
suppose Carrier(l) = {u};
then consider F be FinSequence of DivisibleMod(L) such that
A3: F is one-to-one & rng F = {u} & SumSc(v, l) = Sum(ScFS(v, l, F))
by defSumScDM;
F = <* u *> by A3,FINSEQ_3:97;
then ScFS(v, l, F) = <* (ScProductDM(L)).(v, l.u * u) *> by ThScFSDM3;
hence thesis by A3,RLVECT_1:44;
end;
end;
theorem LmSumScDM1X:
for L being Z_Lattice, v being Vector of DivisibleMod(L),
l1, l2 being Linear_Combination of DivisibleMod(L)
holds SumSc(v, l1+l2) = SumSc(v, l1) + SumSc(v, l2)
proof
let L be Z_Lattice, w be Vector of DivisibleMod(L),
l1, l2 be Linear_Combination of DivisibleMod(L);
set A = Carrier(l1 + l2) \/ Carrier(l1) \/ Carrier(l2);
set C1 = A \ Carrier(l1);
consider p be FinSequence such that
A1: rng p = C1 and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of DivisibleMod(L) by A1,FINSEQ_1:def 4;
A3: A = Carrier(l1) \/ (Carrier(l1 + l2) \/ Carrier(l2)) by XBOOLE_1:4;
set C3 = A \ Carrier(l1 + l2);
consider r be FinSequence such that
A4: rng r = C3 and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r as FinSequence of DivisibleMod(L) by A4,FINSEQ_1:def 4;
A6: A = Carrier(l1 + l2) \/ (Carrier(l1) \/ Carrier(l2)) by XBOOLE_1:4;
set C2 = A \ Carrier(l2);
consider q be FinSequence such that
A7: rng q = C2 and
A8: q is one-to-one by FINSEQ_4:58;
reconsider q as FinSequence of DivisibleMod(L) by A7,FINSEQ_1:def 4;
consider F be FinSequence of DivisibleMod(L) such that
A9: F is one-to-one and
A10: rng F = Carrier(l1 + l2) and
A11: SumSc(w, l1 + l2) = Sum(ScFS(w, l1 + l2, F)) by defSumScDM;
set FF = F ^ r;
consider G be FinSequence of DivisibleMod(L) such that
A12: G is one-to-one and
A13: rng G = Carrier(l1) and
A14: SumSc(w, l1) = Sum(ScFS(w, l1, G)) by defSumScDM;
rng FF = rng F \/ rng r by FINSEQ_1:31;
then rng FF = Carrier(l1 + l2) \/ A by A10,A4,XBOOLE_1:39; then
A15: rng FF = A by A6,XBOOLE_1:7,12;
set GG = G ^ p;
rng GG = rng G \/ rng p by FINSEQ_1:31;
then rng GG = Carrier(l1) \/ A by A13,A1,XBOOLE_1:39; then
A16: rng GG = A by A3,XBOOLE_1:7,12;
rng F misses rng r
proof
set x = the Element of rng F /\ rng r;
assume not thesis;
then x in Carrier(l1 + l2) & x in C3 by A10,A4,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A17: FF is one-to-one by A9,A5,FINSEQ_3:91;
rng G misses rng p
proof
set x = the Element of rng G /\ rng p;
assume not thesis;
then x in Carrier(l1) & x in C1 by A13,A1,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A18: GG is one-to-one by A12,A2,FINSEQ_3:91; then
A19: len GG = len FF by A17,A16,A15,FINSEQ_1:48;
deffunc F(Nat) = FF <- (GG.$1);
consider P be FinSequence such that
A20: len P = len FF and
A21: for k being Nat st k in dom P holds P.k = F(k) from FINSEQ_1:sch 2;
A22: dom P = Seg len FF by A20,FINSEQ_1:def 3;
A23:
now
let x be object;
assume
A24: x in dom GG;
then reconsider n = x as Element of NAT;
GG.n in rng FF by A16,A15,A24,FUNCT_1:def 3; then
A25: FF just_once_values GG.n by A17,FINSEQ_4:8;
n in Seg(len FF) by A19,A24,FINSEQ_1:def 3;
then FF.(P.n) = FF.(FF <- (GG.n)) by A21,A22
.= GG.n by A25,FINSEQ_4:def 3;
hence GG.x = FF.(P.x);
end;
A26: rng P c= dom FF
proof
let x be object;
assume x in rng P;
then consider y be object such that
A27: y in dom P and
A28: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A27;
y in dom GG by A19,A20,A27,FINSEQ_3:29;
then GG.y in rng FF by A16,A15,FUNCT_1:def 3;
then
A29: FF just_once_values GG.y by A17,FINSEQ_4:8;
P.y = FF <- (GG.y) by A21,A27;
hence thesis by A28,A29,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom P & P.x in dom FF
proof
assume x in dom GG;
then x in Seg(len P) by A19,A20,FINSEQ_1:def 3;
hence x in dom P by FINSEQ_1:def 3;
then P.x in rng P by FUNCT_1:def 3;
hence thesis by A26;
end;
assume that
A30: x in dom P and
P.x in dom FF;
x in Seg(len P) by A30,FINSEQ_1:def 3;
hence x in dom GG by A19,A20,FINSEQ_1:def 3;
end; then
A31: GG = FF * P by A23,FUNCT_1:10;
dom FF c= rng P
proof
set f = FF" * GG;
let x be object;
assume
A32: x in dom FF;
dom(FF") = rng GG by A17,A16,A15,FUNCT_1:33; then
A33: rng f = rng(FF") by RELAT_1:28
.= dom FF by A17,FUNCT_1:33;
f = FF " * FF * P by A31,RELAT_1:36
.= id(dom FF) * P by A17,FUNCT_1:39
.= P by A26,RELAT_1:53;
hence thesis by A32,A33;
end; then
A34: dom FF = rng P by A26;
A35: len r = len(ScFS(w, l1 + l2, r)) by defScFSDM;
B1: dom r = Seg(len r) by FINSEQ_1:def 3
.= Seg(len(ScFS(w, l1 + l2, r))) by defScFSDM
.= dom(ScFS(w, l1 + l2, r)) by FINSEQ_1:def 3;
now
let k be Nat;
assume
A36: k in dom(ScFS(w, l1 + l2, r));
then r/.k = r.k by B1,PARTFUN1:def 6;
then r/.k in C3 by A4,A36,B1,FUNCT_1:def 3; then
A37: not r/.k in Carrier((l1 + l2)) by XBOOLE_0:def 5;
(ScFS(w, l1 + l2, r)).k = (ScProductDM(L)).(w, (l1 + l2).(r/.k) * r/.k)
by A36,defScFSDM;
then (ScFS(w, l1 + l2, r)).k = (ScProductDM(L)).(w, 0.INT.Ring * r/.k)
by A37
.= (ScProductDM(L)).(w, 0.DivisibleMod(L)) by VECTSP_1:14
.= 0.F_Real by ZMODLAT2:14;
hence (ScFS(w, l1 + l2, r)).k = - (ScFS(w, l1 + l2, r)).k
.= - (ScFS(w, l1 + l2, r))/.k by A36,PARTFUN1:def 6;
end;
then A38: Sum(ScFS(w, l1 + l2, r)) = - Sum(ScFS(w, l1 + l2, r))
by A35,RLVECT_2:4;
A39: len p = len(ScFS(w, l1, p)) by defScFSDM;
B1: dom p = Seg(len p) by FINSEQ_1:def 3
.= Seg(len(ScFS(w, l1, p))) by defScFSDM
.= dom(ScFS(w, l1, p)) by FINSEQ_1:def 3;
now
let k be Nat;
assume
A40: k in dom(ScFS(w, l1, p));
then p/.k = p.k by B1,PARTFUN1:def 6;
then p/.k in C1 by A1,A40,B1,FUNCT_1:def 3; then
A41: not p/.k in Carrier(l1) by XBOOLE_0:def 5;
(ScFS(w, l1, p)).k = (ScProductDM(L)).(w, l1.(p/.k) * p/.k)
by A40,defScFSDM;
then (ScFS(w, l1, p)).k = (ScProductDM(L)).(w, 0.INT.Ring * p/.k) by A41
.= (ScProductDM(L)).(w, 0.DivisibleMod(L)) by VECTSP_1:14
.= 0.F_Real by ZMODLAT2:14;
hence (ScFS(w, l1, p)).k = - (ScFS(w, l1, p)).k
.= - (ScFS(w, l1, p))/.k by A40,PARTFUN1:def 6;
end;
then A42: Sum(ScFS(w, l1, p)) = -Sum(ScFS(w, l1, p)) by A39,RLVECT_2:4;
A43: len q = len(ScFS(w, l2, q)) by defScFSDM; then
B1: dom q = dom(ScFS(w, l2, q)) by FINSEQ_3:29;
now
let k be Nat;
assume
A44: k in dom(ScFS(w, l2, q));
then q/.k = q.k by B1,PARTFUN1:def 6;
then q/.k in C2 by A7,A44,B1,FUNCT_1:def 3;
then
A45: not q/.k in Carrier(l2) by XBOOLE_0:def 5;
(ScFS(w, l2, q)).k = (ScProductDM(L)).(w, l2.(q/.k) * q/.k)
by A44,defScFSDM;
then (ScFS(w, l2, q)).k = (ScProductDM(L)).(w, 0.INT.Ring * q/.k) by A45
.= (ScProductDM(L)).(w, 0.DivisibleMod(L)) by VECTSP_1:14
.= 0.F_Real by ZMODLAT2:14;
hence (ScFS(w, l2, q)).k = -(ScFS(w, l2, q)).k
.= -(ScFS(w, l2, q))/.k by A44,PARTFUN1:def 6;
end;
then A46: Sum(ScFS(w, l2, q)) = - Sum(ScFS(w, l2, q)) by A43,RLVECT_2:4;
set g = ScFS(w, l1, GG);
A47: len g = len GG by defScFSDM; then
A48: Seg len GG = dom g by FINSEQ_1:def 3;
set f = ScFS(w, l1 + l2, FF);
consider H be FinSequence of DivisibleMod(L) such that
A49: H is one-to-one and
A50: rng H = Carrier(l2) and
A51: Sum(ScFS(w, l2, H)) = SumSc(w, l2) by defSumScDM;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of rng H /\ rng q;
assume not thesis;
then x in Carrier(l2) & x in C2 by A50,A7,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end; then
A52: HH is one-to-one by A49,A8,FINSEQ_3:91;
rng HH = rng H \/ rng q by FINSEQ_1:31;
then rng HH = Carrier(l2) \/ A by A50,A7,XBOOLE_1:39; then
A53: rng HH = A by XBOOLE_1:7,12; then
A54: len GG = len HH by A52,A18,A16,FINSEQ_1:48; then
B1: dom GG = dom HH by FINSEQ_3:29;
deffunc F(Nat) = HH <- (GG.$1);
consider R be FinSequence such that
A55: len R = len HH and
A56: for k being Nat st k in dom R holds R.k = F(k) from FINSEQ_1:sch 2;
A57: dom R = dom HH by A55,FINSEQ_3:29;
A58:
now
let x be object;
assume
A59: x in dom GG;
then reconsider n = x as Element of NAT;
GG.n in rng HH by A16,A53,A59,FUNCT_1:def 3; then
A60: HH just_once_values GG.n by A52,FINSEQ_4:8;
HH.(R.n) = HH.(HH <- (GG.n)) by A56,A57,B1,A59
.= GG.n by A60,FINSEQ_4:def 3;
hence GG.x = HH.(R.x);
end;
A61: rng R c= dom HH
proof
let x be object;
assume x in rng R;
then consider y be object such that
A62: y in dom R and
A63: R.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A62;
y in dom GG by A54,A55,A62,FINSEQ_3:29;
then GG.y in rng HH by A16,A53,FUNCT_1:def 3; then
A64: HH just_once_values GG.y by A52,FINSEQ_4:8;
R.y = HH <- (GG.y) by A56,A62;
hence thesis by A63,A64,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom R & R.x in dom HH
proof
assume x in dom GG;
hence x in dom R by A55,FINSEQ_3:29,A54;
then R.x in rng R by FUNCT_1:def 3;
hence thesis by A61;
end;
assume x in dom R & R.x in dom HH;
hence x in dom GG by A54,A55,FINSEQ_3:29;
end; then
A66: GG = HH * R by A58,FUNCT_1:10;
dom HH c= rng R
proof
set f = HH" * GG;
let x be object;
assume
A67: x in dom HH;
dom(HH") = rng GG by A52,A16,A53,FUNCT_1:33; then
A68: rng f = rng(HH") by RELAT_1:28
.= dom HH by A52,FUNCT_1:33;
f = HH " * HH * R by A66,RELAT_1:36
.= id(dom HH) * R by A52,FUNCT_1:39
.= R by A61,RELAT_1:53;
hence thesis by A67,A68;
end; then
A69: dom HH = rng R by A61;
set h = ScFS(w, l2, HH);
A70: Sum(h) = Sum(ScFS(w, l2, H) ^ ScFS(w, l2, q)) by ThScFSDM6
.= Sum(ScFS(w, l2, H)) + 0.F_Real by A46,RLVECT_1:41
.= Sum(ScFS(w, l2, H));
A71: Sum(g) = Sum(ScFS(w, l1, G) ^ ScFS(w, l1, p)) by ThScFSDM6
.= Sum(ScFS(w, l1, G)) + 0.F_Real by A42,RLVECT_1:41
.= Sum(ScFS(w, l1, G));
A72: dom P = dom FF by A20,FINSEQ_3:29;
A73: P is one-to-one by A20,A34,FINSEQ_3:29,FINSEQ_4:60;
A74: dom R = dom HH by A55,FINSEQ_3:29;
A75: R is one-to-one by A55,A69,FINSEQ_3:29,FINSEQ_4:60;
R is Function of dom HH, dom HH by A61,A74,FUNCT_2:2; then
reconsider R as Permutation of dom HH by A69,A75,FUNCT_2:57;
A76: len h = len HH by defScFSDM;
then dom h = dom HH by FINSEQ_3:29;
then reconsider R as Permutation of dom h;
reconsider Hp = h * R as FinSequence of F_Real by FINSEQ_2:47;
A77: len Hp = len GG by A54,A76,FINSEQ_2:44;
reconsider P as Function of dom FF, dom FF by A26,A72,FUNCT_2:2;
reconsider P as Permutation of dom FF by A34,A73,FUNCT_2:57;
A78: len f = len FF by defScFSDM;
then dom f = dom FF by FINSEQ_3:29;
then reconsider P as Permutation of dom f;
reconsider Fp = f * P as FinSequence of F_Real by FINSEQ_2:47;
A79: Sum(f) = Sum(ScFS(w, l1 + l2, F) ^ ScFS(w, l1 + l2, r)) by ThScFSDM6
.= Sum(ScFS(w, l1 + l2, F)) + 0.F_Real by A38,RLVECT_1:41
.= Sum(ScFS(w, l1 + l2, F));
deffunc F(Nat) = g/.$1 + Hp/.$1;
consider I be FinSequence such that
A80: len I = len GG and
A81: for k being Nat st k in dom I holds I.k = F(k) from FINSEQ_1:sch 2;
A83: dom I = Seg len GG by A80,FINSEQ_1:def 3;
rng I c= the carrier of F_Real
proof
let x be object;
assume x in rng I;
then consider y be object such that
A84: y in dom I and
A85: I.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A84;
I.y = g/.y + Hp/.y by A81,A84;
hence thesis by A85;
end;
then reconsider I as FinSequence of F_Real by FINSEQ_1:def 4;
A86: len Fp = len I by A19,A78,A80,FINSEQ_2:44; then
X1: dom I = Seg(len I) & dom Fp = Seg(len I) by FINSEQ_1:def 3;
X2: dom Hp = Seg(len Hp) by FINSEQ_1:def 3
.= dom I by A54,A76,A80,FINSEQ_1:def 3,FINSEQ_2:44;
X3: dom HH = Seg(len HH) by FINSEQ_1:def 3
.= dom I by A18,A16,A52,A53,A80,FINSEQ_1:48,FINSEQ_1:def 3; then
X4: dom GG = dom I by A54,FINSEQ_3:29;
X5: dom g = Seg(len g) by FINSEQ_1:def 3
.= dom I by A80,defScFSDM,FINSEQ_1:def 3;
A87:
now
let k be Nat;
assume
A88: k in dom I; then
A90: Hp/.k = (h * R).k by X2,PARTFUN1:def 6
.= h.(R.k) by A88,X2,FUNCT_1:12;
set v = GG/.k;
A91: Fp.k = f.(P.k) by A88,X1,FUNCT_1:12;
R.k in dom R by A69,A74,A88,X3,FUNCT_1:def 3;
then reconsider j = R.k as Element of NAT by FINSEQ_3:23;
A94: HH.j = GG.k by A58,A88,X3,B1
.= GG/.k by A88,X3,B1,PARTFUN1:def 6;
A95: dom FF = dom GG by A19,FINSEQ_3:29;
then P.k in dom P by A34,A72,A88,X3,FUNCT_1:def 3,B1;
then reconsider l = P.k as Element of NAT by FINSEQ_3:23;
A96: FF.l = GG.k by A23,A88,X3,B1
.= GG/.k by A88,X3,B1,PARTFUN1:def 6;
R.k in dom HH by A69,A74,A88,X3,FUNCT_1:def 3; then
A97: h.j = (ScProductDM(L)).(w, l2.v * v) by A94,ThScFSDM1;
P.k in dom FF by A34,A72,A88,A95,X4,FUNCT_1:def 3; then
A98: f.l = (ScProductDM(L)).(w, (l1 + l2).v * v) by A96,ThScFSDM1
.= (ScProductDM(L)).(w, (l1.v + l2.v) * v) by VECTSP_6:22
.= (ScProductDM(L)).(w, l1.v * v + l2.v * v) by VECTSP_1:def 15
.= (ScProductDM(L)).(w, l1.v * v) + (ScProductDM(L)).(w, l2.v * v)
by ZMODLAT2:12;
g/.k = g.k by A88,X5,PARTFUN1:def 6
.= (ScProductDM(L)).(w, l1.v * v) by A88,X5,defScFSDM;
hence I.k = Fp.k by A81,A88,A90,A97,A91,A98;
end;
dom I = Seg(len I) & dom Fp = Seg(len I) by A86,FINSEQ_1:def 3;
then A100: I = Fp by A87;
Sum(Fp) = Sum(f) & Sum(Hp) = Sum(h) by RLVECT_2:7;
hence thesis
by A11,A14,A47,A48,A51,A71,A70,A77,A79,A80,A81,A83,A100,RLVECT_2:2;
end;
theorem ThSumScDM1:
for L being Z_Lattice, l being Linear_Combination of DivisibleMod(L),
v being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(v, Sum(l)) = SumSc(v, l)
proof
defpred P[Nat] means
for L being Z_Lattice, l being Linear_Combination of DivisibleMod(L),
v being Vector of DivisibleMod(L) st card(Carrier l) = $1 holds
(ScProductDM(L)).(v, Sum(l)) = SumSc(v, l);
A1: P[0]
proof
let L be Z_Lattice, l be Linear_Combination of DivisibleMod(L),
v be Vector of DivisibleMod(L) such that
B1: card(Carrier l) = 0;
B2: Carrier l = {} by B1;
then Sum(l) = 0.DivisibleMod(L) by VECTSP_6:19;
then (ScProductDM(L)).(v, Sum(l)) = 0.F_Real by ZMODLAT2:14;
hence thesis by B2,LmSumScDM13;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let L be Z_Lattice, l be Linear_Combination of DivisibleMod(L),
v be Vector of DivisibleMod(L) such that
B2: card(Carrier l) = n+1;
Carrier l <> {} by B2;
then consider u be object such that
B3: u in Carrier l by XBOOLE_0:def 1;
reconsider u as Element of DivisibleMod(L) by B3;
B4: card(Carrier(l) \ {u}) = card(Carrier l) - card{u}
by B3,CARD_2:44,ZFMISC_1:31
.= n+1 - 1 by B2,CARD_2:42
.= n;
B5: Carrier(l) = (Carrier(l) \ {u}) \/ {u}
by B3,XBOOLE_1:45,ZFMISC_1:31;
B6: (Carrier(l) \ {u}) /\ {u} = {} by XBOOLE_0:def 7,XBOOLE_1:79;
l is Linear_Combination of Carrier(l) by VECTSP_6:7;
then consider l1 be Linear_Combination of (Carrier (l) \ {u}),
l2 be Linear_Combination of {u} such that
B7: l = l1 + l2 by B5,B6,ZMODUL04:26;
Sum(l) = Sum(l1) + Sum(l2) by B7,ZMODUL02:52;
then B8: (ScProductDM(L)).(v, Sum(l))
= (ScProductDM(L)).(v, Sum(l1)) + (ScProductDM(L)).(v, Sum(l2))
by ZMODLAT2:12;
for x being Vector of DivisibleMod(L) st x in (Carrier(l) \ {u})
holds x in Carrier(l1)
proof
let x be Vector of DivisibleMod(L) such that
C1: x in (Carrier(l) \ {u});
x in Carrier(l) by C1,XBOOLE_0:def 5;
then C2: l.x <> 0.INT.Ring by VECTSP_6:2;
C3: Carrier(l2) c= {u} by VECTSP_6:def 4;
C4: l.x = l1.x + l2.x by B7,VECTSP_6:22;
not x in Carrier(l2) by C1,C3,XBOOLE_0:def 5;
then l1.x <> 0.INT.Ring by C2,C4;
hence thesis;
end;
then (Carrier(l) \ {u}) c= Carrier(l1);
then Carrier(l1) = (Carrier(l) \ {u}) by VECTSP_6:def 4;
then B10: (ScProductDM(L)).(v, Sum(l1)) = SumSc(v, l1) by B1,B4;
SumSc(v, l2) = (ScProductDM(L)).(v, l2.u * u) by LmSumScDM14
.= (ScProductDM(L)).(v, Sum(l2)) by VECTSP_6:17;
hence thesis by B7,B8,B10,LmSumScDM1X;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let L be Z_Lattice, l be Linear_Combination of DivisibleMod(L),
v be Vector of DivisibleMod(L);
reconsider n = card (Carrier l) as Nat;
P[n] by A3;
hence thesis;
end;
theorem INVMN1:
for n being Nat, M being Matrix of n, F_Real
for H being Matrix of n, F_Rat
st M = H & M is invertible
holds H is invertible & M ~ = H ~
proof
let n be Nat;
let M be Matrix of n, F_Real;
let H be Matrix of n, F_Rat;
assume AS: M = H & M is invertible;
then Det M is unital by LAPLACE:34;
then Det M is non zero; then
N1: 0.F_Real <> Det M by STRUCT_0:def 12;
then P0: 0.F_Rat <> Det H by AS,ZMODLAT2:54;
then Det H is non zero by STRUCT_0:def 12;
then Det H is unital;
hence A2: H is invertible by LAPLACE:34;
Q0: Indices (M) = [:(Seg n),(Seg n):] by MATRIX_0:24;
P1:len (M~) = n by MATRIX_0:24
.= len (H~) by MATRIX_0:24;
P2: width (M~) = n by MATRIX_0:24
.= width (H~) by MATRIX_0:24;
P3A: Indices (M~) = [:(Seg n),(Seg n):] by MATRIX_0:24;
P3B: Indices (H~) = [:(Seg n),(Seg n):] by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices M~
holds M~*(i,j) = H~*(i,j)
proof
let i, j be Nat;
assume P01: [i,j] in Indices M~;
then [i,j] in [:Seg n,Seg n:] by MATRIX_0:24;
then i in Seg n & j in Seg n by ZFMISC_1:87; then
P02: [j,i] in Indices M by Q0,ZFMISC_1:87;
set MM = Delete (M,j,i);
set HH = Delete (H,j,i);
MM = HH
proof
per cases;
suppose n <= 1; then
n - 1 <= 1-1 by XREAL_1:9; then
n -' 1 = 0 by XREAL_0:def 2;
hence MM = HH by MATRIX_0:22;
end;
suppose NN21: n > 1; then
NN2: n - 1 > 1 - 1 by XREAL_1:14;
reconsider k = n-1 as Nat by NN21;
n = k+1 & 0 < k by NN2;
hence Delete(M,j,i) = Delete(H,j,i) by AS,P02,ZMODLAT2:52;
end;
end; then
S1: (power F_Real).((- (1_F_Real)),(i + j)) * Minor (M,j,i)
= (power F_Rat).((- (1_F_Rat)),(i + j)) * Minor (H,j,i)
by ZMODLAT2:54,47;
F_Rat is domRing;
thus M~*(i,j) = (Det M)"
* (power F_Real).((- (1_F_Real)),(i + j)) * Minor (M,j,i)
by P01,LAPLACE:36,AS
.= (Det M)"
*( (power F_Real).((- (1_ F_Real)),(i + j)) * Minor (M,j,i))
.= (Det H)"
*( (power F_Rat).((- (1_F_Rat)),(i + j)) * Minor (H,j,i))
by AS,N1,S1,GAUSSINT:14,21,ZMODLAT2:54
.= (Det H)" * (power F_Rat).((- (1_F_Rat)),(i + j)) * Minor (H,j,i)
.= H~*(i,j) by A2,P01,P3A,P3B,LAPLACE:36;
end;
hence M~ = H~ by P1,P2,ZMATRLIN:4;
end;
theorem INVMN2:
for n being Nat, M being Matrix of n, F_Real
st M is Matrix of n, F_Rat & M is invertible
holds M~ is Matrix of n, F_Rat
proof
let n be Nat, M be Matrix of n, F_Real;
assume that
A1: M is Matrix of n, F_Rat and
A2: M is invertible;
reconsider H = M as Matrix of n, F_Rat by A1;
M ~ = H ~ by A2,INVMN1;
hence M ~ is Matrix of n, F_Rat;
end;
theorem ThGM3:
for L being non trivial RATional positive-definite Z_Lattice,
b being OrdBasis of L holds
(GramMatrix(b))~ is Matrix of dim(L),F_Rat
proof
let L be non trivial RATional positive-definite Z_Lattice,
b be OrdBasis of L;
GramMatrix(b) is Matrix of dim(L),F_Rat by ZMODLAT2:45;
hence thesis by INVMN2;
end;
theorem LmDE311A:
for X being finite Subset of RAT
ex a being Element of INT st
a <> 0 &
for r being Element of RAT st r in X holds a*r in INT
proof
defpred P[Nat] means
for X being finite Subset of RAT st card X = $1 holds
ex a being Element of INT st
a <> 0 &
for r being Element of RAT st r in X holds a*r in INT;
P1: P[0]
proof
let X be finite Subset of RAT;
assume AS: card X = 0;
reconsider a = 1 as Element of INT by NUMBERS:17;
take a;
thus a <> 0;
thus for r being Element of RAT st r in X holds a*r in INT by AS;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
let X be finite Subset of RAT;
assume AS2: card X = n+1;
then X <> {};
then consider x be object such that
A1: x in X by XBOOLE_0:def 1;
B6: {x} is Subset of X by A1,SUBSET_1:41;
set Y = X \{x};
reconsider Y as finite Subset of RAT;
D1: X = Y \/ {x} by B6,XBOOLE_1:45;
card Y = card X - card {x} by B6,CARD_2:44
.= n+1 - 1 by AS2,CARD_1:30
.= n;
then consider a0 be Element of INT such that
A4: a0 <> 0 and
A5: for r being Element of RAT st r in Y holds a0*r in INT by AS1;
reconsider x as Element of RAT by A1;
consider x0, ib0 be Integer such that
A6: ib0 > 0 & x = x0 / ib0 by RAT_1:1;
reconsider ia0 = a0 as Integer;
set ia = ia0*ib0;
reconsider a = ia as Element of INT by INT_1:def 2;
for r being Element of RAT st r in X holds a*r in INT
proof
let r be Element of RAT;
assume r in X;
then per cases by D1,XBOOLE_0:def 3;
suppose r in Y;
then reconsider iar = ia0*r as Integer by A5,INT_1:def 2;
a*r = ib0*iar;
hence a*r in INT by INT_1:def 2;
end;
suppose A72: r in {x};
a*r = ia0 * (ib0*r)
.= ia0 *(ib0*(x0/ib0)) by A6,A72,TARSKI:def 1
.= ia0*x0 by A6,XCMPLX_1:87;
hence a*r in INT by INT_1:def 2;
end;
end;
hence thesis by A4,A6;
end;
P3: for n being Nat holds P[n] from NAT_1: sch 2(P1,P2);
let X be finite Subset of RAT;
card X is Nat;
hence ex a being Element of INT st a <> 0 &
for r being Element of RAT st r in X holds a*r in INT by P3;
end;
theorem LmDE311:
for L being non trivial RATional positive-definite Z_Lattice,
b being OrdBasis of L holds
ex a being Element of F_Real st a is Element of INT.Ring &
a <> 0 &
a*((GramMatrix(b))~) is Matrix of dim(L),INT.Ring
proof
let L be non trivial RATional positive-definite Z_Lattice,
b be OrdBasis of L;
set G = (GramMatrix(b))~;
reconsider M = G as Matrix of dim(L),F_Rat by ThGM3;
A2: rng M c= (the carrier of F_Rat)*;
A5: len M = dim(L) & width M = dim(L) by MATRIX_0:24;
B1: for i, j being Nat st [i,j] in Indices G holds
G * (i,j) in the carrier of F_Rat
proof
let i, j be Nat;
assume B10: [i,j] in Indices G;
then consider p be FinSequence of F_Real such that
B11: p = G . i & G * (i,j) = p.j by MATRIX_0:def 5;
B12: i in dom G & j in Seg (width G) by ZFMISC_1:87,B10;
then p in rng G by B11,FUNCT_1:3;
then
B14:len p = width G by A5,MATRIX_0:def 3;
p in (the carrier of F_Rat)* by A2,B11,B12,FUNCT_1:3;
then p is FinSequence of F_Rat by FINSEQ_1:def 11; then
B15: rng p c= the carrier of F_Rat by FINSEQ_1:def 4;
j in dom p by B12,B14,FINSEQ_1:def 3;
hence G * (i,j) in the carrier of F_Rat by B11,B15,FUNCT_1:3;
end;
deffunc F(Nat,Nat) = G * ($1,$2);
set Dn = { F(u,v) where u is Element of NAT, v is Element of NAT :
u in Seg (len G) & v in Seg (width G) };
F1: Seg (len G) is finite;
F2: Seg (width G) is finite;
F3: Dn is finite from FRAENKEL:sch 22(F1,F2);
D2: {G * (i,j) where i,j is Nat : [i,j] in Indices G} c= Dn
proof
let x be object;
assume x in {G * (i,j) where i,j is Nat : [i,j] in Indices G};
then consider i,j be Nat such that
F40: x = G * (i,j) & [i,j] in Indices G;
i in dom G & j in Seg (width G) by ZFMISC_1:87,F40;
then i in Seg (len G) & j in Seg (width G) by FINSEQ_1:def 3;
hence x in Dn by F40;
end;
{G * (i,j) where i,j is Nat : [i,j] in Indices G}
c= the carrier of F_Rat
proof
let x be object;
assume x in {G * (i,j) where i,j is Nat : [i,j] in Indices G};
then consider i,j be Nat such that
D1: x = G * (i,j) & [i,j] in Indices G;
thus x in the carrier of F_Rat by B1,D1;
end;
then reconsider X = {G * (i,j) where i,j is Nat : [i,j] in Indices G}
as finite Subset of F_Rat by D2,F3;
consider a be Element of INT such that
A10: a <> 0 &
for r being Element of RAT st r in X holds a*r in INT by LmDE311A;
reconsider a as Element of F_Real by NUMBERS:15;
A6: len (a*G) = dim(L) & width (a*G) = dim(L) by MATRIX_0:24;
take a;
thus a is Element of INT.Ring & a <> 0 by A10;
for i, j being Nat st [i,j] in Indices (a*G) holds
(a*G) * (i,j) in the carrier of INT.Ring
proof
let i, j be Nat;
assume B1: [i,j] in Indices (a*G);
B2: Indices G = [:(Seg dim L),(Seg dim L):] by MATRIX_0:24
.= Indices (a*G) by MATRIX_0:24; then
B3: (a*G) * (i,j) = a * ( G * (i,j) ) by B1,MATRIX_3:def 5;
G * (i,j) in X by B1,B2;
hence (a*G) * (i,j) in the carrier of INT.Ring by A10,B3;
end;
hence thesis by A6,MATRIX_0:20,ZMATRLIN:5;
end;
LM0:for n being Nat, F being FinSequence of F_Real st F = Seg n --> 0.F_Real
holds Sum F = 0.F_Real
proof
let n be Nat, F be FinSequence of F_Real;
assume AS: F = Seg n --> 0.F_Real;
X2: len F = len F;
for k being Nat
for v being Element of F_Real st k in dom F & v = F.k
holds F.k = - v
proof
let k be Nat;
let v be Element of F_Real;
assume that X3: k in dom F and
X30: v = F.k;
X2: k in Seg n by AS,X3,FUNCT_2:def 1;
then v = 0.F_Real by AS,X30,FUNCOP_1:7;
hence F.k= -v by AS,X2,FUNCOP_1:7;
end;
then Sum F = -(Sum F) by X2,RLVECT_1:40;
hence Sum F = 0.F_Real;
end;
LM1: for L being Z_Lattice, F, F0 being FinSequence of L,
l being Linear_Combination of L, v being Vector of L
st F is one-to-one & F0 is one-to-one & Carrier(l) c= rng F
& canFS (Carrier(l)) = F0
holds Sum(ScFS(v, l, F)) = Sum(ScFS(v, l, F0))
proof
let L be Z_Lattice,
F, F0 be FinSequence of L,
l be Linear_Combination of L,
v be Vector of L;
assume that
A1: F is one-to-one and
A2: F0 is one-to-one and
A3: Carrier(l) c= rng F and
A4: canFS (Carrier(l)) = F0;
A51: card (dom F) = card (rng F) by A1,CARD_1:5,WELLORD2:def 4; then
A5: len F = card (rng F) by CARD_1:62;
Q1: F0 is one-to-one & rng F0 = Carrier(l) by A4,FUNCT_2:def 3;
FA5: card (dom F0) = card (rng F0) by A2,CARD_1:5,WELLORD2:def 4;
R1: len F0 = card (Carrier(l)) by A4,FINSEQ_1:93;
set CLN = (rng F) \ Carrier(l);
reconsider CLN as finite Subset of L;
set g = canFS(CLN);
Q2: g is one-to-one & rng g = CLN by FUNCT_2:def 3;
R2: len g = card CLN by FINSEQ_1:93;
reconsider g as FinSequence of L by Q2,FINSEQ_1:def 4;
set H = F0^g;
reconsider H as FinSequence of L;
rng F0 /\ rng g = Carrier(l) /\ CLN by Q1,FUNCT_2:def 3
.= (Carrier(l) /\ rng F) \ Carrier(l) by XBOOLE_1:49
.= Carrier(l) \ Carrier(l) by A3,XBOOLE_1:28
.= {} by XBOOLE_1:37;
then rng F0 misses rng g; then
Q31: H is one-to-one by A4,FINSEQ_3:91;
Q32: rng H = rng F0 \/ rng g by FINSEQ_1:31
.= Carrier(l) \/ (rng F \ Carrier(l)) by Q1,FUNCT_2:def 3
.= rng F by A3,XBOOLE_1:45;
C12: card CLN + card Carrier(l)
= card (rng F) - card Carrier(l) + card Carrier(l) by A3,CARD_2:44
.= card (rng F);
R3: len H = len F0 + len g by FINSEQ_1:22
.= card (rng F) by C12,R1,FINSEQ_1:93; then
R4: dom H = Seg card (rng F) by FINSEQ_1:def 3;
set P = F"*H;
T3: dom (F") = rng H by A1,Q32,FUNCT_1:33; then
T4: dom P = dom H by RELAT_1:27
.= Seg card (rng F) by R3,FINSEQ_1:def 3;
T5: rng P = rng (F") by RELAT_1:28,T3
.= dom F by FUNCT_1:33,A1
.= Seg card (rng F) by A5,FINSEQ_1:def 3;
then reconsider P as Function of Seg card (rng F),Seg card (rng F)
by T4,FUNCT_2:1;
P is onto by T5;
then reconsider P as Permutation of Seg card (rng F) by A1,Q31;
R5: len ScFS(v, l, F) = len F by defScFS
.= card (rng F) by A51,CARD_1:62; then
R6: dom ScFS(v, l, F) = Seg card (rng F) by FINSEQ_1:def 3;
len ScFS(v, l, F0) = len F0 by defScFS
.= card (rng F0) by FA5,CARD_1:62; then
XR6: dom ScFS(v, l, F0) = Seg card (rng F0) by FINSEQ_1:def 3;
R7: len ScFS(v, l, H) = card (rng F) by R3,defScFS; then
R8: dom ScFS(v, l, H) = Seg card (rng F) by FINSEQ_1:def 3;
R9: for i being Nat st i in dom (ScFS(v, l, F)) holds
(ScFS(v, l, H)).i = (ScFS(v, l, F)).(P.i)
proof
let i be Nat;
assume R90: i in dom (ScFS(v, l, F));
then i in dom (ScFS(v, l, H)) by R6,R7,FINSEQ_1:def 3; then
R92: (ScFS(v, l, H)).i = <; v, l.(H/.i) * H/.i ;> by defScFS;
S3: H.i in dom (F") by R4,R6,R90,T3,FUNCT_1:3;
then F".(H.i) in rng (F") by FUNCT_1:3; then
S4: F".(H.i) in dom F by FUNCT_1:33,A1;
S5: H.i in rng F by A1,FUNCT_1:33,S3;
F/.(P.i) = F/.(F".(H.i)) by R6,R90,T4,FUNCT_1:12
.= F.(F".(H.i)) by S4,PARTFUN1:def 6
.= H.i by FUNCT_1:35,A1,S5
.= H/.i by R4,R6,R90,PARTFUN1:def 6;
hence thesis by R6,R90,R92,defScFS,FUNCT_2:5;
end;
set K = Seg (card CLN) --> 0.F_Real;
rng K c= the carrier of F_Real;
then reconsider K as FinSequence of F_Real by FINSEQ_1:def 4;
K100: dom K = Seg (card CLN) by FUNCT_2:def 1;
K2: dom (ScFS(v, l, F0)^ K) = Seg (len (ScFS(v, l, F0)) + len K)
by FINSEQ_1:def 7
.= Seg (len F0 + len K) by defScFS
.= Seg (card (Carrier(l)) + card CLN ) by R1,K100,FINSEQ_1:def 3
.= dom ScFS(v, l, H) by C12,R7,FINSEQ_1:def 3;
for k being Nat st k in dom (ScFS(v, l, H)) holds
(ScFS(v, l, H)).k = (ScFS(v, l, F0)^ K).k
proof
let k be Nat;
assume K3: k in dom (ScFS(v, l, H)); then
L4: 1<=k & k <= card (rng F) by R8,FINSEQ_1:1;
L5: card (rng F) = len F0 + len g by C12,R1,FINSEQ_1:93;
K4: (ScFS(v, l, H)).k = <; v, l.(H/.k) * H/.k ;> by defScFS,K3;
per cases;
suppose CAS2: k <=len F0;
then CAS21: k in dom F0 by FINSEQ_3:25,L4;
then H.k = F0.k by FINSEQ_1:def 7;
then H.k = F0/.k by CAS21,PARTFUN1:def 6;
then
CAS3: H/.k = F0/.k by K3,R4,R8,PARTFUN1:def 6;
CAS4: k in dom (ScFS(v, l, F0)) by CAS2,L4,XR6,R1,Q1;
then (ScFS(v, l, F0)^ K) . k = (ScFS(v, l, F0)).k by FINSEQ_1:def 7
.= <; v, l.(F0/.k) *F0/.k ;> by CAS4,defScFS;
hence (ScFS(v, l, H)).k = (ScFS(v, l, F0)^ K).k by K3,CAS3,defScFS;
end;
suppose len F0 < k; then
CAS7:k - (len F0) > 0 by XREAL_1:50;
then k - (len F0) in NAT by INT_1:3;
then reconsider k1 = k - (len F0) as Nat;
CAS8:1 <= k1 by NAT_1:14,CAS7;
k1 <= len F0 + len g - len F0 by L4,L5,XREAL_1:9; then
CAS100: k1 in Seg (len g) by CAS8; then
CAS10: k1 in dom g by FINSEQ_1:def 3;
then H.(len F0 + k1) = g.k1 by FINSEQ_1:def 7;
then H.k in CLN by CAS10,Q2,FUNCT_1:3;
then H/.k in CLN by K3,R4,R8,PARTFUN1:def 6;
then CAS11: not H/.k in Carrier(l) by XBOOLE_0:def 5;
X1: (ScFS(v, l, F0)^ K).(len ScFS(v, l, F0) + k1) = K.k1
by CAS100,K100,R2,FINSEQ_1:def 7
.= 0.F_Real by R2,CAS100,FUNCOP_1:7;
CAS5: len ScFS(v, l, F0) + k1 = len F0 + k1 by defScFS;
(ScFS(v, l, H)).k = <; v, 0.INT.Ring *H/.k ;> by K4,CAS11
.= <; 0.INT.Ring *H/.k,v ;> by ZMODLAT1:def 3
.= 0.INT.Ring * <; H/.k,v ;> by ZMODLAT1:def 3
.= 0.INT.Ring;
hence (ScFS(v, l, H)).k = (ScFS(v, l, F0)^ K).k by CAS5,X1;
end;
end; then
R11: ScFS(v, l, H) = ScFS(v, l, F0)^ K by K2;
Sum (ScFS(v, l, H)) = Sum (ScFS(v, l, F0)) + Sum K by R11,RLVECT_1:41
.=Sum (ScFS(v, l, F0)) + 0.F_Real by LM0
.=Sum (ScFS(v, l, F0));
hence thesis by R6,R8,R9,R7,R5,RLVECT_2:6;
end;
theorem LmDE31:
for L being non trivial RATional positive-definite Z_Lattice,
b being OrdBasis of EMLat(L), i being Nat
st i in dom b holds
ex v being Vector of DivisibleMod(L)
st (ScProductDM(L)).(b/.i, v) = 1 &
(for j being Nat st i <> j & j in dom b holds
(ScProductDM(L)).(b/.j, v) = 0)
proof
let L be non trivial RATional positive-definite Z_Lattice,
b be OrdBasis of EMLat(L), i be Nat such that
A1: i in dom b;
A2: dim(L) = dim(EMLat(L)) by ZMODLAT2:42;
consider a be Element of F_Real such that
A3: a is Element of INT.Ring & a <> 0 &
a*((GramMatrix(b))~) is Matrix of dim(L),INT.Ring by A2,LmDE311;
((GramMatrix(b))~) is_reverse_of GramMatrix(b) by MATRIX_6:def 4;
then A5: ((GramMatrix(b))~)*(GramMatrix(b)) = 1.(F_Real,dim(EMLat(L)))
by MATRIX_6:def 2
.= 1.(F_Real,dim(L)) by ZMODLAT2:42;
len ((GramMatrix(b))~) = dim(EMLat(L)) by MATRIX_0:def 2;
then width((GramMatrix(b))~) = dim(EMLat(L)) by MATRIX_0:20
.= len(GramMatrix(b)) by MATRIX_0:def 2;
then A8: (a*((GramMatrix(b))~))*(GramMatrix(b))
= a*(1.(F_Real,dim(L))) by A5,MATRIX15:1;
AX1: len b = dim(EMLat(L)) by ZMATRLIN:49;
then A9: i in Seg(dim(L)) by A1,A2,FINSEQ_1:def 3;
A10: Indices(1.(F_Real,dim(L))) = [:Seg(dim(L)), Seg(dim(L)):]
by MATRIX_0:24;
then A11: [i, i] in Indices(1.(F_Real,dim(L))) by A9,ZFMISC_1:87;
A12: Indices(a*(1.(F_Real,dim(L)))) = [:Seg(dim(L)), Seg(dim(L)):]
by MATRIX_0:24;
then A14: [i, i] in Indices
((a*((GramMatrix(b))~))*(GramMatrix(b))) by A8,A9,ZFMISC_1:87;
AX3: width(a*((GramMatrix(b))~)) = dim(EMLat(L)) by MATRIX_0:23
.= len(GramMatrix(b)) by MATRIX_0:def 2;
A15: Line(a*((GramMatrix(b))~),i) "*" Col(GramMatrix(b),i)
= ((a*((GramMatrix(b))~))*(GramMatrix(b)))*(i,i)
by A14,AX3,MATRIX_3:def 4
.= a*((1.(F_Real,dim(L)))*(i,i)) by A8,A11,MATRIX_3:def 5
.= a*1.F_Real by A11,MATRIX_1:def 3
.= a;
A16: for j being Nat st i <> j & j in dom b holds
Line(a*((GramMatrix(b))~),i) "*" Col(GramMatrix(b),j) = 0
proof
let j be Nat such that
B1: i <> j & j in dom b;
B2: j in Seg(dim(L)) by A2,AX1,B1,FINSEQ_1:def 3;
then B3: [i, j] in Indices(1.(F_Real,dim(L))) by A9,A10,ZFMISC_1:87;
[i, j] in Indices
((a*((GramMatrix(b))~))*(GramMatrix(b))) by A8,A9,A12,B2,ZFMISC_1:87;
hence Line(a*((GramMatrix(b))~),i) "*" Col(GramMatrix(b),j)
= ((a*((GramMatrix(b))~))*(GramMatrix(b)))*(i,j) by AX3,MATRIX_3:def 4
.= a*((1.(F_Real,dim(L)))*(i,j)) by A8,B3,MATRIX_3:def 5
.= a*0.F_Real by B1,B3,MATRIX_1:def 3
.= 0;
end;
reconsider I = rng b as Basis of EMLat(L) by ZMATRLIN:def 5;
defpred P[object,object] means
($1 in I implies
for n being Nat st n = b".$1 & n in dom b holds
$2 = (a*((GramMatrix(b))~))*(i, n)) &
(not $1 in I implies $2 = 0.INT.Ring);
A17: for x being Element of EMLat(L)
ex y being Element of INT.Ring st P[x,y]
proof
let x be Element of EMLat(L);
per cases;
suppose B1: x in I;
b is one-to-one by ZMATRLIN:def 5;
then B3: b".x in dom b by B1,FUNCT_1:32;
then reconsider n = b".x as Nat;
reconsider aG = (a*((GramMatrix(b))~))
as Matrix of dim(L), INT.Ring by A3;
B4: Indices(aG) = [:Seg(dim(L)), Seg(dim(L)):] by MATRIX_0:24;
n in Seg(dim(L)) by A2,AX1,B3,FINSEQ_1:def 3;
then B5: [i, n] in Indices aG by A9,B4,ZFMISC_1:87;
aG*(i, n) is Element of INT.Ring;
then reconsider y = (a*((GramMatrix(b))~))*(i, n)
as Element of INT.Ring by B5,ZMATRLIN:1;
take y;
thus thesis by B1;
end;
suppose B1: not x in I;
take 0.INT.Ring;
thus thesis by B1;
end;
end;
consider l be Function of EMLat(L),INT.Ring such that
A18: for x being Element of EMLat(L) holds P[x,l.x]
from FUNCT_2:sch 3(A17);
l is Element of Funcs(the carrier of EMLat(L), the carrier of INT.Ring)
by FUNCT_2:8;
then reconsider l as Linear_Combination of EMLat(L) by A18,VECTSP_6:def 1;
reconsider ai = a as Element of INT.Ring by A3;
L1: len (GramMatrix(b)) = len b by MATRIX_0:24;
L2: width(a*((GramMatrix(b))~)) = dim(EMLat(L)) by MATRIX_0:23
.= len b by ZMATRLIN:49;
Q7: len Line(a*((GramMatrix(b))~),i) = len b by L2,MATRIX_0:def 7;
Q8: len Col(GramMatrix(b),i) = len b by L1,MATRIX_0:def 8;
A31: len(ScFS(b/.i, l, b)) = len b by defScFS
.= len(mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),i)))
by Q7,Q8,FINSEQ_2:72;
for k being Nat st 1 <= k & k <= len(ScFS(b/.i, l, b))
holds mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),i)).k
= ScFS(b/.i, l, b).k
proof
let k be Nat;
assume AS1: 1 <= k <= len(ScFS(b/.i, l, b));
then Q0: k in dom (ScFS(b/.i, l, b)) by FINSEQ_3:25;
D0: 1 <= k <= len b by AS1,defScFS; then
D1: k in dom b by FINSEQ_3:25;
then b.k in rng b by FUNCT_1:3; then
Q1: b/.k in I by PARTFUN1:def 6,D1;
b is one-to-one by ZMATRLIN:def 5; then
Q2: k = b".(b.k) by FUNCT_1:34,D1
.= b".(b/.k) by PARTFUN1:def 6,D1;
Q3: l.(b/.k) = (a*((GramMatrix(b))~))*(i, k) by Q1,Q2,D0,A18,FINSEQ_3:25;
k in Seg width (a*(GramMatrix(b))~) by D0,L2; then
Q4: (Line(a*((GramMatrix(b))~),i)).k = (a*((GramMatrix(b))~))*(i, k)
by MATRIX_0:def 7;
k in Seg (len GramMatrix(b)) by D0,L1;
then k in dom (GramMatrix(b)) by FINSEQ_1:def 3; then
Q5: (Col(GramMatrix(b),i)).k = (GramMatrix(b))*(k,i)
by MATRIX_0:def 8
.= (InnerProduct(EMLat(L))).(b/.k, b/.i) by D1,A1,ZMODLAT1:def 32
.= <; b/.k, b/.i ;>
.= <; b/.i, b/.k ;> by ZMODLAT1:def 3
.= (InnerProduct(EMLat(L))).(b/.i, b/.k)
.= (GramMatrix(b))*(i,k) by D1,A1,ZMODLAT1:def 32;
Seg len mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),i))
= Seg len b by Q7,Q8,FINSEQ_2:72
.= dom b by FINSEQ_1:def 3; then
Q6: k in dom mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),i))
by D1,FINSEQ_1:def 3;
<; b/.i, l.(b/.k) * (b/.k) ;>
= ((a*((GramMatrix(b))~))*(i, k)) * <; b/.i, b/.k ;> by Q3,ZMODLAT1:9
.= ((a*((GramMatrix(b))~))*(i, k)) * (InnerProduct(EMLat(L)))
.(b/.i, b/.k)
.= ((a*((GramMatrix(b))~))*(i, k)) * ((GramMatrix(b))*(i, k))
by D1,A1,ZMODLAT1:def 32
.= mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),i)).k
by Q4,Q5,Q6,FVSUM_1:60;
hence thesis by Q0,defScFS;
end; then
A32: mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),i))
= ScFS(b/.i, l, b) by A31;
set F = canFS(Carrier(l));
A303: F is one-to-one & rng F = Carrier(l) by FUNCT_2:def 3;
then reconsider F as FinSequence of EMLat(L) by FINSEQ_1:def 4;
A30: SumSc(b/.i, l) = Sum(ScFS(b/.i, l, F)) by A303,defSumSc;
A302: Carrier(l) c= rng b
proof
let x be object;
assume x in Carrier(l);
then consider v be Element of EMLat(L) such that
B30: x = v & l.v <> 0.INT.Ring;
assume not x in rng b;
hence contradiction by A18,B30;
end;
b is one-to-one by ZMATRLIN:def 5;
then A20: SumSc(b/.i, l) = a by A15,A30,A32,A302,LM1;
A21: for j being Nat st i <> j & j in dom b holds
<; b/.j, Sum(l) ;> = 0
proof
let j be Nat such that
BJ1: i <> j & j in dom b;
Q7: len Line(a*((GramMatrix(b))~),i) = len b by L2,MATRIX_0:def 7;
Q8: len Col(GramMatrix(b),j) = len b by L1,MATRIX_0:def 8;
A31: len(ScFS(b/.j, l, b)) = len b by defScFS
.= len(mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),j)))
by Q7,Q8,FINSEQ_2:72;
for k being Nat st 1 <= k & k <= len(ScFS(b/.j, l, b))
holds mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),j)).k
= ScFS(b/.j, l, b).k
proof
let k be Nat;
assume AS1: 1 <= k <= len(ScFS(b/.j, l, b));
then Q0: k in dom (ScFS(b/.j, l, b)) by FINSEQ_3:25;
D0: 1 <= k <= len b by AS1,defScFS; then
D1: k in dom b by FINSEQ_3:25;
then b.k in rng b by FUNCT_1:3; then
Q1: b/.k in I by PARTFUN1:def 6,D1;
b is one-to-one by ZMATRLIN:def 5;
then k = b".(b.k) by FUNCT_1:34,D1
.= b".(b/.k) by PARTFUN1:def 6,D1; then
Q3: l.(b/.k) = (a*((GramMatrix(b))~))*(i, k) by Q1,D0,A18,FINSEQ_3:25;
k in Seg width (a*(GramMatrix(b))~) by D0,L2; then
Q4: (Line(a*((GramMatrix(b))~),i)).k = (a*((GramMatrix(b))~))*(i, k)
by MATRIX_0:def 7;
k in Seg (len GramMatrix(b)) by D0,L1;
then k in dom (GramMatrix(b)) by FINSEQ_1:def 3; then
Q5: (Col(GramMatrix(b),j)).k = (GramMatrix(b))*(k,j)
by MATRIX_0:def 8
.= (InnerProduct(EMLat(L))).(b/.k, b/.j) by D1,BJ1,ZMODLAT1:def 32
.= <; b/.k, b/.j ;>
.= <; b/.j, b/.k ;> by ZMODLAT1:def 3
.= (InnerProduct(EMLat(L))).(b/.j, b/.k)
.= (GramMatrix(b))*(j,k) by D1,BJ1,ZMODLAT1:def 32;
Seg len mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),j))
= Seg len b by Q7,Q8,FINSEQ_2:72
.= dom b by FINSEQ_1:def 3;
then
Q6: k in dom mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),j))
by D1,FINSEQ_1:def 3;
<; b/.j, l.(b/.k) * (b/.k) ;>
= ((a*((GramMatrix(b))~))*(i, k)) * <; b/.j, b/.k ;>
by Q3,ZMODLAT1:9
.= ((a*((GramMatrix(b))~))*(i, k)) * (InnerProduct(EMLat(L)))
.(b/.j, b/.k)
.= ((a*((GramMatrix(b))~))*(i, k)) * ((GramMatrix(b))*(j, k))
by D1,BJ1,ZMODLAT1:def 32
.= mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),j)).k
by Q4,Q5,Q6,FVSUM_1:60;
hence thesis by Q0,defScFS;
end;
then mlt(Line(a*((GramMatrix(b))~),i), Col(GramMatrix(b),j))
= ScFS(b/.j, l, b) by A31;
then
A32: Sum(ScFS(b/.j, l, b))
= Line(a*((GramMatrix(b))~),i) "*" Col(GramMatrix(b),j)
.= 0 by A16,BJ1;
A30:SumSc(b/.j, l) = Sum(ScFS(b/.j, l, F)) by A303,defSumSc;
b is one-to-one by ZMATRLIN:def 5;
then Sum(ScFS(b/.j, l, F)) = Sum(ScFS(b/.j, l, b)) by LM1,A302;
hence thesis by A30,A32,ThSumSc1;
end;
reconsider EL = EMLat(L) as Submodule of DivisibleMod(L) by ZMODLAT2:20;
Sum(l) in EL;
then Sum(l) in DivisibleMod(L) by ZMODUL01:24;
then consider u be Vector of DivisibleMod(L) such that
A22: ai*u = Sum(l) by A3,ZMODUL08:23;
take u;
b/.i in EMLat(L);
then b/.i in rng MorphsZQ(L) by ZMODLAT2:def 4;
then A24: b/.i in EMbedding(L) by ZMODUL08:def 3;
Sum(l) in EMLat(L);
then Sum(l) in rng MorphsZQ(L) by ZMODLAT2:def 4;
then A25: Sum(l) in EMbedding(L) by ZMODUL08:def 3;
b/.i in EL;
then b/.i in DivisibleMod(L) by ZMODUL01:24;
then reconsider bi = b/.i as Element of DivisibleMod(L);
A28: a <> 0.F_Real by A3;
A29: a*((ScProductDM(L)).(bi, u)) = (ScProductDM(L)).(bi, ai*u)
by ZMODLAT2:13
.= (ScProductEM(L)).(b/.i, Sum(l)) by A22,A24,A25,ZMODLAT2:8
.= <; b/.i, Sum(l) ;> by ZMODLAT2:def 4
.= a*1.F_Real by A20,ThSumSc1;
for j being Nat st i <> j & j in dom b holds
(ScProductDM(L)).(b/.j, u) = 0
proof
let j be Nat such that
B1: i <> j & j in dom b;
b/.j in EMLat(L);
then b/.j in rng MorphsZQ(L) by ZMODLAT2:def 4;
then B2: b/.j in EMbedding(L) by ZMODUL08:def 3;
b/.j in EL;
then b/.j in DivisibleMod(L) by ZMODUL01:24;
then reconsider bj = b/.j as Element of DivisibleMod(L);
a*((ScProductDM(L)).(bj, u)) = (ScProductDM(L)).(bj, ai*u)
by ZMODLAT2:13
.= (ScProductEM(L)).(b/.j, Sum(l)) by A22,A25,B2,ZMODLAT2:8
.= <; b/.j, Sum(l) ;> by ZMODLAT2:def 4
.= a*0.F_Real by A21,B1;
hence thesis by A3;
end;
hence thesis by A28,A29,VECTSP_1:5;
end;
begin :: 2. Dual lattice
LmDE00:
for L being Z_Lattice, v being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(0.(DivisibleMod(L)), v) in INT.Ring
proof
let L be Z_Lattice, v be Vector of DivisibleMod(L);
reconsider m1 = -1 as Element of INT.Ring by INT_1:def 2;
A1: -1.INT.Ring = -1;
(ScProductDM(L)).(0.(DivisibleMod(L)), v)
= (ScProductDM(L)).(v + (-v), v) by RLVECT_1:5
.= (ScProductDM(L)).(v, v) + (ScProductDM(L)).((-v), v) by ZMODLAT2:6
.= (ScProductDM(L)).(v, v) + (ScProductDM(L)).(m1*v, v) by A1,ZMODUL01:2
.= (ScProductDM(L)).(v, v) + (-1) * (ScProductDM(L)).(v, v) by ZMODLAT2:6
.= 0.(INT.Ring);
hence thesis;
end;
definition
let L be Z_Lattice;
mode Dual of L -> Vector of DivisibleMod(L) means :defDualElement:
for v being Vector of DivisibleMod(L) st v in EMbedding(L) holds
(ScProductDM(L)).(it, v) in INT.Ring;
existence
proof
take 0.(DivisibleMod(L));
thus thesis by LmDE00;
end;
end;
theorem LmDE0:
for L being Z_Lattice holds 0.DivisibleMod(L) is Dual of L
proof
let L be Z_Lattice;
for v being Vector of DivisibleMod(L) st v in EMbedding(L) holds
(ScProductDM(L)).(0.DivisibleMod(L), v) in INT.Ring by LmDE00;
hence thesis by defDualElement;
end;
theorem LmDE1:
for L being Z_Lattice, v, u being Dual of L holds
v + u is Dual of L
proof
let L be Z_Lattice, v, u be Dual of L;
for x being Vector of DivisibleMod(L) st x in EMbedding(L) holds
(ScProductDM(L)).(v + u, x) in INT.Ring
proof
let x be Vector of DivisibleMod(L) such that
B1: x in EMbedding(L);
(ScProductDM(L)).(v, x) in INT.Ring by B1,defDualElement;
then reconsider iv = (ScProductDM(L)).(v, x) as Element of INT.Ring;
(ScProductDM(L)).(u, x) in INT.Ring by B1,defDualElement;
then reconsider iu = (ScProductDM(L)).(u, x) as Element of INT.Ring;
set iiv = iv;
set iiu = iu;
(ScProductDM(L)).(v + u, x)
= (ScProductDM(L)).(v, x) + (ScProductDM(L)).(u, x) by ZMODLAT2:6
.= iv + iu;
hence thesis;
end;
hence thesis by defDualElement;
end;
theorem LmDE2:
for L being Z_Lattice, v being Dual of L, a being Element of INT.Ring
holds a * v is Dual of L
proof
let L be Z_Lattice, v be Dual of L, a be Element of INT.Ring;
for x being Vector of DivisibleMod(L) st x in EMbedding(L) holds
(ScProductDM(L)).(a * v, x) in INT.Ring
proof
let x be Vector of DivisibleMod(L) such that
B1: x in EMbedding(L);
(ScProductDM(L)).(v, x) in INT.Ring by B1,defDualElement;
then reconsider iv = (ScProductDM(L)).(v, x) as Element of INT.Ring;
(ScProductDM(L)).(a * v, x) = a*iv by ZMODLAT2:6;
hence thesis;
end;
hence thesis by defDualElement;
end;
definition
let L be Z_Lattice;
func DualSet(L) -> non empty Subset of DivisibleMod(L) equals
the set of all v where v is Dual of L;
correctness
proof
set A = the set of all v where v is Dual of L;
0.DivisibleMod(L) is Dual of L by LmDE0;
then A1: 0.DivisibleMod(L) in A;
A c= the carrier of DivisibleMod(L)
proof
let v be object;
assume v in A;
then consider v1 be Dual of L such that
B1: v1 = v;
thus thesis by B1;
end;
hence thesis by A1;
end;
end;
registration
let L be Z_Lattice;
cluster DualSet(L) -> linearly-closed;
coherence
proof
set A = DualSet L;
A2: for v, u being Vector of DivisibleMod(L) st v in A & u in A holds
v + u in A
proof
let v, u be Vector of DivisibleMod(L) such that
B1: v in A & u in A;
consider v1 be Dual of L such that
B2: v1 = v by B1;
consider u1 be Dual of L such that
B3: u1 = u by B1;
v + u is Dual of L by B2,B3,LmDE1;
hence thesis;
end;
for a being Element of INT.Ring, v being Vector of DivisibleMod(L)
st v in A holds a * v in A
proof
let a be Element of INT.Ring, v be Vector of DivisibleMod(L) such that
B1: v in A;
consider v1 be Dual of L such that
B2: v1 = v by B1;
a * v is Dual of L by B2,LmDE2;
hence thesis;
end;
hence thesis by A2,VECTSP_4:def 1;
end;
end;
definition
let L be Z_Lattice;
func DualLatMod(L) -> strict non empty LatticeStr over INT.Ring
means
:defDualMod:
the carrier of it = DualSet(L) &
the addF of it = (the addF of DivisibleMod(L)) || DualSet(L) &
the ZeroF of it = 0.DivisibleMod(L) &
the lmult of it = (the lmult of DivisibleMod(L)) |
[:the carrier of INT.Ring, DualSet(L):] &
the scalar of it = (ScProductDM(L)) | [:DualSet(L), DualSet(L):];
existence
proof
reconsider ad = (the addF of DivisibleMod(L)) || DualSet(L)
as Function of [: DualSet(L), DualSet(L) :], the carrier of DivisibleMod(L)
by FUNCT_2:32;
for z being Element of [: DualSet(L), DualSet(L) :]
holds ad.z in DualSet(L)
proof
let z be Element of [: DualSet(L), DualSet(L) :];
consider x, y be object such that
G1: x in DualSet(L) & y in DualSet(L) & z=[x,y] by ZFMISC_1:def 2;
reconsider x,y as Element of DivisibleMod(L) by G1;
ad.z = x+y by FUNCT_1:49,G1;
hence ad.z in DualSet(L) by G1,VECTSP_4:def 1;
end;
then rng ad c= DualSet(L) by FUNCT_2:114;
then reconsider ad as BinOp of DualSet(L) by FUNCT_2:6;
0.DivisibleMod(L) is Dual of L by LmDE0;
then 0.DivisibleMod(L) in DualSet(L);
then reconsider ze = 0.DivisibleMod(L) as Element of DualSet(L);
[:the carrier of INT.Ring, DualSet(L):]
c= [:the carrier of INT.Ring, the carrier of DivisibleMod(L):]
by ZFMISC_1:95;
then reconsider mu = (the lmult of DivisibleMod(L)) |
[:the carrier of INT.Ring, DualSet(L):]
as Function of [:the carrier of INT.Ring, DualSet(L):],
the carrier of DivisibleMod(L) by FUNCT_2:32;
for z being Element of [:the carrier of INT.Ring, DualSet(L):]
holds mu.z in DualSet(L)
proof
let z be Element of [:the carrier of INT.Ring, DualSet(L):];
consider x, y be object such that
G1: x in the carrier of INT.Ring & y in DualSet(L) & z=[x,y]
by ZFMISC_1:def 2;
reconsider x as Element of INT.Ring by G1;
reconsider y as Element of DivisibleMod(L) by G1;
mu.z = x*y by FUNCT_1:49,G1;
hence mu.z in DualSet(L) by G1,VECTSP_4:def 1;
end;
then rng mu c= DualSet(L) by FUNCT_2:114;
then reconsider mu as Function of [:the carrier of INT.Ring, DualSet(L):],
DualSet(L) by FUNCT_2:6;
reconsider sc = (ScProductDM(L)) | [:DualSet(L), DualSet(L):]
as Function of [:DualSet(L), DualSet(L):],the carrier of F_Real
by FUNCT_2:32;
take IT = LatticeStr (# DualSet(L), ad, ze, mu, sc #);
thus thesis;
end;
uniqueness;
end;
theorem
for L being Z_Lattice holds DualLatMod(L) is Submodule of DivisibleMod(L)
proof
let L be Z_Lattice;
the carrier of DualLatMod(L) = DualSet(L) &
the addF of DualLatMod(L) = (the addF of DivisibleMod(L)) || DualSet(L) &
the ZeroF of DualLatMod(L) = 0.DivisibleMod(L) &
the lmult of DualLatMod(L) = (the lmult of DivisibleMod(L)) |
[:the carrier of INT.Ring, DualSet(L):] &
the scalar of DualLatMod(L) = (ScProductDM(L)) | [:DualSet(L), DualSet(L):]
by defDualMod;
hence thesis by ZMODLAT2:10;
end;
theorem LmDE21:
for L being Z_Lattice,
v being Vector of DivisibleMod(L), I being Basis of EMbedding(L)
st for u being Vector of DivisibleMod(L) st u in I
holds (ScProductDM(L)).(v, u) in INT.Ring
holds v is Dual of L
proof
let L be Z_Lattice, v be Vector of DivisibleMod(L),
I be Basis of EMbedding(L) such that
A1: for u being Vector of DivisibleMod(L) st u in I
holds (ScProductDM(L)).(v, u) in INT.Ring;
defpred P[Nat] means
for I being finite Subset of EMbedding(L) st card I = $1
& I is linearly-independent
& for u being Vector of DivisibleMod(L) st u in I
holds (ScProductDM(L)).(v, u) in INT.Ring
holds for w being Vector of DivisibleMod(L) st w in Lin(I) holds
(ScProductDM(L)).(v, w) in INT.Ring;
P1: P[0]
proof
let I be finite Subset of EMbedding(L) such that
B1: card I = 0 & I is linearly-independent &
for u being Vector of DivisibleMod(L) st u in I
holds (ScProductDM(L)).(v, u) in INT.Ring;
I = {}(the carrier of EMbedding(L)) by B1;
then B2: Lin(I) = (0).EMbedding(L) by ZMODUL02:67;
for w being Vector of DivisibleMod(L) st w in Lin(I)
holds (ScProductDM(L)).(v, w) in INT.Ring
proof
let w be Vector of DivisibleMod(L) such that
C1: w in Lin(I);
w = 0.EMbedding(L) by B2,C1,ZMODUL02:66
.= zeroCoset(L) by ZMODUL08:def 3
.= 0.DivisibleMod(L) by ZMODUL08:def 4;
then (ScProductDM(L)).(w, v) in INT.Ring by LmDE00;
hence thesis by ZMODLAT2:6;
end;
hence thesis;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let I be finite Subset of EMbedding(L) such that
B2: card I = n+1 & I is linearly-independent &
for u being Vector of DivisibleMod(L) st u in I
holds (ScProductDM(L)).(v, u) in INT.Ring;
I is non empty by B2;
then consider u be object such that
B3: u in I;
reconsider u as Vector of EMbedding(L) by B3;
set Iu = I \ {u};
{u} is Subset of I by B3,SUBSET_1:41;
then B4: card(Iu) = n+1 - card({u}) by B2,CARD_2:44
.= n+1 - 1 by CARD_1:30
.= n;
reconsider Iu as finite Subset of EMbedding(L);
I = Iu \/ {u} by B3,XBOOLE_1:45,ZFMISC_1:31;
then B5: Lin(I) = Lin(Iu) + Lin{u} by ZMODUL02:72;
B7: Iu c= I by XBOOLE_1:36;
B6: Iu is linearly-independent by B2,XBOOLE_1:36,ZMODUL02:56;
B8: for w being Vector of DivisibleMod(L) st w in Iu
holds (ScProductDM(L)).(v, w) in INT.Ring by B2,B7;
let w be Vector of DivisibleMod(L) such that
C1: w in Lin(I);
consider w1, w2 be Vector of EMbedding(L) such that
C2: w1 in Lin(Iu) & w2 in Lin{u} & w = w1 + w2 by B5,C1,ZMODUL01:92;
CX: EMbedding(L) is Submodule of DivisibleMod(L) by ZMODUL08:24;
then C9: w1 is Vector of DivisibleMod(L) by ZMODUL01:25;
reconsider ww1 = w1 as Vector of DivisibleMod(L) by CX,ZMODUL01:25;
C3: (ScProductDM(L)).(v, w1) in INT.Ring by B1,B4,B6,B8,C2,C9;
consider i be Element of INT.Ring such that
C4: w2 = i*u by C2,ZMODUL06:19;
u is Element of DivisibleMod(L) by CX,ZMODUL01:25;
then C6: (ScProductDM(L)).(v, u) in INT.Ring by B2,B3;
reconsider uu = u as Element of DivisibleMod(L) by CX,ZMODUL01:25;
i*uu in DivisibleMod(L);
then reconsider ww2 = w2 as Vector of DivisibleMod(L)
by C4,CX,ZMODUL01:29;
C11: (ScProductDM(L)).(v, i*u) = (ScProductDM(L)).(v, i*uu)
by CX,ZMODUL01:29
.= (ScProductDM(L)).(i*uu, v) by ZMODLAT2:6
.= i* (ScProductDM(L)).(uu, v) by ZMODLAT2:6
.= i* (ScProductDM(L)).(v, u) by ZMODLAT2:6;
C10: w = ww1 + ww2 by C2,CX,ZMODUL01:28;
(ScProductDM(L)).(v, w) = (ScProductDM(L)).(w, v) by ZMODLAT2:6
.= (ScProductDM(L)).(ww1, v) + (ScProductDM(L)).(ww2, v)
by C10,ZMODLAT2:6
.= (ScProductDM(L)).(v, w1) + (ScProductDM(L)).(ww2, v) by ZMODLAT2:6
.= (ScProductDM(L)).(v, w1) + (ScProductDM(L)).(v, w2) by ZMODLAT2:6;
hence thesis by C3,C4,C6,C11,INT_1:def 2;
end;
P3: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
P4: card I is Nat;
I is linearly-independent & EMbedding(L) = Lin(I) by VECTSP_7:def 3;
then for w being Vector of DivisibleMod(L) st w in EMbedding(L) holds
(ScProductDM(L)).(v, w) in INT.Ring by A1,P3,P4;
hence thesis by defDualElement;
end;
definition
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
func DualBasis(I) -> Subset of DivisibleMod(L) means :defDualBasis:
for v being Vector of DivisibleMod(L) holds
v in it iff
ex u being Vector of EMLat(L) st u in I &
(ScProductDM(L)).(u, v) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, v) = 0);
existence
proof
defpred P[object] means
ex u being Vector of EMLat(L) st u in I &
(ScProductDM(L)).(u, $1) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, $1) = 0);
consider C be Subset of DivisibleMod(L) such that
A1: for v being Element of DivisibleMod(L) holds
v in C iff P[v] from SUBSET_1:sch 3;
take C;
thus thesis by A1;
end;
uniqueness
proof
let C1, C2 be Subset of DivisibleMod(L) such that
A1: (for v being Vector of DivisibleMod(L) holds
v in C1 iff ex u being Vector of EMLat(L) st u in I &
(ScProductDM(L)).(u, v) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, v) = 0)) and
A2: (for v being Vector of DivisibleMod(L) holds
v in C2 iff ex u being Vector of EMLat(L) st u in I &
(ScProductDM(L)).(u, v) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, v) = 0));
for v being Vector of DivisibleMod(L) st v in C1 holds
v in C2
proof
let v be Vector of DivisibleMod(L) such that
B1: v in C1;
ex u being Vector of EMLat(L) st u in I &
(ScProductDM(L)).(u, v) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, v) = 0) by A1,B1;
hence thesis by A2;
end;
then A3: C1 c= C2;
for v being Vector of DivisibleMod(L) st v in C2 holds
v in C1
proof
let v be Vector of DivisibleMod(L) such that
B1: v in C2;
ex u being Vector of EMLat(L) st u in I &
(ScProductDM(L)).(u, v) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, v) = 0) by A2,B1;
hence thesis by A1;
end;
then C2 c= C1;
hence thesis by A3;
end;
end;
definition
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
func B2DB(I) -> Function of I, DualBasis(I) means :defB2DB:
dom it = I & rng it = DualBasis(I) &
for v being Vector of EMLat(L) st v in I holds
(ScProductDM(L)).(v, it.v) = 1 &
(for w being Vector of EMLat(L) st w in I & v <> w
holds (ScProductDM(L)).(w, it.v) = 0);
existence
proof
per cases;
suppose L is trivial;
then (Omega).L = (0).L by ZMODUL07:41;
then rank L = 0 by ZMODUL05:1;
then rank(EMLat(L)) = 0 by ZMODLAT2:42;
then A1: card I = 0 by ZMODUL03:def 5;
for v being Vector of DivisibleMod(L) holds
v in {} iff ex u being Vector of EMLat(L) st u in I &
(ScProductDM(L)).(u, v) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, v) = 0) by A1;
then A2: DualBasis(I) = {}(the carrier of DivisibleMod(L))
by defDualBasis;
set F = the Function of I,DualBasis(I);
take F;
I = {} by A1;
hence thesis by A2;
end;
suppose X1: L is non trivial;
defpred P[object, object] means
(ScProductDM(L)).($1, $2) = 1 &
(for w being Vector of EMLat(L) st w in I & $1 <> w
holds (ScProductDM(L)).(w, $2) = 0);
consider b be FinSequence such that
A0: rng b = I & b is one-to-one by FINSEQ_4:58;
b is FinSequence of EMLat(L) by A0,FINSEQ_1:def 4;
then reconsider b as OrdBasis of EMLat(L) by A0,ZMATRLIN:def 5;
A1: for x being object st x in I
ex y being object st y in DualBasis(I) & P[x, y]
proof
let x be object such that
B1: x in I;
consider i be Nat such that
B3: i in dom b & b.i = x by A0,B1,FINSEQ_2:10;
b/.i = x by B3,PARTFUN1:def 6;
then consider y be Vector of DivisibleMod(L) such that
B4: (ScProductDM(L)).(x, y) = 1 &
(for j being Nat st i <> j & j in dom b holds
(ScProductDM(L)).(b/.j, y) = 0) by X1,B3,LmDE31;
B5: for w being Vector of EMLat(L) st w in I & x <> w
holds (ScProductDM(L)).(w, y) = 0
proof
let w be Vector of EMLat(L) such that
C1: w in I & x <> w;
consider j be Nat such that
C2: j in dom b & b.j = w by A0,C1,FINSEQ_2:10;
b/.j = w by C2,PARTFUN1:def 6;
hence thesis by B3,B4,C1,C2;
end;
take y;
thus thesis by B1,B4,B5,defDualBasis;
end;
consider f be Function such that
A2: dom f = I & rng f c= DualBasis(I) &
for x being object st x in I holds P[x, f.x] from FUNCT_1:sch 6(A1);
A3: DualBasis(I) c= rng f
proof
for y being object st y in DualBasis(I)
ex x being object st x in dom f & y = f.x
proof
let y be object such that
B1: y in DualBasis(I);
consider u be Vector of EMLat(L) such that
B2: u in I &
(ScProductDM(L)).(u, y) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, y) = 0) by B1,defDualBasis;
take u;
consider i be Nat such that
B6: i in dom b & b.i = u by A0,B2,FINSEQ_2:10;
B8: for n being Nat st n in dom b holds
(ScProductDM(L)).(b/.n, y) = (ScProductDM(L)).(b/.n, f.u)
proof
let n be Nat such that
C1: n in dom b;
per cases;
suppose C2: n = i;
hence (ScProductDM(L)).(b/.n, y) = (ScProductDM(L)).(u, y)
by B6,PARTFUN1:def 6
.= (ScProductDM(L)).(u, f.u) by A2,B2
.= (ScProductDM(L)).(b/.n, f.u) by B6,C2,PARTFUN1:def 6;
end;
suppose n <> i;
then b.n <> b.i by A0,B6,C1;
then C2: b/.n <> u by B6,C1,PARTFUN1:def 6;
b.n in rng b by C1,FUNCT_1:3;
then C3: b/.n in I by A0,C1,PARTFUN1:def 6;
hence (ScProductDM(L)).(b/.n, y) = 0 by B2,C2
.= (ScProductDM(L)).(b/.n, f.u) by A2,B2,C2,C3;
end;
end;
f.u in DualBasis(I) by A2,B2,FUNCT_1:3;
hence thesis by A2,B1,B2,B8,ZMODLAT2:63;
end;
hence thesis by FUNCT_1:9;
end;
then rng f = DualBasis(I) by A2;
then reconsider f as Function of I, DualBasis(I) by A2,FUNCT_2:1;
take f;
thus thesis by A2,A3;
end;
end;
uniqueness
proof
let f1, f2 be Function of I, DualBasis(I);
assume AS1: dom f1 = I & rng f1 = DualBasis(I) &
for v being Vector of EMLat(L) st v in I holds
(ScProductDM(L)).(v, f1.v) = 1 &
(for w being Vector of EMLat(L) st w in I & v <> w
holds (ScProductDM(L)).(w, f1.v) = 0);
assume AS2: dom f2 = I & rng f2 = DualBasis(I) &
for v being Vector of EMLat(L) st v in I holds
(ScProductDM(L)).(v, f2.v) = 1 &
(for w being Vector of EMLat(L) st w in I & v <> w
holds (ScProductDM(L)).(w, f2.v) = 0);
consider b be FinSequence such that
A0: rng b = I & b is one-to-one by FINSEQ_4:58;
b is FinSequence of EMLat(L) by A0,FINSEQ_1:def 4;
then reconsider b as OrdBasis of EMLat(L) by A0,ZMATRLIN:def 5;
for x being Element of I holds f1.x = f2.x
proof
let x be Element of I;
per cases;
suppose I is empty;
hence thesis;
end;
suppose XX1: I is non empty;
then X1: x in I;
A1: for n being Nat st n in dom b holds
(ScProductDM(L)).(b/.n, f1.x) = (ScProductDM(L)).(b/.n, f2.x)
proof
let n be Nat such that
B1: n in dom b;
B2: b.n in I by A0,B1,FUNCT_1:3;
then B2X: b/.n in I by B1,PARTFUN1:def 6;
per cases;
suppose B3: b/.n = x;
hence (ScProductDM(L)).(b/.n, f1.x) = 1 by AS1,B2
.= (ScProductDM(L)).(b/.n, f2.x) by AS2,B2,B3;
end;
suppose B4: b/.n <> x;
hence (ScProductDM(L)).(b/.n, f1.x) = 0 by AS1,X1,B2X
.= (ScProductDM(L)).(b/.n, f2.x) by AS2,X1,B2X,B4;
end;
end;
A2: f1.x in DualBasis(I) by AS1,XX1,FUNCT_1:3;
f2.x in DualBasis(I) by AS2,XX1,FUNCT_1:3;
hence thesis by A1,A2,ZMODLAT2:63;
end;
end;
hence f1 = f2;
end;
end;
registration
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
cluster B2DB(I) -> onto one-to-one;
correctness
proof
set f = B2DB(I);
thus f is onto by defB2DB;
for x1, x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1, x2 be object such that
B1: x1 in dom f & x2 in dom f & f.x1 = f.x2;
B2: x1 in I by B1;
B5: x2 in I by B1;
B6: (ScProductDM(L)).(x1, f.x2) = 1 by B1,B2,defB2DB;
assume x1 <> x2;
hence contradiction by B2,B5,B6,defB2DB;
end;
hence B2DB(I) is one-to-one;
end;
end;
theorem ThDB1:
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L) holds
card I = card DualBasis(I)
proof
let L be RATional positive-definite Z_Lattice,
I be Basis of EMLat(L);
B2DB(I) is one-to-one & dom B2DB(I) = I & rng B2DB(I) = DualBasis(I)
by defB2DB;
hence thesis by CARD_1:5,WELLORD2:def 4;
end;
registration
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
cluster DualBasis(I) -> finite;
correctness
proof
card DualBasis(I) c= card I by ThDB1;
hence thesis;
end;
end;
registration
let L be non trivial RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
cluster DualBasis(I) -> non empty;
correctness
proof
card I <> 0;
hence thesis by ThDB1,CARD_1:27;
end;
end;
theorem LmDE32:
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L), v being Vector of DivisibleMod(L),
l being Linear_Combination of DualBasis(I) st v in I
holds (ScProductDM(L)).(v, Sum(l)) = l.((B2DB(I)).v)
proof
let L be RATional positive-definite Z_Lattice,
I be Basis of EMLat(L), v be Vector of DivisibleMod(L),
l be Linear_Combination of DualBasis(I) such that
A1: v in I;
v in dom(B2DB(I)) by A1,defB2DB;
then (B2DB(I)).v in rng(B2DB(I)) by FUNCT_1:3;
then A2: (B2DB(I)).v in DualBasis(I);
then reconsider bv = (B2DB(I)).v as Vector of DivisibleMod(L);
per cases;
suppose B1: not (B2DB(I)).v in Carrier(l);
consider F be FinSequence of DivisibleMod(L) such that
B2: F is one-to-one & rng F = Carrier(l) &
SumSc(v, l) = Sum(ScFS(v, l, F)) by defSumScDM;
B3: len F = len(ScFS(v, l, F)) by defScFSDM; then
B4: dom(ScFS(v, l, F)) = dom F by FINSEQ_3:29;
for k being Nat st k in dom(ScFS(v, l, F))
holds (ScFS(v, l, F)).k = -(ScFS(v, l, F))/.k
proof
let k be Nat such that
C1: k in dom(ScFS(v, l, F));
CX2: (ScFS(v, l, F)).k = (ScProductDM(L)).(v, l.(F/.k) * F/.k)
by C1,defScFSDM;
F.k in Carrier(l) by B2,B4,C1,FUNCT_1:3;
then C2: F/.k in Carrier(l) by B4,C1,PARTFUN1:def 6;
then F/.k in DualBasis(I) by TARSKI:def 3,VECTSP_6:def 4;
then C4: F/.k in rng B2DB(I) by defB2DB;
then C5: (B2DB(I)).((B2DB(I))".(F/.k)) = F/.k by FUNCT_1:35;
F/.k in dom((B2DB(I))") by C4,FUNCT_1:33;
then (B2DB(I))".(F/.k) in rng((B2DB(I))") by FUNCT_1:3;
then (B2DB(I))".(F/.k) in dom(B2DB(I)) by FUNCT_1:33;
then (B2DB(I))".(F/.k) in I;
then (ScProductDM(L)).(v, F/.k) = 0.F_Real by A1,B1,C2,C5,defB2DB;
then l.(F/.k) * (ScProductDM(L)).(v, F/.k) = 0.F_Real;
then (ScProductDM(L)).(v, l.(F/.k) * F/.k) = 0.F_Real by ZMODLAT2:13;
hence (ScFS(v, l, F)).k = -(ScFS(v, l, F)).k by CX2
.= -(ScFS(v, l, F))/.k by C1,PARTFUN1:def 6;
end;
then B5: Sum(ScFS(v, l, F)) = -Sum(ScFS(v, l, F)) by B3,RLVECT_2:4;
thus l.((B2DB(I)).v) = 0.INT.Ring by A2,B1
.= (ScProductDM(L)).(v, Sum(l)) by B2,B5,ThSumScDM1;
end;
suppose (B2DB(I)).v in Carrier(l);
then C2: Carrier(l) = (Carrier(l) \ {(B2DB(I)).v}) \/ {(B2DB(I)).v}
by XBOOLE_1:45,ZFMISC_1:31;
C3: (Carrier(l) \ {(B2DB(I)).v}) /\ {(B2DB(I)).v} = {}
by XBOOLE_0:def 7,XBOOLE_1:79;
l is Linear_Combination of Carrier(l) by VECTSP_6:7;
then consider l1 be Linear_Combination of (Carrier(l) \ {bv}),
l2 be Linear_Combination of {bv} such that
C4: l = l1 + l2 by C2,C3,ZMODUL04:26;
for x being Vector of DivisibleMod(L) st x in (Carrier(l) \ {bv})
holds x in Carrier(l1)
proof
let x be Vector of DivisibleMod(L) such that
D1: x in (Carrier(l) \ {bv});
x in Carrier(l) by D1,XBOOLE_0:def 5;
then D2: l.x <> 0.INT.Ring by VECTSP_6:2;
D3: Carrier(l2) c= {bv} by VECTSP_6:def 4;
D4: l.x = l1.x + l2.x by C4,VECTSP_6:22;
not x in Carrier(l2) by D1,D3,XBOOLE_0:def 5;
then l1.x <> 0.INT.Ring by D2,D4;
hence thesis;
end;
then (Carrier(l) \ {bv}) c= Carrier(l1);
then C6: Carrier(l1) = (Carrier(l) \ {bv}) by VECTSP_6:def 4;
then C7: not bv in Carrier(l1) by ZFMISC_1:56;
consider F1 be FinSequence of DivisibleMod(L) such that
C8: F1 is one-to-one & rng F1 = Carrier(l1) &
SumSc(v, l1) = Sum(ScFS(v, l1, F1)) by defSumScDM;
C9: len F1 = len(ScFS(v, l1, F1)) by defScFSDM; then
C10: dom(ScFS(v, l1, F1)) = dom F1 by FINSEQ_3:29;
for k being Nat st k in dom(ScFS(v, l1, F1))
holds (ScFS(v, l1, F1)).k = -(ScFS(v, l1, F1))/.k
proof
let k be Nat such that
D1: k in dom(ScFS(v, l1, F1));
D2: (ScFS(v, l1, F1)).k
= (ScProductDM(L)).(v, l1.(F1/.k) * F1/.k) by D1,defScFSDM;
per cases;
suppose E1: F1/.k <> (B2DB(I)).v;
F1.k in Carrier(l1) by C8,C10,D1,FUNCT_1:3;
then F1/.k in Carrier(l1) by C10,D1,PARTFUN1:def 6;
then F1/.k in Carrier(l) by C6,XBOOLE_0:def 5;
then F1/.k in DualBasis(I) by TARSKI:def 3,VECTSP_6:def 4;
then E5: F1/.k in rng B2DB(I) by defB2DB;
then F1/.k in dom((B2DB(I))") by FUNCT_1:33;
then (B2DB(I))".(F1/.k) in rng((B2DB(I))") by FUNCT_1:3;
then (B2DB(I))".(F1/.k) in dom(B2DB(I)) by FUNCT_1:33;
then E7: (B2DB(I))".(F1/.k) in I;
E9: (B2DB(I)).((B2DB(I))".(F1/.k)) = F1/.k by E5,FUNCT_1:35;
(ScProductDM(L)).(v, F1/.k) = 0.F_Real by A1,E1,E7,E9,defB2DB;
then l1.(F1/.k) * (ScProductDM(L)).(v, F1/.k) = 0.F_Real;
then (ScProductDM(L)).(v, l1.(F1/.k) * F1/.k) = 0.F_Real
by ZMODLAT2:13;
hence (ScFS(v, l1, F1)).k = -(ScFS(v, l1, F1)).k by D2
.= -(ScFS(v, l1, F1))/.k by D1,PARTFUN1:def 6;
end;
suppose F1/.k = (B2DB(I)).v;
then (ScFS(v, l1, F1)).k
= (ScProductDM(L)).(v, 0.INT.Ring * F1/.k) by C7,D2
.= (ScProductDM(L)).(v, 0.DivisibleMod(L)) by VECTSP_1:14
.= 0.F_Real by ZMODLAT2:14;
hence (ScFS(v, l1, F1)).k = -(ScFS(v, l1, F1)).k
.= -(ScFS(v, l1, F1))/.k by D1,PARTFUN1:def 6;
end;
end;
then C11: Sum(ScFS(v, l1, F1)) = -Sum(ScFS(v, l1, F1)) by C9,RLVECT_2:4;
C12: SumSc(v, l2) = (ScProductDM(L)).(v, l2.bv * bv) by LmSumScDM14
.= l2.bv * (ScProductDM(L)).(v, bv) by ZMODLAT2:13
.= l2.bv * 1 by A1,defB2DB
.= l2.bv;
C13: l.bv = l1.bv + l2.bv by C4,VECTSP_6:22
.= 0.INT.Ring + l2.bv by C7
.= l2.bv;
thus (ScProductDM(L)).(v, Sum(l)) = SumSc(v, l) by ThSumScDM1
.= SumSc(v, l1) + SumSc(v, l2) by C4,LmSumScDM1X
.= l.((B2DB(I)).v) by C8,C11,C12,C13;
end;
end;
theorem ThDE3:
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L),
v being Vector of DivisibleMod(L) st v is Dual of L holds
v in Lin DualBasis(I)
proof
let L be RATional positive-definite Z_Lattice,
I be Basis of EMLat(L),
v be Vector of DivisibleMod(L) such that
A1: v is Dual of L;
set f = (B2DB(I))";
defpred P[object,object] means
($1 in DualBasis(I) implies $2 = (ScProductDM(L)).(f.$1, v)) &
(not $1 in DualBasis(I) implies $2 = 0.INT.Ring);
A2: for x being object st x in the carrier of DivisibleMod(L)
ex y being object st y in the carrier of INT.Ring & P[x, y]
proof
let x be object such that
x in the carrier of DivisibleMod(L);
per cases;
suppose B2: x in DualBasis(I);
then x in rng B2DB(I) by defB2DB;
then x in dom f by FUNCT_1:33;
then f.x in rng f by FUNCT_1:3;
then f.x in dom B2DB(I) by FUNCT_1:33;
then f.x in I;
then f.x in EMLat(L);
then f.x in rng MorphsZQ(L) by ZMODLAT2:def 4;
then B3: f.x in EMbedding(L) by ZMODUL08:def 3;
EMbedding(L) is Submodule of DivisibleMod(L) by ZMODUL08:24;
then B4: f.x is Vector of DivisibleMod(L) by B3,ZMODUL01:25;
then B5: (ScProductDM(L)).(v, f.x) in INT.Ring by A1,B3,defDualElement;
take (ScProductDM(L)).(f.x, v);
thus thesis by B2,B4,B5,ZMODLAT2:6;
end;
suppose not x in DualBasis(I);
hence thesis;
end;
end;
consider l be Function of DivisibleMod(L),
the carrier of INT.Ring such that
A3: for x being object st x in the carrier of DivisibleMod(L) holds
P[x, l.x] from FUNCT_2:sch 1(A2);
reconsider l as Element of Funcs(the carrier of DivisibleMod(L),
the carrier of INT.Ring) by FUNCT_2:8;
for v being Vector of DivisibleMod(L) st not v in DualBasis(I) holds
l.v = 0.INT.Ring by A3;
then reconsider l as Linear_Combination of DivisibleMod(L)
by VECTSP_6:def 1;
Carrier l c= DualBasis(I)
proof
for x being Vector of DivisibleMod(L) st not x in DualBasis(I) holds
not x in Carrier l
proof
let x be Vector of DivisibleMod(L) such that
B1: not x in DualBasis(I);
l.x = 0.INT.Ring by A3,B1;
hence thesis by VECTSP_6:2;
end;
hence thesis;
end;
then A5: l is Linear_Combination of DualBasis(I) by VECTSP_6:def 4;
consider b be FinSequence such that
A6: rng b = I & b is one-to-one by FINSEQ_4:58;
b is FinSequence of EMLat(L) by A6,FINSEQ_1:def 4;
then reconsider b as OrdBasis of EMLat(L) by A6,ZMATRLIN:def 5;
for n being Nat st n in dom b holds
(ScProductDM(L)).(b/.n, v) = (ScProductDM(L)).(b/.n, Sum(l))
proof
let n be Nat such that
B1: n in dom b;
EMLat(L) is Submodule of DivisibleMod(L) by ZMODLAT2:20;
then reconsider bn = b/.n as Vector of DivisibleMod(L) by ZMODUL01:25;
(ScProductDM(L)).(bn, v) = SumSc(bn, l)
proof
b.n in rng b by B1,FUNCT_1:3;
then B2: bn in I by A6,B1,PARTFUN1:def 6;
then B5: bn in dom B2DB(I) by defB2DB;
then B3: (B2DB(I)).bn in rng B2DB(I) by FUNCT_1:3;
then B31: (B2DB(I)).bn in DualBasis(I);
B4: for v being Vector of DivisibleMod(L) st v <> (B2DB(I)).bn holds
(ScProductDM(L)).(bn, l.v * v) = 0.F_Real
proof
let v be Vector of DivisibleMod(L) such that
C1: v <> (B2DB(I)).bn;
per cases;
suppose not v in DualBasis(I);
then l.v = 0.INT.Ring by A3;
then l.v * v = 0.DivisibleMod(L) by VECTSP_1:14;
hence thesis by ZMODLAT2:14;
end;
suppose v in DualBasis(I); then
C21: v in rng B2DB(I) by defB2DB;
then C0: (B2DB(I)).(f.v) = v by FUNCT_1:35;
v in dom f by C21,FUNCT_1:33;
then f.v in rng f by FUNCT_1:3;
then f.v in dom B2DB(I) by FUNCT_1:33;
then f.v in I;
then (ScProductDM(L)).(bn, v) = 0.F_Real by B2,C0,C1,defB2DB;
then l.v * (ScProductDM(L)).(bn, v) = 0.F_Real;
hence (ScProductDM(L)).(bn, l.v * v) = 0.F_Real by ZMODLAT2:13;
end;
end;
reconsider bbn = (B2DB(I)).bn as Vector of DivisibleMod(L) by B31;
per cases;
suppose C1: not (B2DB(I)).bn in Carrier(l);
consider F be FinSequence of DivisibleMod(L) such that
C2: F is one-to-one & rng F = Carrier(l) &
SumSc(bn, l) = Sum(ScFS(bn, l, F)) by defSumScDM;
C3: len F = len(ScFS(bn, l, F)) by defScFSDM;
for k being Nat st k in dom(ScFS(bn, l, F))
holds (ScFS(bn, l, F)).k = -(ScFS(bn, l, F))/.k
proof
let k be Nat such that
D1: k in dom(ScFS(bn, l, F));
D2: (ScFS(bn, l, F)).k = (ScProductDM(L)).(bn, l.(F/.k) * F/.k)
by D1,defScFSDM;
per cases;
suppose F/.k <> (B2DB(I)).bn;
then (ScFS(bn, l, F)).k = 0.F_Real by B4,D2;
hence (ScFS(bn, l, F)).k = -(ScFS(bn, l, F)).k
.= -(ScFS(bn, l, F))/.k by D1,PARTFUN1:def 6;
end;
suppose F/.k = (B2DB(I)).bn;
then (ScFS(bn, l, F)).k
= (ScProductDM(L)).(bn, 0.INT.Ring * F/.k) by C1,D2
.= (ScProductDM(L)).(bn, 0.DivisibleMod(L)) by VECTSP_1:14
.= 0.F_Real by ZMODLAT2:14;
hence (ScFS(bn, l, F)).k = -(ScFS(bn, l, F)).k
.= -(ScFS(bn, l, F))/.k by D1,PARTFUN1:def 6;
end;
end;
then C4: Sum(ScFS(bn, l, F)) = -Sum(ScFS(bn, l, F)) by C3,RLVECT_2:4;
l.((B2DB(I)).bn) = (ScProductDM(L)).(f.((B2DB(I)).bn), v) by A3,B31;
then (ScProductDM(L)).(f.(bbn), v) = 0.INT.Ring by C1;
hence thesis by B5,C2,C4,FUNCT_1:34;
end;
suppose (B2DB(I)).bn in Carrier(l);
then C2: Carrier(l) = (Carrier(l) \ {(B2DB(I)).bn}) \/ {(B2DB(I)).bn}
by XBOOLE_1:45,ZFMISC_1:31;
C3: (Carrier(l) \ {(B2DB(I)).bn}) /\ {(B2DB(I)).bn} = {}
by XBOOLE_0:def 7,XBOOLE_1:79;
l is Linear_Combination of Carrier(l) by VECTSP_6:7;
then consider l1 be Linear_Combination of (Carrier(l) \ {bbn}),
l2 be Linear_Combination of {bbn} such that
C4: l = l1 + l2 by C2,C3,ZMODUL04:26;
for x being Vector of DivisibleMod(L) st x in (Carrier(l) \ {bbn})
holds x in Carrier(l1)
proof
let x be Vector of DivisibleMod(L) such that
D1: x in (Carrier(l) \ {bbn});
x in Carrier(l) by D1,XBOOLE_0:def 5;
then D2: l.x <> 0.INT.Ring by VECTSP_6:2;
D3: Carrier(l2) c= {bbn} by VECTSP_6:def 4;
D4: l.x = l1.x + l2.x by C4,VECTSP_6:22;
not x in Carrier(l2) by D1,D3,XBOOLE_0:def 5;
then l1.x <> 0.INT.Ring by D2,D4;
hence thesis;
end;
then (Carrier(l) \ {bbn}) c= Carrier(l1);
then Carrier(l1) = (Carrier(l) \ {bbn}) by VECTSP_6:def 4;
then C12: not bbn in Carrier(l1) by ZFMISC_1:56;
consider F1 be FinSequence of DivisibleMod(L) such that
C7: F1 is one-to-one & rng F1 = Carrier(l1) &
SumSc(bn, l1) = Sum(ScFS(bn, l1, F1)) by defSumScDM;
C8: len F1 = len(ScFS(bn, l1, F1)) by defScFSDM;
for k being Nat st k in dom(ScFS(bn, l1, F1))
holds (ScFS(bn, l1, F1)).k = -(ScFS(bn, l1, F1))/.k
proof
let k be Nat such that
D1: k in dom(ScFS(bn, l1, F1));
per cases;
suppose E1: F1/.k <> (B2DB(I)).bn;
then not F1/.k in {bbn} by TARSKI:def 1;
then E2: not F1/.k in Carrier(l2) by TARSKI:def 3,VECTSP_6:def 4;
l.(F1/.k) = l1.(F1/.k) + l2.(F1/.k) by C4,VECTSP_6:22
.= l1.(F1/.k) + 0.INT.Ring by E2
.= l1.(F1/.k);
then (ScFS(bn, l1, F1)).k
= (ScProductDM(L)).(bn, l.(F1/.k) * F1/.k) by D1,defScFSDM
.= 0.F_Real by B4,E1;
hence (ScFS(bn, l1, F1)).k = -(ScFS(bn, l1, F1)).k
.= -(ScFS(bn, l1, F1))/.k by D1,PARTFUN1:def 6;
end;
suppose F1/.k = (B2DB(I)).bn;
then l1.(F1/.k) = 0.INT.Ring by C12;
then (ScFS(bn, l1, F1)).k
= (ScProductDM(L)).(bn, 0.INT.Ring * F1/.k) by D1,defScFSDM
.= (ScProductDM(L)).(bn, 0.DivisibleMod(L)) by VECTSP_1:14
.= 0.F_Real by ZMODLAT2:14;
hence (ScFS(bn, l1, F1)).k = -(ScFS(bn, l1, F1)).k
.= -(ScFS(bn, l1, F1))/.k by D1,PARTFUN1:def 6;
end;
end;
then C9: Sum(ScFS(bn, l1, F1)) = -Sum(ScFS(bn, l1, F1))
by C8,RLVECT_2:4;
C10: SumSc(bn, l2) = (ScProductDM(L)).(bn, l2.bbn * bbn)
by LmSumScDM14
.= l2.bbn * (ScProductDM(L)).(bn, bbn) by ZMODLAT2:13
.= l2.bbn * 1 by B2,defB2DB
.= l2.bbn;
l.bbn = l1.bbn + l2.bbn by C4,VECTSP_6:22
.= 0.INT.Ring + l2.bbn by C12
.= l2.bbn;
then C11: SumSc(bn, l2) = (ScProductDM(L)).(f.bbn, v) by A3,B3,C10
.= (ScProductDM(L)).(bn, v) by B5,FUNCT_1:34;
thus SumSc(bn, l) = SumSc(bn, l1) + SumSc(bn, l2) by C4,LmSumScDM1X
.= (ScProductDM(L)).(bn, v) by C7,C9,C11;
end;
end;
hence thesis by ThSumScDM1;
end;
hence thesis by A5,ZMODLAT2:63,ZMODUL02:64;
end;
registration
let L be RATional positive-definite Z_Lattice;
let I be Basis of EMLat(L);
cluster DualBasis(I) -> linearly-independent;
correctness
proof
assume DualBasis(I) is linearly-dependent;
then consider l be Linear_Combination of DualBasis(I) such that
B1: Sum(l) = 0.DivisibleMod(L) & Carrier(l) <> {} by VECTSP_7:def 1;
consider u be object such that
B2: u in Carrier(l) by B1,XBOOLE_0:def 1;
reconsider u as Element of DivisibleMod(L) by B2;
B21: Carrier(l) c= DualBasis(I) by VECTSP_6:def 4;
then u in DualBasis(I) by B2;
then B31: u in rng B2DB(I) by defB2DB;
then u in dom((B2DB(I))") by FUNCT_1:33;
then ((B2DB(I))").u in rng((B2DB(I))") by FUNCT_1:3;
then B4: ((B2DB(I))").u in dom B2DB(I) by FUNCT_1:33;
then ((B2DB(I))").u in I;
then reconsider bu = ((B2DB(I))").u as Vector of EMLat(L);
EMLat(L) is Submodule of DivisibleMod(L) by ZMODLAT2:20;
then reconsider bu as Vector of DivisibleMod(L) by ZMODUL01:25;
B5: (ScProductDM(L)).(bu, Sum(l)) = SumSc(bu, l) by ThSumScDM1;
B6: Carrier(l) = (Carrier(l) \ {u}) \/ {u}
by B2,XBOOLE_1:45,ZFMISC_1:31;
B7: (Carrier(l) \ {u}) /\ {u} = {} by XBOOLE_0:def 7,XBOOLE_1:79;
l is Linear_Combination of Carrier(l) by VECTSP_6:7;
then consider l1 be Linear_Combination of (Carrier(l) \ {u}),
l2 be Linear_Combination of {u} such that
B8: l = l1 + l2 by B6,B7,ZMODUL04:26;
for x being Vector of DivisibleMod(L) st x in (Carrier(l) \ {u})
holds x in Carrier(l1)
proof
let x be Vector of DivisibleMod(L) such that
C1: x in (Carrier(l) \ {u});
x in Carrier(l) by C1,XBOOLE_0:def 5;
then C2: l.x <> 0.INT.Ring by VECTSP_6:2;
C3: Carrier(l2) c= {u} by VECTSP_6:def 4;
C4: l.x = l1.x + l2.x by B8,VECTSP_6:22;
not x in Carrier(l2) by C1,C3,XBOOLE_0:def 5;
then l1.x <> 0.INT.Ring by C2,C4;
hence thesis;
end;
then (Carrier(l) \ {u}) c= Carrier(l1);
then B10: Carrier(l1) = (Carrier(l) \ {u}) by VECTSP_6:def 4;
then B11: not u in Carrier(l1) by ZFMISC_1:56;
B12: (B2DB(I)).bu = u by B31,FUNCT_1:35;
consider F1 be FinSequence of DivisibleMod(L) such that
B13: F1 is one-to-one & rng F1 = Carrier(l1) &
SumSc(bu, l1) = Sum(ScFS(bu, l1, F1)) by defSumScDM;
B14: len F1 = len(ScFS(bu, l1, F1)) by defScFSDM;
for k being Nat st k in dom(ScFS(bu, l1, F1))
holds (ScFS(bu, l1, F1)).k = -(ScFS(bu, l1, F1))/.k
proof
let k be Nat such that
C1: k in dom(ScFS(bu, l1, F1));
C2: (ScFS(bu, l1, F1)).k
= (ScProductDM(L)).(bu, l1.(F1/.k) * F1/.k) by C1,defScFSDM;
C3: dom(ScFS(bu, l1, F1)) = dom(F1) by B14,FINSEQ_3:29;
per cases;
suppose D1: F1/.k <> (B2DB(I)).bu;
then F1/.k <> u by B31,FUNCT_1:35;
then not F1/.k in {u} by TARSKI:def 1;
then D2: not F1/.k in Carrier(l2) by TARSKI:def 3,VECTSP_6:def 4;
l.(F1/.k) = l1.(F1/.k) + l2.(F1/.k) by B8,VECTSP_6:22
.= l1.(F1/.k) + 0.INT.Ring by D2
.= l1.(F1/.k);
then D3: (ScFS(bu, l1, F1)).k
= (ScProductDM(L)).(bu, l.(F1/.k) * F1/.k) by C1,defScFSDM
.= (ScProductDM(L)).(l.(F1/.k) * F1/.k, bu) by ZMODLAT2:6
.= l.(F1/.k) * (ScProductDM(L)).(F1/.k, bu) by ZMODLAT2:6
.= l.(F1/.k) * (ScProductDM(L)).(bu, F1/.k) by ZMODLAT2:6;
F1.k in Carrier(l1) by B13,C1,C3,FUNCT_1:3;
then F1.k in Carrier(l) by B10,XBOOLE_0:def 5;
then F1.k in DualBasis(I) by B21;
then F1/.k in DualBasis(I) by C1,C3,PARTFUN1:def 6;
then D7: F1/.k in rng(B2DB(I)) by defB2DB;
then F1/.k in dom((B2DB(I))") by FUNCT_1:33;
then ((B2DB(I))").(F1/.k) in rng((B2DB(I))") by FUNCT_1:3;
then ((B2DB(I))").(F1/.k) in dom(B2DB(I)) by FUNCT_1:33;
then D6: ((B2DB(I))").(F1/.k) in I;
EMLat(L) is Submodule of DivisibleMod(L) by ZMODLAT2:20;
then reconsider bf = ((B2DB(I))").(F1/.k)
as Vector of DivisibleMod(L) by D6,ZMODUL01:25;
(B2DB(I)).bf = F1/.k by D7,FUNCT_1:35;
then (ScFS(bu, l1,F1)).k = l.(F1/.k) * 0.F_Real
by B4,D1,D3,D6,defB2DB
.= 0.F_Real;
hence (ScFS(bu, l1, F1)).k = -(ScFS(bu, l1, F1)).k
.= -(ScFS(bu, l1, F1))/.k by C1,PARTFUN1:def 6;
end;
suppose F1/.k = (B2DB(I)).bu;
then F1/.k = u by B31,FUNCT_1:35;
then (ScFS(bu, l1, F1)).k
= (ScProductDM(L)).(bu, 0.INT.Ring * F1/.k) by B11,C2
.= (ScProductDM(L)).(bu, 0.DivisibleMod(L)) by VECTSP_1:14
.= 0.F_Real by ZMODLAT2:14;
hence (ScFS(bu, l1, F1)).k = -(ScFS(bu, l1, F1)).k
.= -(ScFS(bu, l1, F1))/.k by C1,PARTFUN1:def 6;
end;
end;
then B15: Sum(ScFS(bu, l1, F1)) = -Sum(ScFS(bu, l1, F1))
by B14,RLVECT_2:4;
B16: SumSc(bu, l2) = (ScProductDM(L)).(bu, l2.u * u) by LmSumScDM14
.= (ScProductDM(L)).(l2.u * u, bu) by ZMODLAT2:6
.= l2.u * (ScProductDM(L)).(u, bu) by ZMODLAT2:6
.= l2.u * (ScProductDM(L)).(bu, u) by ZMODLAT2:6
.= l2.u * 1 by B4,B12,defB2DB
.= l2.u;
B17: l.u = l1.u + l2.u by B8,VECTSP_6:22
.= 0.INT.Ring + l2.u by B11
.= l2.u;
SumSc(bu, l) = SumSc(bu, l1) + SumSc(bu, l2) by B8,LmSumScDM1X
.= l.u by B13,B15,B16,B17;
hence contradiction by B1,B2,B5,VECTSP_6:2,ZMODLAT2:14;
end;
end;
definition
let L be RATional positive-definite Z_Lattice;
func DualLat(L) -> strict Z_Lattice means :defDualLat:
the carrier of it = DualSet L &
0.it = 0.DivisibleMod(L) &
the addF of it = (the addF of DivisibleMod(L)) || the carrier of it &
the lmult of it = (the lmult of DivisibleMod(L))
| [:the carrier of INT.Ring, the carrier of it:] &
the scalar of it = (ScProductDM(L)) || the carrier of it;
existence
proof
set A = DualSet L;
reconsider A as non empty Subset of DivisibleMod(L);
set ad = (the addF of DivisibleMod(L)) || A;
dom(the addF of DivisibleMod(L))
= [:the carrier of DivisibleMod(L), the carrier of DivisibleMod(L):]
by FUNCT_2:def 1;
then A3: dom ad = [:the carrier of DivisibleMod(L),
the carrier of DivisibleMod(L):] /\ [:A, A:] by RELAT_1:61
.= [:A, A:] by XBOOLE_1:28;
for x being object st x in [:A, A:] holds ad.x in A
proof
let x be object;
assume B1: x in [:A, A:];
then consider x1, x2 be object such that
B2: x1 in A & x2 in A & x = [x1, x2] by ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Vector of DivisibleMod(L) by B2;
ad.(x1, x2) = v1 + v2 by B1,B2,FUNCT_1:49;
hence thesis by B2,VECTSP_4:def 1;
end;
then reconsider ad as Function of [:A, A:],A by A3,FUNCT_2:3;
A6: [:the carrier of INT.Ring, A:] c=
[:the carrier of INT.Ring, the carrier of DivisibleMod(L):]
by ZFMISC_1:95;
set mu = (the lmult of DivisibleMod(L))
| [:the carrier of INT.Ring, A:];
dom(the lmult of DivisibleMod(L)) = [:the carrier of INT.Ring,
the carrier of DivisibleMod(L):] by FUNCT_2:def 1;
then A4: dom mu = [:the carrier of INT.Ring,
the carrier of DivisibleMod(L):]
/\ [:the carrier of INT.Ring, A:] by RELAT_1:61
.= [:the carrier of INT.Ring, A:] by A6,XBOOLE_1:28;
for x being object st x in [:the carrier of INT.Ring, A:] holds mu.x in A
proof
let x be object;
assume B1: x in [:the carrier of INT.Ring, A:];
then consider x1, x2 be object such that
B2: x1 in INT & x2 in A & x = [x1, x2] by ZFMISC_1:def 2;
reconsider i1 = x1 as Element of INT.Ring by B2;
reconsider v2 = x2 as Vector of DivisibleMod(L) by B2;
mu.(x1, x2) = i1*v2 by B1,B2,FUNCT_1:49;
hence thesis by B2,VECTSP_4:def 1;
end;
then reconsider mu as Function of
[:the carrier of INT.Ring, A:],A by A4,FUNCT_2:3;
set sc = (ScProductDM(L)) || A;
dom(ScProductDM(L))
= [:the carrier of DivisibleMod(L), the carrier of DivisibleMod(L):]
by FUNCT_2:def 1;
then A5: dom sc = [:the carrier of DivisibleMod(L),
the carrier of DivisibleMod(L):] /\ [:A, A:] by RELAT_1:61
.= [:A, A:] by XBOOLE_1:28;
for x being object st x in [:A, A:] holds sc.x in the carrier of F_Real
proof
let x be object;
assume B1: x in [:A, A:];
then consider x1, x2 be object such that
B2: x1 in A & x2 in A & x = [x1, x2] by ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Vector of DivisibleMod(L) by B2;
sc.(x1, x2) = (ScProductDM(L)).(v1, v2) by B1,B2,FUNCT_1:49;
hence thesis by B2;
end;
then reconsider sc as Function of [:A, A:],the carrier of F_Real
by A5,FUNCT_2:3;
reconsider ze = 0.DivisibleMod(L) as Element of A by ZMODUL01:18;
set L1 = LatticeStr (# A, ad, ze, mu, sc #);
reconsider L1 as non empty LatticeStr over INT.Ring;
A7: L1 is Submodule of DivisibleMod(L) by ZMODLAT2:10;
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 ZMODLAT2:10;
set I = the Basis of EMLat(L);
for v being Vector of DivisibleMod(L) st v in L1
holds v in Lin DualBasis(I)
proof
let v be Vector of DivisibleMod(L) such that
B1: v in L1;
consider x be Dual of L such that
B2: x = v by B1;
thus thesis by B2,ThDE3;
end;
then L1 is Submodule of Lin DualBasis(I) by A7,ZMODUL01:44;
then reconsider L1 as strict Z_Lattice by A7,ZMODLAT2:27;
take L1;
thus thesis;
end;
uniqueness;
end;
theorem ThDL1:
for L being RATional positive-definite Z_Lattice,
v being Vector of DivisibleMod(L) holds
v in DualLat(L) iff v is Dual of L
proof
let L be RATional positive-definite Z_Lattice,
v be Vector of DivisibleMod(L);
hereby
assume v in DualLat(L);
then v in DualSet L by defDualLat;
then consider x be Dual of L such that
A1: x = v;
thus v is Dual of L by A1;
end;
assume v is Dual of L;
then v in DualSet L;
hence v in DualLat(L) by defDualLat;
end;
theorem ThDL2:
for L being RATional positive-definite Z_Lattice holds
DualLat(L) is Submodule of DivisibleMod(L)
proof
let L be RATional positive-definite Z_Lattice;
A1: the carrier of DualLat(L) c= the carrier of DivisibleMod(L)
proof
let x be object such that
B1: x in the carrier of DualLat(L);
x in DualSet L by B1,defDualLat;
then consider v be Dual of L such that
B2: x = v;
thus thesis by B2;
end;
0.DualLat(L) = 0.DivisibleMod(L) &
the addF of DualLat(L)
= (the addF of DivisibleMod(L)) || the carrier of DualLat(L) &
the lmult of DualLat(L) = (the lmult of DivisibleMod(L))
| [:the carrier of INT.Ring, the carrier of DualLat(L):] by defDualLat;
hence thesis by A1,VECTSP_4:def 2;
end;
theorem ThELEM1:
for L being Z_Lattice, I being Basis of EMLat(L) holds
I is Basis of EMbedding(L)
proof
let L be Z_Lattice, I be Basis of EMLat(L);
the ModuleStr of EMLat(L) = the ModuleStr of EMbedding(L) by ZMODLAT2:28;
hence thesis by ZMODLAT2:35;
end;
theorem
for L being Z_Lattice, I being Basis of EMbedding(L) holds
I is Basis of EMLat(L)
proof
let L be Z_Lattice, I be Basis of EMbedding(L);
the ModuleStr of EMLat(L) = the ModuleStr of EMbedding(L) by ZMODLAT2:28;
hence thesis by ZMODLAT2:35;
end;
theorem ThDB2:
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L), v being Vector of DivisibleMod(L)
st v in DualBasis(I)
holds v is Dual of L
proof
let L be RATional positive-definite Z_Lattice,
I be Basis of EMLat(L), v be Vector of DivisibleMod(L) such that
A1: v in DualBasis(I);
consider u be Vector of EMLat(L) such that
A2: u in I & (ScProductDM(L)).(u, v) = 1 &
(for w being Vector of EMLat(L) st w in I & u <> w
holds (ScProductDM(L)).(w, v) = 0) by A1,defDualBasis;
reconsider J = I as Basis of EMbedding(L) by ThELEM1;
for w being Vector of DivisibleMod(L) st w in J holds
(ScProductDM(L)).(v, w) in INT.Ring
proof
let w be Vector of DivisibleMod(L) such that
B1: w in J;
per cases;
suppose u <> w;
then (ScProductDM(L)).(w, v) = 0 by A2,B1;
then (ScProductDM(L)).(v, w) = 0 by ZMODLAT2:6;
hence thesis;
end;
suppose u = w;
then (ScProductDM(L)).(v, w) = 1 by A2,ZMODLAT2:6;
hence thesis;
end;
end;
hence thesis by LmDE21;
end;
theorem ThDLDB:
for L being RATional positive-definite Z_Lattice,
I being Basis of EMLat(L) holds
DualBasis(I) is Basis of DualLat(L)
proof
let L be RATional positive-definite Z_Lattice,
I be Basis of EMLat(L);
reconsider DL = DualLat(L) as Submodule of DivisibleMod(L) by ThDL2;
for v being Vector of DivisibleMod(L) st v in DualBasis(I)
holds v in the carrier of DualLat(L)
proof
let v be Vector of DivisibleMod(L) such that
B1: v in DualBasis(I);
v in DualLat(L) by B1,ThDB2,ThDL1;
hence thesis;
end;
then DualBasis(I) c= the carrier of DualLat(L);
then reconsider DB = DualBasis(I)
as linearly-independent Subset of DL by ZMODUL03:16;
A2: for v being Vector of DivisibleMod(L) st v in the ModuleStr of DL
holds v in Lin DualBasis(I)
proof
let v be Vector of DivisibleMod(L) such that
B1: v in the ModuleStr of DL;
v in DualLat(L) by B1;
hence thesis by ThDE3,ThDL1;
end;
A3: for v being Vector of DivisibleMod(L) st v in Lin DualBasis(I)
holds v in the ModuleStr of DL
proof
let v be Vector of DivisibleMod(L) such that
B1: v in Lin DualBasis(I);
consider l be Linear_Combination of DualBasis(I) such that
B2: v = Sum(l) by B1,VECTSP_7:7;
reconsider J = I as Basis of EMbedding(L) by ThELEM1;
for u being Vector of DivisibleMod(L) st u in J
holds (ScProductDM(L)).(v, u) in INT.Ring
proof
let u be Vector of DivisibleMod(L) such that
C1: u in J;
C2: (ScProductDM(L)).(u, v) = l.((B2DB(I)).u) by B2,C1,LmDE32;
u in dom(B2DB(I)) by C1,defB2DB;
then (B2DB(I)).u in rng(B2DB(I)) by FUNCT_1:3;
then (B2DB(I)).u in DualBasis(I);
then l.((B2DB(I)).u) in the carrier of INT.Ring by FUNCT_2:5;
hence thesis by C2,ZMODLAT2:6;
end;
then v in DL by LmDE21,ThDL1;
hence thesis;
end;
(Omega).DL is Submodule of DL;
then the ModuleStr of DL is Submodule of DivisibleMod(L) by ZMODUL01:42;
then the ModuleStr of DualLat(L) = Lin DualBasis(I) by A2,A3,ZMODUL01:46
.= Lin DB by ZMODUL03:20;
hence thesis by VECTSP_7:def 3;
end;
theorem
for L being RATional positive-definite Z_Lattice,
b being OrdBasis of EMLat(L), I being Basis of EMLat(L)
st I = rng b holds
(B2DB(I))*b is OrdBasis of DualLat(L)
proof
let L be RATional positive-definite Z_Lattice,
b be OrdBasis of EMLat(L), I be Basis of EMLat(L) such that
A1: I = rng b;
A2: b is one-to-one by ZMATRLIN:def 5;
b is FinSequence of I by A1,FINSEQ_1:def 4; then
A3: (B2DB(I))*b is FinSequence of DualBasis(I) by FINSEQ_2:32;
A4: dom(B2DB(I)) = I by defB2DB;
A5: rng((B2DB(I))*b) = (B2DB(I)).: (rng b) by RELAT_1:127
.= rng(B2DB(I)) by A1,A4,RELAT_1:113
.= DualBasis(I) by defB2DB;
DualBasis(I) is Subset of DualLat(L) by ThDLDB;
then A6: (B2DB(I))*b is FinSequence of DualLat(L) by A3,A5,FINSEQ_1:def 4;
rng((B2DB(I))*b) is Basis of DualLat(L) by A5,ThDLDB;
hence thesis by A2,A6,ZMATRLIN:def 5;
end;
theorem LmEMDetX3:
for L be positive-definite finite-rank free Z_Lattice,
b being OrdBasis of L, e being OrdBasis of EMLat(L)
st e = (MorphsZQ(L))*b
holds GramMatrix(InnerProduct(L), b) = GramMatrix(InnerProduct(EMLat(L)), e)
proof
let L be positive-definite finite-rank free Z_Lattice,
b be OrdBasis of L, e be OrdBasis of EMLat(L);
assume AS: e = (MorphsZQ(L))*b;
R1: rank (L) = rank(EMLat(L)) by ZMODLAT2:42;
R2: len GramMatrix(InnerProduct(L), b) = rank L &
width GramMatrix(InnerProduct(L), b) = rank L &
Indices GramMatrix(InnerProduct(L), b)
= [:Seg (rank L), Seg (rank L):] by MATRIX_0:24;
S2: len GramMatrix(InnerProduct(EMLat(L)), e) = rank EMLat(L) &
width GramMatrix(InnerProduct(EMLat(L)), e) = rank EMLat(L) &
Indices GramMatrix(InnerProduct(EMLat(L)), e)
= [:Seg (rank EMLat(L)), Seg (rank EMLat(L)):] by MATRIX_0:24;
for i,j being Nat st [i,j] in Indices GramMatrix(InnerProduct(L), b)
holds GramMatrix(InnerProduct(L), b)*(i,j)
= GramMatrix(InnerProduct(EMLat(L)), e)*(i,j)
proof
let i, j be Nat;
assume [i, j] in Indices GramMatrix(InnerProduct(L), b);
then X1: i in Seg (rank L) & j in Seg (rank L) by R2,ZFMISC_1:87;
then A2: i in dom b & j in dom b by R2,FINSEQ_1:def 3,MATRIX_0:24;
then A3: GramMatrix(InnerProduct(L), b)*(i,j)
= (InnerProduct(L)).(b/.i, b/.j) by ZMODLAT1:def 32;
A4: i in dom e & j in dom e by R1,S2,X1,FINSEQ_1:def 3,MATRIX_0:24;
Y0: the carrier of EMLat(L) = rng MorphsZQ(L) by ZMODLAT2:def 4
.= the carrier of EMbedding(L) by ZMODUL08:def 3;
Y1: e/.i = e.i by A4,PARTFUN1:def 6
.= (MorphsZQ(L)).(b.i) by A2,AS,FUNCT_1:13
.= (MorphsZQ(L)).(b/.i) by A2,PARTFUN1:def 6;
Y2: e/.j = e.j by A4,PARTFUN1:def 6
.= (MorphsZQ(L)).(b.j) by A2,AS,FUNCT_1:13
.= (MorphsZQ(L)).(b/.j) by A2,PARTFUN1:def 6;
reconsider ei = e/.i, ej = e/.j as Vector of EMbedding(L) by Y0;
(InnerProduct(EMLat(L))).(e/.i, e/.j) = (ScProductEM(L)).(ei, ej)
by ZMODLAT2:def 4
.= <; b/.i, b/.j;> by Y1,Y2,ZMODLAT2:def 2
.= (InnerProduct(L)).(b/.i, b/.j);
hence thesis by A3,A4,ZMODLAT1:def 32;
end;
hence thesis by MATRIX_0:27,R1;
end;
theorem
for L being positive-definite finite-rank free Z_Lattice holds
GramDet(InnerProduct(L)) = GramDet(InnerProduct(EMLat(L)))
proof
let L be positive-definite finite-rank free Z_Lattice;
set b = the OrdBasis of L;
reconsider e = (MorphsZQ(L))*b as OrdBasis of EMLat(L) by ZMODLAT2:41;
P1: GramMatrix(InnerProduct(L), b) = GramMatrix(InnerProduct(EMLat(L)), e)
by LmEMDetX3;
GramDet(InnerProduct(L)) = Det GramMatrix(InnerProduct(L), b)
by ZMODLAT1:def 35
.= Det GramMatrix(InnerProduct(EMLat(L)), e) by P1,ZMODLAT2:42
.= GramDet(InnerProduct(EMLat(L))) by ZMODLAT1:def 35;
hence thesis;
end;
theorem ThRankDL:
for L being RATional positive-definite Z_Lattice holds
rank(L) = rank(DualLat(L))
proof
let L be RATional positive-definite Z_Lattice;
set I = the Basis of EMLat(L);
DualBasis(I) is Basis of DualLat(L) by ThDLDB;
then rank DualLat(L) = card DualBasis(I) by ZMODUL03:def 5
.= card I by ThDB1
.= rank EMLat(L) by ZMODUL03:def 5;
hence thesis by ZMODLAT2:42;
end;
theorem
for L being INTegral positive-definite Z_Lattice holds
EMLat(L) is Z_Sublattice of DualLat(L)
proof
let L be INTegral positive-definite Z_Lattice;
A1: EMLat(L) is Submodule of DivisibleMod(L) by ZMODLAT2:20;
A2: DualLat(L) is Submodule of DivisibleMod(L) by ThDL2;
for v being Vector of DivisibleMod(L) st v in EMLat(L)
holds v in DualLat(L)
proof
let v be Vector of DivisibleMod(L) such that
B1: v in EMLat(L);
set I = the Basis of EMLat(L);
reconsider J = I as Basis of EMbedding(L) by ThELEM1;
for u being Vector of DivisibleMod(L) st u in J
holds (ScProductDM(L)).(v, u) in INT.Ring
proof
let u be Vector of DivisibleMod(L) such that
C1: u in J;
reconsider vv = v as Vector of EMLat(L) by B1;
reconsider uu = u as Vector of EMLat(L) by C1;
the ModuleStr of EMLat(L) = EMbedding(L) by ZMODLAT2:28;
then (ScProductDM(L)).(v, u) = (ScProductEM(L)).(vv, uu) by ZMODLAT2:8
.= <; vv, uu ;> by ZMODLAT2:def 4;
hence thesis by ZMODLAT1:def 5;
end;
hence thesis by LmDE21,ThDL1;
end;
then EMLat(L) is Submodule of DualLat(L) by A1,A2,ZMODUL01:44;
then A3: the carrier of EMLat(L) c= the carrier of DualLat(L) &
0.EMLat(L) = 0.DualLat(L) &
the addF of EMLat(L) = (the addF of DualLat(L)) ||
the carrier of EMLat(L) &
the lmult of EMLat(L) = (the lmult of DualLat(L)) |
[:the carrier of INT.Ring, the carrier of EMLat(L):] by VECTSP_4:def 2;
A4: [:the carrier of EMLat(L), the carrier of EMLat(L):]
c= [:the carrier of DualLat(L), the carrier of DualLat(L):]
by A3,ZFMISC_1:96;
(the scalar of DualLat(L)) || the carrier of EMLat(L)
= ((ScProductDM(L)) || the carrier of DualLat(L)) ||
the carrier of EMLat(L) by defDualLat
.= (ScProductDM(L)) || the carrier of EMLat(L) by A4,FUNCT_1:51
.= (ScProductDM(L)) || (rng MorphsZQ(L)) by ZMODLAT2:def 4
.= ScProductEM(L) by ZMODLAT2:7
.= the scalar of EMLat(L) by ZMODLAT2:def 4;
hence thesis by A3,ZMODLAT1:def 9;
end;
theorem
for L being Z_Lattice,
b being OrdBasis of L
st GramMatrix(InnerProduct(L), b) is Matrix of dim(L), INT.Ring
holds L is INTegral
proof
let L be Z_Lattice, b be OrdBasis of L such that
A1: GramMatrix(InnerProduct(L), b) is Matrix of dim(L), INT.Ring;
set I = rng b;
reconsider I as Basis of L by ZMATRLIN:def 5;
set GM = GramMatrix(InnerProduct(L), b);
reconsider GMI = GM as Matrix of dim(L), INT.Ring by A1;
for v, u being Vector of L st v in I & u in I holds
<; v, u ;> in INT
proof
let v, u be Vector of L such that
B1: v in I & u in I;
consider i be Nat such that
B2: i in dom b & b.i = v by B1,FINSEQ_2:10;
consider j be Nat such that
B3: j in dom b & b.j = u by B1,FINSEQ_2:10;
B4: b/.i = v by B2,PARTFUN1:def 6;
B6: GM*(i, j) = (InnerProduct(L)).(b/.i, b/.j) by B2,B3,ZMODLAT1:def 32
.= <; v, u ;> by B3,B4,PARTFUN1:def 6;
B7: dom b = Seg(len b) by FINSEQ_1:def 3
.= Seg dim(L) by ZMATRLIN:49;
Indices GM = [:Seg dim(L), Seg dim(L):] by MATRIX_0:24;
then [i, j] in Indices GM by B2,B3,B7,ZFMISC_1:87;
then GM*(i, j) = GMI*(i, j) by ZMATRLIN:1;
hence thesis by B6;
end;
hence thesis by ZMODLAT1:15;
end;
theorem ThRatLat1B:
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 RAT holds
for v being Vector of L st v in Lin(I) holds <; v, u ;> in RAT
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 RAT;
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 RAT holds
for v being Vector of L st v in Lin(I) holds <; v, u ;> in RAT;
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 RAT;
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 ZMODLAT1:12;
hence <; v, u ;> in RAT by RAT_1:def 2;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A0: P[n];
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 RAT;
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 RAT
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 RAT by A1;
end;
thus for x being Vector of L st x in Lin(I) holds <; x, u ;> in RAT
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,ZMODLAT1:10;
B14: <; xu1,u ;> in RAT by A0,A5,B8,A10;
<; v,u ;> in RAT by A1,A3;
hence <; x, u ;> in RAT by B13,B14,RAT_1:def 2;
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 ThRatLat1A:
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 RAT
holds for v, u being Vector of L holds <; v, u ;> in RAT
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 RAT
holds
for v, u being Vector of L st v in Lin(I) & u in Lin(I)
holds <; v, u ;> in RAT;
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 RAT;
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 ZMODLAT1:12;
hence <; v, u ;> in RAT by RAT_1:def 2;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A0: P[n];
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 RAT;
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 RAT
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 RAT by A1;
end;
A6X: for x being Vector of L st x in J holds <; x, v ;> in RAT
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 RAT by A1;
end;
thus for x, y being Vector of L st x in Lin(I) & y in Lin(I) holds
<; x, y ;> in RAT
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,ZMODLAT1:8
.= i1 * <; xu1, yu1 ;> + ixu2 * <; v, yu1 ;>
+ <; i1*xu1 + ixu2*v, iyu2*v ;> by ZMODLAT1:10
.= i1 * <; xu1, yu1 ;> + ixu2 * <; v, yu1;>
+ (i1 * <; xu1, iyu2*v ;> + ixu2 * <; v, iyu2*v ;>) by ZMODLAT1:10
.= <; 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 ZMODLAT1:9
.= <; xu1, yu1 ;> + ixu2 * <;v,yu1;>
+ iyu2 * <; xu1, v ;> + (ixu2 * iyu2) * <; v, v ;> by ZMODLAT1:9;
B14: <; xu1, yu1 ;> in RAT by A0,A5,B8,A10,A11;
<; yu1, v ;> in RAT by A11,A6X,ThRatLat1B;
then B15: <; v, yu1 ;> in RAT by ZMODLAT1:def 3;
B16: <; xu1, v ;> in RAT by A10,A6X,ThRatLat1B;
<; v, v ;> in RAT by A3,A1;
hence <; x, y ;> in RAT by B13,B14,B15,B16,RAT_1:def 2;
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 RAT;
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 RAT by X1,X2,X4;
end;
theorem ThRatLat1:
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 RAT
holds L is RATional
proof
let L be Z_Lattice, I be Basis of L such that
A1: for v, u being Vector of L st v in I & u in I holds
<; v, u ;> in RAT;
for v, u being Vector of L holds <; v, u ;> in RAT by A1,ThRatLat1A;
hence thesis by ZMODLAT2:def 1;
end;
theorem
for L being Z_Lattice,
b being OrdBasis of L
st GramMatrix(InnerProduct(L), b) is Matrix of dim(L), F_Rat
holds L is RATional
proof
let L be Z_Lattice, b be OrdBasis of L such that
A1: GramMatrix(InnerProduct(L), b) is Matrix of dim(L), F_Rat;
set I = rng b;
reconsider I as Basis of L by ZMATRLIN:def 5;
set GM = GramMatrix(InnerProduct(L), b);
reconsider GMR = GM as Matrix of dim(L), F_Rat by A1;
for v, u being Vector of L st v in I & u in I holds
<; v, u ;> in RAT
proof
let v, u be Vector of L such that
B1: v in I & u in I;
consider i be Nat such that
B2: i in dom b & b.i = v by B1,FINSEQ_2:10;
consider j be Nat such that
B3: j in dom b & b.j = u by B1,FINSEQ_2:10;
B4: b/.i = v by B2,PARTFUN1:def 6;
B6: GM*(i, j) = (InnerProduct(L)).(b/.i, b/.j) by B2,B3,ZMODLAT1:def 32
.= <; v, u ;> by B3,B4,PARTFUN1:def 6;
B7: dom b = Seg(len b) by FINSEQ_1:def 3
.= Seg dim(L) by ZMATRLIN:49;
Indices GM = [:Seg dim(L), Seg dim(L):] by MATRIX_0:24;
then [i, j] in Indices GM by B2,B3,B7,ZFMISC_1:87;
then GM*(i, j) = GMR*(i, j) by ZMATRLIN:1;
hence thesis by B6;
end;
hence thesis by ThRatLat1;
end;
registration
let L be RATional positive-definite Z_Lattice;
cluster DualLat(L) -> RATional;
correctness
proof
A1: the scalar of DualLat(L) = (ScProductDM(L)) || the carrier of DualLat(L)
by defDualLat;
DualLat(L) is Submodule of DivisibleMod(L) by ThDL2;
hence thesis by A1,ThSLGM1;
end;
end;
theorem ThSLGM2:
for L being RATional Z_Lattice, LX being Z_Lattice,
b being OrdBasis of LX
st LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX
holds GramMatrix(InnerProduct(LX), b) is Matrix of dim(LX), F_Rat
proof
let L be RATional Z_Lattice, LX be Z_Lattice,
b be OrdBasis of LX such that
A1: LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX;
LX is RATional by A1,ThSLGM1;
then GramMatrix(b) is Matrix of dim(LX), F_Rat by ZMODLAT2:45;
hence thesis;
end;
theorem
for L being RATional positive-definite Z_Lattice,
b being OrdBasis of DualLat(L)
holds GramMatrix(InnerProduct(DualLat(L)), b) is Matrix of dim(L), F_Rat
proof
let L be RATional positive-definite Z_Lattice,
b be OrdBasis of DualLat(L);
A1: the scalar of DualLat(L) = (ScProductDM(L)) || the carrier of DualLat(L)
by defDualLat;
A2: DualLat(L) is Submodule of DivisibleMod(L) by ThDL2;
dim(L) = dim(DualLat(L)) by ThRankDL;
hence thesis by A1,A2,ThSLGM2;
end;
theorem ThSLGM3:
for L being positive-definite Z_Lattice,
LX being Z_Lattice
st LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX
holds LX is positive-definite
proof
let L be positive-definite Z_Lattice, LX be Z_Lattice such that
A1: LX is Submodule of DivisibleMod(L) &
the scalar of LX = (ScProductDM(L)) || the carrier of LX;
for v being Vector of LX st v <> 0.LX holds ||. v .|| > 0
proof
let v be Vector of LX such that
B1: v <> 0.LX;
reconsider vv = v as Vector of DivisibleMod(L) by A1,ZMODUL01:25;
B3: ||. v .|| = (ScProductDM(L)).(vv, vv) by A1,FUNCT_1:49;
consider i be Element of INT.Ring such that
B4: i <> 0 & i * vv in EMbedding(L) by ZMODUL08:29;
i * vv in rng MorphsZQ(L) by B4,ZMODUL08:def 3;
then reconsider iv = i * vv as Vector of EMLat(L) by ZMODLAT2:def 4;
B5: (i * i) * ||. v .|| = i * (i* (ScProductDM(L)).(vv, vv)) by B3
.= i * (ScProductDM(L)).(vv, i*vv) by ZMODLAT2:13
.= (ScProductDM(L)).(i*vv, i*vv) by ZMODLAT2:6
.= (ScProductEM(L)).(iv, iv) by B4,ZMODLAT2:8
.= ||. iv .|| by ZMODLAT2:def 4;
i <> 0.INT.Ring by B4;
then i*v <> 0.LX by B1,ZMODUL01:def 7;
then i*vv <> 0.LX by A1,ZMODUL01:29;
then iv <> 0.DivisibleMod(L) by A1,VECTSP_4:def 2;
then iv <> zeroCoset(L) by ZMODUL08:def 4;
then iv <> 0.EMLat(L) by ZMODLAT2:def 4;
then ||. iv .|| > 0 by ZMODLAT1:def 6;
hence ||. v .|| > 0 by B5,XREAL_1:63,XREAL_1:131;
end;
hence thesis;
end;
registration
let L be RATional positive-definite Z_Lattice;
cluster DualLat(L) -> positive-definite;
correctness
proof
A1: DualLat(L) is Submodule of DivisibleMod(L) by ThDL2;
the scalar of DualLat(L) = (ScProductDM(L)) || the carrier of DualLat(L)
by defDualLat;
hence thesis by A1,ThSLGM3;
end;
end;
registration
let L be non trivial RATional positive-definite Z_Lattice;
cluster DualLat(L) -> non trivial;
correctness
proof
rank L > 0;
then rank DualLat(L) <> 0 by ThRankDL;
then (Omega).DualLat(L) <> (0).DualLat(L) by ZMODUL05:1;
hence thesis by ZMODUL07:41;
end;
end;