:: Embedded Lattice and Properties of {G}ram Matrix :: by Yuichi Futa and Yasunari Shidama :: :: Received March 17, 2017 :: Copyright (c) 2017-2019 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 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 BINOP_2, UPROOTS, REALSET1, ALGSTR_1, ZMODUL01, EC_PF_1, ZMODUL04, ZMODUL07, ZMODLAT1, ZMODUL08, MATRIX_6, LAPLACE, MATRIX13, RELSET_1, FVSUM_1; 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, GAUSSINT, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL05, ZMODUL06, MATRIX_0, ZMODLAT1, ZMODUL08, PRVECT_1, MATRIX13; 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, ZMODUL04, PARTFUN1; 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; 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 by VECTSP_1:def 17; y = yy by VECTSP_1:def 17; then C1: b <> 0 & yy = b * y by VECTSP_1:def 17; 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 by VECTSP_1:def 17; B4: x2 = a * xx2 by VECTSP_1:def 17; 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,VECTSP_1:def 17; 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; hence thesis by LAPLACE:34; end; end;