:: Embedded Lattice and Properties of {G}ram Matrix
:: by Yuichi Futa and Yasunari Shidama
::
:: Received March 17, 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, RAT_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, QC_LANG1, BINOP_1, ZFMISC_1, INT_1,
RLVECT_2, ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, FINSEQ_2,
UPROOTS, GROUP_1, INT_3, VECTSP_1, MESFUNC1, XCMPLX_0, FUNCSDOM,
REALSET1, MATRLIN, ZMODUL02, RLVECT_5, NORMSP_1, BHSP_1, MATRIX_1,
MATRIX_3, MOD_3, ZMATRLIN, ZMODLAT1, TREES_1, MFOLD_2, ZMODUL04,
ZMODUL08, FUNCT_2, ZMODLAT2, VECTSP10, VECTSP_2, MSAFREE2, EQREL_1,
VALUED_1, INT_2, RELAT_2, LAPLACE, CLASSES1, LMOD_7, PRVECT_1, MATRIX13;
notations GCD_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1,
FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1,
FUNCOP_1, REALSET1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0,
INT_1, RAT_1, INT_2, FINSEQ_1, FINSEQ_2, EQREL_1, MATRIX_0,
STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, PRVECT_1,
VECTSP_2, VECTSP_4, VECTSP_6, VECTSP_7, RANKNULL, MATRIX_1,
MATRIX_3, INT_3, ZMODUL01, ZMODUL03, GAUSSINT, ZMODUL04, ZMATRLIN,
ZMODLAT1, ZMODUL08, MATRIX_6, LAPLACE, NAT_D, MATRIX13;
constructors GCD_1, BINOP_2, UPROOTS, REALSET1, ALGSTR_1, ZMODUL01, EC_PF_1,
ZMODUL04, ZMODUL07, ZMODLAT1, ZMODUL08, MATRIX_6, LAPLACE, MATRIX13,
RELSET_1, FVSUM_1, MATRIX_3;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0,
STRUCT_0, RLVECT_1, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1,
ZMODUL01, XBOOLE_0, BINOP_2, ORDINAL1, XXREAL_0, NAT_1, INT_3,
REALSET1, RELAT_1, VECTSP_1, VECTSP_2, GAUSSINT, RAT_1, XCMPLX_0,
ZMODUL03, ZMODUL04, ZMODUL05, ZMODUL06, MATRIX_0, ZMODLAT1,
ZMODUL08, PRVECT_1, MATRIX13, RING_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions ZMODLAT1, XBOOLE_0, FUNCT_1, TARSKI;
equalities XCMPLX_0, BINOP_1, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, VECTSP_4,
REALSET1, FINSEQ_1, ZMODLAT1, ZMODUL08, RELAT_1, LAPLACE, FINSEQ_2,
GAUSSINT, VECTSP_6;
expansions TARSKI, STRUCT_0, FINSEQ_1, FUNCT_2, ZMODLAT1, XBOOLE_0, 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, XTUPLE_0, SUBSET_1,
ZMODUL05, RELAT_1, VECTSP_2, ZMODUL03, XBOOLE_0, XBOOLE_1, FUNCOP_1,
XREAL_1, XXREAL_0, PARTFUN1, VECTSP_1, ZMODUL02, VECTSP_7, NUMBERS,
VECTSP_4, MATRIX_0, ZMODUL06, MATRIXR2, ZMATRLIN, ZMODLAT1, ZMODUL04,
ZMODUL08, XCMPLX_1, ZMODUL07, ORDINAL1, INT_2, NAT_D, VECTSP_6, RAT_1,
XREAL_0, GROUP_1, FINSEQ_2, XCMPLX_0, MATRIX_6, LAPLACE, MATRIX13,
PRVECT_1, RLVECT_2, STRUCT_0;
schemes FINSEQ_1, FUNCT_2, NAT_1;
begin :: 1. Inner product of embedded module
LMBASE2A:
for A,B being set, F,G being FinSequence
st F is one-to-one & G is one-to-one
& A /\ B = {} & rng F = A & rng G = B
holds F^G is one-to-one & dom (F^G) = Seg (len F + len G)
& rng (F^G) = (rng F) \/ (rng G)
proof
let A, B be set, F,G be FinSequence such that
A1:F is one-to-one and
A2: G is one-to-one and
A3: A /\ B = {} and
A4: rng F = A & rng G = B;
dom (F^G) = Seg (len (F^G)) by FINSEQ_1:def 3
.= Seg (len F + len G) by FINSEQ_1:22;
hence thesis by A1,A2,A3,A4,FINSEQ_1:31,FINSEQ_3:91,XBOOLE_0:def 7;
end;
LMBASE2C:
for K being Ring,
V being LeftMod of K,
L being Linear_Combination of V,
F being FinSequence of V
st (rng F) /\ Carrier(L) = {}
holds L(#)F = dom F --> 0.V
proof
let K be Ring, V be LeftMod of K,
L be Linear_Combination of V,
F be FinSequence of V;
assume AS:(rng F) /\ Carrier(L) = {};
P1: len (L(#)F) = len F by VECTSP_6:def 5; then
p1: dom (L(#)F) = dom F by FINSEQ_3:29;
for z being object st z in dom (L(#)F) holds (L(#)F).z = 0.V
proof
let z be object;
assume X1: z in dom (L(#)F); then
reconsider i = z as Nat;
X3: i in dom F by X1,P1,FINSEQ_3:29;
then F.i in rng F by FUNCT_1:3; then
X4: not F.i in Carrier(L) by XBOOLE_0:def 4,AS;
F/.i = F.i by X3,PARTFUN1:def 6;
then L.(F/.i) = 0.K by X4;
hence (L(#)F).z = 0.K * F/.i by X1,VECTSP_6:def 5
.= 0.V by VECTSP_1:14;
end;
hence thesis by FUNCOP_1:11,p1;
end;
LMBASE2D:
for K being Ring,
V being LeftMod of K,
F being FinSequence of V
st F = dom F --> 0.V
holds Sum(F) = 0.V
proof
let K be Ring,
V be LeftMod of K,
F be FinSequence of V;
assume AS: F = dom F --> 0.V;
X2: len F = len F;
for k being Nat
for v being Element of V st k in dom F & v = F.k holds F.k = 0.K * v
proof
let k be Nat;
let v be Element of V;
assume k in dom F & v = F.k;
hence F.k = 0.V by FUNCOP_1:7,AS
.= 0.K * v by VECTSP_1:14;
end;
hence Sum F = 0.K * (Sum F) by X2,RLVECT_2:66
.= 0.V by VECTSP_1:14;
end;
theorem EQSUMLF:
for K being Ring,
V being LeftMod of K,
L being Function of the carrier of V, the carrier of K,
A being Subset of V,
F, F1 being FinSequence of the carrier of V
st F is one-to-one & rng F = A
& F1 is one-to-one & rng F1 = A
holds Sum(L (#) F) = Sum(L (#) F1)
proof
let K be Ring,
V be LeftMod of K,
L be Function of the carrier of V, the carrier of K,
A be Subset of V,
F, F1 be FinSequence of the carrier of V;
assume that
A4: F is one-to-one and
A5:rng F = A and
A7: F1 is one-to-one and
A8: rng F1 = A;
set v1 = Sum (L (#) F);
set v2 = Sum (L (#) F1);
defpred S1[object, object] means {$2} = F" {(F1.$1)};
A10: len F = len F1 by A4,A5,A7,A8,FINSEQ_1:48;
A11: dom F = Seg (len F) by FINSEQ_1:def 3;
A12: dom F1 = Seg (len F1) by FINSEQ_1:def 3;
A13: for x being object st x in dom F holds
ex y being object st y in dom F & S1[x,y]
proof
let x be object;
assume x in dom F;
then F1.x in rng F by A5,A8,A10,A11,A12,FUNCT_1:def 3;
then consider y be object such that
A14: F" {(F1.x)} = {y} by A4, FUNCT_1:74;
take y;
y in F" {(F1.x)} by A14,TARSKI:def 1;
hence y in dom F by FUNCT_1:def 7;
thus S1[x,y] by A14;
end;
consider f be Function of (dom F),(dom F) such that
A15: for x being object st x in dom F holds S1[x,f.x]
from FUNCT_2:sch 1(A13);
A16: rng f = dom F
proof
thus rng f c= dom F;
let y be object;
assume A17: y in dom F;
then F.y in rng F1 by A5,A8,FUNCT_1:def 3;
then consider x be object such that
A18: x in dom F1 and
A19: F1.x = F.y by FUNCT_1:def 3;
F" {(F1.x)} = F" (Im(F, y)) by A17,A19,FUNCT_1:59;
then F" {(F1.x)} c= {y} by A4,FUNCT_1:82;
then {(f.x)} c= {y} by A10,A11,A12,A15,A18;
then A20: f.x = y by ZFMISC_1:18;
x in dom f by A10,A11,A12,A18,FUNCT_2:def 1;
hence y in rng f by A20,FUNCT_1:def 3;
end;
reconsider G1 = L (#) F as FinSequence of V;
A21: len G1 = len F by VECTSP_6:def 5;
A22: f is one-to-one
proof
let y1, y2 be object;
assume that
A23: y1 in dom f and
A24: y2 in dom f and
A25: f.y1 = f.y2;
A28: F" {(F1.y2)} = {(f.y2)} by A15,A24;
F1.y1 in rng F by A5,A8,A10,A11,A12,A23,FUNCT_1:def 3;
then A30: {(F1.y1)} c= rng F by ZFMISC_1:31;
F1.y2 in rng F by A5,A8,A10,A11,A12,A24,FUNCT_1:def 3;
then A31: {(F1.y2)} c= rng F by ZFMISC_1:31;
F" {(F1.y1)} = {(f.y1)} by A15,A23;
then {(F1.y1)} = {(F1.y2)} by A25,A28,A30,A31,FUNCT_1:91;
hence y1 = y2 by A7,A10,A11,A12,A23,A24,ZFMISC_1:3;
end;
set G2 = L (#) F1;
A33: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def 3;
reconsider f as Permutation of (dom F) by A16, A22, FUNCT_2:57;
( dom F = Seg (len F) & dom G1 = Seg (len G1)) by FINSEQ_1:def 3;
then reconsider f as Permutation of (dom G1) by A21;
A34: len (L (#) F1) = len F1 by VECTSP_6:def 5;
A35: dom G1 = Seg (len G1) by FINSEQ_1:def 3;
now
let i be Nat;
assume A36: i in dom (L (#) F1);
then A37: ( (L (#) F1).i = (L.(F1/.i)) * (F1/.i) &
F1.i = F1/.i) by A34,A12,A33,VECTSP_6:def 5,PARTFUN1:def 6;
i in dom F1 by A34,A36,FINSEQ_3:29;
then reconsider u = F1.i as Element of V by FINSEQ_2:11;
i in dom f by A10,A21,A34,A35,A33,A36,FUNCT_2:def 1;
then A38: f.i in dom F by A16,FUNCT_1:def 3;
then reconsider m = f.i as Element of NAT;
reconsider v = F.m as Element of V by A38,FINSEQ_2:11;
{(F.(f.i))} = Im(F, (f.i)) by A38,FUNCT_1:59
.= F.: (F" {(F1.i)}) by A10,A34,A11,A33,A15,A36;
then A39: u = v by FUNCT_1:75,ZFMISC_1:18;
F.m = F/.m by A38,PARTFUN1:def 6;
hence (L (#) F1).i = G1.(f.i) by A21,A11,A35,A38,A39,A37,VECTSP_6:def 5;
end;
hence v1 = v2 by A4,A5,A7,A8,A21,A34,FINSEQ_1:48,RLVECT_2:6;
end;
theorem LMBASE2X:
for K being Ring, V being LeftMod of K, A being finite Subset of V
holds
A is linearly-independent
iff
( for L being Linear_Combination of A
st ( ex F being FinSequence of the carrier of V
st F is one-to-one & rng F = A
& Sum(L (#) F) = 0.V)
holds Carrier(L) = {})
proof
let K be Ring, V be LeftMod of K, A be finite Subset of V;
hereby
assume
BS: A is linearly-independent;
let L be Linear_Combination of A;
given F be FinSequence of the carrier of V such that
BS2: F is one-to-one & rng F = A & Sum(L (#) F) = 0.V;
reconsider B = Carrier L as finite Subset of V;
set F0 = canFS (B);
BS3: rng F0 = B by FUNCT_2:def 3;
rng F0 c= the carrier of V by TARSKI:def 3;
then reconsider F0 as FinSequence of the carrier of V by FINSEQ_1:def 4;
reconsider C = A \ B as finite Subset of V;
set G0 = canFS (C);
BS4: rng G0 = C by FUNCT_2:def 3;
rng G0 c= the carrier of V by TARSKI:def 3;
then reconsider G0 as FinSequence of the carrier of V by FINSEQ_1:def 4;
BS5: rng F0 /\ rng G0 = B /\ ( A \ B) by BS3,FUNCT_2:def 3
.= (B /\ A) \ B by XBOOLE_1:49
.= {} by XBOOLE_1:37,XBOOLE_1:17; then
BS6: F0^G0 is one-to-one by LMBASE2A;
BS7: rng (F0^G0) = B \/ (A \ B) by BS3,BS4,BS5,LMBASE2A
.= A \/ B by XBOOLE_1:39
.= A by VECTSP_6:def 4,XBOOLE_1:12;
(rng G0) /\ Carrier(L) = {} by BS5,FUNCT_2:def 3; then
BS10: L (#) G0 = dom G0 --> 0.V by LMBASE2C; then
aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;
BS12: Sum(L (#) F) = Sum(L (#) (F0^G0)) by EQSUMLF,BS6,BS7,BS2
.= Sum((L (#) F0)^ (L(#)G0)) by VECTSP_6:13
.= Sum(L (#) F0) + Sum(L (#) G0) by RLVECT_1:41
.= Sum(L (#) F0) + 0.V by BS10,LMBASE2D,aa
.= Sum(L (#) F0);
Sum(L) = 0.V by BS2,BS3,BS12,VECTSP_6:def 6;
hence Carrier(L) = {} by VECTSP_7:def 1,BS;
end;
assume AS:
for L being Linear_Combination of A
st ( ex F being FinSequence of the carrier of V
st F is one-to-one & rng F = A & Sum(L (#) F) = 0.V)
holds Carrier(L) = {};
for L being Linear_Combination of A
st Sum(L) = 0.V
holds Carrier(L) = {}
proof
let L be Linear_Combination of A;
assume BS: Sum(L) = 0.V;
consider F0 be FinSequence of the carrier of V such that
P3: F0 is one-to-one & rng F0 = Carrier(L)
& Sum(L) = Sum(L (#) F0) by VECTSP_6:def 6;
reconsider B = Carrier L as finite Subset of V;
reconsider C = A \ B as finite Subset of V;
set G0 = canFS (C);
BS4: rng G0 = C by FUNCT_2:def 3;
rng G0 c= the carrier of V by TARSKI:def 3;
then reconsider G0 as FinSequence of the carrier of V by FINSEQ_1:def 4;
set F = F0^G0;
BS5: rng F0 /\ rng G0 = B /\ ( A \ B) by P3,FUNCT_2:def 3
.= (B /\ A) \ B by XBOOLE_1:49
.= {} by XBOOLE_1:37,XBOOLE_1:17; then
BS6: F is one-to-one by LMBASE2A,P3;
BS7: rng F = B \/ (A \ B) by P3,BS4,BS5,LMBASE2A
.= A \/ B by XBOOLE_1:39
.= A by VECTSP_6:def 4,XBOOLE_1:12;
BS10: L (#) G0 = dom G0 --> 0.V by BS5,P3,LMBASE2C; then
aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;
Sum(L (#) F) = Sum((L (#) F0)^ (L(#)G0)) by VECTSP_6:13
.= Sum(L (#) F0) + Sum(L (#) G0) by RLVECT_1:41
.= Sum(L (#) F0) + 0.V by BS10,LMBASE2D,aa
.= Sum(L (#) F0);
hence Carrier(L) = {} by AS,BS,BS6,BS7,P3;
end;
hence thesis by VECTSP_7:def 1;
end;
theorem LMBASE2:
for K being Ring,
V being LeftMod of K,
b being FinSequence of V
st b is one-to-one
holds
( rng b is linearly-independent
iff
for r being FinSequence of K,
rb being FinSequence of V
st len r = len b & len rb = len b
& ( for i be Nat st i in dom rb holds rb.i = r/.i * b/.i)
& Sum (rb) = 0.V
holds r = Seg (len r) --> 0.K)
proof
let K be Ring,
V be LeftMod of K,
b be FinSequence of V;
assume AS: b is one-to-one;
hereby
assume AS1:
rng b is linearly-independent;
let r be FinSequence of K,
rb be FinSequence of V;
assume that
A1: len r = len b & len rb = len b and
A2: for i being Nat st i in dom rb holds rb.i = r/.i * b/.i and
A3: Sum (rb) = 0.V;
DRB: dom r = dom b by A1,FINSEQ_3:29;
defpred P[object, object] means
($1 in rng b & $2 = (r*(b")).$1) or (not $1 in rng b & $2 = 0.K);
XA2: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & P[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x as Vector of V;
per cases;
suppose
XA3: x in rng b;
then
XA31: x in dom (b") by FUNCT_1:33,AS;
(b").x in rng (b") by FUNCT_1:3,XA31;
then (b").x in dom r by AS,DRB,FUNCT_1:33;
then r.((b").x) in rng r by FUNCT_1:3;
then reconsider y = (r*(b")).x as Element of K
by XA31,FUNCT_1:13;
P[x, y] by XA3;
hence thesis;
end;
suppose
not x in rng b;
hence thesis;
end;
end;
consider L be Function of the carrier of V, the carrier of K
such that
XA5: for x being object st x in the carrier of V holds P[x, L.x]
from FUNCT_2:sch 1(XA2);
XA6: for v being Vector of V st not v in rng b holds L.v = 0.K by XA5;
L is Element of Funcs(the carrier of V, the carrier of K) by FUNCT_2:8;
then reconsider L as Linear_Combination of V by XA6,VECTSP_6:def 1;
now
let x be object;
assume that
XA7: x in Carrier(L) and
XA8: not x in rng b;
consider v be Vector of V such that
XA9: x = v and
XA10: L.v <> 0.K by XA7;
thus contradiction by XA5,XA8,XA9,XA10;
end;
then
Carrier(L) c= rng b;
then reconsider L as Linear_Combination of rng b by VECTSP_6:def 4;
XA41: dom L = the carrier of V by FUNCT_2:def 1;
rng (b") = dom r by AS,DRB,FUNCT_1:33; then
XA43: dom (r*(b")) = dom (b") by RELAT_1:27
.= rng b by FUNCT_1:33,AS;
for i being object st i in dom (L | rng b)
holds (L | rng b).i = (r*(b")).i
proof
let i be object;
assume ASXA: i in dom (L | rng b); then
XA45: i in rng b;
(L | rng b).i = L.i by ASXA,FUNCT_1:49;
hence thesis by XA5,XA45;
end; then
A4: L | rng b = r*(b") by XA41,XA43,RELAT_1:62;
ZA2: dom rb = Seg len b by A1,FINSEQ_1:def 3;
ZA3: dom (L(#)b) = Seg len (L(#)b) by FINSEQ_1:def 3
.= Seg len b by VECTSP_6:def 5;
for i being Nat st i in dom (L(#)b) holds (L(#)b).i = rb.i
proof
let i be Nat;
assume ZA40: i in dom (L(#)b); then
ZA41: (L(#)b).i = (L.(b/.i)) * (b/.i) by VECTSP_6:def 5;
ZA42: i in dom b by FINSEQ_1:def 3,ZA40,ZA3; then
ZA45: b.i in rng b by FUNCT_1:3;
then ZA49: b.i in dom (b") by AS,FUNCT_1:33;
L.(b.i) = (r*(b")).(b.i) by XA5,ZA45
.= r.((b").(b.i)) by ZA49,FUNCT_1:13
.= r.i by AS,FUNCT_1:34,ZA42
.= r/.i by PARTFUN1:def 6,ZA42,DRB;
then L.(b/.i) = r/.i by ZA42,PARTFUN1:def 6;
hence thesis by A2,ZA2,ZA3,ZA40,ZA41;
end; then
ZA1: rb = L(#)b by ZA2,ZA3;
reconsider B = Carrier L as finite Subset of V;
set F0 = canFS (B);
BS3: rng F0 = B by FUNCT_2:def 3;
rng F0 c= the carrier of V by TARSKI:def 3;
then reconsider F0 as FinSequence of V by FINSEQ_1:def 4;
reconsider C = (rng b) \ B as finite Subset of V;
set G0 = canFS (C);
BS4: rng G0 = C by FUNCT_2:def 3;
rng G0 c= the carrier of V by TARSKI:def 3;
then reconsider G0 as FinSequence of V by FINSEQ_1:def 4;
BS5: rng F0 /\ rng G0 = B /\ ((rng b) \ B) by BS3,FUNCT_2:def 3
.= (B /\ (rng b)) \ B by XBOOLE_1:49
.= {} by XBOOLE_1:37,XBOOLE_1:17; then
BS6: F0^G0 is one-to-one by LMBASE2A;
BS7: rng (F0^G0) = B \/ ((rng b) \ B) by BS3,BS4,BS5,LMBASE2A
.= (rng b) \/ B by XBOOLE_1:39
.= (rng b) by VECTSP_6:def 4,XBOOLE_1:12;
BS10: L (#) G0 = dom G0 --> 0.V by BS3,BS5,LMBASE2C; then
aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;
A51: Sum(L (#) b) = Sum(L (#) (F0^G0)) by EQSUMLF,BS6,BS7,AS
.= Sum((L (#) F0)^ (L(#)G0)) by VECTSP_6:13
.= Sum(L (#) F0) + Sum(L (#) G0) by RLVECT_1:41
.= Sum(L (#) F0) + 0.V by BS10,LMBASE2D,aa
.= Sum(L) by BS3,VECTSP_6:def 6;
A6: Carrier(L) = {} by AS1,A3,A51,ZA1,VECTSP_7:def 1;
set N = {i where i is Nat : i in dom r & r.i <> 0.K };
for z being object st z in b.:N holds z in Carrier(L)
proof
let z be object;
assume z in b.:N;
then consider x be object such that
D70: x in dom b & x in N & z = b.x by FUNCT_1:def 6;
reconsider x as Nat by D70;
consider i be Nat such that
A80: x = i & i in dom r & r.i <> 0.K by D70;
A81: b.i in rng b by A80,DRB,FUNCT_1:3; then
A86: b.i in dom (b") by AS,FUNCT_1:33;
A83: L.(b.i) = (L | rng b).(b.i) by A80,DRB,FUNCT_1:3,FUNCT_1:49
.= r.(b".(b.i)) by A4,A86,FUNCT_1:13
.= r.i by AS,A80,DRB,FUNCT_1:34;
reconsider bi = b.i as Element of V by A81;
L.bi <> 0.K by A83,A80;
hence z in Carrier(L) by D70,A80;
end;
then A8: b.:N c= Carrier(L);
for z being object st z in N holds z in dom b
proof
let z be object;
assume z in N;
then consider i be Nat such that
A80: z = i & i in dom r & r.i <> 0.K;
thus thesis by A80,A1,FINSEQ_3:29;
end;
then
A9: N c= dom b;
A7: N = {}
proof
per cases;
suppose rng b = {};
then dom b = {} by RELAT_1:42;
then Y2: Seg len r = {} by A1,FINSEQ_1:def 3;
thus N = {}
proof
assume N <> {};
then consider z be object such that
Y3: z in N by XBOOLE_0:def 1;
ex i being Nat st z = i & i in dom r & r.i <> 0.K by Y3;
hence contradiction by Y2,FINSEQ_1:def 3;
end;
end;
suppose Y1: rng b <> {};
b is Function of dom b,rng b by FUNCT_2:1;
then N c= {} by A6,A8,A9,Y1;
hence N = {};
end;
end;
for z being object st z in dom r holds r.z = 0.K
proof
let z be object;
assume X1: z in dom r;
assume X2: r.z <> 0.K;
reconsider i = z as Nat by X1;
i in N by X1,X2;
hence contradiction by A7;
end;
then r = (dom r) --> 0.K by FUNCOP_1:11;
hence r = Seg (len r) --> 0.K by FINSEQ_1:def 3;
end;
assume AS2:
for r being FinSequence of K, rb being FinSequence of V
st len r = len b & len rb = len b &
(for i be Nat st i in dom rb holds rb.i = r/.i * b/.i) &
Sum (rb) = 0.V
holds r = Seg (len r) --> 0.K;
for L being Linear_Combination of rng b
st ( ex F being FinSequence of the carrier of V
st F is one-to-one & rng F = rng b & Sum(L (#) F) = 0.V)
holds Carrier(L) = {}
proof
let L be Linear_Combination of rng b;
given F be FinSequence of the carrier of V such that
A4: F is one-to-one and
A5: rng F = rng b and
A6: Sum(L (#) F) = 0.V;
reconsider rb = L (#) b as FinSequence of V;
rng (L*b) c= the carrier of K;
then reconsider r = L*b as FinSequence of K by FINSEQ_1:def 4;
B24: len rb = len b by VECTSP_6:def 5;
rng b c= the carrier of V &
dom L = the carrier of V by FUNCT_2:def 1; then
X2: dom r = dom b by RELAT_1:27; then
B21: len r = len b by FINSEQ_3:29;
B23: for i being Nat st i in dom rb holds rb.i = r/.i * b/.i
proof
let i be Nat;
assume B231: i in dom rb; then
B233: i in dom b by B24,FINSEQ_3:29;
i in dom r by B231,B24,X2,FINSEQ_3:29;
then r/.i = r.i by PARTFUN1:def 6
.= L.(b.i) by B233,FUNCT_1:13
.= L.(b/.i) by B233,PARTFUN1:def 6;
hence thesis by B231,VECTSP_6:def 5;
end;
Sum (rb) = Sum(L (#) F) by AS,A4,A5,EQSUMLF; then
A5: r = Seg (len r) --> 0.K by A6,AS2,B21,B23,B24;
A6: Carrier(L) c= rng b by VECTSP_6:def 4;
assume Carrier(L) <> {};
then consider x be object such that
A7: x in Carrier(L) by XBOOLE_0:def 1;
consider v be Element of V such that
A8: x = v & L.v <> 0.K by A7;
consider i be object such that
A9: i in dom b & v = b.i by A6,A7,A8,FUNCT_1:def 3;
A10: r.i <> 0.K by A8,A9,FUNCT_1:13;
i in Seg len r by A9,X2,FINSEQ_1:def 3;
hence contradiction by A5,A10,FUNCOP_1:7;
end;
hence rng b is linearly-independent by LMBASE2X;
end;
theorem
for K being Ring, V being LeftMod of K, A being finite Subset of V
holds
A is linearly-independent
iff
ex b being FinSequence of V
st b is one-to-one & rng b = A &
for r being FinSequence of K,
rb being FinSequence of V
st len r = len b & len rb = len b &
( for i being Nat st i in dom rb holds rb.i = r/.i * b/.i) &
Sum (rb) = 0.V
holds r = Seg (len r) --> 0.K
proof
let K be Ring,
V be LeftMod of K,
A be finite Subset of V;
hereby
assume AS: A is linearly-independent;
rng canFS (A) = A by FUNCT_2:def 3;
then reconsider b = canFS (A) as FinSequence of the carrier of V
by FINSEQ_1:def 4;
take b;
thus b is one-to-one;
thus rng b = A by FUNCT_2:def 3;
hence for r being FinSequence of K,
rb being FinSequence of V
st len r = len b & len rb = len b &
( for i being Nat st i in dom rb
holds rb.i = r/.i * b/.i) & Sum (rb) = 0.V
holds r = Seg (len r) --> 0.K by LMBASE2,AS;
end;
given b being FinSequence of V such that
A1: b is one-to-one & rng b = A &
for r being FinSequence of K, rb being FinSequence of V
st len r = len b & len rb = len b &
( for i being Nat st i in dom rb holds rb.i = r/.i * b/.i) &
Sum (rb) = 0.V holds r = Seg (len r) --> 0.K;
thus thesis by A1,LMBASE2;
end;
registration
let V be non trivial free Z_Module;
cluster -> non empty for Basis of V;
correctness
proof
let I be Basis of V;
assume I is empty;
then I = {}(the carrier of V);
then Lin(I) = (0).V by ZMODUL02:67;
then (Omega).V = (0).V by VECTSP_7:def 3;
hence contradiction;
end;
end;
definition
let IT be Z_Lattice;
attr IT is RATional means
:defRational:
for v, u being Vector of IT holds <; v, u ;> in RAT;
end;
registration
cluster non trivial RATional positive-definite for Z_Lattice;
correctness
proof
set L = the non trivial INTegral positive-definite Z_Lattice;
take L;
thus thesis by RAT_1:def 2;
end;
end;
registration
let L be RATional Z_Lattice;
let v, u be Vector of L;
cluster <; v, u ;> -> rational;
correctness by defRational,RAT_1:def 2;
end;
registration
cluster -> RATional for INTegral Z_Lattice;
correctness by RAT_1:def 2;
end;
LMINTFREAL1:
for x be Element of INT, y be Element of F_Real
st x <> 0 & x = y holds x" = y"
proof
let x be Element of INT, y be Element of F_Real;
assume B1: x<>0 & x = y;
reconsider xi = x" as Element of F_Real by XREAL_0:def 1;
X2: xi*y = 1.F_Real by B1,XCMPLX_0:def 7;
y <> 0.F_Real by B1;
hence x" = y" by X2,VECTSP_1:def 10;
end;
definition
let L be Z_Lattice;
func ScProductEM(L) -> Function of
[:the carrier of EMbedding(L), the carrier of EMbedding(L):],
the carrier of F_Real means
:defScProductEM:
for v, u being Vector of L, vv, uu being Vector of EMbedding(L)
st vv = (MorphsZQ(L)).v & uu = (MorphsZQ(L)).u holds
it.(vv, uu) = <; v, u ;>;
existence
proof
set Z = EMbedding(L);
defpred P[object, object] means
ex vv, uu being Vector of Z, v, u being Vector of L
st $1 = [vv, uu] & vv = (MorphsZQ(L)).v & uu = (MorphsZQ(L)).u
& $2 = <; v, u ;>;
A1: for x being Element of [:the carrier of Z, the carrier of Z:]
ex y being Element of the carrier of F_Real st P[x, y]
proof
let x be Element of [:the carrier of Z, the carrier of Z:];
consider vv, uu be object such that
B1: vv in the carrier of Z & uu in the carrier of Z & x = [vv, uu]
by ZFMISC_1:def 2;
reconsider vv, uu as Vector of Z by B1;
consider v be Vector of L such that
B2: vv = (MorphsZQ(L)).v by ZMODUL08:22;
consider u be Vector of L such that
B3: uu = (MorphsZQ(L)).u by ZMODUL08:22;
take <; v, u ;>;
thus thesis by B1,B2,B3;
end;
consider f be Function of [:the carrier of Z, the carrier of Z:],
the carrier of F_Real such that
A2: for x being Element of [:the carrier of Z, the carrier of Z:]
holds P[x, f.x] from FUNCT_2:sch 3(A1);
take f;
for v, u being Vector of L, vv, uu being Vector of Z
st vv = (MorphsZQ(L)).v & uu = (MorphsZQ(L)).u holds
f.(vv, uu) = <; v, u ;>
proof
let v, u be Vector of L, vv, uu be Vector of Z such that
B1: vv = (MorphsZQ(L)).v & uu = (MorphsZQ(L)).u;
consider vv1, uu1 be Vector of Z, v1, u1 be Vector of L such that
B2: [vv1, uu1] = [vv, uu] & vv1 = (MorphsZQ(L)).v1 &
uu1 = (MorphsZQ(L)).u1 & f.(vv, uu) = <; v1, u1 ;> by A2;
B3: MorphsZQ(L) is one-to-one by ZMODUL04:def 6;
vv = (MorphsZQ(L)).v1 by B2,XTUPLE_0:1;
then B4: v1 = v by B1,B3,FUNCT_2:19;
uu = (MorphsZQ(L)).u1 by B2,XTUPLE_0:1;
hence thesis by B1,B2,B3,B4,FUNCT_2:19;
end;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of
[:the carrier of EMbedding(L), the carrier of EMbedding(L):],
the carrier of F_Real;
assume AS1:
for v, u being Vector of L, vv, uu being Vector of EMbedding(L)
st vv = (MorphsZQ(L)).v & uu = (MorphsZQ(L)).u holds
f1.(vv, uu) = <; v, u ;>;
assume AS2:
for v, u being Vector of L, vv, uu being Vector of EMbedding(L)
st vv = (MorphsZQ(L)).v & uu = (MorphsZQ(L)).u holds
f2.(vv, uu) = <; v, u ;>;
for x being Element of
[:the carrier of EMbedding(L), the carrier of EMbedding(L):] holds
f1.x = f2.x
proof
let x be Element of
[:the carrier of EMbedding(L), the carrier of EMbedding(L):];
consider vv, uu be object such that
B0: vv in the carrier of EMbedding(L) & uu in the carrier of EMbedding(L)
& x = [vv, uu] by ZFMISC_1:def 2;
reconsider vv, uu as Vector of EMbedding(L) by B0;
consider v be Vector of L such that
B2: (MorphsZQ(L)).v = vv by ZMODUL08:22;
consider u be Vector of L such that
B3: (MorphsZQ(L)).u = uu by ZMODUL08:22;
thus f1.x = f1.(vv, uu) by B0
.= <; v, u ;> by AS1,B2,B3
.= f2.(vv, uu) by AS2,B2,B3
.= f2.x by B0;
end;
hence f1 = f2;
end;
end;
theorem ThSPEM1:
for L being Z_Lattice holds
(for x being Vector of EMbedding(L)
st for y being Vector of EMbedding(L) holds (ScProductEM(L)).(x, y) = 0
holds x = 0.(EMbedding(L))) &
(for x, y being Vector of EMbedding(L)
holds (ScProductEM(L)).(x, y) = (ScProductEM(L)).(y, x)) &
(for x, y, z being Vector of EMbedding(L), a being Element of INT.Ring
holds (ScProductEM(L)).(x+y, z) =
(ScProductEM(L)).(x, z) + (ScProductEM(L)).(y, z)
& (ScProductEM(L)).(a*x, y) = a * (ScProductEM(L)).(x, y))
proof
let L be Z_Lattice;
set Z = EMbedding(L);
set f = ScProductEM(L);
set T = MorphsZQ(L);
thus for x being Vector of Z
st for y being Vector of Z holds f.(x, y) = 0
holds x = 0.(EMbedding(L))
proof
let x be Vector of Z such that
B1: for y being Vector of Z holds f.(x, y) = 0;
consider xx be Vector of L such that
B2: T.xx = x by ZMODUL08:22;
for yy being Vector of L holds <; xx, yy ;> = 0
proof
let yy be Vector of L;
T.yy in rng T by FUNCT_2:4;
then reconsider y = T.yy as Vector of Z by ZMODUL08:def 3;
f.(x, y) = 0 by B1;
hence thesis by B2,defScProductEM;
end;
hence x = T.(0.L) by B2,ZMODLAT1:def 3
.= Class(EQRZM(L), [0.L, 1]) by ZMODUL04:def 6
.= zeroCoset(L) by ZMODUL04:def 3
.= 0.(EMbedding(L)) by ZMODUL08:def 3;
end;
thus for x, y being Vector of Z holds f.(x, y) = f.(y, x)
proof
let x, y be Vector of Z;
consider xx be Vector of L such that
B1: T.xx = x by ZMODUL08:22;
consider yy be Vector of L such that
B2: T.yy = y by ZMODUL08:22;
thus f.(x, y) = <; xx, yy ;> by B1,B2,defScProductEM
.= <; yy, xx ;> by ZMODLAT1:def 3
.= f.(y, x) by B1,B2,defScProductEM;
end;
thus for x, y, z being Vector of Z, a being Element of INT.Ring holds
f.(x+y, z) = f.(x, z) + f.(y, z) &
f.(a*x,y) = a * f.(x, y)
proof
let x, y, z be Vector of Z, a be Element of INT.Ring;
consider xx be Vector of L such that
B1: T.xx = x by ZMODUL08:22;
consider yy be Vector of L such that
B2: T.yy = y by ZMODUL08:22;
consider zz be Vector of L such that
B3: T.zz = z by ZMODUL08:22;
B4: T.(xx + yy) = T.xx + T.yy by ZMODUL04:def 6
.= x + y by B1,B2,ZMODUL08:19;
reconsider aq = a as Element of F_Rat by NUMBERS:14;
B5: T.(a*xx) = aq * T.xx by ZMODUL04:def 6
.= a * x by B1,ZMODUL08:19;
thus f.(x+y, z) = <; xx+yy, zz ;> by B3,B4,defScProductEM
.= <; xx, zz ;> + <; yy, zz ;> by ZMODLAT1:def 3
.= f.(x, z) + <; yy, zz ;> by B1,B3,defScProductEM
.= f.(x, z) + f.(y, z) by B2,B3,defScProductEM;
thus f.(a*x, y) = <; a*xx, yy ;> by B2,B5,defScProductEM
.= a * <; xx, yy ;> by ZMODLAT1:def 3
.= a * f.(x, y) by B1,B2,defScProductEM;
end;
end;
definition
let L be Z_Lattice;
func ScProductDM(L) -> Function of
[:the carrier of DivisibleMod(L), the carrier of DivisibleMod(L):],
the carrier of F_Real means
:defScProductDM:
for vv, uu being Vector of DivisibleMod(L),
v, u being Vector of EMbedding(L), a, b being Element of INT.Ring,
ai, bi being Element of F_Real
st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu
holds it.(vv, uu) = ai" * bi" * (ScProductEM(L)).(v, u);
existence
proof
set Z = EMbedding(L);
set D = DivisibleMod(L);
defpred P[object, object] means
ex vv, uu being Vector of D, v, u being Vector of Z,
a, b being Element of INT.Ring,
ai, bi being Element of INT
st $1 = [vv, uu] & a=ai & b=bi & ai <> 0 & bi <> 0
& v = a * vv & u = b * uu & $2 = ai" * bi" * (ScProductEM(L)).(v, u);
A1: for x being Element of
[:the carrier of D, the carrier of D:]
ex y being Element of F_Real st P[x, y]
proof
let x be Element of [:the carrier of D, the carrier of D:];
consider vv, uu be object such that
B1: vv in the carrier of D & uu in the carrier of D & x = [vv, uu]
by ZFMISC_1:def 2;
reconsider vv,uu as Vector of D by B1;
consider a be Element of INT.Ring such that
B2: a <> 0.INT.Ring & a * vv in EMbedding(L) by ZMODUL08:29;
reconsider v = a * vv as Vector of EMbedding(L) by B2;
consider b be Element of INT.Ring such that
B3: b <> 0.INT.Ring & b * uu in EMbedding(L) by ZMODUL08:29;
reconsider u = b * uu as Vector of EMbedding(L) by B3;
reconsider ai=a, bi=b as Element of INT;
take ai" * bi" * (ScProductEM(L)).(v, u);
thus thesis by B1,B2,B3,XREAL_0:def 1;
end;
consider f be Function of [:the carrier of D, the carrier of D:], F_Real
such that
A2: for x being Element of [:the carrier of D, the carrier of D:]
holds P[x, f.x] from FUNCT_2:sch 3(A1);
take f;
for vv, uu being Vector of D,
v, u being Vector of Z, a, b being Element of INT.Ring,
ai, bi being Element of F_Real
st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu
holds f.(vv, uu) = ai" * bi" * (ScProductEM(L)).(v, u)
proof
let vv, uu be Vector of D, v, u be Vector of Z,
a, b be Element of INT.Ring,
ai0, bi0 be Element of F_Real such that
B1: a = ai0 & b = bi0 & ai0 <> 0 & bi0 <> 0 & v = a * vv & u = b * uu;
reconsider ai=ai0,bi=bi0 as Element of INT by B1;
consider vv1, uu1 be Vector of D, v1, u1 be Vector of Z,
a1, b1 be Element of INT.Ring,
a1i,b1i be Element of INT such that
B2: [vv1, uu1] = [vv, uu]
& a1 = a1i & b1 = b1i & a1i <> 0 & b1i <> 0
& v1 = a1 * vv1 & u1 = b1 * uu1 &
f.(vv, uu) = a1i" * b1i" * (ScProductEM(L)).(v1, u1) by A2;
B3: v1 = a1 * vv by B2,XTUPLE_0:1;
B4: u1 = b1 * uu by B2,XTUPLE_0:1;
reconsider a1ga = a1i gcd ai, b1gb = b1i gcd bi
as Element of INT.Ring by INT_1:def 2;
BX: Z is Submodule of D by ZMODUL08:24;
B5: a1ga * vv in Z
proof
consider c10, c20 be Integer such that
C10: (a1i gcd ai) = c10 * a1i + c20 * ai by NAT_D:68;
reconsider c1=c10,c2=c20 as Element of INT.Ring by INT_1:def 2;
C2: (c1 * a1) * vv = c1 * (a1 * vv) by VECTSP_1:def 16
.= c1 * v1 by B3,BX,ZMODUL01:29;
C3: (c2 * a) * vv = c2 * (a * vv) by VECTSP_1:def 16
.= c2 * v by B1,BX,ZMODUL01:29;
a1ga * vv = (c1 * a1 + c2 * a) * vv by B1,B2,C10
.= (c1 * a1) * vv + (c2 * a) * vv by VECTSP_1:def 15
.= c1 * v1 + c2 * v by C2,C3,BX,ZMODUL01:28;
hence a1ga * vv in Z;
end;
consider c10, c20 be Integer such that
C10: (b1i gcd bi) = c10 * b1i + c20 * bi by NAT_D:68;
reconsider c1=c10,c2=c20 as Element of INT.Ring by INT_1:def 2;
C2: (c1 * b1) * uu = c1 * (b1 * uu) by VECTSP_1:def 16
.= c1 * u1 by B4,BX,ZMODUL01:29;
C3: (c2 * b) * uu = c2 * (b * uu) by VECTSP_1:def 16
.= c2 * u by B1,BX,ZMODUL01:29;
reconsider agv = a1ga * vv as Vector of Z by B5;
b1gb * uu = (c1 * b1 + c2 * b) * uu by B1,B2,C10
.= (c1 * b1) * uu + (c2 * b) * uu by VECTSP_1:def 15
.= c1 * u1 + c2 * u by C2,C3,BX,ZMODUL01:28; then
reconsider bgu = b1gb * uu as Vector of Z;
consider ci be Integer such that
B7: ai = (a1i gcd ai) * ci by INT_1:def 3,INT_2:21;
consider c1i be Integer such that
B8: a1i = (a1i gcd ai) * c1i by INT_1:def 3,INT_2:21;
consider di be Integer such that
B9: bi = (b1i gcd bi) * di by INT_1:def 3,INT_2:21;
reconsider c = ci, d = di as Element of INT.Ring by INT_1:def 2;
consider d1i be Integer such that
B10: b1i = (b1i gcd bi) * d1i by INT_1:def 3,INT_2:21;
reconsider c = ci,c1 = c1i,
d = di,d1=d1i as Element of INT.Ring by INT_1:def 2;
B11: v = (c * a1ga) * vv by B1,B7
.= c * (a1ga * vv) by VECTSP_1:def 16
.= c * agv by BX,ZMODUL01:29;
B12: v1 = (c1 * a1ga) * vv by B2,B8,XTUPLE_0:1
.= c1 * (a1ga * vv) by VECTSP_1:def 16
.= c1 * agv by BX,ZMODUL01:29;
B13: u = (d * b1gb) * uu by B1,B9
.= d * (b1gb * uu) by VECTSP_1:def 16
.= d * bgu by BX,ZMODUL01:29;
B14: u1 = (d1 * b1gb) * uu by B2,B10,XTUPLE_0:1
.= d1 * (b1gb * uu) by VECTSP_1:def 16
.= d1 * bgu by BX,ZMODUL01:29;
B15: ci <> 0 by B1,B7;
B16: c1i <> 0 by B2,B8;
B17: di <> 0 by B1,B9;
B18: d1i <> 0 by B2,B10;
B19: f.(vv, uu) = a1i" * b1i" * (c1i * (ScProductEM(L)).(agv, d1 * bgu))
by B2,B12,B14,ThSPEM1
.= a1i" * b1i" * (c1i * (ScProductEM(L)).(d1 * bgu, agv)) by ThSPEM1
.= a1i" * b1i" * (c1i * (d1i * (ScProductEM(L)).(bgu, agv))) by ThSPEM1
.= a1i" * b1i" * (c1i * (d1i * (ScProductEM(L)).(agv, bgu))) by ThSPEM1
.= a1i" * b1i" * c1i * d1i * (ScProductEM(L)).(agv, bgu)
.= (a1i gcd ai)" * c1i" * ((b1i gcd bi) * d1i)" * c1i * d1i *
(ScProductEM(L)).(agv, bgu) by B8,B10,XCMPLX_1:204
.= (a1i gcd ai)" * c1i * c1i" * ((b1i gcd bi) * d1i)" * d1i *
(ScProductEM(L)).(agv, bgu)
.= (a1i gcd ai)" * ((b1i gcd bi) * d1i)" * d1i *
(ScProductEM(L)).(agv, bgu) by B16,XCMPLX_1:203
.= ((b1i gcd bi) * d1i)" * d1i * (a1i gcd ai)" *
(ScProductEM(L)).(agv, bgu)
.= (b1i gcd bi)" * d1i" * d1i * (a1i gcd ai)" *
(ScProductEM(L)).(agv, bgu) by XCMPLX_1:204
.= (b1i gcd bi)" * d1i * d1i" * (a1i gcd ai)" *
(ScProductEM(L)).(agv, bgu)
.= (b1i gcd bi)" * (a1i gcd ai)" *
(ScProductEM(L)).(agv, bgu) by B18,XCMPLX_1:203;
X1: ai" * bi" * (ScProductEM(L)).(v, u)
= ai" * bi" * (ci * (ScProductEM(L)).(agv, d * bgu)) by B11,B13,ThSPEM1
.= ai" * bi" * (ci * (ScProductEM(L)).(d * bgu, agv)) by ThSPEM1
.= ai" * bi" * (ci * (di * (ScProductEM(L)).(bgu, agv))) by ThSPEM1
.= ai" * bi" * (ci * (di * (ScProductEM(L)).(agv, bgu))) by ThSPEM1
.= ((a1i gcd ai) * ci)" * ((b1i gcd bi) * di)" * ci * di *
(ScProductEM(L)).(agv, bgu) by B7,B9
.= (a1i gcd ai)" * ci" * ((b1i gcd bi) * di)" * ci * di *
(ScProductEM(L)).(agv, bgu) by XCMPLX_1:204
.= (a1i gcd ai)" * ci * ci" * ((b1i gcd bi) * di)" * di *
(ScProductEM(L)).(agv, bgu)
.= (a1i gcd ai)" * ((b1i gcd bi) * di)" * di *
(ScProductEM(L)).(agv, bgu) by B15,XCMPLX_1:203
.= ((b1i gcd bi) * di)" * di * (a1i gcd ai)" *
(ScProductEM(L)).(agv, bgu)
.= (b1i gcd bi)" * di" * di * (a1i gcd ai)" *
(ScProductEM(L)).(agv, bgu) by XCMPLX_1:204
.= (b1i gcd bi)" * di * di" * (a1i gcd ai)" *
(ScProductEM(L)).(agv, bgu)
.= (b1i gcd bi)" * (a1i gcd ai)" *
(ScProductEM(L)).(agv, bgu) by B17,XCMPLX_1:203;
ai" = ai0" & bi" = bi0" by LMINTFREAL1,B1;
hence f.(vv, uu) = ai0" * bi0" * (ScProductEM(L)).(v, u) by X1,B19;
end;
hence thesis;
end;
uniqueness
proof
set Z = EMbedding(L);
set D = DivisibleMod(L);
let f1, f2 be Function of [:the carrier of D, the carrier of D:], F_Real;
assume AS1:
for vv, uu being Vector of D, v, u being Vector of Z,
a, b being Element of INT.Ring,
ai, bi being Element of F_Real
st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu
holds f1.(vv, uu) = ai" * bi" * (ScProductEM(L)).(v, u);
assume AS2:
for vv, uu being Vector of D, v, u being Vector of Z,
a, b being Element of INT.Ring,
ai, bi being Element of F_Real
st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu
holds f2.(vv, uu) = ai" * bi" * (ScProductEM(L)).(v, u);
for x being Element of [:the carrier of D, the carrier of D:] holds
f1.x = f2.x
proof
let x be Element of [:the carrier of D, the carrier of D:];
consider vv, uu be object such that
B0: vv in the carrier of D & uu in the carrier of D & x = [vv, uu]
by ZFMISC_1:def 2;
reconsider vv, uu as Vector of D by B0;
consider a be Element of INT.Ring such that
B1: a <> 0 & a * vv in Z by ZMODUL08:29;
consider b be Element of INT.Ring such that
B2: b <> 0 & b * uu in Z by ZMODUL08:29;
reconsider v = a * vv as Vector of Z by B1;
reconsider u = b * uu as Vector of Z by B2;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider ai = a,bi = b as Element of F_Real;
thus f1.x = f1.(vv, uu) by B0
.= ai" * bi" * (ScProductEM(L)).(v, u) by AS1,B1,B2
.= f2.(vv, uu) by AS2,B1,B2
.= f2.x by B0;
end;
hence f1 = f2;
end;
end;
theorem ThSPDM1:
for L being Z_Lattice holds
(for x being Vector of DivisibleMod(L)
st for y being Vector of DivisibleMod(L) holds (ScProductDM(L)).(x, y) = 0
holds x = 0.(DivisibleMod(L))) &
(for x, y being Vector of DivisibleMod(L)
holds (ScProductDM(L)).(x, y) = (ScProductDM(L)).(y, x)) &
(for x, y, z being Vector of DivisibleMod(L), a being Element of INT.Ring
holds (ScProductDM(L)).(x+y, z) =
(ScProductDM(L)).(x, z) + (ScProductDM(L)).(y, z)
& (ScProductDM(L)).(a*x, y) = a * (ScProductDM(L)).(x, y))
proof
let L be Z_Lattice;
set D = DivisibleMod(L);
set Z = EMbedding(L);
set f = ScProductDM(L);
A1: Z is Submodule of D by ZMODUL08:24;
thus for x being Vector of D
st for y being Vector of D holds f.(x, y) = 0
holds x = 0.D
proof
let x be Vector of D such that
B1: for y being Vector of D holds f.(x, y) = 0;
consider a be Element of INT.Ring such that
B2: a <> 0.INT.Ring & a * x in Z by ZMODUL08:29;
reconsider xx = a * x as Vector of Z by B2;
for yy being Vector of Z holds (ScProductEM(L)).(xx, yy) = 0
proof
let yy be Vector of Z;
set b = 1.INT.Ring;
yy in Z;
then yy in D by A1,ZMODUL01:24;
then reconsider y = b * yy as Vector of D;
C1: b <> 0 & yy = b * y;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af=a,bf=b as Element of F_Real;
C2: f.(x, y) = af" * bf" * (ScProductEM(L)).(xx, yy)
by B2,C1,defScProductDM;
thus (ScProductEM(L)).(xx, yy) = 0
proof
assume (ScProductEM(L)).(xx, yy) <> 0;
then XX1: af" = 0 or bf" = 0 by B1,C2;
af <> 0.F_Real & bf <> 0.F_Real by B2;
hence contradiction by XX1,VECTSP_1:25;
end;
end;
then xx = 0.Z by ThSPEM1
.= 0.D by A1,ZMODUL01:26;
hence x = 0.D by B2,ZMODUL01:def 7;
end;
thus for x, y being Vector of D holds f.(x, y) = f.(y, x)
proof
let x, y be Vector of D;
consider a be Element of INT.Ring such that
B1: a <> 0 & a * x in Z by ZMODUL08:29;
reconsider xx = a * x as Vector of Z by B1;
consider b be Element of INT.Ring such that
B2: b <> 0 & b * y in Z by ZMODUL08:29;
reconsider yy = b * y as Vector of Z by B2;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af=a,bf=b as Element of F_Real;
thus f.(x, y) = af" * bf" * (ScProductEM(L)).(xx, yy)
by B1,B2,defScProductDM
.= bf" * af" * (ScProductEM(L)).(yy, xx) by ThSPEM1
.= f.(y, x) by B1,B2,defScProductDM;
end;
thus for x, y, z being Vector of D, i being Element of INT.Ring
holds f.(x+y, z) = f.(x, z) + f.(y, z) & f.(i*x, y) = i * f.(x, y)
proof
let x, y, z be Vector of D, i be Element of INT.Ring;
consider a be Element of INT.Ring such that
B1: a <> 0 & a * x in Z by ZMODUL08:29;
reconsider xx = a * x as Vector of Z by B1;
consider b be Element of INT.Ring such that
B2: b <> 0 & b * y in Z by ZMODUL08:29;
reconsider yy = b * y as Vector of Z by B2;
consider c be Element of INT.Ring such that
B3: c <> 0 & c * z in Z by ZMODUL08:29;
reconsider zz = c * z as Vector of Z by B3;
B41: b * (a*x) = b * xx by A1,ZMODUL01:29;
B42: a * (b*y) = a * yy by A1,ZMODUL01:29;
B4: (a*b) * (x + y) = (a*b) * x + (a*b) * y by VECTSP_1:def 14
.= (b*a) * x + a * (b*y) by VECTSP_1:def 16
.= b * (a*x) + a * (b*y) by VECTSP_1:def 16
.= b * xx + a * yy by A1,B41,B42,ZMODUL01:28;
then reconsider xy = (a*b) * (x + y) as Vector of Z;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider af=a,bf=b,cf = c as Element of F_Real;
X2:af <> 0.F_Real & bf <> 0.F_Real by B1,B2; then
X1: (af*bf)" * cf" = af" * bf" * cf" by VECTSP_2:11;
thus f.(x+y, z) = af" * bf" * cf" * (ScProductEM(L)).(xy, zz)
by B1,B2,B3,X1,defScProductDM
.= (af" * bf" * cf") *
((ScProductEM(L)).(b * xx, zz) + (ScProductEM(L)).(a * yy, zz))
by B4,ThSPEM1
.= (af" * bf" * cf") * ((ScProductEM(L)).(b * xx, zz))
+ (af" * bf" * cf") * ((ScProductEM(L)).(a * yy, zz))
.= (af" * bf" * cf") * (b * (ScProductEM(L)).(xx, zz))
+ (af" * bf" * cf") * ((ScProductEM(L)).(a * yy, zz)) by ThSPEM1
.= (af" * (bf" * bf) * cf") * (ScProductEM(L)).(xx, zz)
+ (af" * bf" * cf") * ((ScProductEM(L)).(a * yy, zz))
.= (af" * (1.F_Real) * cf") * (ScProductEM(L)).(xx, zz)
+ (af" * bf" * cf") * ((ScProductEM(L)).(a * yy, zz))
by VECTSP_1:def 10,X2
.= (af" * cf") * (ScProductEM(L)).(xx, zz)
+ (af" * bf" * cf") * (a * (ScProductEM(L)).(yy, zz)) by ThSPEM1
.= af" * cf" * (ScProductEM(L)).(xx, zz)
+ (bf" * (af * af") * cf") * (ScProductEM(L)).(yy, zz)
.= af" * cf" * (ScProductEM(L)).(xx, zz)
+ (bf" * (1.F_Real) * cf") * (ScProductEM(L)).(yy, zz)
by VECTSP_1:def 10,X2
.= f.(x, z) + bf" * cf" * (ScProductEM(L)).(yy, zz)
by B1,B3,defScProductDM
.= f.(x, z) + f.(y, z) by B2,B3,defScProductDM;
a * (i*x) = (a*i) * x by VECTSP_1:def 16
.= i * (a*x) by VECTSP_1:def 16
.= i * xx by A1,ZMODUL01:29;
hence f.(i*x, y) = af" * bf" * (ScProductEM(L)).(i * xx, yy)
by B1,B2,defScProductDM
.= (af" * bf") * (i * (ScProductEM(L)).(xx, yy)) by ThSPEM1
.= i * (af" * bf" * (ScProductEM(L)).(xx, yy))
.= i * f.(x, y) by B1,B2,defScProductDM;
end;
end;
theorem ThSPEM2:
for L being Z_Lattice holds
ScProductEM(L) = (ScProductDM(L)) || (rng MorphsZQ(L))
proof
let L be Z_Lattice;
P1: [:the carrier of EMbedding(L), the carrier of EMbedding(L):]
= [:the carrier of EMbedding(L), rng MorphsZQ(L):] by ZMODUL08:def 3
.= [:rng MorphsZQ(L), rng MorphsZQ(L):] by ZMODUL08:def 3;
P2: [:the carrier of DivisibleMod(L), the carrier of DivisibleMod(L):]
= [:the carrier of DivisibleMod(L), Class EQRZM(L):] by ZMODUL08:def 4
.= [:Class EQRZM(L), Class EQRZM(L):] by ZMODUL08:def 4;
A0: EMbedding(L) is Submodule of DivisibleMod(L) by ZMODUL08:24;
then the carrier of EMbedding(L) c= the carrier of DivisibleMod(L)
by VECTSP_4:def 2;
then rng MorphsZQ(L) c= the carrier of DivisibleMod(L) by ZMODUL08:def 3;
then rng MorphsZQ(L) c= Class EQRZM(L) by ZMODUL08:def 4;
then [:rng MorphsZQ(L), rng MorphsZQ(L):]
c= [:Class EQRZM(L), Class EQRZM(L):] by ZFMISC_1:96;
then reconsider scd = (ScProductDM(L)) || (rng MorphsZQ(L)) as Function of
[:rng MorphsZQ(L), rng MorphsZQ(L):], the carrier of F_Real
by P2,FUNCT_2:32;
for x being object st x in [:rng MorphsZQ(L), rng MorphsZQ(L):]
holds (ScProductEM(L)).x = scd.x
proof
let x be object such that
B1: x in [:rng MorphsZQ(L), rng MorphsZQ(L):];
consider x1, x2 be object such that
B2: x1 in rng MorphsZQ(L) & x2 in rng MorphsZQ(L) & x = [x1, x2]
by B1,ZFMISC_1:def 2;
reconsider x1, x2 as Vector of EMbedding(L) by B2,ZMODUL08:def 3;
set a = 1.(INT.Ring);
x1 in EMbedding(L);
then x1 in DivisibleMod(L) by A0,ZMODUL01:24;
then reconsider xx1 = x1 as Vector of DivisibleMod(L);
x2 in EMbedding(L);
then x2 in DivisibleMod(L) by A0,ZMODUL01:24;
then reconsider xx2 = x2 as Vector of DivisibleMod(L);
B3: x1 = a * xx1;
B4: x2 = a * xx2;
thus (ScProductEM(L)).x
= (1.F_Real) * (1.F_Real)" * (ScProductEM(L)).(x1,x2) by B2
.= (ScProductDM(L)).(xx1, xx2) by B3,B4,defScProductDM
.= scd.x by B2,FUNCT_1:49,ZFMISC_1:87;
end;
hence thesis by P1,FUNCT_2:12;
end;
theorem ThSPEM3:
for L being Z_Lattice, v1, v2 being Vector of DivisibleMod(L),
u1, u2 being Vector of EMbedding(L) st v1 = u1 & v2 = u2 holds
(ScProductEM(L)).(u1, u2) = (ScProductDM(L)).(v1, v2)
proof
let L be Z_Lattice, v1, v2 be Vector of DivisibleMod(L),
u1, u2 be Vector of EMbedding(L) such that
A1: v1 = u1 & v2 = u2;
A2: u1 = 1.INT.Ring * v1 & u2 = 1.INT.Ring * v2 by A1;
thus (ScProductDM(L)).(v1, v2)
= (1.F_Real)" * (1.F_Real)" * (ScProductEM(L)).(u1, u2)
by A2,defScProductDM
.= (ScProductEM(L)).(u1, u2);
end;
theorem ThSPrEM1:
for L being Z_Lattice, r being Element of F_Rat,
v, u being Vector of EMbedding(r, L) holds
((ScProductDM(L)) || (the carrier of EMbedding(r, L))).(v, u)
= (ScProductDM(L)).(v, u)
proof
let L be Z_Lattice, r be Element of F_Rat,
v, u be Vector of EMbedding(r, L);
set Z = EMbedding(r, L);
Z is Submodule of DivisibleMod(L) by ZMODUL08:32;
then the carrier of Z
c= the carrier of DivisibleMod(L) by VECTSP_4:def 2;
then [:the carrier of Z, the carrier of Z:]
c= [:the carrier of DivisibleMod(L), the carrier of DivisibleMod(L):]
by ZFMISC_1:96;
then reconsider sc = (ScProductDM(L)) || (the carrier of Z) as Function of
[: the carrier of Z, the carrier of Z:], the carrier of F_Real
by FUNCT_2:32;
[v, u] in [:the carrier of Z, the carrier of Z:];
hence thesis by FUNCT_1:49;
end;
theorem
for L being Z_Lattice, A being non empty set, ze being Element of A,
ad being BinOp of A,
mu being Function of [:the carrier of INT.Ring, A:],A,
sc being Function of [:A, A:],the carrier of F_Real
st A is linearly-closed Subset of DivisibleMod(L) & ze = 0.DivisibleMod(L) &
ad = (the addF of DivisibleMod(L)) || A &
mu = (the lmult of DivisibleMod(L)) | [:the carrier of INT.Ring, A:] holds
LatticeStr (# A, ad, ze,mu, sc #) is Submodule of DivisibleMod(L)
proof
let L be Z_Lattice, A be non empty set, ze be Element of A,
ad be BinOp of A,
mu be Function of [:the carrier of INT.Ring, A:],A,
sc be Function of [:A, A:], the carrier of F_Real such that
A1: A is linearly-closed Subset of DivisibleMod(L) &
ze = 0.DivisibleMod(L) &
ad = (the addF of DivisibleMod(L)) || A &
mu = (the lmult of DivisibleMod(L)) | [:the carrier of INT.Ring, A:];
set L1 = LatticeStr (# A, ad, ze,mu, sc #);
set V1 = ModuleStr (# A, ad, ze,mu #);
A2: V1 is Submodule of DivisibleMod(L) by A1,ZMODUL01:40;
reconsider V1 as Z_Module by A1,ZMODUL01:40;
reconsider scc = sc as Function of [:the carrier of V1,
the carrier of V1 :], the carrier of F_Real;
L1 = GenLat(V1, scc);
then L1 is Submodule of V1 by ZMODLAT1:2;
hence thesis by A2,ZMODUL01:42;
end;
theorem ThScDM1:
for L being Z_Lattice, v, u being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(-v, u) = -(ScProductDM(L)).(v, u) &
(ScProductDM(L)).(u, -v) = -(ScProductDM(L)).(u, v)
proof
let L be Z_Lattice, v, u be Vector of DivisibleMod(L);
thus A1: (ScProductDM(L)).(-v, u) = (ScProductDM(L)).((-1.(INT.Ring))*v, u)
by ZMODUL01:2
.= (-1) * (ScProductDM(L)).(v, u) by ThSPDM1
.= -(ScProductDM(L)).(v, u);
thus (ScProductDM(L)).(u, -v) = (ScProductDM(L)).(-v, u) by ThSPDM1
.= -(ScProductDM(L)).(u, v) by A1,ThSPDM1;
end;
theorem
for L being Z_Lattice, v, u, w being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(v, u + w)
= (ScProductDM(L)).(v, u) + (ScProductDM(L)).(v, w)
proof
let L be Z_Lattice, v, u, w be Vector of DivisibleMod(L);
thus (ScProductDM(L)).(v, u + w)
= (ScProductDM(L)).(u + w, v) by ThSPDM1
.= (ScProductDM(L)).(u, v) + (ScProductDM(L)).(w, v) by ThSPDM1
.= (ScProductDM(L)).(u, v) + (ScProductDM(L)).(v, w) by ThSPDM1
.= (ScProductDM(L)).(v, u) + (ScProductDM(L)).(v, w) by ThSPDM1;
end;
theorem
for L being Z_Lattice, v, u being Vector of DivisibleMod(L),
a being Element of INT.Ring
holds (ScProductDM(L)).(v, a*u) = a * (ScProductDM(L)).(v, u)
proof
let L be Z_Lattice, v, u be Vector of DivisibleMod(L),
a be Element of INT.Ring;
thus (ScProductDM(L)).(v, a*u) = (ScProductDM(L)).(a*u, v) by ThSPDM1
.= a * (ScProductDM(L)).(u, v) by ThSPDM1
.= a * (ScProductDM(L)).(v, u) by ThSPDM1;
end;
theorem ThScDM6:
for L being Z_Lattice, v being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(0.DivisibleMod(L), v) = 0 &
(ScProductDM(L)).(v, 0.DivisibleMod(L)) = 0
proof
let L be Z_Lattice, v be Vector of DivisibleMod(L);
thus A1: (ScProductDM(L)).(0.DivisibleMod(L), v)
= (ScProductDM(L)).(v-v, v) by RLVECT_1:15
.= (ScProductDM(L)).(v, v) + (ScProductDM(L)).(-v, v) by ThSPDM1
.= (ScProductDM(L)).(v, v) - (ScProductDM(L)).(v, v) by ThScDM1
.= 0;
thus (ScProductDM(L)).(v, 0.DivisibleMod(L)) = 0 by A1,ThSPDM1;
end;
theorem LmDE22:
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) = 0 holds
for u being Vector of DivisibleMod(L) holds (ScProductDM(L)).(v, u) = 0
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) = 0;
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) = 0
holds for w being Vector of DivisibleMod(L) st w in Lin(I) holds
(ScProductDM(L)).(v, w) = 0;
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) = 0;
I = {}(the carrier of EMbedding(L)) by B1;
then B2: Lin(I) = (0).EMbedding(L) by ZMODUL02:67;
thus for w being Vector of DivisibleMod(L) st w in Lin(I)
holds (ScProductDM(L)).(v, w) = 0
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;
hence thesis by ThScDM6;
end;
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) = 0;
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) = 0 by B2,B7;
thus for w being Vector of DivisibleMod(L) st w in Lin(I)
holds (ScProductDM(L)).(v, w) = 0
proof
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;
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) = 0 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;
C8: (ScProductDM(L)).(v, i*u) = (ScProductDM(L)).(v, i*uu)
by CX,ZMODUL01:29
.= (ScProductDM(L)).(i*uu, v) by ThSPDM1
.= i* (ScProductDM(L)).(uu, v) by ThSPDM1
.= i* (ScProductDM(L)).(v, u) by ThSPDM1;
C10: w = ww1 + ww2 by C2,CX,ZMODUL01:28;
(ScProductDM(L)).(v, w) = (ScProductDM(L)).(w, v) by ThSPDM1
.= (ScProductDM(L)).(ww1, v) + (ScProductDM(L)).(ww2, v) by C10,ThSPDM1
.= (ScProductDM(L)).(v, w1) + (ScProductDM(L)).(ww2, v) by ThSPDM1
.= (ScProductDM(L)).(v, w1) + (ScProductDM(L)).(v, w2) by ThSPDM1;
hence thesis by B1,B4,B6,B8,C2,C4,C6,C8,C9;
end;
end;
P3: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
P4: card I is Nat;
P5: I is linearly-independent & EMbedding(L) = Lin(I) by VECTSP_7:def 3;
thus for w being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(v, w) = 0
proof
let w be Vector of DivisibleMod(L);
consider a be Element of INT.Ring such that
B1: a <> 0.INT.Ring & a * w in EMbedding(L) by ZMODUL08:29;
(ScProductDM(L)).(v, a*w) = (ScProductDM(L)).(a*w, v) by ThSPDM1
.= a * (ScProductDM(L)).(w, v) by ThSPDM1
.= a * (ScProductDM(L)).(v, w) by ThSPDM1;
hence thesis by A1,B1,P3,P4,P5;
end;
end;
theorem
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) = 0
holds v = 0.DivisibleMod(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) = 0;
for u being Vector of DivisibleMod(L)
holds (ScProductDM(L)).(v, u) = 0 by A1,LmDE22;
hence thesis by ThSPDM1;
end;
theorem
for R being Ring, V being LeftMod of R, v being Vector of V,
u being object st u in Lin{v} holds
ex i being Element of R st u = i*v
proof
let R be Ring, V be LeftMod of R, v be Vector of V,
u be object such that
A1: u in Lin{v};
consider l be Linear_Combination of {v} such that
A2: u = Sum(l) by A1,VECTSP_7:7;
take l.v;
thus thesis by A2,VECTSP_6:17;
end;
theorem ThLin2:
for R being Ring, V being LeftMod of R, v being Vector of V holds
v in Lin{v} by VECTSP_7:8,ZFMISC_1:31;
theorem
for R being Ring, V being LeftMod of R, v being Vector of V,
i being Element of R holds i*v in Lin{v} by ThLin2,VECTSP_4:21;
begin :: 2. Embedding of lattice
definition
let L be Z_Lattice;
func EMLat(L) -> strict Z_Lattice means
:defEMLat:
the carrier of it = rng MorphsZQ(L) &
the ZeroF of it = zeroCoset(L) &
the addF of it = (addCoset(L)) || (rng MorphsZQ(L)) &
the lmult of it = (lmultCoset(L)) | [:the carrier of INT.Ring,
rng MorphsZQ(L):] &
the scalar of it = ScProductEM(L);
existence
proof
set Z = LatticeStr
(# the carrier of EMbedding(L), the addF of EMbedding(L),
0.(EMbedding(L)), the lmult of EMbedding(L), ScProductEM(L) #);
AX: Z = GenLat(EMbedding(L), ScProductEM(L));
then reconsider Z as Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring;
reconsider Z as free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr over INT.Ring by AX;
Z is Z_Lattice-like
proof
thus for x being Vector of Z
st for y being Vector of Z holds <; x, y ;> = 0
holds x = 0.Z
proof
let x be Vector of Z such that
B1: for y being Vector of Z holds <; x, y ;> = 0;
for y being Vector of Z holds (ScProductEM(L)).(x, y) = 0
proof
let y be Vector of Z;
thus (ScProductEM(L)).(x, y) = <; x, y ;>
.= 0 by B1;
end;
hence thesis by ThSPEM1;
end;
thus for x, y being Vector of Z holds <; x, y ;> = <; y, x ;>
proof
let x, y be Vector of Z;
thus <; x, y ;> = (ScProductEM(L)).(x, y)
.= (ScProductEM(L)).(y, x) by ThSPEM1
.= <; y, x ;>;
end;
thus for x, y, z being Vector of Z, a being Element of INT.Ring
holds <; x+y, z ;> = <; x, z ;> + <; y, z ;> &
<; a*x, y ;> = a * <; x, y ;>
proof
let x, y, z be Vector of Z, a be Element of INT.Ring;
reconsider xx = x, yy = y, zz = z as Vector of EMbedding(L);
thus <; x+y, z ;> = (ScProductEM(L)).(xx+yy, zz)
.= (the scalar of Z).(x, z) + (the scalar of Z).(y, z) by ThSPEM1
.= <; x, z ;> + <; y, z ;>;
thus <; a*x, y ;> = (ScProductEM(L)).(a*xx, y)
.= a * (ScProductEM(L)).(xx, y) by ThSPEM1
.= a * <; x, y ;>;
end;
end;
then reconsider Z as strict Z_Lattice by AX;
take Z;
thus thesis by ZMODUL08:def 3;
end;
uniqueness;
end;
definition
let L be Z_Lattice;
let r be Element of F_Rat;
func EMLat(r, L) -> strict Z_Lattice means
:defrEMLat:
the carrier of it = r * (rng MorphsZQ(L)) &
the ZeroF of it = zeroCoset(L) &
the addF of it = (addCoset(L)) || ( r * (rng MorphsZQ(L))) &
the lmult of it = (lmultCoset(L)) |
[:the carrier of INT.Ring, r * (rng MorphsZQ(L)):] &
the scalar of it = (ScProductDM(L)) || (r * (rng MorphsZQ(L)));
existence
proof
EMbedding(r, L) is Submodule of DivisibleMod(L) by ZMODUL08:32;
then the carrier of EMbedding(r, L) c= the carrier of DivisibleMod(L)
by VECTSP_4:def 2;
then [:the carrier of EMbedding(r, L), the carrier of EMbedding(r, L):]
c= [:the carrier of DivisibleMod(L), the carrier of DivisibleMod(L):]
by ZFMISC_1:96;
then reconsider sc = (ScProductDM(L)) || (the carrier of EMbedding(r, L))
as Function of
[: the carrier of EMbedding(r, L), the carrier of EMbedding(r, L):],
the carrier of F_Real by FUNCT_2:32;
set Z = LatticeStr (# the carrier of EMbedding(r, L),
the addF of EMbedding(r, L), 0.(EMbedding(r, L)),
the lmult of EMbedding(r, L), sc #);
AZ: Z = GenLat(EMbedding(r, L), sc);
A0: Z is Submodule of EMbedding(r, L) by AZ,ZMODLAT1:2;
reconsider Z as Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr
over INT.Ring by AZ;
AX: EMbedding(r, L) is Submodule of DivisibleMod(L) by ZMODUL08:32;
then AX2: Z is Submodule of DivisibleMod(L) by A0,ZMODUL01:42;
reconsider Z as free Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty LatticeStr
over INT.Ring by AZ;
Z is Z_Lattice-like
proof
thus for x being Vector of Z
st for y being Vector of Z holds <; x, y ;> = 0
holds x = 0.Z
proof
let x be Vector of Z such that
B1: for y being Vector of Z holds <; x, y ;> = 0;
per cases;
suppose C1: r is zero;
x in the carrier of EMbedding(r, L);
then x in r * (rng MorphsZQ(L)) by ZMODUL08:def 6;
then consider y be Vector of Z_MQ_VectSp(L) such that
C2: x = 0.F_Rat*y & y in rng MorphsZQ(L) by C1;
thus x = 0.Z_MQ_VectSp(L) by C2,VECTSP_1:14
.= 0.Z by ZMODUL08:25;
end;
suppose AS: r is non zero; then
consider T be linear-transformation of EMbedding(L), EMbedding(r, L)
such that
B2: (for v being Element of Z_MQ_VectSp(L) st v in EMbedding(L)
holds T.v = r * v) & T is bijective by ZMODUL08:27;
consider rm0, rn0 be Integer such that
BX: rn0 > 0 & r= rm0/rn0 by RAT_1:1;
reconsider rn=rn0,rm=rm0 as Element of INT.Ring by INT_1:def 2;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider rnf=rn, rmf=rm as Element of F_Real;
x in the carrier of EMbedding(r, L);
then x in rng T by B2,FUNCT_2:def 3;
then consider xe be object such that
B3: xe in the carrier of EMbedding(L) & x = T.xe by FUNCT_2:11;
reconsider xz = xe as Vector of Z_MQ_VectSp(L) by B3,ZMODUL08:19;
reconsider xd = xz as Vector of DivisibleMod(L) by ZMODUL08:30;
consider zxd be Vector of DivisibleMod(L) such that
BY: xd = rn * zxd & r * xz = rm * zxd by AS,BX,ZMODUL08:31;
reconsider xe as Vector of EMbedding(L) by B3;
for ye being Vector of EMbedding(L) holds
(ScProductEM(L)).(xe, ye) = 0
proof
let ye be Vector of EMbedding(L);
reconsider yz = ye as Vector of Z_MQ_VectSp(L) by ZMODUL08:19;
reconsider yd = yz as Vector of DivisibleMod(L) by ZMODUL08:30;
consider zyd be Vector of DivisibleMod(L) such that
C1: yd = rn * zyd & r * yz = rm * zyd by AS,BX,ZMODUL08:31;
reconsider y = T.ye as Vector of EMbedding(r, L);
reconsider y as Vector of Z;
reconsider xd1 = xd as Vector of EMbedding(L) by B3;
reconsider yd1 = yd as Vector of EMbedding(L);
C7: xz in EMbedding(L) by B3;
C8: yz in EMbedding(L);
C5: x = rm * zxd by B2,B3,BY,C7;
C6: y = rm * zyd by B2,C1,C8;
CX: <; x, y ;> = sc.(x, y)
.= (ScProductDM(L)).(rm * zxd, y) by C5,ThSPrEM1
.= rm * (ScProductDM(L)).(zxd, rm * zyd) by C6,ThSPDM1
.= rm * (ScProductDM(L)).(rm * zyd, zxd) by ThSPDM1
.= rm * (rm * (ScProductDM(L)).(zyd, zxd)) by ThSPDM1
.= rm * (rm * (ScProductDM(L)).(zxd, zyd)) by ThSPDM1
.= (rmf * rmf) * (ScProductDM(L)).(zxd, zyd)
.= (rmf * rmf) * (rnf" * rnf" * (ScProductEM(L)).(xd1, yd1))
by BX,BY,C1,defScProductDM
.= (rmf * rmf * rnf" * rnf") * (ScProductEM(L)).(xd, yd);
rnf <> 0.F_Real by BX;
then rmf <> 0 & rnf" <> 0 by AS,BX,VECTSP_1:25;
hence (ScProductEM(L)).(xe, ye) = 0 by B1,CX;
end;
then B6: xz = 0.(EMbedding(L)) by ThSPEM1
.= 0.(Z_MQ_VectSp(L)) by ZMODUL08:19;
xe in EMbedding(L);
then T.xe = r * xz by B2
.= 0.(Z_MQ_VectSp(L)) by B6,VECTSP_1:15
.= 0.Z by ZMODUL08:25;
hence thesis by B3;
end;
end;
thus for x, y being Vector of Z holds <; x, y ;> = <; y, x ;>
proof
let x, y be Vector of Z;
reconsider xx = x, yy = y as Vector of DivisibleMod(L)
by AX,ZMODUL01:25;
thus <; x, y ;> = (the scalar of Z).(x, y)
.= (ScProductDM(L)).(xx, yy) by ThSPrEM1
.= (ScProductDM(L)).(yy, xx) by ThSPDM1
.= (the scalar of Z).(y, x) by ThSPrEM1
.= <; y, x ;>;
end;
thus for x, y, z being Vector of Z, a being Element of INT.Ring
holds <; x+y, z ;> = <; x, z ;> + <; y, z ;> &
<; a*x, y ;> = a * <; x, y ;>
proof
let x, y, z be Vector of Z, a be Element of INT.Ring;
reconsider xx = x, yy = y, zz = z as Vector of DivisibleMod(L)
by AX,ZMODUL01:25;
thus <; x+y, z ;> = (the scalar of Z).(x+y, z)
.= (ScProductDM(L)).(x+y, z) by ThSPrEM1
.= (ScProductDM(L)).(xx+yy, zz) by AX2,ZMODUL01:28
.= (ScProductDM(L)).(xx, zz) + (ScProductDM(L)).(yy, zz) by ThSPDM1
.= (the scalar of Z).(x, z) + (ScProductDM(L)).(yy, zz) by ThSPrEM1
.= (the scalar of Z).(x, z) + (the scalar of Z).(y, z) by ThSPrEM1
.= <; x, z ;> + <; y, z ;>;
thus <; a*x, y ;> = (the scalar of Z).(a*x, y)
.= (ScProductDM(L)).(a*x, y) by ThSPrEM1
.= (ScProductDM(L)).(a*xx, y) by AX2,ZMODUL01:29
.= a * (ScProductDM(L)).(xx, yy) by ThSPDM1
.= a * (the scalar of Z).(x, y) by ThSPrEM1
.= a * <; x, y ;>;
end;
end;
then reconsider Z as strict Z_Lattice by AZ;
take Z;
thus thesis by ZMODUL08:def 6;
end;
uniqueness;
end;
registration
let L be non trivial Z_Lattice;
cluster EMLat(L) -> non trivial;
correctness
proof
consider T be linear-transformation of L, EMbedding(L) such that
A1: T is bijective & T = MorphsZQ(L) &
(for v being Vector of L holds T.v = Class(EQRZM(L), [v,1]))
by ZMODUL08:21;
set v = the non zero Vector of L;
T.v in the carrier of EMbedding(L);
then A2: T.v in rng MorphsZQ(L) by ZMODUL08:def 3;
T.v <> 0.EMbedding(L)
proof
assume T.v = 0.EMbedding(L);
then T.v = T.(0.L) by ZMODUL05:19;
hence contradiction by A1,FUNCT_2:19;
end;
then T.v <> zeroCoset(L) by ZMODUL08:def 3;
then T.v <> 0.EMLat(L) by defEMLat;
then not T.v in (0).EMLat(L) by ZMODUL02:66;
then (Omega).EMLat(L) <> (0).EMLat(L) by A2,defEMLat;
hence thesis by ZMODUL07:41;
end;
end;
registration
let L be non trivial Z_Lattice, r be non zero Element of F_Rat;
cluster EMLat(r,L) -> non trivial;
correctness
proof
consider T be linear-transformation of EMbedding(L), EMbedding(r,L)
such that
A1: (for v being Element of Z_MQ_VectSp(L) st v in EMbedding(L)
holds T.v = r*v) & T is bijective by ZMODUL08:27;
set v = the non zero Vector of EMbedding(L);
T.v in the carrier of EMbedding(r,L);
then A2: T.v in r*(rng MorphsZQ(L)) by ZMODUL08:def 6;
T.v <> 0.EMbedding(r,L)
proof
assume T.v = 0.EMbedding(r,L);
then T.v = T.(0.EMbedding(L)) by ZMODUL05:19;
hence contradiction by A1,FUNCT_2:19;
end;
then T.v <> zeroCoset(L) by ZMODUL08:def 6;
then T.v <> 0.EMLat(r,L) by defrEMLat;
then not T.v in (0).EMLat(r,L) by ZMODUL02:66;
then (Omega).EMLat(r,L) <> (0).EMLat(r,L) by A2,defrEMLat;
hence thesis by ZMODUL07:41;
end;
end;
registration
let L be INTegral Z_Lattice;
cluster EMLat(L) -> INTegral;
correctness
proof
set Z = EMLat(L);
for v, u being Vector of Z holds <; v, u ;> in INT
proof
let v, u be Vector of Z;
v in the carrier of Z;
then v in rng MorphsZQ(L) by defEMLat;
then B3: v is Vector of EMbedding(L) by ZMODUL08:def 3;
then consider vv be Vector of L such that
B1: (MorphsZQ(L)).vv = v by ZMODUL08:22;
u in the carrier of Z;
then u in rng MorphsZQ(L) by defEMLat;
then B4: u is Vector of EMbedding(L) by ZMODUL08:def 3;
then consider uu be Vector of L such that
B2: (MorphsZQ(L)).uu = u by ZMODUL08:22;
<; v, u ;> = (ScProductEM(L)).(v, u) by defEMLat
.= <; vv, uu ;> by B1,B2,B3,B4,defScProductEM;
hence thesis by ZMODLAT1:def 5;
end;
hence thesis;
end;
end;
theorem ThDivisibleL1:
for L being Z_Lattice holds EMLat(L) is Submodule of DivisibleMod(L)
proof
let L be Z_Lattice;
A1: the carrier of EMbedding(L) = rng MorphsZQ(L) by ZMODUL08:def 3
.= the carrier of EMLat(L) by defEMLat;
A2: the addF of EMLat(L) = (addCoset(L)) || (rng MorphsZQ(L)) by defEMLat
.= the addF of EMbedding(L) by ZMODUL08:def 3;
then reconsider ad = the addF of EMbedding(L)
as BinOp of the carrier of EMLat(L);
A3: 0.EMbedding(L) = zeroCoset(L) by ZMODUL08:def 3
.= 0.EMLat(L) by defEMLat;
then reconsider ze = 0.EMbedding(L) as Vector of EMLat(L);
A4: the lmult of EMLat(L) = (lmultCoset(L)) |
[:the carrier of INT.Ring,rng MorphsZQ(L):] by defEMLat
.= the lmult of EMbedding(L) by ZMODUL08:def 3;
then reconsider mu = the lmult of EMbedding(L)
as Function of [:the carrier of INT.Ring,the carrier of EMLat(L):],
the carrier of EMLat(L);
reconsider sc = the scalar of EMLat(L) as Function of
[:the carrier of EMbedding(L), the carrier of EMbedding(L):],
the carrier of F_Real by A1;
EMLat(L) = GenLat(EMbedding(L), sc) by A1,A2,A3,A4;
then A2: EMLat(L) is Submodule of EMbedding(L) by ZMODLAT1:2;
EMbedding(L) is Submodule of DivisibleMod(L) by ZMODUL08:24;
hence thesis by A2,ZMODUL01:42;
end;
theorem ThDivisibleL2:
for L being Z_Lattice, r being Element of F_Rat holds
EMLat(r, L) is Submodule of DivisibleMod(L)
proof
let L be Z_Lattice, r be Element of F_Rat;
A1: the carrier of EMbedding(r, L)
= r * (rng MorphsZQ(L)) by ZMODUL08:def 6
.= the carrier of EMLat(r, L) by defrEMLat;
A2: the addF of EMLat(r, L) = (addCoset(L)) || (r * (rng MorphsZQ(L)))
by defrEMLat
.= the addF of EMbedding(r, L) by ZMODUL08:def 6;
then reconsider ad = the addF of EMbedding(r, L)
as BinOp of the carrier of EMLat(r, L);
A3: 0.EMbedding(r, L) = zeroCoset(L) by ZMODUL08:def 6
.= 0.EMLat(r, L) by defrEMLat;
then reconsider ze = 0.EMbedding(r, L) as Vector of EMLat(r, L);
A4: the lmult of EMLat(r, L)
= (lmultCoset(L)) | [:the carrier of INT.Ring,r*(rng MorphsZQ(L)):]
by defrEMLat
.= the lmult of EMbedding(r, L) by ZMODUL08:def 6;
then reconsider mu = the lmult of EMbedding(r, L)
as Function of
[:the carrier of INT.Ring,the carrier of EMLat(r, L):],
the carrier of EMLat(r, L);
reconsider sc = the scalar of EMLat(r, L) as Function of
[:the carrier of EMbedding(r, L), the carrier of EMbedding(r, L):],
the carrier of F_Real by A1;
EMLat(r, L) = GenLat(EMbedding(r, L), sc) by A1,A2,A3,A4;
then A2: EMLat(r, L) is Submodule of EMbedding(r, L) by ZMODLAT1:2;
EMbedding(r, L) is Submodule of DivisibleMod(L) by ZMODUL08:32;
hence thesis by A2,ZMODUL01:42;
end;
theorem ThrEMLat1:
for L being Z_Lattice, r being non zero Element of F_Rat,
m, n being Element of INT.Ring, m1,n1 being Element of INT,
v being Vector of EMLat(r, L)
st m = m1 & n = n1 & r = m1/n1 & n1 <> 0
holds ex x being Vector of EMLat(L) st n*v = m*x
proof
let L be Z_Lattice, r be non zero Element of F_Rat,
m, n be Element of INT.Ring,
m1, n1 be Element of INT,
v be Vector of EMLat(r, L) such that
A1: m=m1 & n=n1 & r = m1/n1 & n1 <> 0;
consider T be linear-transformation of EMbedding(L),EMbedding(r,L)
such that
A2: (for u being Element of Z_MQ_VectSp(L) st u in EMbedding(L)
holds T.u = r*u) & T is bijective by ZMODUL08:27;
v in the carrier of EMLat(r, L);
then v in r * (rng MorphsZQ(L)) by defrEMLat;
then v in the carrier of EMbedding(r, L) by ZMODUL08:def 6;
then v in rng T by A2,FUNCT_2:def 3;
then consider ve be object such that
A3: ve in the carrier of EMbedding(L) & v = T.ve by FUNCT_2:11;
reconsider vz = ve as Vector of Z_MQ_VectSp(L) by A3,ZMODUL08:19;
reconsider vd = vz as Vector of DivisibleMod(L) by ZMODUL08:30;
consider zvd be Vector of DivisibleMod(L) such that
A4: vd = n * zvd & r * vz = m * zvd by A1,ZMODUL08:31;
A5: vz in EMbedding(L) by A3;
vz in rng MorphsZQ(L) by A3,ZMODUL08:def 3;
then reconsider x = vz as Vector of EMLat(L) by defEMLat;
B1: EMLat(L) is Submodule of DivisibleMod(L) by ThDivisibleL1;
B2: EMLat(r, L) is Submodule of DivisibleMod(L) by ThDivisibleL2;
A7: m * x = m * vd by B1,ZMODUL01:29
.= (m * n) * zvd by A4,VECTSP_1:def 16
.= n * (m * zvd) by VECTSP_1:def 16
.= n * v by A2,A3,A4,A5,B2,ZMODUL01:29;
take x;
thus thesis by A7;
end;
theorem ThrEMLat2:
for L being Z_Lattice, r being Element of F_Rat,
v, u being Vector of EMLat(r, L), x, y being Vector of EMLat(L)
st v = x & u = y holds <; v, u ;> = <; x, y ;>
proof
let L be Z_Lattice, r be Element of F_Rat,
v, u be Vector of EMLat(r, L), x, y be Vector of EMLat(L) such that
A1: v = x & u = y;
v in the carrier of EMLat(L)& u in the carrier of EMLat(L) by A1;
then A2: v in rng MorphsZQ(L) & u in rng MorphsZQ(L) by defEMLat;
v in the carrier of EMLat(r, L) & u in the carrier of EMLat(r, L);
then v in (r * rng MorphsZQ(L)) & u in (r * rng MorphsZQ(L))
by defrEMLat;
then A3: v is Vector of EMbedding(r, L) & u is Vector of EMbedding(r, L)
by ZMODUL08:def 6;
thus <; v, u ;> = ((ScProductDM(L)) || (r * rng MorphsZQ(L))).(v, u)
by defrEMLat
.= ((ScProductDM(L)) || the carrier of EMbedding(r, L)).(v, u)
by ZMODUL08:def 6
.= (ScProductDM(L)).(v, u) by A3,ThSPrEM1
.= ((ScProductDM(L)) || rng MorphsZQ(L)).(v, u)
by A2,FUNCT_1:49,ZFMISC_1:87
.= (ScProductEM(L)).(x, y) by A1,ThSPEM2
.= <; x, y ;> by defEMLat;
end;
theorem
for L being INTegral Z_Lattice, r being non zero Element of F_Rat,
a being Rational, v, u being Vector of EMLat(r, L)
st r = a holds
a" * a" * <; v, u ;> in INT
proof
let L be INTegral Z_Lattice, r be non zero Element of F_Rat,
a be Rational, v, u be Vector of EMLat(r, L) such that
A1: r = a;
consider m0, n0 be Integer such that
A2: n0 > 0 & a = m0/n0 by RAT_1:2;
reconsider n=n0,m=m0 as Element of INT.Ring by INT_1:def 2;
consider vv be Vector of EMLat(L) such that
A3: n*v = m*vv by A1,A2,ThrEMLat1;
consider uu be Vector of EMLat(L) such that
A4: n*u = m*uu by A1,A2,ThrEMLat1;
r <> 0.F_Rat;
then A5: m <> 0 by A1,A2;
A6: n * n * <; v, u ;> = n * (n * <; v, u ;>)
.= n * <; v, n*u ;> by ZMODLAT1:9
.= <; n*v, n*u ;> by ZMODLAT1:def 3
.= <; m*vv, m*uu ;> by A3,A4,ThrEMLat2
.= m * <; vv, m*uu ;> by ZMODLAT1:def 3
.= m * (m * <; vv, uu ;>) by ZMODLAT1:9
.= m * m * <; vv, uu ;>;
A7: (1/m0) * (1/m0) * (n0 * n0 * <; v, u ;>)
= (n0/m0) * (n0/m0) * <; v, u ;>
.= a" * (n0/m0) * <; v, u ;> by A2,XCMPLX_1:213
.= a" * a" * <; v, u ;> by A2,XCMPLX_1:213;
(1/m0) * (1/m0) * (m0 * m0 * <; vv, uu ;>)
= m0 * (1/m0) * (m0 * (1/m0) * <; vv, uu ;>)
.= 1 * (m0 * (1/m0) * <; vv, uu ;>) by A5,XCMPLX_1:106
.= 1.F_Real * <; vv, uu ;> by A5,XCMPLX_1:106
.= <; vv, uu ;>;
hence thesis by A6,A7,ZMODLAT1:def 5;
end;
registration
let L be positive-definite Z_Lattice;
cluster EMLat(L) -> positive-definite;
correctness
proof
set Z = EMLat(L);
for v being Vector of Z st v <> 0.Z holds ||. v .|| > 0
proof
let v be Vector of Z such that
AS: v <> 0.Z;
v in the carrier of Z;
then v in rng MorphsZQ(L) by defEMLat;
then B1: v is Vector of EMbedding(L) by ZMODUL08:def 3;
then consider vv be Vector of L such that
B2: (MorphsZQ(L)).vv = v by ZMODUL08:22;
B3: vv <> 0.L
proof
assume vv = 0.L;
then v = 0.(Z_MQ_VectSp(L)) by B2,ZMODUL04:def 6
.= 0.(EMbedding(L)) by ZMODUL08:19
.= zeroCoset(L) by ZMODUL08:def 3
.= 0.Z by defEMLat;
hence contradiction by AS;
end;
||. v .|| = (ScProductEM(L)).(v, v) by defEMLat
.= ||. vv .|| by B1,B2,defScProductEM;
hence thesis by B3,ZMODLAT1:def 6;
end;
hence thesis;
end;
end;
registration
let L be positive-definite Z_Lattice;
let r be non zero Element of F_Rat;
cluster EMLat(r, L) -> positive-definite;
correctness
proof
set Z = EMLat(r, L);
consider rm0, rn0 be Integer such that
A1: rn0 > 0 & r = rm0/rn0 by RAT_1:1;
a1: rn0 <> 0.INT.Ring by A1;
reconsider rn = rn0, rm = rm0 as Element of INT.Ring by INT_1:def 2;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider rnf = rn, rmf = rm as Element of F_Real;
for v being Vector of Z st v <> 0.Z holds ||. v .|| > 0
proof
let v be Vector of Z such that
B1: v <> 0.Z;
consider T be linear-transformation of EMbedding(L), EMbedding(r, L)
such that
B2: (for v being Vector of Z_MQ_VectSp(L) st v in EMbedding(L)
holds T.v = r * v) & T is bijective by ZMODUL08:27;
v in the carrier of Z;
then B0: v in r * (rng MorphsZQ(L)) by defrEMLat;
then v in the carrier of EMbedding(r, L) by ZMODUL08:def 6;
then v in rng T by B2,FUNCT_2:def 3;
then consider ve be object such that
B3: ve in the carrier of EMbedding(L) & v = T.ve by FUNCT_2:11;
reconsider vz = ve as Vector of Z_MQ_VectSp(L) by B3,ZMODUL08:19;
reconsider vd = vz as Vector of DivisibleMod(L) by ZMODUL08:30;
consider zvd be Vector of DivisibleMod(L) such that
B4: vd = rn * zvd & r * vz = rm * zvd by A1,ZMODUL08:31;
BX: vz in EMbedding(L) by B3;
B5: v = rm * zvd by B2,B3,B4,BX;
B6: v is Vector of EMbedding(r, L) by B0,ZMODUL08:def 6;
reconsider vd as Vector of EMbedding(L) by B3;
B8: ||. v .|| = ((ScProductDM(L)) || (r * (rng MorphsZQ(L)))).(v, v)
by defrEMLat
.= ((ScProductDM(L)) || (the carrier of EMbedding(r, L))).(v, v)
by ZMODUL08:def 6
.= (ScProductDM(L)).(v, v) by B6,ThSPrEM1
.= rm0 * (ScProductDM(L)).(zvd, rm * zvd) by B5,ThSPDM1
.= rm0 * (ScProductDM(L)).(rm * zvd, zvd) by ThSPDM1
.= rm0 * (rm0 * (ScProductDM(L)).(zvd, zvd)) by ThSPDM1
.= (rm0 * rm0) * (ScProductDM(L)).(zvd, zvd)
.= (rmf * rmf) * (rnf" * rnf" * (ScProductEM(L)).(vd, vd))
by A1,B4,defScProductDM
.= ((rmf * rmf) * (rnf" * rnf")) * (ScProductEM(L)).(vd, vd);
BY: rnf <> 0.F_Real by A1;
rm0 <> 0
proof
assume rm0 = 0;
then r = 0.F_Rat by A1;
hence contradiction;
end;
then rmf <> 0 & rnf" <> 0 by BY,VECTSP_1:25;
then B9: rmf * rmf > 0 & rnf" * rnf" > 0 by XREAL_1:63;
vd in the carrier of EMbedding(L);
then vd in rng MorphsZQ(L) by ZMODUL08:def 3;
then reconsider vl = vd as Vector of EMLat(L) by defEMLat;
vd <> 0.(EMbedding(L))
proof
assume C1: vd = 0.(EMbedding(L));
rn * zvd = zeroCoset(L) by B4,C1,ZMODUL08:def 3
.= 0.(DivisibleMod(L)) by ZMODUL08:def 4;
then zvd = 0.(DivisibleMod(L)) by ZMODUL01:def 7,a1;
then v = 0.(DivisibleMod(L)) by B5,ZMODUL01:1
.= zeroCoset(L) by ZMODUL08:def 4
.= 0.Z by defrEMLat;
hence contradiction by B1;
end;
then vd <> zeroCoset(L) by ZMODUL08:def 3;
then B10: vd <> 0.(EMLat(L)) by defEMLat;
(ScProductEM(L)).(vd, vd) = ||. vl .|| by defEMLat;
then (ScProductEM(L)).(vd, vd) > 0 by B10,ZMODLAT1:def 6;
hence thesis by B8,B9;
end;
hence thesis;
end;
end;
theorem ThSPDM2:
for L being positive-definite Z_Lattice,
v being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(v, v) = 0 iff v = 0.DivisibleMod(L)
proof
let L be positive-definite Z_Lattice, v be Vector of DivisibleMod(L);
consider a be Element of INT.Ring such that
A1: a <> 0 & a * v in EMbedding(L) by ZMODUL08:29;
a1: a <> 0.INT.Ring by A1;
reconsider u = a * v as Vector of EMbedding(L) by A1;
u in the carrier of EMbedding(L);
then u in rng MorphsZQ(L) by ZMODUL08:def 3;
then reconsider ul = u as Vector of EMLat(L) by defEMLat;
A2: a * a * (ScProductDM(L)).(v, v) = a * (a * (ScProductDM(L)).(v, v))
.= a * (ScProductDM(L)).(a*v, v) by ThSPDM1
.= a * (ScProductDM(L)).(v, a*v) by ThSPDM1
.= (ScProductDM(L)).(a*v, a*v) by ThSPDM1;
ScProductEM(L) = (ScProductDM(L)) || (rng MorphsZQ(L)) by ThSPEM2
.= (ScProductDM(L)) || (the carrier of EMbedding(L)) by ZMODUL08:def 3;
then A4: (ScProductDM(L)).(a*v, a*v) = (ScProductEM(L)).(u, u)
by FUNCT_1:49,ZFMISC_1:87
.= ||. ul .|| by defEMLat;
hereby
assume B1: (ScProductDM(L)).(v, v) = 0;
assume v <> 0.DivisibleMod(L);
then a * v <> 0.DivisibleMod(L) by a1,ZMODUL01:def 7;
then u <> zeroCoset(L) by ZMODUL08:def 4;
then ul <> 0.EMLat(L) by defEMLat;
hence contradiction by A2,A4,B1,ZMODLAT1:16;
end;
assume v = 0.DivisibleMod(L);
then u = 0.DivisibleMod(L) by ZMODUL01:1
.= zeroCoset(L) by ZMODUL08:def 4
.= 0.EMLat(L) by defEMLat;
hence thesis by A1,A2,A4,ZMODLAT1:16;
end;
theorem ThSLX2:
for L being positive-definite Z_Lattice,
Z being non empty LatticeStr over INT.Ring st
Z is Submodule of DivisibleMod(L) &
the scalar of Z = (ScProductDM(L)) || (the carrier of Z) holds
Z is Z_Lattice-like
proof
let L be positive-definite Z_Lattice,
Z be non empty LatticeStr over INT.Ring such that
A1: Z is Submodule of DivisibleMod(L) &
the scalar of Z = (ScProductDM(L)) || (the carrier of Z);
set A = the carrier of Z;
A2: for x, y being Vector of Z holds
(the scalar of Z).(x, y) = (ScProductDM(L)).(x, y)
proof
let x, y be Vector of Z;
[x, y] in [:A, A:];
hence (the scalar of Z).(x, y) = (ScProductDM(L)).(x, y)
by A1,FUNCT_1:49;
end;
Z is Z_Lattice-like
proof
thus for x being Vector of Z
st for y being Vector of Z holds <; x, y ;> = 0
holds x = 0.Z
proof
let x be Vector of Z such that
B1: for y being Vector of Z holds <; x, y ;> = 0;
B2: x is Vector of DivisibleMod(L) by A1,ZMODUL01:25;
assume x <> 0.Z;
then x <> 0.DivisibleMod(L) by A1,ZMODUL01:26;
then (ScProductDM(L)).(x, x) <> 0 by B2,ThSPDM2;
then (the scalar of Z).(x, x) <> 0 by A2;
then <; x, x ;> <> 0;
hence contradiction by B1;
end;
thus for x, y being Vector of Z holds <; x, y ;> = <; y, x ;>
proof
let x, y be Vector of Z;
reconsider xx = x, yy = y as Vector of DivisibleMod(L)
by A1,ZMODUL01:25;
thus <; x, y ;> = (the scalar of Z).(x, y)
.= (ScProductDM(L)).(x, y) by A2
.= (ScProductDM(L)).(yy, xx) by ThSPDM1
.= (the scalar of Z).(y, x) by A2
.= <; y, x ;>;
end;
thus for x, y, z being Vector of Z, a being Element of INT.Ring
holds <; x + y, z ;> = <; x, z ;> + <; y, z ;> &
<; a*x, y ;> = a * <; x, y ;>
proof
let x, y, z be Vector of Z, a be Element of INT.Ring;
reconsider xx = x, yy = y, zz = z as Vector of DivisibleMod(L)
by A1,ZMODUL01:25;
B1: xx + yy = x + y by A1,ZMODUL01:28;
thus <; x + y, z ;> = (the scalar of Z).(x + y, z)
.= (ScProductDM(L)).(xx + yy, zz) by A2,B1
.= (ScProductDM(L)).(xx, zz) + (ScProductDM(L)).(yy, zz) by ThSPDM1
.= (the scalar of Z).(x, z) + (ScProductDM(L)).(y, z) by A2
.= (the scalar of Z).(x, z) + (the scalar of Z).(y, z) by A2
.= <; x, z ;> + <; y, z ;>;
B2: a * xx = a * x by A1,ZMODUL01:29;
thus <; a*x, y ;> = (the scalar of Z).(a*x, y)
.= (ScProductDM(L)).(a*xx, yy) by A2,B2
.= a * (ScProductDM(L)).(xx, yy) by ThSPDM1
.= a * (the scalar of Z).(x, y) by A2
.= a * <; x, y ;>;
end;
end;
hence thesis;
end;
theorem
for L being positive-definite Z_Lattice,
Z being non empty LatticeStr over INT.Ring
st Z is finitely-generated Submodule of DivisibleMod(L) &
the scalar of Z = (ScProductDM(L)) || (the carrier of Z) holds
Z is Z_Lattice by ThSLX2;
theorem LmEMDetX0:
for L being Z_Lattice holds
the ModuleStr of EMLat(L) = EMbedding(L)
proof
let L be Z_Lattice;
Q1: the carrier of EMLat(L) = rng MorphsZQ(L) by defEMLat
.= the carrier of EMbedding(L) by ZMODUL08:def 3;
Q2: the ZeroF of EMLat(L) = zeroCoset(L) by defEMLat
.= the ZeroF of EMbedding(L) by ZMODUL08:def 3;
Q3: the addF of EMLat(L) = (addCoset(L)) || (rng MorphsZQ(L)) by defEMLat
.= the addF of EMbedding(L) by ZMODUL08:def 3;
Q4: the lmult of EMLat(L) = (lmultCoset(L)) | [:the carrier of INT.Ring,
rng MorphsZQ(L):] by defEMLat
.= the lmult of EMbedding(L) by ZMODUL08:def 3;
thus the ModuleStr of EMLat(L) = EMbedding(L) by Q1,Q2,Q3,Q4;
end;
theorem LmEMDetX53:
for L, E being Z_Module st the ModuleStr of L = the ModuleStr of E
holds L is Submodule of E
proof
let L, E be Z_Module;
assume AS: the ModuleStr of L = the ModuleStr of E;
P2: 0.L = 0.E by AS;
P3: the addF of L = (the addF of E) || the carrier of L by AS;
the lmult of L
= (the lmult of E) | ( [: the carrier of INT.Ring, the carrier of L:]
qua set) by AS;
hence thesis by AS,P2,P3,VECTSP_4:def 2;
end;
theorem LmEMDetX541:
for E, L being Z_Module, I being Subset of L, J being Subset of E,
K being Linear_Combination of J
st I = J & the ModuleStr of L = the ModuleStr of E
holds K is Linear_Combination of I
proof
let E, L be Z_Module, I be Subset of L, J be Subset of E,
K be Linear_Combination of J;
assume that AS1: I = J
and AS2: the ModuleStr of L = the ModuleStr of E;
P1: K is Linear_Combination of E &
Carrier K c= J by VECTSP_6:def 4;
consider T be finite Subset of E such that
P4: for v being Element of E st not v in T holds
K.v = 0.(INT.Ring) by VECTSP_6:def 1;
reconsider S = T as finite Subset of L by AS2;
reconsider H = K as Linear_Combination of L by AS2,P4,VECTSP_6:def 1;
Carrier H c= I by P1,AS1,AS2;
hence thesis by VECTSP_6:def 4;
end;
theorem
for E, L being Z_Module,
K being Linear_Combination of E,
H being Linear_Combination of L
st K = H & the ModuleStr of L = the ModuleStr of E
holds Carrier K = Carrier H;
theorem LmEMDetX543:
for E, L being Z_Module,
K being Linear_Combination of E,
H being Linear_Combination of L
st K = H & the ModuleStr of L = the ModuleStr of E
holds Sum K = Sum H
proof
let E, L be Z_Module,
K be Linear_Combination of E,
H be Linear_Combination of L;
assume AS: K = H & the ModuleStr of L = the ModuleStr of E;
B3: L is Submodule of E by AS,LmEMDetX53;
B4: Carrier K c= the carrier of L by AS;
H = K | the carrier of L by AS;
hence Sum K = Sum H by ZMODUL03:11,B3,B4;
end;
theorem LmEMDetX51:
for L, E being Z_Module, I being Subset of L, J being Subset of E
st the ModuleStr of L = the ModuleStr of E & I = J
holds (I is linearly-independent iff J is linearly-independent)
proof
for E, L being Z_Module, I being Subset of L, J being Subset of E
st I = J & the ModuleStr of L = the ModuleStr of E
& I is linearly-independent
holds J is linearly-independent
proof
let E, L be Z_Module, I be Subset of L, J be Subset of E;
assume that
A1: I = J and
A3: the ModuleStr of L = the ModuleStr of E
and A2: I is linearly-independent;
for K being Linear_Combination of J st Sum K = 0. E holds
Carrier K = {}
proof
let K be Linear_Combination of J;
assume P0: Sum K = 0.E;
reconsider H = K as Linear_Combination of I by A1,A3,LmEMDetX541;
P1: Carrier K = Carrier H by A3;
Sum H = 0. L by A3,P0,LmEMDetX543;
hence thesis by A2,P1,VECTSP_7:def 1;
end;
hence thesis by VECTSP_7:def 1;
end;
hence thesis;
end;
theorem LmEMDetX52:
for L, E being Z_Module, I being Subset of L, J be Subset of E
st the ModuleStr of L = the ModuleStr of E & I = J
holds Lin I = Lin J
proof
let L, E be Z_Module, I be Subset of L, J be Subset of E;
assume that
A1: the ModuleStr of L = the ModuleStr of E and
A2: I = J;
L is Submodule of E by A1,LmEMDetX53;
hence Lin I = Lin J by A2,ZMODUL03:20;
end;
theorem LmEMDetX5:
for L, E being free Z_Module, I being Subset of L, J being Subset of E
st the ModuleStr of L = the ModuleStr of E & I = J
holds ( I is Basis of L iff J is Basis of E)
proof
let L,E be free Z_Module, I be Subset of L, J be Subset of E;
assume that
A1: the ModuleStr of L = the ModuleStr of E and
A2: I = J;
hereby
assume P1: I is Basis of L;
then I is linearly-independent &
Lin I = ModuleStr(# the carrier of L, the addF of L,
the ZeroF of L, the lmult of L #) by VECTSP_7:def 3;
then P2: J is linearly-independent by A1,A2,LmEMDetX51;
Lin J = Lin I by A1,A2,LmEMDetX52
.= ModuleStr(# the carrier of E, the addF of E,
the ZeroF of E, the lmult of E #) by A1,P1,VECTSP_7:def 3;
hence J is Basis of E by P2,VECTSP_7:def 3;
end;
assume P1: J is Basis of E;
then J is linearly-independent &
Lin J = ModuleStr(# the carrier of E, the addF of E,
the ZeroF of E, the lmult of E #) by VECTSP_7:def 3;
then P2: I is linearly-independent by A1,A2,LmEMDetX51;
Lin I = Lin J by A1,A2,LmEMDetX52
.= ModuleStr(# the carrier of L, the addF of L,
the ZeroF of L, the lmult of L #) by A1,P1,VECTSP_7:def 3;
hence I is Basis of L by P2,VECTSP_7:def 3;
end;
theorem LmEMDetX4:
for L, E being finite-rank free Z_Module
st the ModuleStr of L = the ModuleStr of E
holds rank L = rank E
proof
let L, E be finite-rank free Z_Module;
assume AS: the ModuleStr of L = the ModuleStr of E;
set I = the Basis of L;
P1: rank L = card I by ZMODUL03:def 5;
reconsider J = I as Subset of E by AS;
J is Basis of E by LmEMDetX5,AS;
hence thesis by P1,ZMODUL03:def 5;
end;
theorem LmEMDetX6:
for L being Z_Lattice, I being Subset of L
holds I is Basis of L
iff (MorphsZQ(L)).: I is Basis of EMbedding(L)
proof
let L be Z_Lattice, I be Subset of L;
consider T be linear-transformation of L, EMbedding(L) such that
A1: T is bijective and
A2: T = MorphsZQ(L) and
for v being Vector of L holds T.v = Class(EQRZM(L),[v,1])
by ZMODUL08:21;
thus thesis by A1,A2,ZMODUL06:49;
end;
theorem
for L being Z_Lattice, I being Subset of L
holds I is Basis of L
iff (MorphsZQ(L)).: I is Basis of EMLat(L)
proof
let L be Z_Lattice, I be Subset of L;
P1: I is Basis of L iff (MorphsZQ(L)).: I is Basis of EMbedding(L)
by LmEMDetX6;
the ModuleStr of EMLat(L) = the ModuleStr of EMbedding(L) by LmEMDetX0;
hence thesis by P1,LmEMDetX5;
end;
theorem LmEMDetX8:
for L being Z_Lattice, b being FinSequence of L
holds b is OrdBasis of L
iff (MorphsZQ(L))*b is OrdBasis of EMbedding(L)
proof
let L be Z_Lattice, b be FinSequence of L;
E1: ex T being linear-transformation of L, EMbedding(L)
st T is bijective & T = MorphsZQ(L) &
(for v being Vector of L holds T.v = Class(EQRZM(L),[v,1]))
by ZMODUL08:21;
E4: (MorphsZQ(L))*b is FinSequence of EMbedding(L) by E1,FINSEQ_2:32;
P3: rng ((MorphsZQ(L))*b) =(MorphsZQ(L)).: (rng b) by RELAT_1:127;
hereby
assume b is OrdBasis of L;
then P1: b is one-to-one & rng b is Basis of L by ZMATRLIN:def 5;
then (MorphsZQ(L)).: (rng b) is Basis of EMbedding(L) by LmEMDetX6;
hence (MorphsZQ(L))*b is OrdBasis of EMbedding(L)
by E1,E4,P1,P3,ZMATRLIN:def 5;
end;
assume (MorphsZQ(L))*b is OrdBasis of EMbedding(L);
then P1: (MorphsZQ(L))*b is one-to-one
& rng ((MorphsZQ(L))*b) is Basis of EMbedding(L)
by ZMATRLIN:def 5;
dom (MorphsZQ(L)) = the carrier of L by FUNCT_2:def 1;
then rng b c= dom (MorphsZQ(L));
then P2: b is one-to-one by P1,FUNCT_1:25;
rng b is Basis of L by LmEMDetX6,P1,P3 ;
hence b is OrdBasis of L by ZMATRLIN:def 5,P2;
end;
theorem LmEMDetX9:
for L being Z_Lattice,
E being finite-rank free Z_Module,
I being FinSequence of L,
J being FinSequence of E
st the ModuleStr of L = the ModuleStr of E & I = J
holds ( I is OrdBasis of L iff J is OrdBasis of E)
proof
let L be Z_Lattice, E be finite-rank free Z_Module,
I be FinSequence of L, J be FinSequence of E;
assume that
AS1: the ModuleStr of L = the ModuleStr of E and
AS2: I = J;
hereby
assume I is OrdBasis of L;
then P2: I is one-to-one & rng I is Basis of L by ZMATRLIN:def 5;
then rng J is Basis of E by AS1,AS2,LmEMDetX5;
hence J is OrdBasis of E by AS2,P2,ZMATRLIN:def 5;
end;
assume J is OrdBasis of E;
then P2: J is one-to-one & rng J is Basis of E by ZMATRLIN:def 5;
then rng I is Basis of L by AS1,AS2,LmEMDetX5;
hence I is OrdBasis of L by AS2,P2,ZMATRLIN:def 5;
end;
theorem
for L being Z_Lattice, b being FinSequence of L
holds b is OrdBasis of L
iff (MorphsZQ(L))*b is OrdBasis of EMLat(L)
proof
let L be Z_Lattice, b be FinSequence of L;
P1: b is OrdBasis of L iff (MorphsZQ(L))*b is OrdBasis of EMbedding(L)
by LmEMDetX8;
the ModuleStr of EMLat(L) = the ModuleStr of EMbedding(L) by LmEMDetX0;
hence thesis by P1,LmEMDetX9;
end;
theorem
for L being Z_Lattice holds rank (L) = rank(EMLat(L))
proof
let L be Z_Lattice;
consider T be linear-transformation of L, EMbedding(L) such that
A1: T is bijective and
T = MorphsZQ(L) and
for v being Vector of L holds T.v = Class(EQRZM(L),[v,1])
by ZMODUL08:21;
P1: rank L = rank EMbedding(L) by A1,ZMODUL06:51;
the ModuleStr of EMLat(L) = EMbedding(L) by LmEMDetX0;
hence thesis by P1,LmEMDetX4;
end;
theorem ThEME1:
for L being Z_Lattice, x being object holds
x is Vector of EMLat(L) iff x is Vector of EMbedding(L)
proof
let L be Z_Lattice, x be object;
hereby
assume x is Vector of EMLat(L);
then x in the ModuleStr of EMLat(L);
hence x is Vector of EMbedding(L) by LmEMDetX0;
end;
assume x is Vector of EMbedding(L);
then x in EMbedding(L);
then x in the ModuleStr of EMLat(L) by LmEMDetX0;
hence x is Vector of EMLat(L);
end;
registration
let L be RATional Z_Lattice;
let v, u be Vector of EMLat(L);
cluster (ScProductEM(L)).(v, u) -> rational;
correctness
proof
A1: v is Vector of EMbedding(L) by ThEME1;
then consider vv be Vector of L such that
A2: (MorphsZQ(L)).vv = v by ZMODUL08:22;
A3: u is Vector of EMbedding(L) by ThEME1;
then consider uu be Vector of L such that
A4: (MorphsZQ(L)).uu = u by ZMODUL08:22;
(ScProductEM(L)).(v, u) = <; vv, uu ;> by A1,A2,A3,A4,defScProductEM;
hence thesis;
end;
end;
registration
let L be RATional Z_Lattice;
let v, u be Vector of DivisibleMod(L);
cluster (ScProductDM(L)).(v, u) -> rational;
correctness
proof
consider i be Element of INT.Ring such that
A1: i <> 0 & i * v in EMbedding(L) by ZMODUL08:29;
consider j be Element of INT.Ring such that
A2: j <> 0 & j * u in EMbedding(L) by ZMODUL08:29;
reconsider iv = i * v, ju = j * u as Vector of EMbedding(L) by A1,A2;
reconsider a = i, b = j as Element of INT;
reconsider a, b as Element of F_Real by XREAL_0:def 1;
A3: (ScProductDM(L)).(v, u) = a" * b" * (ScProductEM(L)).(iv, ju)
by A1,A2,defScProductDM;
A4: iv is Vector of EMLat(L) & ju is Vector of EMLat(L) by ThEME1;
reconsider ar = a, br = b as Element of F_Rat by RAT_1:def 2;
a <> 0.F_Real & b <> 0.F_Real by A1,A2;
then a" = ar" & b" = br" by GAUSSINT:14,GAUSSINT:21;
hence thesis by A3,A4;
end;
end;
begin :: 3. Properties of Gram Matrix
definition
let V be ModuleStr over INT.Ring;
let f be FrForm of V,V;
attr f is symmetric means :defSymForm:
for v, w being Vector of V holds f.(v, w) = f.(w, v);
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster NulFrForm(V,V) -> symmetric;
correctness
proof
set f = NulFrForm(V,V);
for v, w being Vector of V holds f.(v, w) = f.(w, v)
proof
let v, w be Vector of V;
thus f.(v, w) = 0.F_Real by FUNCOP_1:70
.= f.(w, v) by FUNCOP_1:70;
end;
hence thesis;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster symmetric for FrForm of V, V;
correctness
proof
take NulFrForm(V,V);
thus thesis;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster symmetric for bilinear-FrForm of V, V;
correctness
proof
take NulFrForm(V,V);
thus thesis;
end;
end;
registration
let L be Z_Lattice;
cluster InnerProduct(L) -> symmetric;
correctness
proof
set f = InnerProduct(L);
for v, w being Vector of L holds f.(v, w) = f.(w, v)
proof
let v, w be Vector of L;
thus f.(v, w) = <; v, w ;>
.= <; w, v ;> by ZMODLAT1:def 3
.= f.(w, v);
end;
hence thesis;
end;
end;
registration
let V be finite-rank free Z_Module;
let f be symmetric bilinear-FrForm of V, V;
let b be OrdBasis of V;
cluster GramMatrix(f, b) -> symmetric;
correctness
proof
set M = GramMatrix(f, b);
set MT = M@;
for i, j being Nat st [i, j] in Indices M
holds M*(i, j) = MT*(i, j)
proof
let i, j be Nat such that
A1: [i, j] in Indices M;
A2: [j, i] in Indices M by A1,MATRIX_0:28;
Indices M = [:Seg rank(V), Seg rank(V):] by MATRIX_0:24;
then A3: i in Seg rank(V) & j in Seg rank(V) by A1,ZFMISC_1:87;
len b = rank(V) by ZMATRLIN:49;
then A4: i in dom b & j in dom b by A3,FINSEQ_1:def 3;
thus M*(i, j) = f.(b/.i, b/.j) by A4,ZMODLAT1:def 32
.= f.(b/.j, b/.i) by defSymForm
.= BilinearM(f, b, b)*(j, i) by A4,ZMODLAT1:def 32
.= MT*(i, j) by A2,MATRIX_0:def 6;
end;
then M = MT by MATRIX_0:27;
hence thesis by MATRIX_6:def 5;
end;
end;
theorem
for L being RATional Z_Lattice,
v, u being Vector of DivisibleMod(L)
holds (ScProductDM(L)).(v, u) in F_Rat by RAT_1:def 2;
theorem ThGM1:
for L being RATional Z_Lattice, b being OrdBasis of L holds
GramMatrix(b) is Matrix of dim(L),F_Rat
proof
let L be RATional Z_Lattice, b be OrdBasis of L;
X1: len GramMatrix(b) = dim L & width GramMatrix(b) = dim L
& Indices GramMatrix(b) = [:Seg dim L, Seg dim L:] by MATRIX_0:24;
X3: len b = dim L by ZMATRLIN:49;
for i, j being Nat st [i, j] in Indices GramMatrix(b)
holds (GramMatrix(b))*(i,j) in the carrier of F_Rat
proof
let i, j be Nat;
assume [i, j] in Indices GramMatrix(b);
then i in Seg dim L & j in Seg dim L by X1,ZFMISC_1:87; then
D1: i in dom b & j in dom b by X3,FINSEQ_1:def 3;
(GramMatrix(b))*(i,j) = (InnerProduct(L)).(b/.i, b/.j)
by D1,ZMODLAT1:def 32
.= <; b/.i, b/.j ;>;
hence (GramMatrix(b))*(i,j) in the carrier of F_Rat by defRational;
end;
hence GramMatrix(b) is Matrix of dim(L),F_Rat by ZMODLAT1:1;
end;
theorem ZMATRLIN42:
for F being FinSequence of F_Real, G being FinSequence of F_Rat st F = G
holds Sum F = Sum G
proof
defpred P[Nat] means
for F being FinSequence of F_Real,
G being FinSequence of F_Rat
st len F = $1 & F = G
holds Sum F = Sum G;
P1: P[0]
proof
let F be FinSequence of F_Real,
G be FinSequence of F_Rat;
assume AS1: len F = 0 & F = G ;
F = <*> the carrier of F_Real by AS1;
then X1: Sum F = 0.F_Real by RLVECT_1:43
.= 0;
G = <*> the carrier of F_Rat by AS1;
then Sum G = 0.F_Rat by RLVECT_1:43
.= 0;
hence Sum F = Sum G by X1;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
let F be FinSequence of F_Real,
G be FinSequence of F_Rat;
assume AS2: len F = n+1 & F = G ;
reconsider F0 = F| n as FinSequence of F_Real;
reconsider G0 = G| n as FinSequence of F_Rat;
n+1 in Seg (n+1) by FINSEQ_1:4; then
A70: n+1 in dom F by AS2,FINSEQ_1:def 3;
then F.(n+1) in rng F by FUNCT_1:3;
then reconsider af = F.(n+1) as Element of F_Real;
G.(n+1) in rng G by AS2,A70,FUNCT_1:3;
then reconsider ag = G.(n+1) as Element of F_Rat;
P1: len F0 = n by FINSEQ_1:59,AS2,NAT_1:11;
len G0 = n by FINSEQ_1:59,AS2,NAT_1:11; then
BP4: dom G0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by AS2,FINSEQ_1:59,NAT_1:11;
BP3: Sum G = Sum G0 + ag by AS2,A9,BP4,RLVECT_1:38;
Sum F0 + af = Sum G0 + ag by AS1,AS2,P1;
hence Sum F = Sum G by AS2,A9,BP3,BP4,RLVECT_1:38;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
let F be FinSequence of F_Real, G be FinSequence of F_Rat;
assume F = G;
hence Sum F = Sum G by X1;
end;
theorem ZMATRLIN43:
for i being Nat, j being Element of F_Real, k being Element of F_Rat
st j = k
holds power(F_Real).(-1_F_Real,i)*j = power(F_Rat).(-1_F_Rat,i)*k
proof
let i be Nat,j be Element of F_Real,k be Element of F_Rat;
assume AS: j = k;
defpred P[Nat] means
power(F_Real).(-1_F_Real,$1)*j = power(F_Rat).(-1_F_Rat,$1)*k;
P1: P[0]
proof
power(F_Real).(-1_F_Real,0)*j = 1_(F_Real) *j by GROUP_1:def 7
.= power(F_Rat).(-1_F_Rat,0)*k by AS,GROUP_1:def 7;
hence thesis;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
P3: power(F_Real).(-1_F_Real,n+1)*j
= ((power(F_Real).(-1_F_Real,n)) * (-1_F_Real)) *j by GROUP_1:def 7
.= (-1_F_Real) * (( power(F_Real).(-1_F_Real,n)) * j);
power(F_Rat).(-1_F_Rat,n+1)*k
= ((power(F_Rat).(-1_F_Rat,n)) * (-1_F_Rat)) *k by GROUP_1:def 7
.= (-1_F_Rat) * (( power(F_Rat).(-1_F_Rat,n)) * k);
hence power(F_Real).(-1_F_Real,n+1)*j
= power(F_Rat).(-1_F_Rat,n+1)*k by AS1,P3;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
hence thesis;
end;
theorem LmSign1C:
for F being FinSequence of F_Real
st for i being Nat st i in dom F holds F.i in F_Rat
holds Sum F in F_Rat
proof
defpred P[Nat] means
for F being FinSequence of F_Real
st len F = $1 &
for i being Nat st i in dom F holds F.i in F_Rat
holds Sum F in F_Rat;
P1: P[0]
proof
let F be FinSequence of F_Real;
assume AS1: len F = 0 &
for i being Nat st i in dom F holds F.i in F_Rat;
F = <*> the carrier of F_Real by AS1;
then Sum F = 0.F_Real by RLVECT_1:43
.= 0;
hence Sum F in F_Rat;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
let F be FinSequence of F_Real;
assume AS2: len F = n+1 &
for i being Nat st i in dom F holds F.i in F_Rat;
reconsider F0 = F| n as FinSequence of F_Real;
n+1 in Seg (n+1) by FINSEQ_1:4; then
A70: n+1 in dom F by AS2,FINSEQ_1:def 3;
then F.(n+1) in rng F by FUNCT_1:3;
then reconsider af = F.(n+1) as Element of F_Real;
P1: len F0 = n by FINSEQ_1:59,AS2,NAT_1:11; then
P4: dom F0 = Seg n by FINSEQ_1:def 3;
len F = (len F0) + 1 by AS2,FINSEQ_1:59,NAT_1:11; then
P3: Sum F = Sum F0 + af by AS2,P4,RLVECT_1:38;
for i being Nat st i in dom F0 holds F0.i in F_Rat
proof
let i be Nat;
assume P40: i in dom F0;
dom F = Seg (n+1) by AS2,FINSEQ_1:def 3;
then dom F0 c= dom F by P4,FINSEQ_1:5,NAT_1:11;
then F.i in F_Rat by AS2,P40;
hence thesis by P40,FUNCT_1:47;
end;
then Sum F0 in F_Rat by P1,AS1;
then reconsider i1 = Sum F0 as Element of F_Rat;
F.(n+1) in F_Rat by A70,AS2;
then reconsider i2 = af as Element of F_Rat;
Sum F = i1 + i2 by P3;
hence Sum F in F_Rat;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
let F be FinSequence of F_Real;
assume X2: for i being Nat st i in dom F holds F.i in F_Rat;
len F is Nat;
hence Sum F in F_Rat by X1,X2;
end;
theorem LmSign1D:
for i being Nat holds power(F_Real).(-1_F_Real,i) in F_Rat
proof
let i be Nat;
power(F_Real).(-1_F_Real,i)*1.F_Real = power(F_Rat).(-1_F_Rat,i)*1.F_Rat
by ZMATRLIN43;
hence thesis;
end;
theorem LmSign1F:
for n, i, j, k, m being Nat, M being Matrix of n+1,F_Real
for L being Matrix of n+1,F_Rat
st 0 < n & M = L &
[i, j] in Indices M & [k, m] in Indices (Delete(M,i,j))
holds (Delete(M,i,j))*(k,m) = (Delete(L,i,j))*(k,m)
proof
let n, i, j, k, m be Nat, M be Matrix of n+1,F_Real;
let L be Matrix of n+1,F_Rat;
assume that 0 < n and
A2: M = L and
A3: [i, j] in Indices M and
A4: [k, m] in Indices (Delete(M,i,j));
[i, j] in [:Seg (n+1),Seg (n+1):] by A3,MATRIX_0:24;
then
A5: i in Seg (n+1) & j in Seg (n+1) by ZFMISC_1:87;
set M0 = Delete(M,i,j);
(n+1)-'1 = n by NAT_D:34;
then len M0 = n & width M0 = n & Indices M0 = [:(Seg n),(Seg n):]
by MATRIX_0:24; then
D5: k in Seg n & m in Seg n by A4,ZFMISC_1:87;
then
D3: k in Seg ((n+1)-'1) & m in Seg ((n+1)-'1) by NAT_D:34;
FC0: 1<=k & k <= n & 1<=m & m <= n by FINSEQ_1:1,D5;
then 1<=k & k+0 <= n+1 & 1<=m & m+0 <= n+1 by XREAL_1:7;
then
FC1: k in Seg (n+1) & m in Seg (n+1);
1+0<=k+1 & k+1 <= n+1 & 1+0<=m+1 & m+1 <= n+1 by FC0,XREAL_1:6;
then
FC3: k+1 in Seg (n+1) & m+1 in Seg (n+1);
per cases;
suppose CS1: k < i & m < j; then
F11: Delete(M,i,j)*(k,m) = M*(k,m) by LAPLACE:13,A5,D3;
BF11: Delete(L,i,j)*(k,m) = L*(k,m) by LAPLACE:13,A5,D3,CS1;
[k, m] in [:Seg (n+1),Seg (n+1):] by FC1,ZFMISC_1:87;
then [k, m] in Indices M by MATRIX_0:24;
hence thesis by A2,F11,BF11,ZMATRLIN:1;
end;
suppose CS2: k < i & m >= j; then
F21: Delete(M,i,j)*(k,m) = M*(k,m+1) by LAPLACE:13,A5,D3;
BF21: Delete(L,i,j)*(k,m) = L*(k,m+1) by LAPLACE:13,A5,D3,CS2;
[k, m+1] in [:Seg (n+1),Seg (n+1):] by FC1,FC3,ZFMISC_1:87;
then [k, m+1] in Indices M by MATRIX_0:24;
hence thesis by A2,F21,BF21,ZMATRLIN:1;
end;
suppose CS3: k >= i & m < j; then
F31: Delete(M,i,j)*(k,m) = M*(k+1,m) by LAPLACE:13,A5,D3;
BF31: Delete(L,i,j)*(k,m) = L*(k+1,m) by LAPLACE:13,A5,CS3,D3;
[k+1, m] in [:Seg (n+1),Seg (n+1):] by FC1,FC3,ZFMISC_1:87;
then [k+1, m] in Indices M by MATRIX_0:24;
hence thesis by A2,F31,BF31,ZMATRLIN:1;
end;
suppose CS4: k >= i & m >= j; then
F41: Delete(M,i,j)*(k,m) = M*(k+1,m+1) by LAPLACE:13,A5,D3;
BF41: Delete(L,i,j)*(k,m) = L*(k+1,m+1) by LAPLACE:13,A5,D3,CS4;
[k+1, m+1] in [:Seg (n+1),Seg (n+1):] by FC3,ZFMISC_1:87;
then [k+1, m+1] in Indices M by MATRIX_0:24;
hence thesis by A2,F41,BF41,ZMATRLIN:1;
end;
end;
theorem
for n, i, j, k, m being Nat, M being Matrix of n+1, F_Real
st 0 < n & M is Matrix of n+1, F_Rat &
[i, j] in Indices M & [k, m] in Indices (Delete(M,i,j))
holds (Delete(M,i,j))*(k,m) is Element of F_Rat
proof
let n, i, j, k, m be Nat, M be Matrix of n+1,F_Real;
assume that
A1: 0 < n and
A2: M is Matrix of n+1, F_Rat and
A3: [i, j] in Indices M and
A4: [k, m] in Indices (Delete(M,i,j));
reconsider L = M as Matrix of n+1, F_Rat by A2;
(Delete(M,i,j))*(k,m) = (Delete(L,i,j))*(k,m)
by LmSign1F,A1,A3,A4;
hence thesis;
end;
theorem LmSign1E:
for n, i, j being Nat, M being Matrix of n+1, F_Real
for L being Matrix of n+1, F_Rat
st 0 < n & M = L & [i, j] in Indices M
holds Delete(M,i,j) = Delete(L,i,j)
proof
let n, i, j be Nat, M be Matrix of n+1,F_Real;
let L be Matrix of n+1,F_Rat;
assume that
A1: 0 < n and
A2: M = L and
A3: [i, j] in Indices M;
set M0 = Delete(M,i,j);
set L0 = Delete(L,i,j);
X39: (n+1)-'1 = n by NAT_D:34; then
D2: len M0 = n & width M0 = n & Indices M0 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
BD2: len L0 = n & width L0 = n & Indices L0 = [:(Seg n),(Seg n):]
by MATRIX_0:24,X39;
for i1,j1 being Nat st [i1,j1] in Indices M0
holds M0*(i1,j1) = L0*(i1,j1) by LmSign1F,A1,A2,A3;
hence thesis by BD2,D2,ZMATRLIN:4;
end;
theorem LmSign1EX:
for n, i, j being Nat, M being Matrix of n+1, F_Real
st 0 < n & M is Matrix of n+1,F_Rat & [i, j] in Indices M
holds Delete(M,i,j) is Matrix of n, F_Rat
proof
let n, i, j be Nat, M be Matrix of n+1,F_Real;
assume that
A1: 0 < n and
A2: M is Matrix of n+1, F_Rat and
A3: [i, j] in Indices M;
reconsider L = M as Matrix of n+1, F_Rat by A2;
X1: Delete(M,i,j) = Delete(L,i,j) by LmSign1E,A1,A3;
(n+1)-'1 = n by NAT_D:34;
hence thesis by X1;
end;
theorem LmSign1A:
for n being Nat, M being Matrix of n, F_Real
for H being Matrix of n, F_Rat
st M = H
holds Det M = Det H
proof
defpred P[Nat] means
for M being Matrix of $1, F_Real
for H being Matrix of $1, F_Rat st M = H holds Det M = Det H;
P0: P[0]
proof
let M be Matrix of 0, F_Real;
let H be Matrix of 0, F_Rat;
assume M = H;
Det M = 1.F_Real by MATRIXR2:41
.= 1.F_Rat
.= Det H by MATRIXR2:41;
hence thesis;
end;
P1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P10: P[n];
let M be Matrix of n+1, F_Real;
let H be Matrix of n+1, F_Rat;
assume AS1: M = H;
reconsider j = 1 as Nat;
X0: 1 <= 1 & 1 <= n+1 by NAT_1:14;
then JX:j in Seg (n+1);
then
X1: Det M = Sum LaplaceExpC(M,j) by LAPLACE:27;
HX1: Det H = Sum LaplaceExpC(H,j) by JX,LAPLACE:27;
set L = LaplaceExpC(M,j);
set I = LaplaceExpC(H,j);
X2: len L = n+1
& for i being Nat st i in dom L holds
L.i = M*(i,j)*Cofactor(M,i,j) by LAPLACE:def 8;
Y3: dom L = Seg len I by X2,FINSEQ_1:def 3,LAPLACE:def 8
.= dom I by FINSEQ_1:def 3;
for i being Nat st i in dom L holds L.i = I.i
proof
let i be Nat;
assume X30:i in dom L; then
X31: L.i = M*(i,j)*Cofactor(M,i,j) by LAPLACE:def 8;
HX31: I.i = H*(i,j)*Cofactor(H,i,j) by Y3,X30,LAPLACE:def 8;
i in Seg (n+1) & j in Seg (n+1) by X0,X2,X30,FINSEQ_1:def 3;
then [i,j] in [:Seg (n+1),Seg (n+1):] by ZFMISC_1:87; then
X41: [i, j] in Indices M by MATRIX_0:24; then
X32: M*(i,j) = H*(i,j) by AS1,ZMATRLIN:1;
Y1: (n+1)-'1 = n by NAT_D:34;
set DD= Delete(M,i,j);
set EE= Delete(H,i,j);
Det DD = Det EE
proof
per cases;
suppose 0 < n;
hence Det DD = Det EE by AS1,P10,X41,Y1,LmSign1E;
end;
suppose not 0 < n;
then Y2: n = 0;
then Det DD = 1.F_Real by Y1,MATRIXR2:41
.= 1.F_Rat
.= Det EE by Y2,MATRIXR2:41,Y1;
hence thesis;
end;
end;
hence L.i = I.i by X32,X31,HX31,ZMATRLIN43;
end;
then L = I by Y3;
hence thesis by X1,HX1,ZMATRLIN42;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P0,P1);
hence thesis;
end;
theorem LmGM11:
for n being Nat, M being Matrix of n, F_Real st M is Matrix of n, F_Rat
holds Det M in F_Rat
proof
defpred P[Nat] means
for M being Matrix of $1, F_Real st M is Matrix of $1, F_Rat
holds Det M in F_Rat;
P0: P[0]
proof
let M be Matrix of 0, F_Real;
assume M is Matrix of 0, F_Rat;
Det M = 1.F_Real by MATRIXR2:41
.= 1;
hence Det M in F_Rat;
end;
P1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P10: P[n];
let M be Matrix of n+1, F_Real;
assume AS1: M is Matrix of n+1, F_Rat;
reconsider j = 1 as Nat;
X0: 1 <= 1 & 1 <= n+1 by NAT_1:14;
then j in Seg (n+1);
then
X1: Det M = Sum LaplaceExpC(M,j) by LAPLACE:27;
set L = LaplaceExpC(M,j);
X2: len L = n+1
& for i being Nat st i in dom L holds
L.i = M*(i,j)*Cofactor(M,i,j) by LAPLACE:def 8;
for i being Nat st i in dom L holds L.i in F_Rat
proof
let i be Nat;
assume X30:i in dom L; then
X31: L.i = M*(i,j)*Cofactor(M,i,j) by LAPLACE:def 8;
i in Seg (n+1) & j in Seg (n+1) by X0,X2,X30,FINSEQ_1:def 3;
then [i,j] in [:Seg (n+1),Seg (n+1):] by ZFMISC_1:87;
then
X41: [i, j] in Indices M by MATRIX_0:24;
then
X32: M*(i,j) is Element of F_Rat by AS1,ZMATRLIN:41;
(n+1)-'1 = n by NAT_D:34;
then reconsider DD= Delete(M,i,j) as Matrix of n,F_Real;
Det DD in F_Rat
proof
per cases;
suppose 0 < n;
then DD is Matrix of n, F_Rat by LmSign1EX,AS1,X41;
hence Det DD in F_Rat by P10;
end;
suppose not 0 < n;
then n = 0;
then Det DD = 1.F_Real by MATRIXR2:41
.= 1;
hence Det DD in F_Rat;
end;
end;
then A1: Minor(M,i,j) in F_Rat by NAT_D:34;
power(F_Real).(-1_F_Real,i+j) in F_Rat by LmSign1D;
hence L.i in F_Rat by A1,X32,X31,RAT_1:def 2;
end;
hence thesis by X1,LmSign1C;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P0,P1);
hence thesis;
end;
theorem
for n, i, j being Nat, M being Matrix of n+1, F_Real
st M is Matrix of n+1, F_Rat & [i, j] in Indices M
holds Cofactor(M,i,j) in F_Rat
proof
let n, i, j be Nat, M be Matrix of n+1, F_Real such that
AS: M is Matrix of n+1, F_Rat & [i, j] in Indices M;
(n+1)-'1 = n by NAT_D:34;
then reconsider DD= Delete(M,i,j) as Matrix of n,F_Real;
Det DD in F_Rat
proof
per cases;
suppose 0 < n;
then DD is Matrix of n, F_Rat by LmSign1EX,AS;
hence Det DD in F_Rat by LmGM11;
end;
suppose not 0 < n;
then n = 0;
then Det DD = 1.F_Real by MATRIXR2:41
.= 1;
hence Det DD in F_Rat;
end;
end;
then A1: Minor(M,i,j) in F_Rat by NAT_D:34;
power(F_Real).(-1_F_Real,i+j) in F_Rat by LmSign1D;
hence thesis by A1,RAT_1:def 2;
end;
theorem
for L being RATional Z_Lattice, b being OrdBasis of L holds
Det GramMatrix(b) in F_Rat
proof
let L be RATional Z_Lattice, b be OrdBasis of L;
GramMatrix(b) is Matrix of dim(L), F_Rat by ThGM1;
hence thesis by LmGM11;
end;
theorem ZL2LmSc1:
for L being positive-definite Z_Lattice, I being Basis of L,
v, w being Vector of L holds
(for u being Vector of L st u in I holds <; u, v ;> = <; u, w ;>)
implies
(for u being Vector of L holds <; u, v ;> = <; u, w ;>)
proof
let L be positive-definite Z_Lattice, I be Basis of L,
v, w be Vector of L;
assume AS:
for u being Vector of L st u in I holds <; u, v ;> = <; u, w ;>;
defpred P[Nat] means
for u being Vector of L, J being finite Subset of L
st J c= I & card(J) = $1 & u in Lin(J) holds
<; u, v ;> = <; u, w ;>;
A1: P[0]
proof
let u be Vector of L, J be finite Subset of L such that
B1: J c= I & card(J) = 0 & u in Lin(J);
J = {}(the carrier of L) by B1;
then Lin(J) = (0).L by VECTSP_7:9;
then B2: u = 0.L by B1,VECTSP_4:35;
then <; u, v ;> = 0 by ZMODLAT1:12;
hence thesis by B2,ZMODLAT1:12;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let u be Vector of L, J be finite Subset of L such that
B2: J c= I & card(J) = n+1 & u in Lin(J);
J is non empty by B2;
then consider s be object such that
B3: s in J;
reconsider s as Vector of L by B3;
set Js = J \ {s};
{s} is Subset of J by B3,SUBSET_1:41;
then B4: card(Js) = n+1 - card({s}) by B2,CARD_2:44
.= n+1 - 1 by CARD_1:30
.= n;
reconsider Js as finite Subset of L;
reconsider S = {s} as finite Subset of L;
B6: Js /\ S = {} by XBOOLE_0:def 7,XBOOLE_1:79;
consider l be Linear_Combination of J such that
B7: u = Sum(l) by B2,VECTSP_7:7;
reconsider lx = l as Linear_Combination of Js \/ S
by B3,XBOOLE_1:45,ZFMISC_1:31;
consider lx1 be Linear_Combination of Js,
lx2 be Linear_Combination of S such that
B8: lx = lx1 + lx2 by B6,ZMODUL04:26;
B9: u = Sum(lx1) + Sum(lx2) by B7,B8,VECTSP_6:44;
B10: Sum(lx1) in Lin(Js) by VECTSP_7:7;
Js c= J by XBOOLE_1:36;
then B11: Js c= I by B2;
B12: Sum(lx2) = lx2.s * s by VECTSP_6:17;
B14: <; Sum(lx2), v ;> = lx2.s * <; s, v ;> by B12,ZMODLAT1:def 3
.= lx2.s * <; s, w ;> by AS,B2,B3
.= <; Sum(lx2), w ;> by B12,ZMODLAT1:def 3;
thus <; u, v ;> = <; Sum(lx1), v ;> + <; Sum(lx2), v ;>
by B9,ZMODLAT1:def 3
.= <; Sum(lx1), w ;> + <; Sum(lx2), w ;> by B1,B4,B10,B11,B14
.= <; u, w ;> by B9,ZMODLAT1:def 3;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let u be Vector of L;
A4: u in Lin(I) by ZMODUL03:14;
reconsider n = card(I) as Nat;
P[n] by A3;
hence thesis by A4;
end;
theorem ZL2ThSc1:
for L being positive-definite Z_Lattice, b being OrdBasis of L,
v, w being Vector of L
st for n being Nat st n in dom b holds <; b/.n, v ;> = <; b/.n, w ;>
holds v = w
proof
let L be positive-definite Z_Lattice, b be OrdBasis of L,
v, w be Vector of L such that
A1: for n being Nat st n in dom b holds <; b/.n, v ;> = <; b/.n, w ;>;
reconsider I = rng b as Basis of L by ZMATRLIN:def 5;
for u being Vector of L st u in I holds <; u, v ;> = <; u, w ;>
proof
let u be Vector of L such that
B1: u in I;
consider i be Nat such that
B2: i in dom b & b.i = u by B1,FINSEQ_2:10;
b/.i = u by B2,PARTFUN1:def 6;
hence thesis by A1,B2;
end;
then <; v - w, v ;> = <; v - w, w ;> by ZL2LmSc1;
then <; v - w, v ;> - <; v - w, w ;> = 0.INT.Ring;
then ||. v - w .|| = 0.INT.Ring by ZMODLAT1:11;
then v - w = 0.L by ZMODLAT1:16;
hence thesis by RLVECT_1:21;
end;
theorem
for n being Nat, M being Matrix of n, F_Rat
st M is without_repeated_line
holds Det M <> 0.F_Rat iff lines M is linearly-independent
proof
let n be Nat, M being Matrix of n, F_Rat;
assume AS: M is without_repeated_line;
hereby assume Det M <> 0.F_Rat;
then the_rank_of M = n by MATRIX13:83;
hence lines M is linearly-independent by MATRIX13:110;
end;
assume lines M is linearly-independent;
then the_rank_of M = n by AS,MATRIX13:121;
hence Det M <> 0.F_Rat by MATRIX13:83;
end;
theorem
for L being positive-definite Z_Lattice, I being Basis of L,
v, w being Vector of L holds
(for u being Vector of L st u in I holds <; v,u ;> = <; w,u ;>)
implies
(for u being Vector of L holds <; v,u ;> = <; w,u;>)
proof
let L be positive-definite Z_Lattice, I be Basis of L,
v, w be Vector of L;
assume AS:
for u being Vector of L st u in I holds <; v,u ;> = <; w,u ;>;
P1: for u being Vector of L st u in I holds <; u,v ;> = <; u,w ;>
proof
let u be Vector of L;
assume P0: u in I;
thus <; u,v ;> = <; v,u ;> by ZMODLAT1:def 3
.= <; w,u ;> by AS,P0
.= <; u,w ;> by ZMODLAT1:def 3;
end;
thus for u being Vector of L holds <; v,u ;> = <; w,u ;>
proof
let u be Vector of L;
thus <; v,u ;> = <; u,v ;> by ZMODLAT1:def 3
.= <; u,w ;> by P1,ZL2LmSc1
.= <; w,u ;> by ZMODLAT1:def 3;
end;
end;
theorem ZL2ThSc1X:
for L being positive-definite Z_Lattice, b being OrdBasis of L,
v, w being Vector of L
st for n being Nat st n in dom b holds <; v, b/.n;> = <; w, b/.n ;>
holds v = w
proof
let L be positive-definite Z_Lattice, b be OrdBasis of L,
v, w be Vector of L such that
A1: for n being Nat st n in dom b holds <; v,b/.n ;> = <; w,b/.n;>;
for n being Nat st n in dom b holds <; b/.n,v ;> = <; b/.n,w;>
proof
let n be Nat;
assume A2: n in dom b;
thus <; b/.n,v ;> = <; v,b/.n ;> by ZMODLAT1:def 3
.= <; w,b/.n ;> by A1,A2
.= <; b/.n,w ;> by ZMODLAT1:def 3;
end;
hence thesis by ZL2ThSc1;
end;
theorem ZL2ThSc1D:
for L being positive-definite Z_Lattice, b being OrdBasis of EMLat(L),
v, w being Vector of DivisibleMod(L)
st for n being Nat st n in dom b holds
(ScProductDM(L)).(b/.n, v) = (ScProductDM(L)).(b/.n, w)
holds v = w
proof
let L be positive-definite Z_Lattice, b be OrdBasis of EMLat(L),
v, w be Vector of DivisibleMod(L) such that
A1: for n being Nat st n in dom b holds
(ScProductDM(L)).(b/.n, v) = (ScProductDM(L)).(b/.n, w);
consider i be Element of INT.Ring such that
A2: i <> 0 & i * v in EMbedding(L) by ZMODUL08:29;
consider j be Element of INT.Ring such that
A3: j <> 0 & j * w in EMbedding(L) by ZMODUL08:29;
i * v in rng MorphsZQ(L) by A2,ZMODUL08:def 3;
then reconsider iv = i * v as Vector of EMLat(L) by defEMLat;
j * w in rng MorphsZQ(L) by A3,ZMODUL08:def 3;
then reconsider jw = j * w as Vector of EMLat(L) by defEMLat;
A4: EMLat(L) is Submodule of DivisibleMod(L) by ThDivisibleL1;
for n being Nat st n in dom b holds <; b/.n, j*iv ;> = <; b/.n, i*jw ;>
proof
let n be Nat such that
B1: n in dom b;
b/.n in EMLat(L);
then b/.n in DivisibleMod(L) by A4,ZMODUL01:24;
then reconsider bn = b/.n as Vector of DivisibleMod(L);
b/.n in EMLat(L);
then b/.n in rng MorphsZQ(L) by defEMLat;
then B2: b/.n in EMbedding(L) by ZMODUL08:def 3;
B3: (i*j) * ((ScProductDM(L)).(b/.n, v))
= j * (i * (ScProductDM(L)).(bn, v))
.= j * (i * (ScProductDM(L)).(v, bn)) by ThSPDM1
.= j * ((ScProductDM(L)).(i*v, bn)) by ThSPDM1
.= j * ((ScProductEM(L)).(iv, b/.n)) by A2,B2,ThSPEM3
.= j * <; iv, b/.n ;> by defEMLat
.= <; j*iv, b/.n ;> by ZMODLAT1:def 3
.= <; b/.n, j*iv ;> by ZMODLAT1:def 3;
(i*j) * ((ScProductDM(L)).(b/.n, w)) = i * (j * (ScProductDM(L)).(bn, w))
.= i * (j * (ScProductDM(L)).(w, bn)) by ThSPDM1
.= i * ((ScProductDM(L)).(j*w, bn)) by ThSPDM1
.= i * ((ScProductEM(L)).(jw, b/.n)) by A3,B2,ThSPEM3
.= i * <; jw, b/.n ;> by defEMLat
.= <; i*jw, b/.n ;> by ZMODLAT1:def 3
.= <; b/.n, i*jw ;> by ZMODLAT1:def 3;
hence thesis by A1,B1,B3;
end;
then j*iv = i*jw by ZL2ThSc1
.= i*(j*w) by A4,ZMODUL01:29;
then j*(i*v) = i*(j*w) by A4,ZMODUL01:29
.= (i*j)*w by VECTSP_1:def 16;
then (i*j)*v = (i*j)*w by VECTSP_1:def 16;
hence thesis by A2,A3,ZMODUL01:10;
end;
theorem
for L being positive-definite Z_Lattice, b being OrdBasis of EMLat(L),
v, w being Vector of DivisibleMod(L)
st for n being Nat st n in dom b holds
(ScProductDM(L)).(v, b/.n) = (ScProductDM(L)).(w, b/.n)
holds v = w
proof
let L be positive-definite Z_Lattice, b be OrdBasis of EMLat(L),
v, w be Vector of DivisibleMod(L) such that
A1: for n being Nat st n in dom b holds
(ScProductDM(L)).(v, b/.n) = (ScProductDM(L)).(w, b/.n);
for n being Nat st n in dom b holds
(ScProductDM(L)).(b/.n, v) = (ScProductDM(L)).(b/.n, w)
proof
let n be Nat such that
B1: n in dom b;
B2: EMLat(L) is Submodule of DivisibleMod(L) by ThDivisibleL1;
b/.n in EMLat(L);
then b/.n in DivisibleMod(L) by B2,ZMODUL01:24;
then reconsider bn = b/.n as Vector of DivisibleMod(L);
thus (ScProductDM(L)).(b/.n, v) = (ScProductDM(L)).(v, bn) by ThSPDM1
.= (ScProductDM(L)).(w, b/.n) by A1,B1
.= (ScProductDM(L)).(bn, w) by ThSPDM1
.= (ScProductDM(L)).(b/.n, w);
end;
hence thesis by ZL2ThSc1D;
end;
theorem LMThGM21:
for L being non trivial RATional
positive-definite Z_Lattice,
v being Element of L,
b being FinSequence of L,
sbv being FinSequence of F_Rat
st len b = len sbv
& for n being Nat st n in dom sbv
holds sbv.n = <; b/.n, v ;>
holds <; Sum (b), v ;> = Sum sbv
proof
let L be non trivial RATional positive-definite Z_Lattice;
let v be Element of L;
defpred P[Nat] means
for F being FinSequence of L,
Fv being FinSequence of F_Rat
st len F = $1 & len F = len Fv &
for i being Nat st i in dom Fv holds Fv.i = <; F/.i, v ;>
holds <; Sum F, v ;> = Sum Fv;
P1: P[0]
proof
let F be FinSequence of L,
Fv be FinSequence of F_Rat;
assume AS1: len F = 0 & len F = len Fv &
for i being Nat st i in dom Fv holds Fv.i = <; F/.i, v ;> ;
F = <*> the carrier of L by AS1;
then Sum F = 0.L by RLVECT_1:43; then
X1: <; Sum F, v ;> = 0.F_Rat by ZMODLAT1:12;
Fv = <*> the carrier of F_Rat by AS1;
hence <; Sum F, v ;> = Sum Fv by X1,RLVECT_1:43;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
let F be FinSequence of L,
Fv be FinSequence of F_Rat;
assume AS2: len F = n+1 & len F = len Fv &
for i being Nat st i in dom Fv holds Fv.i = <; F/.i, v ;>;
reconsider F0 = F| n as FinSequence of L;
n+1 in Seg (n+1) by FINSEQ_1:4;
then
A70: n+1 in dom F by AS2,FINSEQ_1:def 3;
then F.(n+1) in rng F by FUNCT_1:3;
then reconsider af = F.(n+1) as Element of L;
P1: len F0 = n by FINSEQ_1:59,AS2,NAT_1:11; then
P4: dom F0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by AS2,FINSEQ_1:59,NAT_1:11;
A11: F0 = F | dom F0 by P1,FINSEQ_1:def 3;
reconsider Fv0 = Fv| n as FinSequence of F_Rat;
n+1 in Seg (n+1) by FINSEQ_1:4; then
A70F: n+1 in dom Fv by AS2,FINSEQ_1:def 3;
then Fv.(n+1) in rng Fv by FUNCT_1:3;
then reconsider afv = Fv.(n+1) as Element of F_Rat;
P1F: len Fv0 = n by FINSEQ_1:59,AS2,NAT_1:11; then
P4F: dom Fv0 = Seg n by FINSEQ_1:def 3;
A9F: len Fv = (len Fv0) + 1 by AS2,FINSEQ_1:59,NAT_1:11;
P3F: Fv0 = Fv | dom Fv0 by P1F,FINSEQ_1:def 3;
X0: for i being Nat st i in dom Fv0 holds Fv0.i = <; F0/.i, v ;>
proof
let i be Nat;
assume P40: i in dom Fv0;
dom Fv = Seg (n+1) by AS2,FINSEQ_1:def 3;
then dom Fv0 c= dom Fv by P4F,FINSEQ_1:5,NAT_1:11;
then X1: Fv.i = <;F/.i,v ;> by AS2,P40;
i in dom F0 by P40,P4,P1F,FINSEQ_1:def 3;
then F/.i = F0/.i by PARTFUN1:80;
hence thesis by X1,P40,FUNCT_1:47;
end;
reconsider i1 = Sum F0 as Element of L;
X3:F/.(n+1) = af by A70,PARTFUN1:def 6;
thus <; Sum F, v ;> = <; i1+af, v ;> by AS2,A9,A11,RLVECT_1:38
.= <; i1, v ;> + <; af, v ;> by ZMODLAT1:def 3
.= Sum Fv0 + <; af, v ;> by P1,P1F,AS1,X0
.= Sum Fv0 + afv by A70F,AS2,X3
.= Sum Fv by AS2,P3F,A9F,RLVECT_1:38;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
hence thesis;
end;
LMThGM2311:
for r being Element of F_Rat
ex K being Integer st K > 0 & K*r in INT
proof
let r be Element of F_Rat;
consider m,n be Integer such that
P1: n>0 & r = m/n by RAT_1:1;
take n;
thus n> 0 by P1;
n*r = m by P1,XCMPLX_1:87;
hence n*r in INT by INT_1:def 2;
end;
LMThGM231:
for n being Nat, r being FinSequence of F_Rat st len r = n
holds
ex K being Integer st K <> 0 &
for i being Nat st i in Seg n
holds K*r/.i in INT
proof
defpred P[Nat] means
for r being FinSequence of F_Rat st len r = $1
holds
ex K being Integer st K <> 0 &
for i being Nat st i in Seg $1
holds K * r/.i in INT;
P1: P[0]
proof
let r be FinSequence of F_Rat;
assume len r = 0;
set K = 1;
take K;
thus K <> 0;
thus for i being Nat st i in Seg 0 holds K * r/.i in INT;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
let r be FinSequence of F_Rat;
assume AS2: len r = n+1;
reconsider r0 = r| n as FinSequence of F_Rat;
consider L0 be Integer such that
Q0: L0 > 0 & L0*(r/.(n+1)) in INT by LMThGM2311;
P1: len r0 = n by FINSEQ_1:59,AS2,NAT_1:11;
then consider K0 be Integer such that
Q1: K0 <> 0 &
for i being Nat st i in Seg n
holds K0 * r0/.i in INT by AS1;
P4: dom r0 = Seg n by P1,FINSEQ_1:def 3;
set K = L0*K0;
take K;
thus K <> 0 by Q0,Q1;
thus for i being Nat st i in Seg (n+1) holds K * r/.i in INT
proof
let i be Nat;
assume i in Seg (n+1);
then
Q3: 1 <= i & i <= n+1 by FINSEQ_1:1;
per cases;
suppose i <= n; then
Q5: i in Seg n by Q3;
then K0 * r0/.i in INT by Q1;
then reconsider KR = K0 * r/.i as Integer by P4,Q5,PARTFUN1:80;
reconsider iL0 = L0 as Integer;
L0 * KR in INT by INT_1:def 2;
hence K * r/.i in INT;
end;
suppose i > n;
then n+1 <= i by NAT_1:13;
then reconsider LR = L0 * r/.i as Integer by Q0,Q3,XXREAL_0:1;
reconsider iK0 = K0 as Integer;
K0 * LR in INT by INT_1:def 2;
hence K* (r/.i) in INT;
end;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
hence thesis;
end;
theorem LMThGM23:
for n being Nat, r being FinSequence of F_Rat st len r = n
holds
ex K being Integer, Kr being FinSequence of INT.Ring
st K <> 0 & len Kr = n
& for i being Nat st i in dom Kr
holds Kr.i = K * r/.i
proof
let n be Nat, r be FinSequence of F_Rat;
assume len r = n;
then consider K be Integer such that
P1: K <> 0 &
for i being Nat st i in Seg n holds K * r/.i in INT by LMThGM231;
defpred Q[Nat,object] means $2 = K * (r/.$1);
Z510: for i being Nat st i in Seg n
ex x being Element of the carrier of INT.Ring st Q[i,x]
proof
let i be Nat;
assume i in Seg n;
then reconsider x = K*r/.i as Element of INT.Ring by P1;
take x;
thus thesis;
end;
consider Kr be FinSequence of the carrier of INT.Ring such that
Z511: dom Kr = Seg n &
for k being Nat st k in Seg n holds Q[k,Kr.k] from FINSEQ_1:sch 5(Z510) ;
take K, Kr;
thus K <> 0 by P1;
n is Element of NAT by ORDINAL1:def 12;
hence len Kr = n by Z511,FINSEQ_1:def 3;
thus for i being Nat st i in dom Kr holds Kr.i = K * r/.i by Z511;
end;
theorem LMThGM24:
for i, j being Nat
for K being Field
for a, aj being Element of K
for R being Element of i-VectSp_over K
st j in Seg i & aj = R.j holds
(a * R).j = a * aj
proof
let i, j be Nat;
let K be Field;
let a, aj be Element of K;
let R be Element of i-VectSp_over K;
assume AS: j in Seg i & aj = R.j;
P0: the carrier of i-VectSp_over K = i -tuples_on the carrier of K
by MATRIX13:102;
reconsider R0 = R as Element of i -tuples_on the carrier of K
by MATRIX13:102;
P3: a * R = (i -Mult_over K).(a,R) by PRVECT_1:def 5
.= (the multF of K)[;](a,R0) by PRVECT_1:def 4;
a*R in i -tuples_on the carrier of K by P0;
then consider s be Element of (the carrier of K)* such that
P4: a*R = s & len s = i;
dom ((the multF of K)[;](a,R0)) = Seg i by P3,P4,FINSEQ_1:def 3;
hence (a * R).j = a * aj by P3,AS,FUNCOP_1:32;
end;
theorem LMThGM25:
for i, j being Nat
for K being Field
for aj, bj being Element of K
for A,B being Element of i-VectSp_over K
st j in Seg i & aj = A.j & bj = B.j holds
(A+B).j = aj + bj
proof
let i, j be Nat;
let K be Field;
let aj, bj be Element of K;
let A, B be Element of i-VectSp_over K;
assume AS: j in Seg i & aj = A.j & bj = B.j;
P1: the addLoopStr of i-VectSp_over K = i-Group_over K by PRVECT_1:def 5;
P2:i-Group_over K = addLoopStr(# i-tuples_on the carrier of K,
product(the addF of K,i), (i |-> 0.K) qua Element
of i-tuples_on the carrier of K#) by PRVECT_1:def 3;
P0: the carrier of i-VectSp_over K = i-tuples_on the carrier of K
by MATRIX13:102;
reconsider A0 = A, B0 = B as Element of i-tuples_on the carrier of K
by MATRIX13:102;
P3: A+B = (the addF of K).:(A0,B0) by P1,P2,PRVECT_1:def 1;
A+B in i -tuples_on the carrier of K by P0;
then consider s be Element of (the carrier of K)* such that
P4: A+B = s & len s = i;
dom ((the addF of K).:(A0,B0)) = Seg i by P3,P4,FINSEQ_1:def 3;
hence (A+B).j = aj+bj by P3,AS,FUNCOP_1:22;
end;
theorem LMSUM1:
for K being Field, n, i being Nat st i in Seg n holds
for s being FinSequence of n-VectSp_over K holds
ex si being FinSequence of K
st len si = len s & Sum(s).i = Sum(si)
& for k being Nat st k in dom si holds si.k = (s/.k).i
proof
let K be Field, n, i be Nat;
assume AS: i in Seg n;
XP1: the addLoopStr of n-VectSp_over K = n -Group_over K
by PRVECT_1:def 5;
XP2: n -Group_over K = addLoopStr(# n-tuples_on the carrier of K,
product(the addF of K,n), (n |-> 0.K) qua Element
of n-tuples_on the carrier of K#) by PRVECT_1:def 3;
defpred P[Nat] means
for s being FinSequence of n-VectSp_over K st len s = $1 holds
ex si being FinSequence of K
st len si = len s
& Sum(s).i = Sum(si)
& for k being Nat st k in dom si
holds si.k = (s/.k).i;
P1: P[0]
proof
let s be FinSequence of n-VectSp_over K;
assume AS1: len s = 0;
P1: s = <*> (the carrier of n-VectSp_over K) by AS1;
set si = <*> (the carrier of K);
take si;
thus len si = len s by AS1;
( 0.(n-VectSp_over K)).i = 0.K by XP1,XP2,FUNCOP_1:7,AS;
hence Sum(s).i = 0.K by P1,RLVECT_1:43
.= Sum(si) by RLVECT_1:43;
thus for k being Nat st k in dom si holds si.k = (s/.k).i;
end;
P2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume AS1: P[k];
let s be FinSequence of n-VectSp_over K;
assume AS2: len s = k+1;
reconsider s0 = s| k as FinSequence of the carrier of n-VectSp_over K;
k+1 in Seg (k+1) by FINSEQ_1:4;
then
A70: k+1 in dom s by AS2,FINSEQ_1:def 3;
then s.(k+1) in rng s by FUNCT_1:3;
then reconsider sk1 = s.(k+1)
as Element of the carrier of n-VectSp_over K;
P1: len s0 = k by FINSEQ_1:59,AS2,NAT_1:11;
then
P4: dom s0 = Seg k by FINSEQ_1:def 3;
A9: len s = (len s0) + 1 by AS2,FINSEQ_1:59,NAT_1:11;
s0 = s | dom s0 by P1,FINSEQ_1:def 3;
then
P3: Sum s = Sum s0 + sk1 by AS2,A9,RLVECT_1:38;
consider si0 be FinSequence of K such that
P1F: len si0 = len s0
& Sum(s0).i = Sum(si0)
& for k being Nat st k in dom si0
holds si0.k = (s0/.k).i by P1,AS1;
s/.(k+1) in the carrier of n-VectSp_over K;
then s/.(k+1) in
n-tuples_on the carrier of K by MATRIX13:102;
then consider ss be Element of (the carrier of K)* such that
XP4: s/.(k+1) = ss & len ss = n;
XP5: dom ss = Seg n by XP4,FINSEQ_1:def 3;
reconsider ss as FinSequence of the carrier of K;
ss.i in rng ss by XP5,AS,FUNCT_1:3;
then reconsider si0k1 = (s/.(k+1)).i as Element of K by XP4;
P2F: sk1.i = si0k1 by A70,PARTFUN1:def 6;
reconsider si = si0 ^ <* si0k1 *> as FinSequence of K ;
Y0: Sum(si) = Sum(si0) + Sum(<* si0k1 *>) by RLVECT_1:41
.= Sum(si0) + si0k1 by RLVECT_1:44;
Y1: len si = len si0 + len <* si0k1 *> by FINSEQ_1:22
.= len si0 + 1 by FINSEQ_1:39
.= len s by AS2,P1F,FINSEQ_1:59,NAT_1:11;
for j being Nat st j in dom si holds si.j = (s/.j).i
proof
let j be Nat;
assume j in dom si; then
A2: 1 <= j & j <= k+1 by Y1,AS2,FINSEQ_3:25;
per cases;
suppose j <= k; then
Q50: j in Seg k by A2; then
Q5: j in dom si0 by P1,P1F,FINSEQ_1:def 3;
hence si.j = si0.j by FINSEQ_1:def 7
.= (s0/.j).i by P1F,Q5
.= (s/.j).i by P4,Q50,PARTFUN1:80;
end;
suppose j > k;
then k+1 <= j by NAT_1:13;
then j = k+1 by A2,XXREAL_0:1;
hence si.j = (s/.j).i by P1,P1F,FINSEQ_1:42;
end;
end;
hence thesis by Y1,P3,P1F,P2F,AS,Y0,LMThGM25;
end;
for k being Nat holds P[k] from NAT_1:sch 2(P1,P2);
hence thesis;
end;
theorem ThGM2:
for L being non trivial RATional positive-definite Z_Lattice,
b being OrdBasis of L holds
Det GramMatrix(b) <> 0.F_Real
proof
let L be non trivial RATional positive-definite Z_Lattice,
b be OrdBasis of L;
reconsider M = GramMatrix(b) as Matrix of rank(L),F_Rat by ThGM1;
assume Det GramMatrix(b) = 0.F_Real; then
AS: Det M = 0.F_Rat by LmSign1A;
A1: len M = rank L by MATRIX_0:def 2;
A2: the_rank_of M <> rank L by AS,MATRIX13:83;
B3: dom M = Seg (len M) by FINSEQ_1:def 3
.= Seg (rank L) by MATRIX_0:def 2;
B4: dom M = Seg (len b) by B3,ZMATRLIN:49
.= dom b by FINSEQ_1:def 3;
dom b = Seg (rank L) & rank L is Element of NAT
by B3,B4,ORDINAL1:def 12;
then len b = rank L by FINSEQ_1:def 3; then
C4:Indices (BilinearM(InnerProduct(L),b,b))
= [:Seg (rank L),Seg (rank L):] by MATRIX_0:24;
OTO2: M is one-to-one
proof
assume not M is one-to-one;
then consider m1,m2 be object such that
B1: m1 in dom M & m2 in dom M &
M.m1 = M.m2 & m1 <> m2;
B3: dom M = Seg (len GramMatrix(b)) by FINSEQ_1:def 3
.= Seg (rank L) by MATRIX_0:def 2;
B4: dom M = Seg (len b) by B3,ZMATRLIN:49
.= dom b by FINSEQ_1:def 3;
reconsider m1, m2 as Nat by B1;
B5: for n being Nat st n in dom b holds
<; b/.n, b/.m1 ;> = <; b/.n, b/.m2 ;>
proof
let n be Nat such that
C1: n in dom b;
C3: [m1,n] in Indices (BilinearM(InnerProduct(L),b,b))
by C1,B1,B3,B4,C4,ZFMISC_1:87;
C6: [m2,n] in Indices (BilinearM(InnerProduct(L),b,b))
by C4,C1,B1,B3,B4,ZFMISC_1:87;
X1: ex p being FinSequence of F_Real
st p = (BilinearM(InnerProduct(L),b,b)).m1
& (BilinearM(InnerProduct(L),b,b))*(m1,n) = p.n
by MATRIX_0:def 5,C3;
thus <; b/.n, b/.m1 ;> = <; b/.m1, b/.n ;> by ZMODLAT1:def 3
.= (InnerProduct(L)).(b/.m1, b/.n)
.= (BilinearM(InnerProduct(L),b,b))*(m1,n)
by B1,B4,C1,ZMODLAT1:def 32
.= (BilinearM(InnerProduct(L),b,b))*(m2,n) by B1,C6,X1,MATRIX_0:def 5
.= (InnerProduct(L)).(b/.m2, b/.n)
by B1,B4,C1,ZMODLAT1:def 32
.= <; b/.m2, b/.n ;>
.= <; b/.n, b/.m2 ;> by ZMODLAT1:def 3;
end;
b.m1 = b/.m1 by B1,B4,PARTFUN1:def 6
.= b/.m2 by B5,ZL2ThSc1
.= b.m2 by B1,B4,PARTFUN1:def 6;
then not b is one-to-one by B1,B4;
hence contradiction by ZMATRLIN:def 5;
end; then
AA1: lines M is linearly-dependent by A2,MATRIX13:121;
lines M c= the carrier of (rank L)-VectSp_over F_Rat;
then reconsider M1 = M as FinSequence of (rank L)-VectSp_over F_Rat
by FINSEQ_1:def 4;
consider r be FinSequence of F_Rat,
rM1 be FinSequence of (rank L)-VectSp_over F_Rat such that
Z1:len r = (rank L) & len rM1 = (rank L) &
(for i being Nat st i in dom rM1
holds rM1.i = r/.i * M1/.i) &
Sum (rM1) = 0.((rank L)-VectSp_over F_Rat) &
r <> Seg (len r) --> 0.F_Rat by A1,AA1,OTO2,LMBASE2;
consider K be Integer,Kr be FinSequence of INT.Ring such that
Z2: K <> 0 & len Kr = (rank L)
& for i being Nat st i in dom Kr holds Kr.i = K*r/.i by Z1,LMThGM23;
reconsider K1 = K as Element of F_Rat by INT_1:def 2,NUMBERS:14;
defpred P[Nat,object] means
ex rM1i being Element of (rank L)-VectSp_over F_Rat
st rM1i = rM1.$1 & $2 = K1 * rM1i;
KRM10: for k being Nat st k in Seg (rank L)
ex x being Element of the carrier of (rank L)-VectSp_over F_Rat st P[k,x]
proof
let k be Nat;
assume KRM12: k in Seg (rank L);
dom rM1 = Seg (rank L) by Z1,FINSEQ_1:def 3;
then rM1.k = rM1/.k by KRM12,PARTFUN1:def 6;
then reconsider rM1i = rM1.k as Element of (rank L)-VectSp_over F_Rat;
K1 * rM1i is Element of the carrier of (rank L)-VectSp_over F_Rat;
hence thesis;
end;
consider KrM1 be FinSequence of the carrier of (rank L)-VectSp_over F_Rat
such that
KRM11: dom KrM1 = Seg (rank L) &
for k being Nat st k in Seg (rank L) holds P[k,KrM1.k]
from FINSEQ_1:sch 5(KRM10);
KRM1Z: rank L is Element of NAT by ORDINAL1:def 12; then
KRM1: len KrM1 = rank L by FINSEQ_1:def 3,KRM11;
Z3: for i being Nat st i in dom KrM1 holds
ex M1i being Element of (rank L)-VectSp_over F_Rat,
Kri being Element of F_Rat
st M1i = M1.i & Kri = Kr.i & KrM1.i = Kri * M1i
proof
let i be Nat;
assume Z300: i in dom KrM1;
then consider rM1i be Element of (rank L)-VectSp_over F_Rat such that
Z301: rM1i = rM1.i & KrM1.i = K1 * rM1i by KRM11;
Z303: i in dom rM1 by Z1,Z300,KRM11,FINSEQ_1:def 3;
Z305: i in dom Kr by Z2,Z300,KRM11,FINSEQ_1:def 3;
Z307: dom M1 = Seg (rank L) by A1,FINSEQ_1:def 3;
then M1/.i = M1.i by KRM11,Z300,PARTFUN1:def 6;
then reconsider M1i = M1.i as Element of (rank L)-VectSp_over F_Rat;
Kr.i = Kr/.i by PARTFUN1:def 6,Z305;
then reconsider Kri = Kr.i as Element of F_Rat by NUMBERS:14;
take M1i,Kri;
thus M1i = M1.i & Kri = Kr.i;
thus KrM1.i = K1 * (r/.i * M1/.i) by Z1,Z301,Z303
.= K1 * (r/.i * M1i) by Z300,Z307,KRM11,PARTFUN1:def 6
.= (K1*r/.i) * M1i by VECTSP_1:def 16
.= Kri * M1i by Z2,Z305;
end;
for k being Nat for v being Element of (rank L)-VectSp_over F_Rat
st k in dom KrM1 & v = rM1.k holds KrM1.k = K1 * v
proof
let k be Nat;
let v be Element of (rank L)-VectSp_over F_Rat;
assume Z41: k in dom KrM1 & v = rM1.k;
then consider rM1i be Element of (rank L)-VectSp_over F_Rat such that
Z42: rM1i = rM1.k & KrM1.k = K1 * rM1i by KRM11;
thus thesis by Z42,Z41;
end;
then
Z4A: Sum (KrM1) = K1*Sum(rM1) by KRM1,Z1,RLVECT_2:66
.= 0.((rank L)-VectSp_over F_Rat) by Z1,VECTSP_1:15;
Z4B: Kr <> Seg (len Kr) --> 0.(INT.Ring)
proof
set f = Seg (len Kr) --> 0.(INT.Ring);
set g = Seg (len r) --> 0.F_Rat;
dom r = Seg len r by FINSEQ_1:def 3
.= dom g by FUNCT_2:def 1;
then consider i be object such that
R1: i in dom r & r.i <> g.i by Z1;
R2: i in Seg len r by FINSEQ_1:def 3,R1;
reconsider i as Nat by R1;
r.i <> 0.F_Rat by R1,R2,FUNCOP_1:7; then
R3: r/.i <> 0.(INT.Ring) by R1,PARTFUN1:def 6;
R9: i in Seg len Kr by R1,Z1,Z2,FINSEQ_1:def 3;
then i in dom Kr by FINSEQ_1:def 3;
then Kr.i = K1 * r/.i by Z2;
hence thesis by R3,R9,Z2,FUNCOP_1:7;
end;
set SKrM1 = Sum (KrM1);
Z5: for n being Nat st n in dom b
holds SKrM1.n = 0.(INT.Ring)
proof
let n be Nat;
assume Z55: n in dom b;
Z51: the addLoopStr of (rank L)-VectSp_over F_Rat
= (rank L) -Group_over F_Rat by PRVECT_1:def 5;
(rank L) -Group_over F_Rat
= addLoopStr(# (rank L)-tuples_on the carrier of F_Rat,
product(the addF of F_Rat,(rank L)), ((rank L) |-> 0.F_Rat)
qua Element of (rank L)-tuples_on the carrier of F_Rat #)
by PRVECT_1:def 3;
hence SKrM1.n = 0.(INT.Ring) by B3,B4,Z4A,Z51,Z55,FUNCOP_1:7;
end;
defpred Q[Nat,object] means $2 = (Kr/.$1) * (b/.$1);
Z510: for k being Nat st k in Seg (rank L)
ex x being Element of the carrier of L st Q[k,x];
consider Krb be FinSequence of the carrier of L such that
Z511: dom Krb = Seg (rank L) &
for k being Nat st k in Seg (rank L) holds Q[k,Krb.k]
from FINSEQ_1:sch 5(Z510);
Z51Z: rank L is Element of NAT by ORDINAL1:def 12;
then
Z51: len Krb = rank L by FINSEQ_1:def 3,Z511;
Z6: for n be Nat st n in dom b holds SKrM1.n = <; Sum (Krb), b/.n ;>
proof
let n be Nat;
assume Z61: n in dom b;
then consider SKrM1n be FinSequence of F_Rat such that
Z62: len SKrM1n = len KrM1
& SKrM1.n = Sum(SKrM1n)
& for k being Nat st k in dom SKrM1n
holds SKrM1n.k = (KrM1/.k).n by B3,B4,LMSUM1;
Z63: len Krb = rank L by Z511,Z51Z,FINSEQ_1:def 3
.= len SKrM1n by Z62,KRM11,KRM1Z,FINSEQ_1:def 3;
for k being Nat st k in dom SKrM1n holds SKrM1n.k = <; Krb/.k, b/.n ;>
proof
let k be Nat;
assume X0: k in dom SKrM1n;
then XX11: k in Seg len Krb by Z63,FINSEQ_1:def 3; then
XX1: k in dom Krb by FINSEQ_1:def 3; then
Z65: Krb/.k = Krb.k by PARTFUN1:def 6
.= Kr/.k * b/.k by Z511,XX1;
KrM1/.k in the carrier of (rank L)-VectSp_over F_Rat;
then KrM1/.k in (rank L) -tuples_on the carrier of F_Rat
by MATRIX13:102;
then consider KrM1k be Element of (the carrier of F_Rat)* such that
T660: KrM1/.k = KrM1k & len KrM1k = rank L;
T66: KrM1k = KrM1.k & SKrM1n.k = KrM1k.n
by KRM11,XX1,Z511,T660,Z62,X0,PARTFUN1:def 6;
Z70: k in dom b by XX11,Z511,B3,B4,FINSEQ_1:def 3;
k in dom KrM1 by KRM1,KRM11,X0,Z62,FINSEQ_1:def 3;
then consider M1k be Element of (rank L)-VectSp_over F_Rat,
Krk be Element of F_Rat such that
Z31: M1k = M1.k & Krk = Kr.k & KrM1.k = Krk * M1k by Z3;
E10: [k,n] in Indices M by Z70,Z61,B3,B4,C4,ZFMISC_1:87;
then consider p be FinSequence of F_Rat such that
W34: p = M.k & M*(k,n) = p.n by MATRIX_0:def 5;
reconsider MMkn = M*(k,n) as Element of F_Rat;
E3: k in dom Kr by Z2,Z70,B3,B4,FINSEQ_1:def 3;
Z90: KrM1k.n= Krk * (M*(k,n)) by T66,W34,Z31,Z61,B3,B4,LMThGM24
.= Kr/.k * (M*(k,n)) by Z31,E3,PARTFUN1:def 6;
<; Krb/.k, b/.n ;> = <; b/.n, (Kr/.k) * (b/.k) ;>
by Z65,ZMODLAT1:def 3
.= (Kr/.k) * <; b/.n, b/.k ;> by ZMODLAT1:9
.= Kr/.k * <; b/.k, b/.n ;> by ZMODLAT1:def 3
.= Kr/.k * (InnerProduct(L)).(b/.k, b/.n)
.= Kr/.k * ((BilinearM(InnerProduct(L),b,b))*(k,n))
by ZMODLAT1:def 32,Z61,Z70
.= Kr/.k * (M*(k,n)) by E10,ZMATRLIN:1
.= SKrM1n.k by T660,Z62,X0,Z90;
hence thesis;
end;
hence thesis by Z62,Z63,LMThGM21;
end;
for n being Nat st n in dom b
holds <; 0.L, b/.n ;> = <; Sum (Krb), b/.n ;>
proof
let n be Nat;
assume Z71: n in dom b;
thus <; 0.L, b/.n ;> = 0.(INT.Ring) by ZMODLAT1:12
.= SKrM1.n by Z5,Z71
.= <; Sum (Krb), b/.n ;> by Z6,Z71;
end; then
Z8: Sum (Krb) = 0.L by ZL2ThSc1X;
Z9: b is one-to-one by ZMATRLIN:def 5;
len Kr = len b by B3,B4,Z2,FINSEQ_1:def 3;
then rng b is linearly-dependent by Z51,Z511,Z4B,Z2,Z8,Z9,LMBASE2;
then not rng b is base by VECTSP_7:def 3;
hence contradiction by ZMATRLIN:def 5;
end;
registration
let L be non trivial RATional positive-definite Z_Lattice;
let b be OrdBasis of L;
cluster GramMatrix(b) -> invertible;
correctness
proof
Det GramMatrix(b) <> 0.F_Real by ThGM2;
then Det GramMatrix(b) is non zero by STRUCT_0:def 12;
then Det GramMatrix(b) is unital;
hence thesis by LAPLACE:34;
end;
end;