:: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation
:: by Krzysztof Treyderowski and Christoph Schwarzweller
::
:: Received October 12, 2006
:: Copyright (c) 2006-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;