:: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation :: by Krzysztof Treyderowski and Christoph Schwarzweller :: :: Received October 12, 2006 :: Copyright (c) 2006-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 NUMBERS, INT_1, XXREAL_0, CARD_1, ARYTM_1, ARYTM_3, SUBSET_1, VECTSP_1, VECTSP_2, STRUCT_0, XBOOLE_0, ALGSTR_0, SUPINF_2, NEWTON, RELAT_1, GROUP_1, BINOP_1, RLVECT_1, MESFUNC1, LATTICES, ALGSTR_1, FINSEQ_1, PARTFUN1, CARD_3, NAT_1, FUNCT_1, ORDINAL4, FINSEQ_2, TARSKI, MATRIX_1, TREES_1, INCSP_1, FVSUM_1, RVSUM_1, ZFMISC_1, ALGSEQ_1, POLYNOM1, COMPLEX1, MCART_1, POLYNOM2, POLYNOM3, POLYNOM8; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, VECTSP_2, BINOP_1, BINOM, ALGSTR_1, PARTFUN1, FINSEQ_1, FINSEQ_2, INT_1, NAT_1, NAT_D, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FVSUM_1, ALGSEQ_1, LOPBAN_3, POLYNOM5, POLYNOM3, MATRIX_0, MATRIX_1, MATRIX_3, POLYNOM4, XTUPLE_0, MCART_1, INT_2; constructors REAL_1, NAT_D, VECTSP_2, ALGSTR_2, TOPREAL1, MATRIX_3, POLYNOM4, POLYNOM5, BINOM, RELSET_1, FVSUM_1, XTUPLE_0, MATRIX_1, ALGSEQ_1, BINOP_1, LOPBAN_3; registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, STRUCT_0, VECTSP_1, ALGSTR_1, GCD_1, POLYNOM3, CARD_1, XTUPLE_0; requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM; equalities VECTSP_1, RLVECT_1, BINOM, FINSEQ_1, MATRIX_0, POLYNOM3, ALGSTR_0; expansions VECTSP_1; theorems FVSUM_1, GROUP_1, BINOM, VECTSP_1, ALGSEQ_1, NAT_1, FINSEQ_4, INT_1, FUNCT_2, XREAL_1, VECTSP_2, ALGSTR_1, MATRIX_0, FUNCT_1, MATRIX_3, FINSEQ_1, ZFMISC_1, COMPLEX1, RLVECT_1, POLYNOM4, TARSKI, MCART_1, FINSEQ_2, POLYNOM1, ABSVALUE, POLYNOM3, POLYNOM5, FINSEQ_3, ORDINAL1, XXREAL_0, FUNCOP_1, PARTFUN1, XREAL_0, XTUPLE_0, MATRIX_1, LOPBAN_3; schemes NAT_1, FUNCT_2, MATRIX_0, FINSEQ_1, INT_1; begin :: Preliminaries Lm1: for j being Integer holds j >= 0 or j = - 1 or j < - 1 proof let j be Integer; per cases; suppose j >= 0; hence thesis; end; suppose A1: j < 0; then reconsider n = - j as Element of NAT by INT_1:3; n <> -0 by A1; then n >= 1 by NAT_1:14; then n > 1 or n = 1 by XXREAL_0:1; then - 1 > - (- j) or - 1 = j by XREAL_1:24; hence thesis; end; end; Lm2: for j being Integer holds j >= 1 or j = 0 or j < 0 proof let j be Integer; j < 0 or j is Element of NAT & (j <> 0 or j = 0) by INT_1:3; hence thesis by NAT_1:14; end; theorem Th1: for n being Nat, L being well-unital domRing-like non degenerated non empty doubleLoopStr, x being Element of L st x <> 0.L holds x |^ n <> 0.L proof let n be Nat; let L be well-unital domRing-like non degenerated non empty doubleLoopStr, x being Element of L; defpred P[Nat] means x |^ $1 <> 0.L; assume A1: x <> 0.L; A2: now let n be Nat; assume P[n]; then (x |^ n) * x <> 0.L by A1,VECTSP_2:def 1; hence P[n+1] by GROUP_1:def 7; end; x |^ 0 = 1_L by BINOM:8; then A3: P[0]; for n being Nat holds P[n] from NAT_1:sch 2(A3,A2); hence thesis; end; registration cluster almost_left_invertible -> domRing-like for associative well-unital add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr; coherence proof let L be associative well-unital add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr; assume A1: L is almost_left_invertible; for x,y being Element of L holds x*y = 0.L implies x = 0.L or y = 0.L proof let x,y be Element of L; assume A2: x*y = 0.L; now assume that A3: x <> 0.L and A4: y <> 0.L; consider xx being Element of L such that A5: xx * x = 1.L by A1,A3; y = 1.L * y .= xx * (x * y) by A5,GROUP_1:def 3 .= 0.L by A2; hence contradiction by A4; end; hence thesis; end; hence thesis by VECTSP_2:def 1; end; end; theorem Th2: for L being add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr, x,y being Element of L st x <> 0.L & y <> 0.L holds (x * y)" = x" * y" proof let L be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr; let x,y be Element of L; assume that A1: x <> 0.L and A2: y <> 0.L; A3: (x" * y") * (x * y) = x" * y" * y * x by GROUP_1:def 3 .= x" * (y" * y) * x by GROUP_1:def 3 .= x" * 1.L * x by A2,VECTSP_1:def 10 .= x" * x .= 1.L by A1,VECTSP_1:def 10; x * y <> 0.L by A1,A2,VECTSP_1:12; hence thesis by A3,VECTSP_1:def 10; end; theorem Th3: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, z,z1 being Element of L holds z <> 0.L implies z1 = (z1 * z) / z proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, z,z1 be Element of L; assume A1: z <> 0.L; thus (z1 * z) / z = z1 * (z * z") by GROUP_1:def 3 .= z1 * 1.L by A1,VECTSP_1:def 10 .= z1; end; theorem Th4: for L being left_zeroed right_zeroed add-associative right_complementable non empty doubleLoopStr, m being Element of NAT, s being FinSequence of L st len s = m & for k being Element of NAT st 1 <= k & k <= m holds s/.k = 1.L holds Sum s = m * 1.L proof let L be left_zeroed right_zeroed add-associative right_complementable non empty doubleLoopStr, m be Element of NAT, s be FinSequence of L; assume A1: len s = m & for k being Element of NAT st 1 <= k & k <= m holds s/.k = 1.L; defpred P[Nat] means for s being FinSequence of L st len s = $1 & for k being Element of NAT st 1 <= k & k <= $1 holds s/.k = 1.L holds Sum s = $1 * 1.L; A2: for l being Nat st P[l] holds P[l+1] proof let l be Nat; assume A3: for g being FinSequence of L st (len g = l & for k being Element of NAT st 1 <= k & k <= l holds g/.k = 1.L) holds Sum g = l * 1.L; for s being FinSequence of L st len s = l+1 & for k being Element of NAT st 1 <= k & k <= l+1 holds s/.k = 1.L holds Sum s = (l+1) * 1.L proof ex G being FinSequence of L st (dom G = Seg l & for k being Nat st k in Seg l holds G.k = 1.L) proof defpred P[Nat,set] means $2 = 1.L; A4: for n being Nat st n in Seg l holds ex x being Element of L st P[ n,x]; ex G be FinSequence of L st dom G = Seg l & for nn be Nat st nn in Seg l holds P[nn,G.nn] from FINSEQ_1:sch 5(A4); hence thesis; end; then consider g being FinSequence of L such that A5: dom g = Seg l and A6: for k being Nat st k in Seg l holds g.k = 1.L; A7: l in NAT by ORDINAL1:def 12; then A8: len g = l by A5,FINSEQ_1:def 3; A9: for k being Nat st 1 <= k & k <= l holds g/.k = 1.L proof let k be Nat; assume A10: 1 <= k & k <= l; then A11: k in dom g by A5; k in Seg l by A10; then 1.L = g.k by A6 .= g/.k by A11,PARTFUN1:def 6; hence thesis; end; then A12: for k being Element of NAT st 1 <= k & k <= l holds g/.k = 1.L; dom <*1.L*> = Seg 1 by FINSEQ_1:def 8; then A13: len <*1.L*> = 1 by FINSEQ_1:def 3; let s be FinSequence of L; assume that A14: len s = l+1 and A15: for k being Element of NAT st 1 <= k & k <= l+1 holds s/.k = 1. L; A16: dom s = Seg (l + 1) by A14,FINSEQ_1:def 3; A17: for k being Nat st k in dom s holds s.k = (g^<*1.L*>).k proof A18: dom s = Seg(l + 1) by A14,FINSEQ_1:def 3; let k be Nat; A19: k in NAT by ORDINAL1:def 12; assume A20: k in dom s; per cases by A20,A18,FINSEQ_1:1; suppose A21: 1 <= k & k <= l; then A22: k <= l+1 by NAT_1:12; A23: k in dom g by A5,A21; then (g^<*1.L*>).k = g.k by FINSEQ_1:def 7 .= g/.k by A23,PARTFUN1:def 6 .= 1.L by A9,A21 .= s/.k by A15,A19,A21,A22 .= s.k by A20,PARTFUN1:def 6; hence thesis; end; suppose A24: l < k & k <= l+1; then k - k <= (l+1) - k by XREAL_1:9; then reconsider ii = (l+1) - k + 1 as Element of NAT by INT_1:3; l+1 <= k by A24,NAT_1:13; then dom <*1.L*> = Seg 1 & ii = k - k + 1 by A24,FINSEQ_1:def 8 ,XXREAL_0:1; then A25: ii in dom <*1.L*>; l + 0 < k + l by A24,XREAL_1:8; then l+1 <= k+l by NAT_1:13; then A26: (l+1)-l <= (k+l)-l by XREAL_1:9; l+1 <= k by A24,NAT_1:13; then A27: ii = k - k + 1 by A24,XXREAL_0:1; then (g^<*1.L*>).k = (g^<*1.L*>).(len g + ii) by A5,FINSEQ_1:def 3,A7 .= <*1.L*>.1 by A25,A27,FINSEQ_1:def 7 .= 1.L by FINSEQ_1:def 8 .= s/.k by A15,A19,A24,A26 .= s.k by A20,PARTFUN1:def 6; hence thesis; end; end; dom (g^<*1.L*>) = Seg (len g + len <*1.L*>) by FINSEQ_1:def 7 .= dom s by A5,A13,A16,FINSEQ_1:def 3,A7; then s = g^<*1.L*> by A17,FINSEQ_1:13; then Sum s = Sum g + 1.L by FVSUM_1:71 .= (l*1.L) + 1.L by A3,A8,A12 .= (l*1.L) + (1*1.L) by BINOM:13 .= (l+1) * 1.L by BINOM:15; hence thesis; end; hence thesis; end; for s being FinSequence of L st len s = 0 & for k being Element of NAT st 1 <= k & k <= 0 holds s/.k = 1.L holds Sum s = 0 * 1.L proof let s be FinSequence of L; assume that A28: len s = 0 and for k being Element of NAT st 1 <= k & k <= 0 holds s/.k = 1.L; A29: <*>the carrier of L is Element of 0-tuples_on the carrier of L by FINSEQ_2:131; s = {} by A28; then Sum s = Sum (<*>(the carrier of L)) .= 0.L by A29,FVSUM_1:74 .= 0 * 1.L by BINOM:12; hence thesis; end; then A30: P[0]; for l being Nat holds P[l] from NAT_1:sch 2(A30,A2); hence thesis by A1; end; theorem Th5: for L being add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, s being FinSequence of L, q being Element of L st q <> 1. L & for i being Nat st 1 <= i & i <= len s holds s.i = q |^ (i-'1) holds Sum s = (1.L - q |^ (len s)) / (1.L - q) proof let L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, s be FinSequence of L, q be Element of L; assume A1: q <> 1.L & for i being Nat st 1 <= i & i <= len s holds s.i = q |^ ( i-'1); defpred P[Nat] means for s being FinSequence of L st len s = $1 for q being Element of L st q <> 1.L & for i being Nat st 1 <= i & i <= len s holds s.i = q |^ (i-'1) holds Sum s = (1.L - q |^ (len s)) / (1.L - q); A2: for k being Nat st P[k] holds P[k + 1] proof let k be Nat; assume A3: P[k]; now let s be FinSequence of L; set f = s| (Seg k); reconsider f as FinSequence by FINSEQ_1:15; assume A4: len s = k+1; then A5: 1 <= len s by NAT_1:12; then len s in dom s by FINSEQ_3:25; then A6: s/.(len s) = s.(len s) by PARTFUN1:def 6; A7: k <= len s by A4,NAT_1:13; then A8: len f = k by FINSEQ_1:17; now let u be object; assume u in rng f; then consider x being object such that A9: x in dom f and A10: f.x = u by FUNCT_1:def 3; reconsider x9 = x as Element of NAT by A9; x9 <= len f by A9,FINSEQ_3:25; then A11: x9 <= len s by A4,A8,NAT_1:12; 1 <= x9 by A9,FINSEQ_3:25; then A12: x in dom s by A11,FINSEQ_3:25; f.x = s.x by A9,FUNCT_1:47 .= s/.x by A12,PARTFUN1:def 6; hence u in the carrier of L by A10; end; then rng f c= the carrier of L by TARSKI:def 3; then reconsider f as FinSequence of L by FINSEQ_1:def 4; A13: len s = len f + 1 by A4,A7,FINSEQ_1:17; let q be Element of L; assume that A14: q <> 1.L and A15: for i being Nat st 1 <= i & i <= len s holds s.i = q |^ (i-'1); A16: now assume 1.L - q = 0.L; then (1.L - q) + q = q by ALGSTR_1:def 2; then 1.L + (-q + q) = q by RLVECT_1:def 3; then 1.L + 0.L = q by RLVECT_1:5; hence contradiction by A14,RLVECT_1:def 4; end; len s - 1 >= 1 - 1 by A5,XREAL_1:9; then A17: len(s) -' 1 = len(s) - 1 by XREAL_0:def 2 .= len f + 1 - 1 by A4,A7,FINSEQ_1:17; A18: now let i be Nat; assume that A19: 1 <= i and A20: i <= len f; A21: i <= len s by A4,A8,A20,NAT_1:13; i in dom f by A19,A20,FINSEQ_3:25; hence f.i = s.i by FUNCT_1:47 .= q |^ (i-'1) by A15,A19,A21; end; f = s| (dom f) by A7,FINSEQ_1:17; hence Sum(s) = Sum(f) + s/.(len s) by A13,A6,RLVECT_1:38 .= (1.L - q |^ (len f)) / (1.L - q) + s/.(len s) by A3,A14,A7,A18, FINSEQ_1:17 .= (1.L - q |^ (len f)) / (1.L - q) + q |^ (len f) by A15,A5,A17,A6 .= (1.L - q |^ (len f)) / (1.L - q) + (q |^ (len f) * (1.L - q)) / ( 1.L - q) by A16,Th3 .= ((1.L - q |^ (len f)) + (q |^ (len f) * (1.L - q))) /(1.L - q) by VECTSP_1:def 3 .= ((1.L - q |^ (len f)) + ((q |^ (len f) * 1.L) + (q |^ (len f) * ( -q)))) / (1.L - q) by VECTSP_1:def 2 .= ((1.L - q |^ (len f)) + (q |^ (len f) + (q |^ (len f) * (-q)))) / (1.L - q) .= (1.L + (-q |^ (len f) + (q |^ (len f) + (q |^ (len f) * (-q))))) / (1.L - q) by RLVECT_1:def 3 .= (1.L + ((-q |^ (len f) + q |^ (len f)) + (q |^ (len f) * (-q)))) / (1.L - q) by RLVECT_1:def 3 .= (1.L + (0.L + (q |^ (len f) * (-q)))) / (1.L - q) by RLVECT_1:5 .= (1.L + (q |^ (len f) * (-q))) / (1.L - q) by ALGSTR_1:def 2 .= (1.L + -((q |^ (len f) * q))) / (1.L - q) by VECTSP_1:8 .= (1.L - q |^ (len s)) / (1.L - q) by A13,GROUP_1:def 7; end; hence thesis; end; now let s be FinSequence of L; assume len s = 0; then A22: s = <*>(the carrier of L); let q be Element of L; assume that q <> 1.L and for i being Nat st 1 <= i & i <= len s holds s.i = q |^ (i-'1); thus (1.L - q |^ 0) / (1.L - q) = (1.L - 1_L) / (1.L - q) by BINOM:8 .= 0.L / (1.L - q) by RLVECT_1:15 .= 0.L .= Sum s by A22,RLVECT_1:43; end; then A23: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A23,A2); hence thesis by A1; end; definition let L be well-unital non empty doubleLoopStr, m be Element of NAT; func emb(m,L) -> Element of L equals m * 1.L; coherence; end; theorem Th6: for L being Field, m,n,k being Element of NAT st m > 0 & n > 0 for M1 being Matrix of m,n,L, M2 being Matrix of n,k,L holds (emb(m,L) * M1) * M2 = emb(m,L) * (M1 * M2) proof let L be Field; let m,n,k be Element of NAT; assume that A1: m > 0 and A2: n > 0; let M1 be Matrix of m,n,L; let M2 be Matrix of n,k,L; A3: width M1 = n by A1,MATRIX_0:23 .= len M2 by A2,MATRIX_0:23; A4: width (emb(m,L) * M1) = width M1 by MATRIX_3:def 5 .= n by A1,MATRIX_0:23 .= len M2 by A2,MATRIX_0:23; A5: for i,j being Nat st [i,j] in Indices ((emb(m,L) * M1) * M2) holds ((emb (m,L) * M1) * M2)*(i,j) = (emb(m,L) * (M1 * M2))*(i,j) proof let i,j be Nat; A6: len M1 = len (M1 * M2) by A3,MATRIX_3:def 4; len((emb(m,L) * M1) * M2) = len(emb(m,L) * M1) by A4,MATRIX_3:def 4 .= len M1 by MATRIX_3:def 5; then A7: dom((emb(m,L) * M1) * M2) = Seg len M1 by FINSEQ_1:def 3 .= dom (M1 * M2) by A6,FINSEQ_1:def 3; Seg (len (emb(m,L) * Line(M1,i))) = dom (emb(m,L) * Line(M1,i)) by FINSEQ_1:def 3 .= dom (Line(M1,i)) by POLYNOM1:def 1 .= Seg (len Line(M1,i)) by FINSEQ_1:def 3; then A8: len (emb(m,L) * Line(M1,i)) = len Line(M1,i) by FINSEQ_1:6 .= width M1 by MATRIX_0:def 7; A9: len Line(M1,i) = len M2 by A3,MATRIX_0:def 7 .= len Col(M2,j) by MATRIX_0:def 8; assume A10: [i,j] in Indices ((emb(m,L) * M1) * M2); then A11: ((emb(m,L) * M1) * M2)*(i,j) = Line(emb(m,L) * M1,i) "*" Col(M2,j) by A4, MATRIX_3:def 4 .= Sum(mlt(Line(emb(m,L) * M1,i),Col(M2,j))) by FVSUM_1:def 9; len Line(emb(m,L) * M1,i) = width (emb(m,L) * M1) by MATRIX_0:def 7 .= width M1 by MATRIX_3:def 5; then dom Line(emb(m,L)*M1,i) = Seg(width M1) by FINSEQ_1:def 3; then A12: dom Line(emb(m,L) * M1,i) = dom (emb(m,L) * Line(M1,i)) by A8, FINSEQ_1:def 3; for k being Nat st k in dom Line(emb(m,L) * M1,i) holds (Line(emb(m,L ) * M1,i)).k = (emb(m,L) * Line(M1,i)).k proof len (M1 * M2) = len M1 by A3,MATRIX_3:def 4 .= m by A1,MATRIX_0:23; then A13: dom (M1 * M2) = Seg m by FINSEQ_1:def 3; A14: Indices M1 = [:Seg m, Seg n:] & i in dom (M1 * M2) by A1,A10,A7, MATRIX_0:23,ZFMISC_1:87; let k be Nat; assume A15: k in dom Line(emb(m,L) * M1,i); A16: len Line(emb(m,L) * M1,i) = width (emb(m,L) * M1) by MATRIX_0:def 7 .= width M1 by MATRIX_3:def 5; then A17: k in Seg width M1 by A15,FINSEQ_1:def 3; len Line(M1,i) = width M1 by MATRIX_0:def 7; then k in dom Line(M1,i) by A17,FINSEQ_1:def 3; then (Line(M1,i)).k = (Line(M1,i))/.k by PARTFUN1:def 6; then reconsider a = Line(M1,i).k as Element of L; A18: a = M1*(i,k) by A17,MATRIX_0:def 7; k in Seg n by A1,A17,MATRIX_0:23; then [i,k] in Indices M1 by A14,A13,ZFMISC_1:87; then A19: emb(m,L) * a = (emb(m,L) * M1)*(i,k) by A18,MATRIX_3:def 5; dom Line(emb(m,L)*M1,i) = Seg(width M1) by A16,FINSEQ_1:def 3; then A20: k in Seg width (emb(m,L) * M1) by A15,MATRIX_3:def 5; (emb(m,L) * Line(M1,i)).k = emb(m,L) * a by A12,A15,FVSUM_1:50; hence thesis by A20,A19,MATRIX_0:def 7; end; then A21: Line(emb(m,L) * M1,i) = emb(m,L) * Line(M1,i) by A12,FINSEQ_1:13; Seg (len (emb(m,L) * Line(M1,i))) = dom (emb(m,L) * Line(M1,i)) by FINSEQ_1:def 3 .= dom (Line(M1,i)) by POLYNOM1:def 1 .= Seg (len (Line(M1,i))) by FINSEQ_1:def 3; then A22: len (emb(m,L) * Line(M1,i)) = len (Line(M1,i)) by FINSEQ_1:6 .= len M2 by A3,MATRIX_0:def 7 .= len Col(M2,j) by MATRIX_0:def 8; A23: dom (emb(m,L) * Line(M1,i)) = Seg len (emb(m,L) * Line(M1,i)) by FINSEQ_1:def 3 .= Seg (len (mlt(emb(m,L) * Line(M1,i), Col(M2,j)))) by A22,MATRIX_3:6 .= dom(mlt(emb(m,L)*Line(M1,i),Col(M2,j))) by FINSEQ_1:def 3; A24: dom(emb(m,L) * Line(M1,i)) = dom(Line(M1,i)) by POLYNOM1:def 1 .= Seg(len (Line(M1,i))) by FINSEQ_1:def 3 .= Seg(len (mlt(Line(M1,i), Col(M2,j)))) by A9,MATRIX_3:6 .= dom(mlt(Line(M1,i), Col(M2,j))) by FINSEQ_1:def 3; then A25: dom mlt(emb(m,L) * Line(M1,i), Col(M2,j)) = dom (emb(m,L)*mlt(Line(M1 ,i), Col(M2,j))) by A23,POLYNOM1:def 1; for k being Nat st k in dom mlt(emb(m,L)*Line(M1,i),Col(M2,j)) holds (mlt(emb(m,L) * Line(M1,i), Col(M2,j))).k = (emb(m,L)*mlt(Line(M1,i), Col(M2,j) )).k proof A26: len Line(M1,i) = len M2 by A3,MATRIX_0:def 7 .= len Col(M2,j) by MATRIX_0:def 8; A27: len Line(M1,i) = width M1 by MATRIX_0:def 7; let k be Nat; assume A28: k in dom mlt(emb(m,L)*Line(M1,i),Col(M2,j)); dom (Line(M1,i)) = Seg len (Line(M1,i)) by FINSEQ_1:def 3 .= Seg(len (mlt(Line(M1,i), Col(M2,j)))) by A26,MATRIX_3:6 .= dom mlt(Line(M1,i), Col(M2,j)) by FINSEQ_1:def 3; then A29: k in Seg width M1 by A23,A24,A28,A27,FINSEQ_1:def 3; then k in dom M2 by A3,FINSEQ_1:def 3; then A30: Col(M2, j).k = M2*(k,j) by MATRIX_0:def 8; Line(M1, i).k = M1*(i,k) by A29,MATRIX_0:def 7; then reconsider c = (Col(M2,j)).k, d = (Line(M1,i)).k as Element of L by A30; (mlt(Line(M1,i), Col(M2,j))).k = c * d by A23,A24,A28,FVSUM_1:60; then reconsider a = (mlt(Line(M1,i), Col(M2,j))).k as Element of L; A31: (emb(m,L)*mlt(Line(M1,i), Col(M2,j))).k = emb(m,L) * a by A25,A28, FVSUM_1:50; (emb(m,L) * Line(M1,i)).k = emb(m,L) * d by A23,A28,FVSUM_1:50; then reconsider b = (emb(m,L) * Line(M1,i)).k as Element of L; b * c = (emb(m,L) * d) * c by A23,A28,FVSUM_1:50 .= emb(m,L) * (d * c) by GROUP_1:def 3 .= emb(m,L) * a by A23,A24,A28,FVSUM_1:60; hence thesis by A28,A31,FVSUM_1:60; end; then A32: emb(m,L)*mlt(Line(M1,i),Col(M2,j)) = mlt(Line(emb(m,L)*M1,i),Col(M2,j )) by A21,A25,FINSEQ_1:13; Seg width ((emb(m,L) * M1) * M2) = Seg width M2 by A4,MATRIX_3:def 4 .= Seg width (M1 * M2) by A3,MATRIX_3:def 4; then A33: [i,j] in Indices (M1 * M2) by A10,A7; then (emb(m,L) * (M1 * M2))*(i,j) = emb(m,L) * ((M1 * M2)*(i,j)) by MATRIX_3:def 5 .= emb(m,L) * (Line(M1,i) "*" Col(M2,j)) by A3,A33,MATRIX_3:def 4 .= emb(m,L) * Sum(mlt(Line(M1,i),Col(M2,j))) by FVSUM_1:def 9; hence thesis by A11,A32,FVSUM_1:73; end; A34: len (emb(m,L) * (M1 * M2)) = len (M1 * M2) by MATRIX_3:def 5 .= len M1 by A3,MATRIX_3:def 4; width (emb(m,L) * (M1 * M2)) = width (M1 * M2) by MATRIX_3:def 5 .= width M2 by A3,MATRIX_3:def 4; then A35: width ((emb(m,L) * M1) * M2) = width (emb(m,L) * (M1 * M2)) by A4, MATRIX_3:def 4; len((emb(m,L) * M1) * M2) = len(emb(m,L) * M1) by A4,MATRIX_3:def 4 .= len M1 by MATRIX_3:def 5; hence thesis by A34,A35,A5,MATRIX_0:21; end; theorem Th7: for L being non empty ZeroStr, p being AlgSequence of L, i being Element of NAT holds p.i <> 0.L implies len p >= i + 1 proof let L be non empty ZeroStr,p be AlgSequence of L, i be Element of NAT; A1: len p is_at_least_length_of p by ALGSEQ_1:def 3; assume p.i <> 0.L; then len p > i by A1,ALGSEQ_1:def 2; hence thesis by NAT_1:13; end; theorem Th8: for L being non empty ZeroStr, s being AlgSequence of L holds len s > 0 implies s.(len(s)-1) <> 0.L proof let L be non empty ZeroStr, s be AlgSequence of L; assume len s > 0; then len s >= 0 + 1 by NAT_1:13; then len s - 1 >= 1 - 1 by XREAL_1:9; then reconsider l = len(s) - 1 as Element of NAT by INT_1:3; assume A1: s.(len(s)-1) = 0.L; now let i be Nat; assume A2: i >= l; per cases by A2,XXREAL_0:1; suppose i = l; hence s.i = 0.L by A1; end; suppose i > l; then i >= l + 1 by NAT_1:13; hence s.i = 0.L by ALGSEQ_1:8; end; end; then A3: l is_at_least_length_of s by ALGSEQ_1:def 2; len(s) < len(s) + 1 by NAT_1:13; then len(s) - 1 < len(s) + 1 - 1 by XREAL_1:9; hence contradiction by A3,ALGSEQ_1:def 3; end; theorem Th9: for L being add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr, p,q being Polynomial of L st len p > 0 & len q > 0 holds len(p *'q) <= len p + len q proof let L be add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr; let p,q be Polynomial of L; assume that A1: len p > 0 and A2: len q > 0; A3: (len p + len q) - 1 <= (len p + len q) - 0 by XREAL_1:13; len q + 1 > 0 + 1 by A2,XREAL_1:6; then len q >= 1 by NAT_1:13; then A4: len q - 1 >= 1 - 1 by XREAL_1:13; q.(len(q)-1) <> 0.L by A2,Th8; then A5: q.(len(q)-'1) <> 0.L by A4,XREAL_0:def 2; len p + 1 > 0 + 1 by A1,XREAL_1:6; then len p >= 1 by NAT_1:13; then A6: len p - 1 >= 1 - 1 by XREAL_1:13; p.(len(p)-1) <> 0.L by A1,Th8; then p.(len(p)-'1) <> 0.L by A6,XREAL_0:def 2; then p.(len p -'1) * q.(len q -'1) <> 0.L by A5,VECTSP_2:def 1; hence thesis by A3,POLYNOM4:10; end; theorem Th10: for L being associative non empty doubleLoopStr, k,l being Element of L, seq being sequence of L holds k * (l * seq) = (k * l) * seq proof let L be associative non empty doubleLoopStr, k,l be Element of L, seq be sequence of L; now let i be Element of NAT; thus (k * (l * seq)).i = k * (l * seq).i by POLYNOM5:def 4 .= k * (l * seq.i) by POLYNOM5:def 4 .= (k * l) * seq.i by GROUP_1:def 3 .= ((k * l) * seq).i by POLYNOM5:def 4; end; hence thesis by FUNCT_2:63; end; begin :: Multiplication of AlgSequences definition ::$CD end; registration let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr; let m1,m2 be AlgSequence of L; cluster m1 * m2 -> finite-Support; coherence proof set f = m1*m2; ex n being Nat st for i being Nat st i >= n holds f.i = 0.L proof take (len m1) + 1; now let i be Nat; assume i >= (len m1) + 1; then i > len m1 by NAT_1:13; then m1.i = 0.L by ALGSEQ_1:8; hence 0.L = m1.i * m2.i .= f.i by LOPBAN_3:def 7; end; hence thesis; end; hence thesis by ALGSEQ_1:def 1; end; end; theorem Th11: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, m1,m2 being AlgSequence of L holds len( m1 * m2) <= min(len m1, len m2) proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, m1,m2 be AlgSequence of L; set p = m1 * m2, k = min(len m1, len m2); reconsider k as Element of NAT; now let i be Nat; assume A1: i >= k; per cases by XXREAL_0:15; suppose k = len m1; then m1.i = 0.L by A1,ALGSEQ_1:8; hence 0.L = m1.i * m2.i .= p.i by LOPBAN_3:def 7; end; suppose k = len m2; then m2.i = 0.L by A1,ALGSEQ_1:8; hence 0.L = m1.i * m2.i .= p.i by LOPBAN_3:def 7; end; end; then k is_at_least_length_of p by ALGSEQ_1:def 2; hence thesis by ALGSEQ_1:def 3; end; theorem for L being add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, m1,m2 being AlgSequence of L st len m1 = len m2 holds len(m1 * m2) = len m1 proof let L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, m1,m2 be AlgSequence of L; set p = m1 * m2; assume A1: len m1 = len m2; A2: now per cases; case len m1 = 0; hence len p >= len m1; end; case len m1 <> 0; then len m1 >= 0 + 1 by NAT_1:13; then (len m1) - 1 >= 1 - 1 by XREAL_1:9; then reconsider l = (len m1) - 1 as Element of NAT by INT_1:3; A3: l + 1 = len m1 + 0; then m1.l <> 0.L & m2.l <> 0.L by A1,ALGSEQ_1:10; then m1.l * m2.l <> 0.L by VECTSP_2:def 1; then p.l <> 0.L by LOPBAN_3:def 7; hence len p >= len m1 by A3,Th7; end; end; min(len m1, len m2) = len m1 by A1; then len p <= len m1 by Th11; hence thesis by A2,XXREAL_0:1; end; begin :: Powers in doubleLoopStrs definition let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, a be Element of L; let i be Integer; func pow(a,i) -> Element of L equals :Def2: power(L).(a,i) if 0 <= i otherwise (power(L).(a,|.i.|))"; coherence proof 0 <= i implies power(L).(a,i) is Element of L proof assume 0 <= i; then reconsider i9 = i as Element of NAT by INT_1:3; power(L).(a,i9) is Element of L; hence thesis; end; hence thesis; end; consistency; end; theorem Th13: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x being Element of L holds pow(x,0) = 1.L proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L; pow(x,0) = x |^ 0 by Def2 .= 1_L by BINOM:8; hence thesis; end; Lm3: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, a being Element of L, i being Integer holds 0 > i implies pow(a,i) = (pow(a, |.i.|))" proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, a be Element of L, i be Integer; assume A1: 0 > i; pow(a, |.i.|) = power(L).(a,|.i.|) by Def2; hence thesis by A1,Def2; end; Lm4: for L being associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, i being Integer, x being Element of L holds i <= 0 implies pow(x,i) = (pow(x, |.i.|))" proof let L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr; let i be Integer; let x be Element of L; A1: 1.L <> 0.L; assume A2: i <= 0; per cases by A2; suppose i < 0; hence thesis by Lm3; end; suppose A3: i = 0; hence pow(x, i) = 1.L by Th13 .= 1.L * (1.L)" by A1,VECTSP_1:def 10 .= (1_L)" .= (x |^ 0)" by BINOM:8 .= (x |^ |.i.|)" by A3,ABSVALUE:def 1 .= (pow(x, |.i.|))" by Def2; end; end; theorem Th14: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x being Element of L holds pow(x,1) = x proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr; let x be Element of L; thus pow(x, 1) = x |^ 1 by Def2 .= x by BINOM:8; end; theorem Th15: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x being Element of L holds pow(x,-1) = x" proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L; |.-1 .| = --1 by ABSVALUE:def 1; hence pow(x, -1) = (pow(x, 1))" by Lm3 .= x" by Th14; end; Lm5: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, i being Element of NAT holds pow(1.L,i) = 1.L proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr; let i be Element of NAT; defpred P[Nat] means pow(1.L,$1) = 1.L; A1: now let k be Nat; assume A2: P[k]; pow(1.L,k+1) = power(L).(1.L,k+1) by Def2 .= power(L).(1.L,k) * 1.L by GROUP_1:def 7 .= 1.L * 1.L by A2,Def2 .= 1.L; hence P[k+1]; end; pow(1_L,0) = power(L).(1.L,0) by Def2; then A3: P[0] by GROUP_1:def 7; for k being Nat holds P[k] from NAT_1:sch 2(A3,A1); hence thesis; end; theorem Th16: for L being associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, i being Integer holds pow(1.L,i) = 1.L proof let L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr; let i be Integer; per cases; suppose 0 <= i; then i is Element of NAT by INT_1:3; hence thesis by Lm5; end; suppose A1: 0 > i; A2: 1.L <> 0.L & 1.L * 1.L = 1.L; A3: pow(1.L,|.i.|) = 1.L by Lm5; pow(1.L,i) = (power(L).(1.L,|.i.|))" by A1,Def2 .= (1.L)" by A3,Def2; hence thesis by A2,VECTSP_1:def 10; end; end; theorem Th17: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x being Element of L, n being Element of NAT holds pow(x,n+1) = pow(x,n) * x & pow(x,n+1) = x * pow(x,n) proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr; let x be Element of L; let n be Element of NAT; pow(x,n+1) = x |^ (n+1) by Def2 .= (x |^ n) * x by GROUP_1:def 7 .= pow(x,n) * x by Def2; hence thesis; end; Lm6: for L being well-unital non empty doubleLoopStr, n being Element of NAT holds (1.L) |^ n = 1.L proof let L be well-unital non empty doubleLoopStr, n be Element of NAT; defpred P[Nat] means (1.L) |^$1 = 1_L; A1: now let k be Nat; assume A2: P[k]; (1.L) |^(k+1) = (1.L) |^k * 1.L by GROUP_1:def 7 .= 1.L by A2; hence P[k+1]; end; A3: P[0] by BINOM:8; for k being Nat holds P[k] from NAT_1:sch 2(A3,A1); hence thesis; end; Lm7: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, m being Element of NAT, x being Element of L st x <> 0.L holds (x|^m) * ((x") |^m) = 1.L proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, m be Element of NAT, x be Element of L; assume A1: x <> 0.L; (x |^ m) * ((x") |^ m) = (x * x") |^ m by BINOM:9 .= (1.L) |^ m by A1,VECTSP_1:def 10 .= 1.L by Lm6; hence thesis; end; theorem Th18: for L being add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, i being Integer, x being Element of L st x <> 0.L holds (pow(x, i))" = pow(x, -i) proof let L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr; let i be Integer; let x be Element of L; assume A1: x <> 0.L; A2: 1.L <> 0.L; per cases; suppose A3: i >= 0; per cases by A3,XREAL_1:24; suppose A4: - i < -0; hence pow(x, -i) = (pow(x, |.- i .|))" by Lm3 .= (pow(x, (--i)))" by A4,ABSVALUE:def 1 .= (pow(x, i))"; end; suppose A5: i = 0; hence pow(x, (- i)) = 1.L by Th13 .= 1.L * (1.L)" by A2,VECTSP_1:def 10 .= (1.L)" .= (pow(x, i))" by A5,Th13; end; end; suppose A6: i < 0; A7: pow(x, |.i.|) = x |^ (|.i.|) by Def2; pow(x, i) = (pow(x, |.i.|))" by A6,Lm3; then (pow(x, i))" = pow(x, |.i.|) by A1,A7,Th1,VECTSP_1:24; hence thesis by A6,ABSVALUE:def 1; end; end; theorem Th19: for L being Field, j being Integer, x being Element of L st x <> 0.L holds pow(x,j+1) = pow(x,j) * pow(x,1) proof let L be Field; let j be Integer; let x be Element of L; A1: pow(x, -1) = (x |^ (|.-1 .|))" by Def2; assume A2: x <> 0.L; then x |^ (|.-1 .|) <> 0.L by Th1; then A3: pow(x, -1) <> 0.L by A1,VECTSP_1:25; A4: pow(x, -j) <> 0.L proof per cases; suppose 0 <= -j; then reconsider k = -j as Element of NAT by INT_1:3; pow(x, -j) = x |^ k by Def2; hence thesis by A2,Th1; end; suppose A5: -j < 0; A6: x |^ (|.-j.|) <> 0.L by A2,Th1; pow(x, -j) = (x |^ (|.-j.|))" by A5,Def2; hence thesis by A6,VECTSP_1:25; end; end; A7: pow(x, j+1) <> 0.L proof per cases; suppose 0 <= j+1; then reconsider k = j+1 as Element of NAT by INT_1:3; pow(x, j+1) = x |^ k by Def2; hence thesis by A2,Th1; end; suppose A8: j+1 < 0; A9: x |^ (|.j+1 .|) <> 0.L by A2,Th1; pow(x, j+1) = (x |^ (|.j+1 .|))" by A8,Def2; hence thesis by A9,VECTSP_1:25; end; end; A10: now per cases by Lm1; suppose A11: j >= 0; then reconsider n = j as Element of NAT by INT_1:3; A12: n + 1 = |.j + 1 .| by ABSVALUE:def 1; pow(x, |.j.|) = x |^ (|.j.|) by Def2; then A13: pow(x, |.j.|) <> 0.L by A2,Th1; pow(x, |.j+1 .|) = x |^ (|.j+1 .|) by Def2; then A14: pow(x, |.j+1 .|) <> 0.L by A2,Th1; n + 1 >= 0; hence pow(x, j + 1) * (pow(x, -1) * pow(x, -j)) = pow(x, |.j+1 .|) * (pow (x, -1) * pow(x, -j)) by ABSVALUE:def 1 .= pow(x, |.j+1 .|) * (x" * pow(x, -j)) by Th15 .= pow(x, |.j+1 .|) * (x" * (pow(x, j))") by A2,Th18 .= pow(x, |.j+1 .|) * (x" * (pow(x, |.j.|))") by A11,ABSVALUE:def 1 .= pow(x, |.j+1 .|) * ((x * pow(x, |.j.|))") by A2,A13,Th2 .= pow(x, |.j+1 .|) * (pow(x, |.j.| + 1))" by Th17 .= pow(x, |.j+1 .|) * (pow(x, |.j+1 .|))" by A12,ABSVALUE:def 1 .= 1.L by A14,VECTSP_1:def 10; end; suppose A15: j < - 1; A16: pow(x, -j) <> 0.L proof reconsider k = -j as Element of NAT by A15,INT_1:3; pow(x, -j) = x |^ k by Def2; hence thesis by A2,Th1; end; pow(x, |.j+1 .|) = x |^ (|.j+1 .|) by Def2; then A17: pow(x, |.j+1 .|) <> 0.L by A2,Th1; A18: j + 1 < - 1 + 1 by A15,XREAL_1:6; hence pow(x, j+1) * (pow(x, -1) * pow(x, -j)) = (pow(x, |.j+1 .|))" * ( pow(x, -1) * pow(x, -j)) by Lm3 .= (pow(x, |.j+1 .|))" * (x" * pow(x, -j)) by Th15 .= (pow(x, |.j+1 .|))" * x" * pow(x, -j) by GROUP_1:def 3 .= (pow(x, |.j+1 .|) * x)" * pow(x, -j) by A2,A17,Th2 .= (pow(x, (|.j + 1 .| + 1)))" * pow(x, -j) by Th17 .= (pow(x, (- (j + 1) + 1)))" * pow(x, -j) by A18,ABSVALUE:def 1 .= 1.L by A16,VECTSP_1:def 10; end; suppose A19: j = - 1; A20: x" <> 0.L by A2,VECTSP_1:25; thus pow(x, j+1) * (pow(x, -1) * pow(x, -j)) = 1.L * (pow(x, -1) * pow(x , -j)) by A19,Th13 .= (pow(x, -1) * pow(x, -j)) .= x" * pow(x, -j) by Th15 .= x" * (pow(x, j))" by A2,Th18 .= x" * (x")" by A19,Th15 .= 1.L by A20,VECTSP_1:def 10; end; end; A21: pow(x, j+1) <> 0.L proof per cases; suppose 0 <= j+1; then reconsider k = j+1 as Element of NAT by INT_1:3; pow(x, j+1) = x |^ k by Def2; hence thesis by A2,Th1; end; suppose A22: j+1 < 0; A23: x |^ (|.j+1 .|) <> 0.L by A2,Th1; pow(x, j+1) = (x |^ (|.j+1 .|))" by A22,Def2; hence thesis by A23,VECTSP_1:25; end; end; pow(x, j+1) * pow(x, -(j+1)) = pow(x, j+1) * (pow(x, j+1))" by A2,Th18 .= 1.L by A7,VECTSP_1:def 10; then A24: pow(x, -(j + 1)) = pow(x, -1) * pow(x, -j) by A10,A21,VECTSP_1:5; thus pow(x, j+1) = pow(x, -(-(j+1))) .= (pow(x, -1) * pow(x, -j))" by A2,A24,Th18 .= (pow(x, -j))" * (pow(x, -1))" by A4,A3,Th2 .= pow(x, -(-j)) * (pow(x, -1))" by A2,Th18 .= pow(x, j) * pow(x, -(- 1)) by A2,Th18 .= pow(x, j) * pow(x, 1); end; theorem Th20: for L being Field, j being Integer, x being Element of L st x <> 0.L holds pow(x,j-1) = pow(x,j) * pow(x,-1) proof let L be Field; let j be Integer; let x be Element of L; assume A1: x <> 0.L; A2: pow(x, j-1) <> 0.L proof per cases; suppose 0 <= j-1; then reconsider k = j-1 as Element of NAT by INT_1:3; pow(x, j-1) = x |^ k by Def2; hence thesis by A1,Th1; end; suppose A3: j-1 < 0; A4: x |^ (|.j-1 .|) <> 0.L by A1,Th1; pow(x, j-1) = (x |^ (|.j-1 .|))" by A3,Def2; hence thesis by A4,VECTSP_1:25; end; end; A5: now per cases by Lm2; suppose A6: j >= 1; then A7: |.j.| = j by ABSVALUE:def 1; pow(x, |.-j.|) = x |^ (|.-j.|) by Def2; then A8: pow(x, |.-j.|) <> 0.L by A1,Th1; A9: |.j.| = |.- j.| by COMPLEX1:52; j >= 1 + 0 by A6; then A10: j - 1 >= 0 by XREAL_1:19; then A11: |.j - 1 .| + 1 = j - 1 + 1 by ABSVALUE:def 1 .= j; thus pow(x, j-1) * (x * pow(x, -j)) = pow(x, j-1) * x * pow(x, -j) by GROUP_1:def 3 .= pow(x, |.j-1 .|) * x * pow(x, -j) by A10,ABSVALUE:def 1 .= pow(x, |.j-1 .|) * x * ((pow(x, |.-j.|))") by A6,Lm4 .= pow(x, |.j-1 .| + 1) * ((pow(x, |.-j.|))") by Th17 .= 1.L by A8,A11,A7,A9,VECTSP_1:def 10; end; suppose A12: j < 0; pow(x, |.j-1 .|) = x |^ (|.j-1 .|) by Def2; then A13: pow(x, |.j-1 .|) <> 0.L by A1,Th1; A14: 1 - j = - (j - 1); thus pow(x, j-1) * (x * pow(x, -j)) = (pow(x, |.j-1 .|))" * (x * pow(x, -j)) by A12,Lm3 .= (pow(x, |.j-1 .|))" * (x * pow(x, |.-j.|)) by A12,ABSVALUE:def 1 .= (pow(x, |.j-1 .|))" * pow(x, 1 + |.-j.|) by Th17 .= (pow(x, |.j-1 .|))" * pow(x, 1 + (-j)) by A12,ABSVALUE:def 1 .= (pow(x, |.j-1 .|))" * pow(x, |.j-1 .|) by A12,A14,ABSVALUE:def 1 .= 1.L by A13,VECTSP_1:def 10; end; suppose A15: j = 0; hence pow(x, j-1) * (x * pow(x, -j)) = x" * (x * pow(x, -j)) by Th15 .= x" * x * pow(x, -j) by GROUP_1:def 3 .= 1.L * pow(x, -j) by A1,VECTSP_1:def 10 .= pow(x, 0) by A15 .= 1.L by Th13; end; end; A16: pow(x, -j) <> 0.L proof per cases; suppose 0 <= -j; then reconsider k = -j as Element of NAT by INT_1:3; pow(x, -j) = x |^ k by Def2; hence thesis by A1,Th1; end; suppose A17: -j < 0; A18: x |^ (|.-j.|) <> 0.L by A1,Th1; pow(x, -j) = (x |^ (|.-j.|))" by A17,Def2; hence thesis by A18,VECTSP_1:25; end; end; A19: pow(x, j-1) <> 0.L proof per cases; suppose 0 <= j-1; then reconsider k = j-1 as Element of NAT by INT_1:3; pow(x, j-1) = x |^ k by Def2; hence thesis by A1,Th1; end; suppose A20: j-1 < 0; A21: x |^ (|.j-1 .|) <> 0.L by A1,Th1; pow(x, j-1) = (x |^ (|.j-1 .|))" by A20,Def2; hence thesis by A21,VECTSP_1:25; end; end; pow(x, j-1) * (pow(x, 1-j)) = pow(x, j-1) * pow(x, -(j-1)) .= pow(x, j-1) * (pow(x, j-1))" by A1,Th18 .= 1.L by A2,VECTSP_1:def 10; then x * pow(x, -j) = pow(x, 1-j) by A5,A19,VECTSP_1:5; then (pow(x, 1-j))" = (pow(x, -j))" * x" by A1,A16,Th2 .= pow(x, -(- j)) * x" by A1,Th18 .= pow(x, j) * pow(x, -1) by Th15; then pow(x, j) * pow(x, -1) = pow(x, -(1-j)) by A1,Th18; hence thesis; end; theorem Th21: for L being Field, i,j being Integer, x being Element of L st x <> 0.L holds pow(x,i) * pow(x,j) = pow(x,i+j) proof let L be Field; let i,j be Integer; let x be Element of L; defpred P[Integer] means for i being Integer holds pow(x, i+$1) = pow(x, i) * pow(x, $1); assume A1: x <> 0.L; A2: for j being Integer holds P[j] implies P[j - 1] & P[j + 1] proof let j be Integer; assume A3: for i being Integer holds pow(x, i+j) = pow(x, i) * pow(x, j); thus for i being Integer holds pow(x, i + (j - 1)) = pow(x, i) * pow(x, j - 1) proof let i be Integer; thus pow(x, i + (j - 1)) = pow(x, (i - 1) + j) .= pow(x, i - 1) * pow(x, j) by A3 .= (pow(x, i) * pow(x, -1)) * pow(x, j) by A1,Th20 .= pow(x, i) * (pow(x, -1) * pow(x, j)) by GROUP_1:def 3 .= pow(x, i) * pow(x, j + (-1)) by A3 .= pow(x, i) * pow(x, j - 1); end; let i be Integer; thus pow(x, i + (j + 1)) = pow(x, (i + 1) + j) .= pow(x, i + 1) * pow(x, j) by A3 .= (pow(x, i) * pow(x, 1)) * pow(x, j) by A1,Th19 .= pow(x, i) * (pow(x, 1) * pow(x, j)) by GROUP_1:def 3 .= pow(x, i) * pow(x, j + 1) by A3; end; A4: P[0] proof let i be Integer; thus pow(x, i+0) = pow(x, i) * 1.L .= pow(x, i) * pow(x, 0) by Th13; end; for j being Integer holds P[j] from INT_1:sch 4(A4,A2); hence thesis; end; Lm8: for L being almost_left_invertible associative well-unital add-associative right_zeroed right_complementable left-distributive commutative non degenerated non empty doubleLoopStr, k being Element of NAT, x being Element of L st x <> 0.L holds x" |^ k = (x |^ k)" proof let L be almost_left_invertible associative well-unital add-associative right_zeroed right_complementable left-distributive commutative non degenerated non empty doubleLoopStr; let k be Element of NAT; let x be Element of L; A1: 1.L <> 0.L; defpred P[Nat] means x" |^ $1 = (x |^ $1)"; assume A2: x <> 0.L; A3: now let n be Nat; assume A4: P[n]; A5: x |^ n <> 0.L by A2,Th1; x" |^ (n + 1) = (x" |^ n) * x" by GROUP_1:def 7 .= (x * (x |^ n))" by A2,A4,A5,Th2 .= ((x |^ 1) * (x |^ n))" by BINOM:8 .= (x |^ (n + 1))" by BINOM:10; hence P[n+1]; end; x" |^ 0 = 1_L by BINOM:8 .= 1.L * (1.L)" by A1,VECTSP_1:def 10 .= (1_L)" .= (x |^ 0)" by BINOM:8; then A6: P[0]; for n being Nat holds P[n] from NAT_1:sch 2(A6,A3); hence thesis; end; theorem Th22: for L being almost_left_invertible associative well-unital add-associative right_zeroed right_complementable left-distributive commutative non degenerated non empty doubleLoopStr, k being Element of NAT, x being Element of L st x <> 0.L holds pow(x", k) = pow(x, -k) proof let L be almost_left_invertible associative well-unital add-associative right_zeroed right_complementable left-distributive commutative non degenerated non empty doubleLoopStr; let k be Element of NAT; let x be Element of L; assume A1: x <> 0.L; pow(x", k) = (x") |^ k by Def2 .= (x |^ k)" by A1,Lm8 .= (pow(x,k))" by Def2 .= pow(x,-k) by A1,Th18; hence thesis; end; theorem Th23: for L being Field, x being Element of L st x <> 0.L for i,j,k being Nat holds pow(x,(i-1)*(k-1)) * pow(x,-(j-1)*(k-1)) = pow(x,(i-j)*(k-1)) proof let L be Field; let x be Element of L; assume A1: x <> 0.L; let i,j,k be Nat; pow(x, (i-1)*(k-1)) * pow(x, -(j-1)*(k-1)) = pow(x, (i-1)*(k-1) + (-(j-1 )*(k-1))) by A1,Th21 .= pow(x, (i-j)*(k-1)); hence thesis; end; theorem Th24: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x being Element of L, n,m being Element of NAT holds pow(x, n * m) = pow(pow(x, n), m) proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr; let x be Element of L; let n,m be Element of NAT; pow(x, n*m) = x |^ (n*m) by Def2 .= (x|^n) |^m by BINOM:11 .= pow(x |^ n, m) by Def2 .= pow(pow(x, n), m) by Def2; hence thesis; end; Lm9: for L being add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non degenerated non empty doubleLoopStr, x being Element of L st x <> 0.L for n being Element of NAT holds pow(x", n) = (pow(x, n))" proof let L be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non degenerated non empty doubleLoopStr; let x be Element of L; A1: 1.L <> 0.L; defpred P[Nat] means pow(x", $1) = (pow(x, $1))"; assume A2: x <> 0.L; now let n be Nat; assume A3: P[n]; A4: x |^ n <> 0.L by A2,Th1; thus pow(x", n+1) = (x") |^ (n+1) by Def2 .= ((x") |^ n) * x" by GROUP_1:def 7 .= (pow(x", n)) * x" by Def2 .= ((power(L).(x, n))") * x" by A3,Def2 .= (x * (x |^ n))" by A2,A4,Th2 .= ((x |^ 1) * (x |^ n))" by BINOM:8 .= (x |^ (n + 1))" by BINOM:10 .= (pow(x, n+1))" by Def2; hence P[n+1]; end; then A5: for n being Nat st P[n] holds P[n+1]; let n be Nat; pow(x", 0) = 1.L by Th13 .= 1.L * (1.L)" by A1,VECTSP_1:def 10 .= (1.L)" .= (pow(x, 0))" by Th13; then A6: P[0]; for n being Nat holds P[n] from NAT_1:sch 2(A6,A5); hence thesis; end; theorem Th25: for L being Field, x being Element of L st x <> 0.L for i being Integer holds pow(x", i) = (pow(x, i))" proof let L be Field; let x be Element of L; assume A1: x <> 0.L; let i be Integer; per cases; suppose i >= 0; then reconsider n = i as Element of NAT by INT_1:3; thus pow(x", i) = (pow(x, n))" by A1,Lm9 .= (pow(x, i))"; end; suppose A2: i < 0; A3: pow(x, |.i.|) = x |^ (|.i.|) by Def2; thus pow(x", i) = (pow(x", |.i.|))" by A2,Lm3 .= pow((x")", |.i.|) by A1,Lm9,VECTSP_1:25 .= pow(x, |.i.|) by A1,VECTSP_1:24 .= (pow(x, |.i.|))"" by A1,A3,Th1,VECTSP_1:24 .= (pow(x, i))" by A2,Lm3; end; end; theorem Th26: for L being Field, x being Element of L st x <> 0.L for i,j being Integer holds pow(x,i * j) = pow(pow(x,i), j) proof let L be Field, x being Element of L; assume A1: x <> 0.L; let i,j be Integer; per cases; suppose i >= 0 & j >= 0; then reconsider m = i, n = j as Element of NAT by INT_1:3; thus pow(x, i*j) = pow(pow(x, m), n) by Th24 .= pow(pow(x, i), j); end; suppose A2: i >= 0 & j < 0; then reconsider m = i, n = - j as Element of NAT by INT_1:3; A3: pow(x, i) = x |^ m by Def2; then A4: pow(x, i) <> 0.L by A1,Th1; A5: pow(pow(x, i), j) = ((pow(x, i)) |^ |.j.|)" by A2,Def2; i * j = - (i * n); hence pow(x, i*j) = (pow(x, i * n))" by A1,Th18 .= pow(x", i*n) by A1,Th25 .= pow(pow(x", m), n) by Th24 .= pow((pow(x, i))", n) by A1,Th25 .= (pow((pow(x, i))", j))" by A4,Th18,VECTSP_1:25 .= ((pow(pow(x, i), j))")" by A1,A3,Th1,Th25 .= pow(pow(x, i), j) by A4,A5,Th1,VECTSP_1:24; end; suppose A6: i < 0 & j >= 0; then reconsider m = - i, n = j as Element of NAT by INT_1:3; A7: pow(x, i) = (x |^ (|.i.|))" by A6,Def2; i * j = - (m * j); hence pow(x, i*j) = (pow(x, m*j))" by A1,Th18 .= pow(x", m*j) by A1,Th25 .= pow(pow(x", m), n) by Th24 .= pow((pow(x", i))", n) by A1,Th18,VECTSP_1:25 .= pow((pow(x, i))"", j) by A1,Th25 .= pow(pow(x, i), j) by A1,A7,Th1,VECTSP_1:24; end; suppose A8: j < 0 & i < 0; then reconsider m = - i, n = - j as Element of NAT by INT_1:3; A9: pow(x, -i) = x |^ m by Def2; x" <> 0.L by A1,VECTSP_1:25; then A10: (x") |^ (|.i.|) <> 0.L by Th1; A11: pow(x", i) = ((x") |^ (|.i.|))" by A8,Def2; i * j * ((- 1) * (- 1)) = m * n; hence pow(x, i*j) = pow(pow(x, m), n) by Th24 .= (pow(pow(x, -i), j))" by A1,A9,Th1,Th18 .= (pow((pow(x, i))", j))" by A1,Th18 .= (pow(pow(x", i), j))" by A1,Th25 .= pow((pow(x", i))", j) by A11,A10,Th25,VECTSP_1:25 .= pow(pow(x"", i), j) by A1,Th25,VECTSP_1:25 .= pow(pow(x, i), j) by A1,VECTSP_1:24; end; end; theorem Th27: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x being Element of L, i,k being Element of NAT st 1 <= k holds pow(x, i*(k-1)) = pow(x|^i, k-1) proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr; let x be Element of L; let i,k be Element of NAT; assume 1 <= k; then 0 < k; then reconsider m = k-1 as Element of NAT by NAT_1:20; pow(x, i*(k-1)) = x|^(i*m) by Def2 .= (x|^i) |^m by BINOM:11 .= pow(x|^i,m) by Def2; hence thesis; end; Lm10: for L being associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x being Element of L, m being Element of NAT holds (x <> 0.L & x |^ m = 1.L) implies (x") |^ m = 1.L proof let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L, m be Element of NAT; assume x <> 0.L & x |^ m = 1.L; then 1.L * ((x") |^ m) = 1.L by Lm7; hence thesis; end; Lm11: for L being associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, x being Element of L, i being Element of NAT holds (x <> 0.L & (x") |^ i = 1.L) implies x |^ i = 1.L proof let L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, x be Element of L, i be Element of NAT; assume that A1: x <> 0.L and A2: (x") |^ i = 1.L; A3: 1_L = x |^ 0 by BINOM:8; ((x") |^ i) * 1.L = 1.L by A2; then ((x") |^i)*(x|^0) = ((x") |^i)*(x|^i) by A1,A3,Lm7; hence thesis by A1,A2,A3,VECTSP_1:5; end; begin :: Conversion between AlgSequences and Matrices definition let m be Nat, L be non empty ZeroStr, p be AlgSequence of L; func mConv(p,m) -> Matrix of m,1,L means :Def3: for i being Nat st 1 <= i & i <= m holds it*(i,1) = p.(i-1); existence proof defpred P[Nat,set,set] means $3 = p.($1-1); reconsider m9=m as Element of NAT by ORDINAL1:def 12; A1: for i,j being Nat st [i,j] in [:Seg m9, Seg 1:] ex x being Element of L st P[i,j,x] proof let i,j be Nat; assume A2: [i,j] in [:Seg m9, Seg 1:]; take p/.(i-1); [i,j]`1 in Seg m by A2,MCART_1:10; then i in Seg m; then 1 <= i by FINSEQ_1:1; then dom p = NAT & 1-1 <= i-1 by FUNCT_2:def 1,XREAL_1:9; hence thesis by INT_1:3,PARTFUN1:def 6; end; consider M being Matrix of m9,1,L such that A3: for i,j being Nat st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_0:sch 2(A1); reconsider M as Matrix of m,1,L; take M; now let i be Nat; assume 1 <= i & i <= m; then A4: i in Seg m & Indices M = [:Seg m, Seg 1:] by MATRIX_0:23; 1 in Seg 1; then [i,1] in Indices M by A4,ZFMISC_1:def 2; hence M*(i,1) = p.(i-1) by A3; end; hence thesis; end; uniqueness proof let M1,M2 be Matrix of m,1,L; assume that A5: for i being Nat st 1 <= i & i <= m holds M1*(i,1) = p.(i-1) and A6: for i being Nat st 1 <= i & i <= m holds M2*(i,1) = p.(i-1); per cases; suppose A7: m = 0; then A8: for i,j being Nat st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j) by MATRIX_0:22; A9: width M1 = 0 by A7,MATRIX_0:22 .= width M2 by A7,MATRIX_0:22; len M1 = 0 by A7,MATRIX_0:22 .= len M2 by A7,MATRIX_0:22; hence thesis by A9,A8,MATRIX_0:21; end; suppose A10: m > 0; A11: now let i,j be Nat; assume [i,j] in Indices M1; then A12: [i,j] in [:Seg m, Seg 1:] by A10,MATRIX_0:23; then [i,j]`2 in Seg 1 by MCART_1:10; then j in Seg 1; then 1 <= j & j <= 1 by FINSEQ_1:1; then A13: j = 1 by XXREAL_0:1; [i,j]`1 in Seg m by A12,MCART_1:10; then i in Seg m; then A14: 1 <= i & i <= m by FINSEQ_1:1; hence M1*(i,j) = p.(i-1) by A5,A13 .= M2*(i,j) by A6,A14,A13; end; A15: width M1 = 1 by A10,MATRIX_0:23 .= width M2 by A10,MATRIX_0:23; len M1 = m by A10,MATRIX_0:23 .= len M2 by A10,MATRIX_0:23; hence thesis by A15,A11,MATRIX_0:21; end; end; end; theorem Th28: for m being Nat st m > 0 for L being non empty ZeroStr, p being AlgSequence of L holds len mConv(p,m) = m & width mConv(p,m) = 1 & for i being Nat st i < m holds mConv(p,m)*(i+1,1) = p.i proof let m be Nat; assume A1: m > 0; let L be non empty ZeroStr, p be AlgSequence of L; set q = mConv(p,m); thus len q = m by A1,MATRIX_0:23; thus width q = 1 by A1,MATRIX_0:23; now let i be Nat; assume i < m; then 0 + 1 <= i + 1 & i+1 <= m by NAT_1:13; then q*(i+1,1) = p.(i+1-1) by Def3; hence q*(i+1,1) = p.i; end; hence thesis; end; theorem Th29: for m being Nat st m > 0 for L being non empty ZeroStr, a being AlgSequence of L, M being Matrix of m,1,L holds (for i being Nat st i < m holds M*(i+1,1) = a.i) implies mConv(a,m) = M proof let m be Nat; assume A1: m > 0; let L be non empty ZeroStr; let a be AlgSequence of L; let M be Matrix of m,1,L; A2: width mConv(a, m) = 1 by A1,Th28 .= width M by A1,MATRIX_0:23; assume A3: for i being Nat st i < m holds M*(i+1,1) = a.i; A4: for i,j being Nat st [i,j] in Indices mConv(a,m) holds (mConv(a,m))*(i,j ) = M*(i,j) proof let i,j be Nat; assume A5: [i,j] in Indices mConv(a,m); then A6: i in dom mConv(a, m) by ZFMISC_1:87; len mConv(a, m) = m by A1,Th28; then A7: i in Seg m by A6,FINSEQ_1:def 3; then 0 < i by FINSEQ_1:1; then reconsider k=i-1 as Nat by NAT_1:20; A8: j in Seg width mConv(a, m) by A5,ZFMISC_1:87; then A9: 1 <= j by FINSEQ_1:1; j in Seg 1 by A1,A8,Th28; then A10: j <= 1 by FINSEQ_1:1; k+1 <= m by A7,FINSEQ_1:1; then A11: k < m by NAT_1:13; then M*(k+1,1) = a.k by A3 .= (mConv(a, m))*(k+1,1) by A11,Th28 .= (mConv(a, m))*(i,j) by A9,A10,XXREAL_0:1; hence thesis by A9,A10,XXREAL_0:1; end; len mConv(a,m) = m by A1,Th28 .= len M by A1,MATRIX_0:23; hence thesis by A2,A4,MATRIX_0:21; end; definition let L be non empty ZeroStr, M be Matrix of L; func aConv(M) -> AlgSequence of L means :Def4: (for i being Nat st i < len M holds it.i = M*(i+1,1)) & for i being Nat st i >= len M holds it.i = 0.L; existence proof defpred P[object,object] means ex k being Element of NAT st k = $1 & ((k < len M & $2 = M*(k+1,1)) or (len M <= k & $2 = 0.L)); A1: for x being object st x in NAT ex y being object st y in the carrier of L & P[x,y] proof let u be object; assume u in NAT; then reconsider u9 = u as Element of NAT; thus ex y being object st y in the carrier of L & P[u,y] proof per cases; suppose A2: u9 < len M; take M*(u9+1,1); thus thesis by A2; end; suppose A3: u9 >= len M; take 0.L; thus thesis by A3; end; end; end; consider f being sequence of the carrier of L such that A4: for x being object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A1); reconsider f as sequence of L; ex n being Nat st for i being Nat st i >= n holds f.i = 0.L proof take len M; now let i be Nat; i in NAT by ORDINAL1:def 12; then A5: ex k being Element of NAT st k = i &( k < len M & f.i = M *(k+1,1) or len M <= k & f.i = 0.L) by A4; assume i >= len M; hence f.i = 0.L by A5; end; hence thesis; end; then reconsider q = f as AlgSequence of L by ALGSEQ_1:def 1; A6: now let i be Nat; i in NAT by ORDINAL1:def 12; then A7: ex k being Element of NAT st k = i &( k < len M & q.i = M *(k+1,1) or len M <= k & q.i = 0.L) by A4; assume i >= len M; hence q.i = 0.L by A7; end; take q; now let i be Nat; i in NAT by ORDINAL1:def 12; then A8: ex k being Element of NAT st k = i &( k < len M & q.i = M *(k+1,1) or len M <= k & q.i = 0.L) by A4; assume i < len M; hence q.i = M*(i+1,1) by A8; end; hence thesis by A6; end; uniqueness proof let z1,z2 be AlgSequence of L; assume that A9: for i being Nat st i < len M holds z1.i = M*(i+1,1) and A10: for i being Nat st i >= len M holds z1.i = 0.L; assume that A11: for i being Nat st i < len M holds z2.i = M*(i+1,1) and A12: for i being Nat st i >= len M holds z2.i = 0.L; A13: now let u be object; assume u in dom z1; then reconsider u9 = u as Element of NAT by FUNCT_2:def 1; per cases; suppose A14: u9 < len M; hence z1.u = M*(u9+1,1) by A9 .= z2.u by A11,A14; end; suppose A15: len M <= u9; hence z1.u = 0.L by A10 .= z2.u by A12,A15; end; end; dom z1 = NAT by FUNCT_2:def 1 .= dom z2 by FUNCT_2:def 1; hence z1 = z2 by A13,FUNCT_1:2; end; end; begin :: Primitive Roots, DFT and Vandermonde Matrix definition let L be well-unital non empty doubleLoopStr, x be Element of L, n be Element of NAT; pred x is_primitive_root_of_degree n means n <> 0 & x|^n = 1.L & for i being Element of NAT st 0 < i & i < n holds x|^i <> 1.L; end; theorem Th30: for L being well-unital add-associative right_zeroed right_complementable right-distributive non degenerated non empty doubleLoopStr, n being Element of NAT holds not(0.L is_primitive_root_of_degree n) proof let L be well-unital add-associative right_zeroed right_complementable right-distributive non degenerated non empty doubleLoopStr, n be Element of NAT; defpred P[Nat] means (0.L) |^$1 = 0.L; A1: for j being Nat st 1 <= j holds P[j] implies P[j+1] proof let j be Nat; assume 1 <= j; assume P[j]; (0.L) |^(j+1) = ((0.L) |^j) * 0.L by GROUP_1:def 7 .= 0.L; hence thesis; end; A2: P[1] by BINOM:8; A3: for m being Nat st 1 <= m holds P[m] from NAT_1:sch 8(A2,A1); assume A4: 0.L is_primitive_root_of_degree n; then n <> 0; then 0 + 1 < n + 1 by XREAL_1:8; then 1 <= n by NAT_1:13; then (0.L) |^n <> 1.L by A3; hence contradiction by A4; end; theorem Th31: for L being add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, m being Element of NAT, x being Element of L st x is_primitive_root_of_degree m holds x" is_primitive_root_of_degree m proof let L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr; let m be Element of NAT; let x be Element of L; assume A1: x is_primitive_root_of_degree m; then A2: x <> 0.L by Th30; A3: for i being Element of NAT st 0 < i & i < m holds x" |^i <> 1.L proof let i be Element of NAT; assume 0 < i & i < m; then x |^ i <> 1.L by A1; hence thesis by A2,Lm11; end; x |^ m = 1.L by A1; then A4: x" |^ m = 1.L by A2,Lm10; m <> 0 by A1; hence thesis by A4,A3; end; theorem Th32: for L being add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, m being Element of NAT, x being Element of L st x is_primitive_root_of_degree m for i,j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds pow(x,i-j) <> 1.L proof let L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr; let m be Element of NAT; let x be Element of L; assume A1: x is_primitive_root_of_degree m; then A2: x <> 0.L by Th30; let i,j be Nat; assume that A3: 1 <= i and A4: i <= m and A5: 1 <= j and A6: j <= m and A7: i <> j; per cases; suppose A8: i > j; then reconsider k = i - j as Element of NAT by INT_1:5; k <= i - 1 by A5,XREAL_1:13; then k + 1 <= (i - 1) + 1 by XREAL_1:6; then k < i by NAT_1:13; then A9: k < m by A4,XXREAL_0:2; i - j > j - j by A8,XREAL_1:14; then x|^k <> 1.L by A1,A9; hence thesis by Def2; end; suppose i <= j; then A10: i < j by A7,XXREAL_0:1; then A11: j - i > i - i by XREAL_1:14; A12: i - j < j - j by A10,XREAL_1:14; then A13: |.i-j.| = -(i-j) by ABSVALUE:def 1; then reconsider k = -(i-j) as Element of NAT; j - i <= j - 1 by A3,XREAL_1:13; then k + 1 <= (j - 1) + 1 by XREAL_1:6; then k < j by NAT_1:13; then A14: k < m by A6,XXREAL_0:2; A15: x|^k <> 0.L by A2,Th1; now assume (x|^k)" = 1.L; then 1.L = x|^k * 1.L by A15,VECTSP_1:def 10 .= x|^k; hence contradiction by A1,A11,A14; end; hence thesis by A12,A13,Def2; end; end; definition let m be Nat, L be well-unital non empty doubleLoopStr, p be Polynomial of L, x be Element of L; func DFT(p,x,m) -> AlgSequence of L means :Def6: (for i being Nat st i < m holds it.i = eval(p,x |^ i)) & for i being Nat st i >= m holds it.i = 0.L; existence proof defpred P[object,object] means ex k being Element of NAT st k = $1 & ((k < m & $2 = eval(p,x |^ k)) or (m <= k & $2 = 0.L)); A1: for x being object st x in NAT ex y being object st y in the carrier of L & P[x,y] proof let u be object; assume u in NAT; then reconsider u9 = u as Element of NAT; per cases; suppose A2: u9 < m; take eval(p,x |^ u9); thus thesis by A2; end; suppose A3: u9 >= m; take 0.L; thus thesis by A3; end; end; consider f being sequence of the carrier of L such that A4: for x being object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A1); reconsider f as sequence of L; ex n being Nat st for i being Nat st i >= n holds f.i = 0.L proof reconsider m as Element of NAT by ORDINAL1:def 12; take m; now let i be Nat; i in NAT by ORDINAL1:def 12; then A5: ex k being Element of NAT st k = i &( k < m & f.i = eval( p,x |^ k ) or m <= k & f.i = 0.L) by A4; assume i >= m; hence f.i = 0.L by A5; end; hence thesis; end; then reconsider q = f as AlgSequence of L by ALGSEQ_1:def 1; A6: now let i be Nat; i in NAT by ORDINAL1:def 12; then A7: ex k being Element of NAT st k = i &( k < m & q.i = eval( p,x |^ k) or m <= k & q.i = 0.L) by A4; assume i >= m; hence q.i = 0.L by A7; end; take q; now let i be Nat; i in NAT by ORDINAL1:def 12; then A8: ex k being Element of NAT st k = i &( k < m & q.i = eval( p,x |^ k) or m <= k & q.i = 0.L) by A4; assume i < m; hence q.i = eval(p,x |^ i) by A8; end; hence thesis by A6; end; uniqueness proof let z1,z2 be AlgSequence of L; assume that A9: for i being Nat st i < m holds z1.i = eval(p,x |^ i) and A10: for i being Nat st i >= m holds z1.i = 0.L; assume that A11: for i being Nat st i < m holds z2.i = eval(p,x |^ i) and A12: for i being Nat st i >= m holds z2.i = 0.L; A13: now let u be object; assume u in dom z1; then reconsider u9 = u as Element of NAT by FUNCT_2:def 1; per cases; suppose A14: u9 < m; hence z1.u = eval(p,x |^ u9) by A9 .= z2.u by A11,A14; end; suppose A15: m <= u9; hence z1.u = 0.L by A10 .= z2.u by A12,A15; end; end; dom z1 = NAT by FUNCT_2:def 1 .= dom z2 by FUNCT_2:def 1; hence z1 = z2 by A13,FUNCT_1:2; end; end; theorem Th33: for m being Nat, L being well-unital non empty doubleLoopStr, x being Element of L holds DFT(0_.(L),x,m) = 0_.(L) proof let m be Nat, L be well-unital non empty doubleLoopStr, x be Element of L; set q = DFT(0_.(L),x,m); A1: now let u be object; assume u in dom q; then reconsider n = u as Element of NAT by FUNCT_2:def 1; per cases; suppose n < m; hence q.u = eval(0_.(L),x |^ n) by Def6 .= 0.L by POLYNOM4:17 .= (0_.(L)).n by FUNCOP_1:7 .= (0_.(L)).u; end; suppose n >= m; hence q.u = 0.L by Def6 .= (0_.(L)).n by FUNCOP_1:7 .= (0_.(L)).u; end; end; dom q = NAT by FUNCT_2:def 1 .= dom 0_.(L) by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; theorem Th34: for m being Nat, L being Field, p,q being Polynomial of L, x being Element of L holds DFT(p, x, m) * DFT(q, x, m) = DFT(p *' q, x, m) proof let m be Nat; let L be Field; let p,q be Polynomial of L; let x be Element of L; set ep = DFT(p, x, m), eq = DFT(q, x, m), epq = DFT(p *' q, x, m); A1: now let u9 be object; assume u9 in dom(ep*eq); then reconsider u = u9 as Element of NAT by FUNCT_2:def 1; per cases; suppose A2: u < m; hence epq.u9 = eval(p*'q,x|^u) by Def6 .= eval(p,x|^u) * eval(q,x|^u) by POLYNOM4:24 .= ep.u * eval(q,x|^u) by A2,Def6 .= ep.u * eq.u by A2,Def6 .= (ep * eq).u9 by LOPBAN_3:def 7; end; suppose A3: m <= u; thus (ep * eq).u9 = ep.u * eq.u by LOPBAN_3:def 7 .= 0.L * eq.u by A3,Def6 .= 0.L .= epq.u9 by A3,Def6; end; end; dom(ep*eq) = NAT by FUNCT_2:def 1 .= dom epq by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:2; end; definition let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, m be Nat, x be Element of L; func Vandermonde(x,m) -> Matrix of m,L means :Def7: for i,j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds it*(i,j) = pow(x,(i-1)*(j-1)); existence proof defpred P[Nat,Nat,set] means $3 = pow(x,(($1)-1)*(($2)-1)); reconsider m9=m as Element of NAT by ORDINAL1:def 12; A1: for i,j being Nat st [i,j] in [:Seg m9, Seg m9:] ex x being Element of L st P[i,j,x]; consider M being Matrix of m9,m9,L such that A2: for i,j being Nat st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_0:sch 2(A1); reconsider M as Matrix of m,m,L; take M; now let i be Nat; assume 1 <= i & i <= m; then A3: Indices M = [:Seg m, Seg m:] & i in Seg m by MATRIX_0:24; let j be Nat; assume 1 <= j & j <= m; then j in Seg m; then [i,j] in Indices M by A3,ZFMISC_1:def 2; hence M*(i,j) = pow(x,(i-1)*(j-1)) by A2; end; hence thesis; end; uniqueness proof let M1,M2 be Matrix of m,L; assume A4: for i,j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds M1*( i,j) = pow(x,(i-1)*(j-1)); assume A5: for i,j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds M2*( i,j) = pow(x,(i-1)*(j-1)); now let i,j be Nat; A6: Indices M1 = [:Seg m, Seg m:] by MATRIX_0:24; assume [i,j] in Indices M1; then ex x,y being object st x in Seg m & y in Seg m & [x,y] = [i,j] by A6, ZFMISC_1:def 2; then consider z,y being set such that A7: [i,j] = [z,y] and A8: z in Seg m and A9: y in Seg m; j = y by A7,XTUPLE_0:1; then A10: 1 <= j & j <= m by A9,FINSEQ_1:1; i = z by A7,XTUPLE_0:1; then A11: 1 <= i & i <= m by A8,FINSEQ_1:1; hence M1*(i,j) = pow(x,(i-1)*(j-1)) by A4,A10 .= M2*(i,j) by A5,A11,A10; end; hence thesis by MATRIX_0:27; end; end; notation let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, m be Nat, x be Element of L; synonym VM(x,m) for Vandermonde(x,m); end; theorem Th35: for L being Field, m,n being Nat st m > 0 for M being Matrix of m,n,L holds 1.(L,m) * M = M proof let L be Field, m,n be Nat; assume A1: m > 0; let M be Matrix of m,n,L; A2: width 1.(L,m) = m by A1,MATRIX_0:23 .= len M by A1,MATRIX_0:23; set M2 = 1.(L,m) * M; A3: len M = m by A1,MATRIX_0:23; len 1.(L,m) = m by A1,MATRIX_0:23; then A4: m = len M2 by A2,MATRIX_3:def 4; A5: now let i,j be Nat; assume A6: [i,j] in Indices M; then A7: i in dom M by ZFMISC_1:87; dom M = Seg len M by FINSEQ_1:def 3 .= dom M2 by A3,A4,FINSEQ_1:def 3; then Indices M = Indices M2 by A2,MATRIX_3:def 4; then A8: M2*(i,j) = Line(1.(L,m),i) "*" Col(M,j) by A2,A6,MATRIX_3:def 4 .= Sum(mlt(Line(1.(L,m),i), Col(M,j))) by FVSUM_1:def 9; len Line(1.(L,m),i) = width 1.(L,m) by MATRIX_0:def 7 .= m by MATRIX_0:24; then A9: dom Line(1.(L,m),i) = Seg(m) by FINSEQ_1:def 3; A10: len M = m by A1,MATRIX_0:23; then A11: i in dom Line(1.(L,m),i) by A7,A9,FINSEQ_1:def 3; A12: Indices 1.(L,m) = [:Seg m,Seg m:] by A1,MATRIX_0:23; then A13: [i,i] in Indices 1.(L,m) by A9,A11,ZFMISC_1:87; A14: for k being Nat st k in dom Line(1.(L,m),i) & k<>i holds Line(1.(L,m) ,i).k = 0.L proof let k be Nat; assume that A15: k in dom Line(1.(L,m),i) and A16: k<>i; A17: [i,k] in Indices 1.(L,m) by A9,A11,A12,A15,ZFMISC_1:87; k in Seg width 1.(L,m) by A9,A15,MATRIX_0:24; then Line(1.(L,m),i).k = 1.(L,m)*(i,k) by MATRIX_0:def 7 .= 0.L by A16,A17,MATRIX_1:def 3; hence thesis; end; len Col(M,j) = len M by MATRIX_0:def 8 .= m by A1,MATRIX_0:23; then dom Col(M,j) = Seg(m) by FINSEQ_1:def 3; then A18: i in dom Col(M,j) by A7,A10,FINSEQ_1:def 3; i in Seg width 1.(L,m) by A9,A11,MATRIX_0:24; then A19: Line(1.(L,m),i).i = 1.(L,m)*(i,i) by MATRIX_0:def 7 .= 1.L by A13,MATRIX_1:def 3; i in dom Line(1.(L,m),i) by A7,A10,A9,FINSEQ_1:def 3; then Sum(mlt(Line(1.(L,m),i),Col(M,j))) = (Col(M,j)).i by A19,A14,A18, MATRIX_3:17; hence M*(i,j) = M2*(i,j) by A8,A7,MATRIX_0:def 8; end; width M = width M2 by A2,MATRIX_3:def 4; hence thesis by A3,A4,A5,MATRIX_0:21; end; theorem Th36: for L being Field, m being Element of NAT st 0 < m for u,v,u1 being Matrix of m,L holds (for i,j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (u * v)*(i,j) = emb(m,L) * (u1*(i,j))) implies u * v = emb(m,L) * u1 proof let L be Field; let m be Element of NAT; assume A1: m > 0; let u,v,u1 be Matrix of m,L; assume A2: for i,j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (u * v) *(i,j) = emb(m,L) * (u1*(i,j)); A3: for i,j being Nat st [i,j] in Indices (u*v) holds (u*v)*(i,j) = (emb(m,L ) * u1)*(i,j) proof let i,j be Nat; A4: [i,j] in Indices (u*v) implies 1 <= i & i <= m & 1 <= j & j <= m proof width u = m by MATRIX_0:24 .= len v by MATRIX_0:24; then A5: width(u*v) = width(v) by MATRIX_3:def 4 .= m by MATRIX_0:24; assume A6: [i,j] in Indices (u*v); then A7: j in Seg m by A5,ZFMISC_1:87; width u = m by MATRIX_0:24 .= len v by MATRIX_0:24; then len(u*v) = len u by MATRIX_3:def 4 .= m by MATRIX_0:24; then (u*v) is Matrix of m,m,L by A1,A5,MATRIX_0:20; then Indices (u*v) = [:Seg m,Seg m:] by A5,MATRIX_0:25; then i in Seg m by A6,ZFMISC_1:87; hence thesis by A7,FINSEQ_1:1; end; assume A8: [i,j] in Indices (u*v); then i in Seg m & j in Seg m by A4; then [i,j] in [:Seg m, Seg m:] by ZFMISC_1:87; then [i,j] in Indices u1 by MATRIX_0:24; then (emb(m,L) * u1)*(i,j) = emb(m,L) * (u1*(i,j)) by MATRIX_3:def 5; hence thesis by A2,A8,A4; end; A9: width(emb(m,L) * u1) = width(u1) by MATRIX_3:def 5 .= m by MATRIX_0:24; width u = m by MATRIX_0:24 .= len v by MATRIX_0:24; then A10: width(u*v) = width(v) by MATRIX_3:def 4 .= m by MATRIX_0:24; width u = m by MATRIX_0:24 .= len v by MATRIX_0:24; then A11: len(u*v) = len u by MATRIX_3:def 4 .= m by MATRIX_0:24; len (emb(m,L) * u1) = len u1 by MATRIX_3:def 5 .= m by MATRIX_0:24; hence thesis by A11,A9,A10,A3,MATRIX_0:21; end; Lm12: for L being Field, m being Element of NAT st m > 0 for p,q being Polynomial of L holds emb(2*m,L) * (1.(L,2*m) * mConv(p*'q, 2*m)) = emb(2*m,L) * mConv(p*'q, 2*m) proof let L be Field, m be Element of NAT; assume A1: m > 0; let p,q be Polynomial of L; 2 * m > 2 * 0 by A1,XREAL_1:68; hence thesis by Th35; end; theorem Th37: for L being Field, x being Element of L, s being FinSequence of L, i,j,m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & for k being Nat st 1 <= k & k <= m holds s /.k = pow(x,(i-j)*(k-1)) holds (VM(x,m) * VM(x",m))*(i,j) = Sum s proof let L be Field, x be Element of L, s be FinSequence of L, i,j,m being Element of NAT; assume that A1: x is_primitive_root_of_degree m and A2: 1 <= i & i <= m and A3: 1 <= j and A4: j <= m and A5: len s = m and A6: for k being Nat st 1 <= k & k <= m holds s/.k = pow(x,(i-j)*(k-1)); len Line(VM(x,m),i) = width VM(x,m) by MATRIX_0:def 7 .= m by MATRIX_0:24 .= len VM(x",m) by MATRIX_0:24 .= len Col(VM(x",m),j) by MATRIX_0:def 8; then A7: len (mlt(Line(VM(x,m), i),Col(VM(x",m),j))) = len (Line(VM(x,m),i)) by MATRIX_3:6 .= width VM(x,m) by MATRIX_0:def 7 .= m by MATRIX_0:24; A8: x <> 0.L by A1,Th30; A9: for k being Nat st 1 <= k & k <= m holds Line(VM(x,m),i)/.k * Col(VM(x" ,m),j)/.k = pow(x, (i-j)*(k-1)) proof len Col(VM(x",m),j) = len VM(x",m) by MATRIX_0:def 8 .= m by MATRIX_0:24; then A10: Seg m = dom Col(VM(x",m),j) by FINSEQ_1:def 3; len Line(VM(x,m),i) = width VM(x,m) by MATRIX_0:def 7 .= m by MATRIX_0:24; then A11: Seg m = dom Line(VM(x,m),i) by FINSEQ_1:def 3; A12: 1 - 1 <= j - 1 by A3,XREAL_1:9; let k be Nat; assume that A13: 1 <= k and A14: k <= m; len VM(x",m) = m & k in Seg m by A13,A14,MATRIX_0:24; then A15: k in dom VM(x",m) by FINSEQ_1:def 3; k in Seg m by A13,A14; then A16: Line(VM(x,m),i)/.k = Line(VM(x,m),i).k by A11,PARTFUN1:def 6; 1 - 1 <= k - 1 by A13,XREAL_1:9; then A17: (j-1)*(k-1) in NAT by A12,INT_1:3; width VM(x,m) = m by MATRIX_0:24; then k in Seg width VM(x,m) by A13,A14; then A18: Line(VM(x,m),i).k = VM(x,m)*(i,k) by MATRIX_0:def 7; k in Seg m by A13,A14; then A19: Col(VM(x",m),j)/.k = Col(VM(x",m),j).k by A10,PARTFUN1:def 6; VM(x",m)*(k,j) = pow(x",(j-1)*(k-1)) by A3,A4,A13,A14,Def7 .= pow(x, -(j-1)*(k-1)) by A8,A17,Th22; then Col(VM(x",m),j).k = pow(x,-(j-1)*(k-1)) by A15,MATRIX_0:def 8; then Line(VM(x,m),i)/.k * Col(VM(x",m),j)/.k = pow(x,(i-1)*(k-1)) * pow(x, -(j-1)*(k-1)) by A2,A13,A14,A16,A18,A19,Def7 .= pow(x, (i-j)*(k-1)) by A8,Th23; hence thesis; end; A20: for k being Nat st 1 <= k & k <= m holds mlt(Line(VM(x,m),i),Col(VM(x", m),j))/.k = s/.k proof len Col(VM(x",m),j) = len VM(x",m) by MATRIX_0:def 8 .= m by MATRIX_0:24; then A21: Seg m = dom Col(VM(x",m),j) by FINSEQ_1:def 3; let k be Nat; len Line(VM(x,m),i) = width VM(x,m) by MATRIX_0:def 7 .= m by MATRIX_0:24; then A22: Seg m = dom Line(VM(x,m),i) by FINSEQ_1:def 3; assume A23: 1 <= k & k <= m; then A24: Line(VM(x,m),i)/.k * Col(VM(x",m),j)/.k = pow(x,(i-j)*(k-1)) by A9 .= s/.k by A6,A23; k in Seg m by A23; then A25: Col(VM(x",m),j).k = Col(VM(x",m),j)/.k by A21,PARTFUN1:def 6; Seg m = dom mlt(Line(VM(x,m),i),Col(VM(x",m),j)) by A7,FINSEQ_1:def 3; then A26: k in dom mlt(Line(VM(x,m),i),Col(VM(x",m),j)) by A23; k in Seg m by A23; then Line(VM(x,m),i).k = Line(VM(x,m),i)/.k by A22,PARTFUN1:def 6; then mlt(Line(VM(x,m),i),Col(VM(x",m),j)).k = Line(VM(x,m),i)/.k * Col(VM( x",m) ,j)/.k by A26,A25,FVSUM_1:60; hence thesis by A26,A24,PARTFUN1:def 6; end; A27: for k being Nat st k in dom mlt(Line(VM(x,m),i),Col(VM(x",m),j)) holds mlt(Line(VM(x,m),i),Col(VM(x",m),j)).k = s.k proof let k be Nat; assume A28: k in dom mlt(Line(VM(x,m),i),Col(VM(x",m),j)); A29: Seg m = dom mlt(Line(VM(x,m),i),Col(VM(x",m),j)) by A7,FINSEQ_1:def 3; then A30: 1 <= k & k <= m by A28,FINSEQ_1:1; A31: k in dom s by A5,A28,A29,FINSEQ_1:def 3; mlt(Line(VM(x,m),i),Col(VM(x",m),j)).k = mlt(Line(VM(x,m),i),Col(VM(x ",m),j))/.k by A28,PARTFUN1:def 6 .= s/.k by A20,A30 .= s.k by A31,PARTFUN1:def 6; hence thesis; end; dom mlt(Line(VM(x,m),i),Col(VM(x",m),j)) = Seg m by A7,FINSEQ_1:def 3 .= dom s by A5,FINSEQ_1:def 3; then A32: Sum(mlt(Line(VM(x,m),i),Col(VM(x",m),j))) = Sum s by A27,FINSEQ_1:13; width VM(x,m) = m by MATRIX_0:24; then A33: width VM(x,m) = len VM(x",m) by MATRIX_0:24; A34: width VM(x,m) = m & len VM(x",m) = m by MATRIX_0:24; len VM(x,m) = m by MATRIX_0:24; then A35: len(VM(x,m) * VM(x",m)) = m by A34,MATRIX_3:def 4; width VM(x",m) = m by MATRIX_0:24; then width (VM(x,m) * VM(x",m)) = m by A34,MATRIX_3:def 4; then (VM(x,m) * VM(x",m)) is Matrix of m,L by A2,A35,MATRIX_0:20; then A36: Indices(VM(x,m) * VM(x",m)) = [:Seg m, Seg m:] by MATRIX_0:24; i in Seg m & j in Seg m by A2,A3,A4; then [i,j] in Indices (VM(x,m) * VM(x",m)) by A36,ZFMISC_1:def 2; then (VM(x,m) * VM(x",m))*(i,j) = Line(VM(x,m),i) "*" Col(VM(x",m),j) by A33, MATRIX_3:def 4; hence thesis by A32,FVSUM_1:def 9; end; theorem Th38: for L being Field, m,i,j being Element of NAT, x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds (VM(x,m) * VM(x",m))*(i,j) = 0.L proof let L be Field, m,i,j be Element of NAT, x be Element of L; assume that A1: i <> j and A2: 1 <= i & i <= m & 1 <= j & j <= m and A3: x is_primitive_root_of_degree m; A4: x <> 0.L by A3,Th30; then A5: pow(x, m*(i-j)) = pow(pow(x, m), i-j) by Th26 .= pow(x|^m, i-j) by Def2 .= pow(1.L, i-j) by A3 .= 1.L by Th16; ex G being FinSequence of L st (dom G = Seg m & for k being Nat st k in Seg m holds G.k = pow(x,(i-j)*(k-1))) proof defpred P[Nat,set] means $2 = pow(x, (i-j)*($1-1)); A6: for n being Nat st n in Seg m holds ex x being Element of L st P[n,x]; ex G be FinSequence of L st dom G = Seg m & for nn be Nat st nn in Seg m holds P[nn,G.nn] from FINSEQ_1:sch 5(A6); hence thesis; end; then consider s being FinSequence of L such that A7: dom s = Seg m and A8: for k being Nat st k in Seg m holds s.k = pow(x,(i-j)*(k-1)); A9: for k being Nat st 1 <= k & k <= m holds s/.k = pow(x,(i-j)*(k-1)) proof let k be Nat; assume A10: 1 <= k & k <= m; then A11: k in dom s by A7; k in Seg m by A10; then pow(x, (i-j)*(k-1)) = s.k by A8 .= s/.k by A11,PARTFUN1:def 6; hence thesis; end; consider r being Element of L such that A12: r = pow(x, i-j); A13: len s = m by A7,FINSEQ_1:def 3; for k being Nat st 1 <= k & k <= len s holds s.k = (pow(x,i-j)) |^ (k-' 1) proof let k be Nat; assume that A14: 1 <= k and A15: k <= len s; A16: 1 - 1 <= k - 1 by A14,XREAL_1:9; s.k = s/.k by A14,A15,FINSEQ_4:15 .= pow(x, (i-j)*(k-1)) by A9,A13,A14,A15 .= pow(x, (i-j)*(k-'1)) by A16,XREAL_0:def 2 .= pow(pow(x,i-j),k-'1) by A4,Th26 .= (pow(x,i-j)) |^ (k-'1) by Def2; hence thesis; end; then Sum s = (1.L-((pow(x, i-j)) |^ (len s)) ) / (1.L-pow(x, i-j)) by A1,A2 ,A3,Th5,Th32 .= (1.L-((pow(x, i-j)) |^ m))/(1.L-pow(x, i-j)) by A7,FINSEQ_1:def 3 .= (1.L - (pow(pow(x,i-j),m))) / (1.L - pow(x,i-j)) by Def2 .= (1.L - (pow(x,(i-j)*m))) / (1.L - pow(x,i-j)) by A4,Th26 .= 0.L / (1.L - r) by A5,A12,VECTSP_1:19 .= 0.L; hence thesis by A2,A3,A9,A13,Th37; end; theorem Th39: for L being Field, m being Element of NAT st m > 0 for x being Element of L st x is_primitive_root_of_degree m holds VM(x,m) * VM(x",m) = emb( m,L) * 1.(L,m) proof let L be Field, m be Element of NAT; assume A1: m > 0; let x be Element of L; assume A2: x is_primitive_root_of_degree m; for i,j being Nat st i >= 1 & i <= m & j >= 1 & j <= m holds (VM(x,m) * VM(x",m))*(i,j) = emb(m,L) * (1.(L,m)*(i,j)) proof let i,j be Nat; A3: i in NAT & j in NAT by ORDINAL1:def 12; ex G being FinSequence of L st (dom G = Seg m & for k being Nat st k in Seg m holds G.k = pow(x, (i-j)*(k-1))) proof defpred P[Nat,set] means $2 = pow(x, (i-j)*($1-1)); A4: for n being Nat st n in Seg m holds ex x being Element of L st P[n,x ]; ex G be FinSequence of L st dom G = Seg m & for nn be Nat st nn in Seg m holds P[nn,G.nn] from FINSEQ_1:sch 5(A4); hence thesis; end; then consider s being FinSequence of L such that A5: dom s = Seg m and A6: for k being Nat st k in Seg m holds s.k = pow(x, (i-j)*(k-1)); A7: len s = m by A5,FINSEQ_1:def 3; A8: for k being Nat st 1 <= k & k <= m holds s/.k = pow(x, (i-j)*(k-1)) proof let k be Nat; assume A9: 1 <= k & k <= m; then A10: k in dom s by A5; k in Seg m by A9; then pow(x, (i-j)*(k-1)) = s.k by A6 .= s/.k by A10,PARTFUN1:def 6; hence thesis; end; A11: Indices 1.(L,m) = [:Seg m, Seg m:] by MATRIX_0:24; assume that A12: 1 <= i & i <= m and A13: 1 <= j & j <= m; per cases; suppose A14: i = j; A15: for k being Element of NAT st 1 <= k & k <= m holds s/.k = 1.L proof let k be Element of NAT; assume 1 <= k & k <= m; then s/.k = pow(x, (i-j)*(k-1)) by A8 .= 1.L by A14,Th13; hence thesis; end; i in Seg m by A12; then A16: [i,i] in Indices 1.(L,m) by A11,ZFMISC_1:87; (VM(x,m) * VM(x",m))*(i,j) = Sum s by A2,A3,A12,A13,A7,A8,Th37 .= m * 1.L by A7,A15,Th4 .= emb(m,L) * 1.L; hence thesis by A14,A16,MATRIX_1:def 3; end; suppose A17: i <> j; i in Seg m & j in Seg m by A12,A13; then A18: [i,j] in Indices 1.(L,m) by A11,ZFMISC_1:87; (VM(x,m) * VM(x",m))*(i,j) = 0.L by A2,A3,A12,A13,A17,Th38 .= emb(m,L) * 0.L; hence thesis by A17,A18,MATRIX_1:def 3; end; end; hence thesis by A1,Th36; end; theorem Th40: for L being Field, m being Element of NAT, x being Element of L st m > 0 & x is_primitive_root_of_degree m holds VM(x,m) * VM(x",m) = VM(x",m) * VM(x,m) proof let L be Field; let m be Element of NAT; let x be Element of L; assume that 0 < m and A1: x is_primitive_root_of_degree m; x <> 0.L by A1,Th30; then VM(x",m) * VM(x,m) = VM(x",m) * VM((x")",m) by VECTSP_1:24 .= emb(m,L) * 1.(L,m) by A1,Th31,Th39; hence thesis by A1,Th39; end; begin :: DFT-Multiplication of Polynomials theorem Th41: for L being Field, p being Polynomial of L, m being Element of NAT st m > 0 & len p <= m for x being Element of L, i being Element of NAT st i < m holds DFT(p,x,m).i = VM(x,m) * mConv(p,m)*(i+1,1) proof let L be Field; let p be Polynomial of L; let m be Element of NAT; assume that A1: m > 0 and A2: len p <= m; let x be Element of L; set v = VM(x,m); for i being Element of NAT st i < m holds (DFT(p, x, m)).i = (v * mConv( p, m))*(i+1,1) proof A3: for k being Nat st k < m holds Col(mConv(p,m),1).(k+1) = p.k proof let k be Nat; assume A4: k < m; then 1 <= k+1 & k+1 <= m by NAT_1:11,13; then A5: (k+1) in Seg m; len (mConv(p, m)) = m by A1,Th28; then (k+1) in dom (mConv(p, m)) by A5,FINSEQ_1:def 3; then Col(mConv(p, m), 1).(k+1) = (mConv(p, m))*(k+1,1) by MATRIX_0:def 8; hence thesis by A4,Th28; end; A6: width v = m by MATRIX_0:24 .= len (mConv(p, m)) by A1,Th28; then A7: len (v * mConv(p, m)) = len v by MATRIX_3:def 4 .= m by MATRIX_0:24; width (v * mConv(p, m)) = width (mConv(p, m)) by A6,MATRIX_3:def 4 .= 1 by A1,Th28; then v * mConv(p, m) is Matrix of m,1,L by A1,A7,MATRIX_0:20; then A8: Indices (v * mConv(p, m)) = [:Seg m, Seg width(v * mConv(p, m)):] by MATRIX_0:25; A9: len mConv(p,m) = m by A1,Th28 .= width v by MATRIX_0:24; width (v * mConv(p, m)) = width (mConv(p, m)) by A6,MATRIX_3:def 4 .= 1 by A1,Th28; then A10: 1 in Seg width(v * mConv(p, m)); let i be Element of NAT; assume A11: i < m; A12: for k being Nat st k < m holds Line(v,i+1).(k+1) = v*(i+1,k+1) proof let k be Nat; assume k < m; then 1 <= k+1 & k+1 <= m by NAT_1:11,13; then (k+1) in Seg m; then (k+1) in Seg width v by MATRIX_0:24; hence thesis by MATRIX_0:def 7; end; A13: for k being Nat st k < m holds Line(v,i+1).(k+1) = pow(x,i*k) proof let k be Nat; assume A14: k < m; then A15: 1 <= k+1 & k+1 <= m by NAT_1:11,13; A16: 1 <= i+1 & i+1 <= m by A11,NAT_1:11,13; Line(v, i+1).(k+1) = v*(i+1,k+1) by A12,A14 .= pow(x, ((i+1)-1)*((k+1)-1)) by A16,A15,Def7 .= pow(x, i*k); hence thesis; end; A17: for k being Nat, a,b,c being Element of L st a = Line(v, i+1).(k+1) & b = Col(mConv(p, m), 1).(k+1) & c = p.k holds k < m implies a*b = pow(x, i*k) * c proof let k be Nat; let a,b,c be Element of L; assume that A18: a = Line(v, i+1).(k+1) and A19: b = Col(mConv(p,m),1).(k+1) & c = p.k and A20: k < m; a = pow(x, i*k) by A13,A18,A20; hence thesis by A3,A19,A20; end; A21: for k being Element of NAT st 1 <= k & k <= m holds (mlt(Line(v, i+1) ,Col(mConv(p, m), 1))).k = p.(k-'1) * (power L).(x|^i,k-'1) proof A22: len mConv(p, m) = m by A1,Th28; let k be Element of NAT; assume that A23: 1 <= k and A24: k <= m; k in Seg m by A23,A24; then k in dom mConv(p, m) by A22,FINSEQ_1:def 3; then A25: Col(mConv(p, m), 1).k = (mConv(p, m))*(k,1) by MATRIX_0:def 8; 0 < k by A23; then dom p = NAT & k-1 is Element of NAT by FUNCT_2:def 1,NAT_1:20; then A26: p.(k-1) = p/.(k-1) by PARTFUN1:def 6; Seg width v = Seg m by MATRIX_0:24; then k in Seg width v by A23,A24; then Line(v, i+1).k = v*(i+1,k) by MATRIX_0:def 7; then reconsider a = Line(v, i+1).k, b = Col(mConv(p, m), 1).k, c = p.(k-1) as Element of L by A25,A26; len Line(v, i+1) = width v by MATRIX_0:def 7 .= m by MATRIX_0:24 .= len mConv(p, m) by A1,Th28 .= len (Col(mConv(p, m), 1)) by MATRIX_0:def 8; then len (mlt(Line(v, i+1),Col(mConv(p, m), 1))) = len (Line(v, i+1)) by MATRIX_3:6 .= width v by MATRIX_0:def 7 .= m by MATRIX_0:24; then dom (mlt(Line(v, i+1),Col(mConv(p, m), 1))) = Seg m by FINSEQ_1:def 3; then k in dom (mlt(Line(v, i+1),Col(mConv(p, m), 1))) by A23,A24; then A27: (mlt(Line(v, i+1),Col(mConv(p, m), 1))).k = a * b by FVSUM_1:60; A28: a*b = pow(x, i*(k-1)) * c proof A29: 0 < k by A23; then A30: k-1 is Nat by NAT_1:20; k-1 <= m-1 & m-1 is Nat by A1,A24,NAT_1:20,XREAL_1:9; then A31: k-1 < (m-1)+1 by A30,NAT_1:13; reconsider l=k-1 as Nat by A29,NAT_1:20; a = Line(v, i+1).(l+1); hence thesis by A17,A31; end; reconsider d = pow(x, i*(k-1)) as Element of L; A32: k - 1 >= 0 by A23,NAT_1:20; d = pow(x|^i, k-1) by A23,Th27 .= (power L).(x|^i, k-1) by A32,Def2 .= (power L).(x|^i,k-'1) by A32,XREAL_0:def 2; hence thesis by A28,A27,A32,XREAL_0:def 2; end; A33: Sum(mlt(Line(v, i+1),Col(mConv(p, m), 1))) = eval(p, x|^i) proof A34: for k being Nat st len p < k & k <= m holds (mlt(Line(v, i+1),Col( mConv(p, m), 1))).k = 0.L proof A35: 1 <= 1 + len p by NAT_1:11; let k be Nat; assume that A36: len p < k and A37: k <= m; A38: len p < (k - 1) + 1 by A36; len p + 1 <= k by A36,NAT_1:13; then A39: 1 <= k by A35,XXREAL_0:2; then 1 - 1 <= k - 1 by XREAL_1:9; then k-'1 = k - 1 by XREAL_0:def 2; then A40: k-'1 >= len p by A38,NAT_1:13; k in NAT by ORDINAL1:def 12; then (mlt(Line(v, i+1),Col(mConv(p, m), 1))).k = p.(k-'1) * (power L). (x|^i,k-'1) by A21,A37,A39 .= 0.L * ((power L).(x|^i,k-'1)) by A40,ALGSEQ_1:8 .= 0.L; hence thesis; end; len (Line(v, i+1)) = width v by MATRIX_0:def 7 .= m by MATRIX_0:24 .= len (mConv(p, m)) by A1,Th28 .= len (Col(mConv(p, m), 1)) by MATRIX_0:def 8; then A41: len (mlt(Line(v, i+1),Col(mConv(p, m), 1))) = len (Line(v, i+1)) by MATRIX_3:6 .= width v by MATRIX_0:def 7 .= m by MATRIX_0:24; len p - len p <= m - len p by A2,XREAL_1:9; then reconsider lengthG = m - len p as Element of NAT by INT_1:3; consider F being FinSequence of L such that A42: eval(p, x|^i) = Sum F and A43: len F = len p and A44: for k being Element of NAT st k in dom F holds F.k = p.(k-'1) * ( power L).(x|^i,k-'1) by POLYNOM4:def 2; ex G being FinSequence of L st (dom G = Seg lengthG & for k being Nat st k in Seg lengthG holds G.k = 0.L) proof defpred P[set,set] means $2 = 0.L; A45: for n being Nat st n in Seg lengthG holds ex x being Element of L st P[n,x]; ex G be FinSequence of L st dom G = Seg lengthG & for nn be Nat st nn in Seg lengthG holds P[nn,G.nn] from FINSEQ_1:sch 5(A45); hence thesis; end; then consider G being FinSequence of L such that A46: dom G = Seg lengthG and A47: for k being Nat st k in Seg lengthG holds G.k = 0.L; A48: for k being Element of NAT st k in Seg lengthG holds G.k = 0.L by A47; A49: len G = m - len p by A46,FINSEQ_1:def 3; then len F + len G = m by A43; then dom (F ^ G) = Seg m by FINSEQ_1:def 7; then A50: dom (mlt(Line(v, i+1),Col(mConv(p, m), 1))) = dom (F ^ G) by A41, FINSEQ_1:def 3; A51: for k being Element of NAT st 1 <= k & k <= len p holds F.k = (mlt( Line(v, i+1),Col(mConv(p, m), 1))).k proof let k be Element of NAT; assume that A52: 1 <= k and A53: k <= len p; A54: k <= m by A2,A53,XXREAL_0:2; dom F = Seg len p by A43,FINSEQ_1:def 3; then k in dom F by A52,A53; then F.k = p.(k-'1) * (power L).(x|^i,k-'1) by A44 .= (mlt(Line(v, i+1),Col(mConv(p, m), 1))).k by A21,A52,A54; hence thesis; end; for k being Nat st k in dom (mlt(Line(v, i+1),Col(mConv(p, m), 1)) ) holds (mlt(Line(v, i+1),Col(mConv(p, m), 1))).k = (F ^ G).k proof let k be Nat; len F + len G = m by A43,A49; then A55: dom (F ^ G) = Seg m by FINSEQ_1:def 7; assume A56: k in dom mlt(Line(v,i+1),Col(mConv(p,m),1)); per cases by A50,A56,A55,FINSEQ_1:1; suppose A57: 1 <= k & k <= len F; then k in dom F by FINSEQ_3:25; then (F ^ G).k = F.k by FINSEQ_1:def 7 .= (mlt(Line(v,i+1),Col(mConv(p,m),1))).k by A43,A51,A56,A57; hence thesis; end; suppose A58: len F < k & k <= m; then len F + 1 <= k by NAT_1:13; then (len F + 1) - len F <= k - len F by XREAL_1:9; then reconsider l = k - len F as Element of NAT by INT_1:3; len p - m <= m - m by A2,XREAL_1:9; then -(len p - m) >= 0; then reconsider lengthG = m - len p as Element of NAT by INT_1:3; len F + 1 <= k by A58,NAT_1:13; then A59: (len F + 1) - len F <= k - len F by XREAL_1:9; l <= lengthG by A43,A58,XREAL_1:9; then A60: l in dom G by A46,A59; len F + len G = m by A43,A49; then dom (F ^ G) = Seg m by FINSEQ_1:def 7; then len (F ^ G) = m by FINSEQ_1:def 3; then (F ^ G).k = G.(k - len F) by A58,FINSEQ_1:24 .= 0.L by A46,A47,A60 .= (mlt(Line(v, i+1),Col(mConv(p,m), 1))).k by A43,A34,A58; hence thesis; end; end; then mlt(Line(v, i+1),Col(mConv(p, m), 1)) = F ^ G by A50,FINSEQ_1:13; then Sum(mlt(Line(v, i+1),Col(mConv(p, m), 1))) = Sum(F) + Sum(G) by RLVECT_1:41 .= Sum(F) + 0.L by A46,A48,POLYNOM3:1 .= eval(p, x|^i) by A42,RLVECT_1:def 4; hence thesis; end; A61: Line(v, i+1) "*" Col(mConv(p, m), 1) = Sum(mlt(Line(v,i+1),Col(mConv( p, m), 1))) by FVSUM_1:def 9; 1 <= i+1 & i+1 <= m by A11,NAT_1:11,13; then (i+1) in Seg m; then [i+1,1] in Indices (v * mConv(p, m)) by A8,A10,ZFMISC_1:def 2; then (v * mConv(p, m))*(i+1,1) = eval(p, x|^i) by A9,A61,A33,MATRIX_3:def 4 ; hence thesis by A11,Def6; end; hence thesis; end; theorem Th42: for L being Field, p being Polynomial of L for m being Nat st 0 < m & len p <= m for x being Element of L holds DFT(p,x,m) = aConv(VM(x,m) * mConv(p, m)) proof let L be Field; let p be Polynomial of L; let m be Nat; assume that A1: 0 < m and A2: len p <= m; let x be Element of L; A3: m in NAT by ORDINAL1:def 12; A4: now let u9 be object; assume u9 in dom DFT(p, x, m); then reconsider u = u9 as Element of NAT by FUNCT_2:def 1; per cases; suppose A5: u < m; width VM(x,m) = m by MATRIX_0:24 .= len mConv(p,m) by A1,Th28; then A6: len (VM(x,m) * mConv(p,m)) = len VM(x,m) by MATRIX_3:def 4 .= m by MATRIX_0:24; thus (DFT(p,x,m)).u9 = (VM(x,m)*mConv(p,m))*(u+1,1) by A3,A2,A5,Th41 .= (aConv(VM(x,m)*mConv(p, m))).u9 by A5,A6,Def4; end; suppose A7: m <= u; width VM(x,m) = m by MATRIX_0:24 .= len (mConv(p, m)) by A1,Th28; then A8: len (VM(x,m) * mConv(p, m)) = len VM(x,m) by MATRIX_3:def 4 .= m by MATRIX_0:24; thus (DFT(p, x, m)).u9 = 0.L by A7,Def6 .= (aConv(VM(x,m) * mConv(p, m))).u9 by A7,A8,Def4; end; end; dom DFT(p, x, m) = NAT by FUNCT_2:def 1 .= dom (aConv(VM(x,m) * mConv(p,m))) by FUNCT_2:def 1; hence thesis by A4,FUNCT_1:2; end; theorem Th43: for L being Field, p,q being Polynomial of L, m being Element of NAT st m > 0 & len p <= m & len q <= m for x being Element of L st x is_primitive_root_of_degree 2*m holds DFT(DFT(p*'q, x, 2*m), x", 2*m) = emb(2*m ,L) * (p*'q) proof let L be Field; let p,q be Polynomial of L; let m be Element of NAT; assume that A1: m > 0 and A2: len p <= m & len q <= m; let x be Element of L; assume A3: x is_primitive_root_of_degree 2*m; per cases; suppose A4: len p = 0 or len q = 0; per cases by A4; suppose len p = 0; then p = 0_.L by POLYNOM4:5; then p *' q = 0_.L by POLYNOM3:34; then emb(2*m,L) * (p*'q) = 0_.L & DFT(DFT(p*'q, x, 2*m), x", 2*m) = DFT( 0_.L, x", 2*m) by Th33,POLYNOM5:28; hence thesis by Th33; end; suppose len q = 0; then q = 0_.L by POLYNOM4:5; then p *' q = 0_.L by POLYNOM3:34; then emb(2*m,L) * (p*'q) = 0_.L & DFT(DFT(p*'q, x, 2*m), x", 2*m) = DFT( 0_.L, x", 2*m) by Th33,POLYNOM5:28; hence thesis by Th33; end; end; suppose A5: len p <> 0 & len q <> 0; set v1 = VM(x,2*m), v2 = VM(x",2*m); A6: len p + len q <= m + m by A2,XREAL_1:7; len (p*'q) <= len p + len q by A5,Th9; then A7: len (p*'q) <= 2*m by A6,XXREAL_0:2; A8: for i being Nat st i < 2*m holds (v1 * mConv(p*'q,2*m))*(i+1,1) = ( DFT(p*'q,x,2*m)).i proof let i be Nat; i in NAT by ORDINAL1:def 12; hence thesis by A7,Th41; end; for i being Nat st i >= 2*m holds DFT(p*'q,x,2*m).i = 0.L by Def6; then 2*m is_at_least_length_of DFT(p*'q, x, 2*m) by ALGSEQ_1:def 2; then A9: len DFT(p*'q, x, 2*m) <= 2*m by ALGSEQ_1:def 3; A10: width v2 = 2*m by MATRIX_0:24 .= len v1 by MATRIX_0:24; A11: m + m <> 0 by A1; A12: v2 * v1 = v1 * v2 by A3,Th40 .= emb(2*m,L) * 1.(L,2*m) by A3,Th39; A13: now let u9 be object; assume u9 in dom(aConv(emb(2*m,L) * mConv(p*'q, 2*m))); then reconsider u = u9 as Element of NAT by FUNCT_2:def 1; per cases; suppose A14: u < 2*m; then 0+1 <= u+1 & u+1 <= 2*m by NAT_1:13; then A15: u+1 in Seg (2*m); len (mConv(p*'q, 2*m)) = 2*m by A11,Th28; then A16: dom (mConv(p*'q, 2*m)) = Seg (2*m) by FINSEQ_1:def 3; Seg width (mConv(p*'q, 2*m)) = Seg 1 & 1 in Seg 1 by A11,Th28; then A17: [u+1,1] in Indices mConv(p*'q, 2*m) by A16,A15,ZFMISC_1:87; len (emb(2*m,L) * mConv(p*'q, 2*m)) = len (mConv(p*'q, 2*m)) by MATRIX_3:def 5 .= 2*m by A11,Th28; hence (aConv(emb(2*m,L) * mConv(p*'q, 2*m))).u9 = (emb(2*m,L) * mConv(p *'q, 2*m))*(u+1, 1) by A14,Def4 .= emb(2*m,L) * ((mConv(p*'q, 2*m))*(u+1, 1)) by A17,MATRIX_3:def 5 .= emb(2*m,L) * (p*'q).u by A14,Th28 .= (emb(2*m,L) * (p*'q)).u9 by POLYNOM5:def 4; end; suppose A18: 2*m <= u; len (emb(2*m,L) * mConv(p*'q, 2*m)) = len (mConv(p*'q, 2*m)) by MATRIX_3:def 5 .= 2*m by A11,Th28; hence (aConv(emb(2*m,L) * mConv(p*'q, 2*m))).u9 = 0.L by A18,Def4 .= emb(2*m,L) * 0.L .= emb(2*m,L) * (p*'q).u by A7,A18,ALGSEQ_1:8,XXREAL_0:2 .= (emb(2*m,L) * (p*'q)).u9 by POLYNOM5:def 4; end; end; dom (aConv(emb(2*m,L) * mConv(p*'q, 2*m))) = NAT by FUNCT_2:def 1 .= dom (emb(2*m,L) * (p*'q)) by FUNCT_2:def 1; then A19: aConv(emb(2*m,L) * mConv(p*'q, 2*m)) = emb(2*m,L) * (p*'q) by A13, FUNCT_1:2; A20: len mConv(p*'q,2*m) = 2*m by A11,Th28 .= width v1 by MATRIX_0:24; then A21: len (v1 * mConv(p*'q, 2*m)) = len v1 by MATRIX_3:def 4 .= 2*m by MATRIX_0:24; width(v1 * mConv(p*'q, 2*m)) = width(mConv(p*'q,2*m)) by A20,MATRIX_3:def 4 .= 1 by A11,Th28; then v1 * mConv(p*'q,2*m) is Matrix of 2*m,1,L by A11,A21,MATRIX_0:20; then aConv(v2 * mConv(DFT(p*'q,x,2*m), 2*m)) = aConv(v2 * (v1 * mConv(p*'q ,2*m))) by A11,A8,Th29 .= aConv((v2 * v1) * mConv(p*'q,2*m)) by A10,A20,MATRIX_3:33 .= aConv(emb(2*m,L)*(1.(L,2*m)*mConv(p*'q,2*m))) by A11,A12,Th6 .= aConv(emb(2*m,L) * mConv(p*'q, 2*m)) by A1,Lm12; hence thesis by A11,A9,A19,Th42; end; end; ::$N Multiplication of Polynomials using Discrete Fourier Transformation theorem for L being Field, p,q being Polynomial of L, m being Element of NAT st m > 0 & len p <= m & len q <= m for x being Element of L st x is_primitive_root_of_degree 2*m holds emb(2*m,L) <> 0.L implies (emb(2*m,L))" * DFT(DFT(p,x,2*m) * DFT(q,x,2*m), x", 2*m) = p *' q proof let L be Field; let p,q be Polynomial of L; let m be Element of NAT; assume A1: m > 0 & len p <= m & len q <= m; let x be Element of L; assume A2: x is_primitive_root_of_degree 2*m; assume A3: emb(2*m,L) <> 0.L; (emb(2*m,L))" * DFT(DFT(p,x,2*m) * DFT(q,x,2*m), x", 2*m) = (emb(2*m,L)) " * DFT(DFT(p*'q,x,2*m), x", 2*m) by Th34 .= (emb(2*m,L))" * (emb(2*m,L) * (p*'q)) by A1,A2,Th43 .= ((emb(2*m,L))" * emb(2*m,L)) * (p*'q) by Th10 .= 1.L * (p*'q) by A3,VECTSP_1:def 10 .= p*'q by POLYNOM5:27; hence thesis; end;