let L be Field; :: thesis: for p being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m holds
for x being Element of L
for i being Element of NAT st i < m holds
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1
let p be Polynomial of L; :: thesis: for m being Element of NAT st m > 0 & len p <= m holds
for x being Element of L
for i being Element of NAT st i < m holds
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1
let m be Element of NAT ; :: thesis: ( m > 0 & len p <= m implies for x being Element of L
for i being Element of NAT st i < m holds
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1 )
assume A1: ( m > 0 & len p <= m ) ; :: thesis: for x being Element of L
for i being Element of NAT st i < m holds
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1
let x be Element of L; :: thesis: for i being Element of NAT st i < m holds
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1
set v = VM x,m;
for 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 i be Element of NAT ; :: thesis: ( i < m implies (DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1 )
assume A2: i < m ; :: thesis: (DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1
((VM x,m) * (mConv p,m)) * (i + 1),1 = eval p,(x |^ i)

proof

A3: [(i + 1),1] in Indices ((VM x,m) * (mConv p,m))

proof

A4: width (VM x,m) = m by MATRIX_1:25
.= len (mConv p,m) by A1, Th28 ;
(VM x,m) * (mConv p,m) is Matrix of m,1,L

proof

A5: len ((VM x,m) * (mConv p,m)) = len (VM x,m) by A4, MATRIX_3:def 4
.= m by MATRIX_1:25 ;
width ((VM x,m) * (mConv p,m)) = width (mConv p,m) by A4, MATRIX_3:def 4
.= 1 by A1, Th28 ;
hence (VM x,m) * (mConv p,m) is Matrix of m,1,L by A1, A5, MATRIX_1:20; :: thesis: verum

end;

then A6: Indices ((VM x,m) * (mConv p,m)) = [:(Seg m),(Seg (width ((VM x,m) * (mConv p,m)))):] by MATRIX_1:26;
A7: 1 <= i + 1 by NAT_1:11;
i + 1 <= m by A2, NAT_1:13;
then A8: i + 1 in Seg m by A7;
width ((VM x,m) * (mConv p,m)) = width (mConv p,m) by A4, MATRIX_3:def 4
.= 1 by A1, Th28 ;
then 1 in Seg (width ((VM x,m) * (mConv p,m))) ;
hence [(i + 1),1] in Indices ((VM x,m) * (mConv p,m)) by A6, A8, ZFMISC_1:def 2; :: thesis: verum

end;

A9: len (mConv p,m) = m by A1, Th28
.= width (VM x,m) by MATRIX_1:25 ;
A10: (Line (VM x,m),(i + 1)) "*" (Col (mConv p,m),1) = Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) by FVSUM_1:def 10;
Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = eval p,(x |^ i)

proof

A11: for k being Nat st k < m holds
(Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),(k + 1)

proof

let k be Nat; :: thesis: ( k < m implies (Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),(k + 1) )
assume A12: k < m ; :: thesis: (Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),(k + 1)
k + 1 in Seg m

proof

A13: 1 <= k + 1 by NAT_1:11;
k + 1 <= m by A12, NAT_1:13;
hence k + 1 in Seg m by A13; :: thesis: verum

end;

then k + 1 in Seg (width (VM x,m)) by MATRIX_1:25;
hence (Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),(k + 1) by MATRIX_1:def 8; :: thesis: verum

end;

A14: for k being Nat st k < m holds
(Line (VM x,m),(i + 1)) . (k + 1) = pow x,(i * k)

proof

let k be Nat; :: thesis: ( k < m implies (Line (VM x,m),(i + 1)) . (k + 1) = pow x,(i * k) )
assume A15: k < m ; :: thesis: (Line (VM x,m),(i + 1)) . (k + 1) = pow x,(i * k)
A16: ( 1 <= i + 1 & i + 1 <= m ) by A2, NAT_1:11, NAT_1:13;
A17: ( 1 <= k + 1 & k + 1 <= m ) by A15, NAT_1:11, NAT_1:13;
(Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),(k + 1) by A11, A15
.= pow x,(((i + 1) - 1) * ((k + 1) - 1)) by A16, A17, Def8
.= pow x,(i * k) ;
hence (Line (VM x,m),(i + 1)) . (k + 1) = pow x,(i * k) ; :: thesis: verum

end;

A18: for k being Nat st k < m holds
(Col (mConv p,m),1) . (k + 1) = p . k

proof

let k be Nat; :: thesis: ( k < m implies (Col (mConv p,m),1) . (k + 1) = p . k )
assume A19: k < m ; :: thesis: (Col (mConv p,m),1) . (k + 1) = p . k
(Col (mConv p,m),1) . (k + 1) = (mConv p,m) * (k + 1),1

proof

k + 1 in dom (mConv p,m)

proof

A20: len (mConv p,m) = m by A1, Th28;
( 1 <= k + 1 & k + 1 <= m ) by A19, NAT_1:11, NAT_1:13;
then k + 1 in Seg m ;
hence k + 1 in dom (mConv p,m) by A20, FINSEQ_1:def 3; :: thesis: verum

end;

hence (Col (mConv p,m),1) . (k + 1) = (mConv p,m) * (k + 1),1 by MATRIX_1:def 9; :: thesis: verum

end;

hence (Col (mConv p,m),1) . (k + 1) = p . k by A19, Th28; :: thesis: verum

end;

A21: for k being Nat
for a, b, c being Element of L st a = (Line (VM x,m),(i + 1)) . (k + 1) & b = (Col (mConv p,m),1) . (k + 1) & c = p . k & k < m holds
a * b = (pow x,(i * k)) * c

proof

let k be Nat; :: thesis: for a, b, c being Element of L st a = (Line (VM x,m),(i + 1)) . (k + 1) & b = (Col (mConv p,m),1) . (k + 1) & c = p . k & k < m holds
a * b = (pow x,(i * k)) * c
let a, b, c be Element of L; :: thesis: ( a = (Line (VM x,m),(i + 1)) . (k + 1) & b = (Col (mConv p,m),1) . (k + 1) & c = p . k & k < m implies a * b = (pow x,(i * k)) * c )
assume A22: ( a = (Line (VM x,m),(i + 1)) . (k + 1) & b = (Col (mConv p,m),1) . (k + 1) & c = p . k & k < m ) ; :: thesis: a * b = (pow x,(i * k)) * c
then a = pow x,(i * k) by A14;
hence a * b = (pow x,(i * k)) * c by A18, A22; :: thesis: verum

end;

A23: for k being Element of NAT st 1 <= k & k <= m holds
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1))

proof

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= m implies (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1)) )
assume A24: ( 1 <= k & k <= m ) ; :: thesis: (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1))
k in Seg (width (VM x,m))

proof

Seg (width (VM x,m)) = Seg m by MATRIX_1:25;
hence k in Seg (width (VM x,m)) by A24; :: thesis: verum

end;

then A25: (Line (VM x,m),(i + 1)) . k = (VM x,m) * (i + 1),k by MATRIX_1:def 8;
A26: len (mConv p,m) = m by A1, Th28;
k in Seg m by A24;
then k in dom (mConv p,m) by A26, FINSEQ_1:def 3;
then A27: (Col (mConv p,m),1) . k = (mConv p,m) * k,1 by MATRIX_1:def 9;
A28: dom p = NAT by FUNCT_2:def 1;
0 < k by A24;
then k - 1 is Element of NAT by NAT_1:20;
then p . (k - 1) = p /. (k - 1) by A28, PARTFUN1:def 8;
then reconsider a = (Line (VM x,m),(i + 1)) . k, b = (Col (mConv p,m),1) . k, c = p . (k - 1) as Element of L by A25, A27;
A29: a * b = (pow x,(i * (k - 1))) * c

proof

A30: 0 < k by A24;
then A31: k - 1 is Nat by NAT_1:20;
reconsider l = k - 1 as Nat by A30, NAT_1:20;
A32: k - 1 <= m - 1 by A24, XREAL_1:11;
m - 1 is Nat by A1, NAT_1:20;
then A33: k - 1 < (m - 1) + 1 by A31, A32, NAT_1:13;
( a = (Line (VM x,m),(i + 1)) . (l + 1) & c = p . l ) ;
hence a * b = (pow x,(i * (k - 1))) * c by A21, A33; :: thesis: verum

end;

A34: (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = a * b

proof

k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1))

proof

len (Line (VM x,m),(i + 1)) = width (VM x,m) by MATRIX_1:def 8
.= m by MATRIX_1:25
.= len (mConv p,m) by A1, Th28
.= len (Col (mConv p,m),1) by MATRIX_1:def 9 ;
then len (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = len (Line (VM x,m),(i + 1)) by MATRIX_3:8
.= width (VM x,m) by MATRIX_1:def 8
.= m by MATRIX_1:25 ;
then dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = Seg m by FINSEQ_1:def 3;
hence k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) by A24; :: thesis: verum

end;

hence (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = a * b by FVSUM_1:73; :: thesis: verum

end;

A35: k - 1 >= 0 by A24, NAT_1:20;
reconsider d = pow x,(i * (k - 1)) as Element of L ;
d = pow (x |^ i),(k - 1) by A24, Th27
.= (power L) . (x |^ i),(k - 1) by A35, Def3
.= (power L) . (x |^ i),(k -' 1) by A35, XREAL_0:def 2 ;
hence (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1)) by A29, A34, A35, XREAL_0:def 2; :: thesis: verum

end;

Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = eval p,(x |^ i)

proof

consider F being FinSequence of L such that
A36: ( eval p,(x |^ i) = Sum F & len F = len p & ( 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;
A37: for k being Element of NAT st 1 <= k & k <= len p holds
F . k = (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k

proof

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len p implies F . k = (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k )
assume A38: ( 1 <= k & k <= len p ) ; :: thesis: F . k = (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k
dom F = Seg (len p) by A36, FINSEQ_1:def 3;
then A39: k in dom F by A38;
A40: ( 1 <= k & k <= m ) by A1, A38, XXREAL_0:2;
F . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1)) by A36, A39
.= (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k by A23, A40 ;
hence F . k = (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k ; :: thesis: verum

end;

A41: for k being Nat st len p < k & k <= m holds
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = 0. L

proof

let k be Nat; :: thesis: ( len p < k & k <= m implies (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = 0. L )
assume A42: ( len p < k & k <= m ) ; :: thesis: (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = 0. L
A43: ( 1 <= k & k <= m )

proof

A44: (len p) + 1 <= k by A42, NAT_1:13;
1 <= 1 + (len p) by NAT_1:11;
hence ( 1 <= k & k <= m ) by A42, A44, XXREAL_0:2; :: thesis: verum

end;

A45: k -' 1 >= len p

proof

1 - 1 <= k - 1 by A43, XREAL_1:11;
then A46: k -' 1 = k - 1 by XREAL_0:def 2;
len p < (k - 1) + 1 by A42;
hence k -' 1 >= len p by A46, NAT_1:13; :: thesis: verum

end;

k in NAT by ORDINAL1:def 13;
then (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1)) by A23, A43
.= (0. L) * ((power L) . (x |^ i),(k -' 1)) by A45, ALGSEQ_1:22
.= 0. L by VECTSP_1:39 ;
hence (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = 0. L ; :: thesis: verum

end;

(len p) - (len p) <= m - (len p) by A1, XREAL_1:11;
then reconsider lengthG = m - (len p) as Element of NAT by INT_1:16;
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 S₁[ set , set ] means $2 = 0. L;
A47: for n being Nat st n in Seg lengthG holds
ex x being Element of L st S₁[n,x] ;
ex G being FinSequence of L st
( dom G = Seg lengthG & ( for nn being Nat st nn in Seg lengthG holds
S₁[nn,G . nn] ) ) from FINSEQ_1:sch 5(A47);
hence 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 ) ) ; :: thesis: verum

end;

then consider G being FinSequence of L such that
A48: ( dom G = Seg lengthG & ( for k being Nat st k in Seg lengthG holds
G . k = 0. L ) ) ;
A49: for k being Element of NAT st k in Seg lengthG holds
G . k = 0. L by A48;
A50: ( len G = m - (len p) & ( for k being Element of NAT st k in dom G holds
G . k = 0. L ) ) by A48, FINSEQ_1:def 3;
mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1) = F ^ G

proof

A51: dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = dom (F ^ G)

proof

len (Line (VM x,m),(i + 1)) = width (VM x,m) by MATRIX_1:def 8
.= m by MATRIX_1:25
.= len (mConv p,m) by A1, Th28
.= len (Col (mConv p,m),1) by MATRIX_1:def 9 ;
then A52: len (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = len (Line (VM x,m),(i + 1)) by MATRIX_3:8
.= width (VM x,m) by MATRIX_1:def 8
.= m by MATRIX_1:25 ;
(len F) + (len G) = m by A36, A50;
then dom (F ^ G) = Seg m by FINSEQ_1:def 7;
hence dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = dom (F ^ G) by A52, FINSEQ_1:def 3; :: thesis: verum

end;

for k being Nat st k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) holds
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k

proof

let k be Nat; :: thesis: ( k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) implies (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k )
assume A53: k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) ; :: thesis: (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k
(len F) + (len G) = m by A36, A50;
then A54: dom (F ^ G) = Seg m by FINSEQ_1:def 7;

per cases ( ( 1 <= k & k <= len F ) or ( len F < k & k <= m ) ) by A51, A53, A54, FINSEQ_1:3;

suppose A55: ( 1 <= k & k <= len F ) ; :: thesis: (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k

then k in dom F by FINSEQ_3:27;
then (F ^ G) . k = F . k by FINSEQ_1:def 7
.= (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k by A36, A37, A53, A55 ;
hence (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k ; :: thesis: verum

end;

suppose A56: ( len F < k & k <= m ) ; :: thesis: (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k

(len F) + (len G) = m by A36, A50;
then dom (F ^ G) = Seg m by FINSEQ_1:def 7;
then A57: len (F ^ G) = m by FINSEQ_1:def 3;
(len F) + 1 <= k by A56, NAT_1:13;
then ((len F) + 1) - (len F) <= k - (len F) by XREAL_1:11;
then reconsider l = k - (len F) as Element of NAT by INT_1:16;
(len p) - m <= m - m by A1, XREAL_1:11;
then (len p) - m <= - 0 ;
then - ((len p) - m) >= 0 ;
then reconsider lengthG = m - (len p) as Element of NAT by INT_1:16;
(len F) + 1 <= k by A56, NAT_1:13;
then ((len F) + 1) - (len F) <= k - (len F) by XREAL_1:11;
then ( 1 <= l & l <= lengthG ) by A36, A56, XREAL_1:11;
then A58: l in dom G by A48;
(F ^ G) . k = G . (k - (len F)) by A56, A57, FINSEQ_1:37
.= 0. L by A48, A58
.= (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k by A36, A41, A56 ;
hence (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k ; :: thesis: verum

end;

end;

end;

hence mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1) = F ^ G by A51, FINSEQ_1:17; :: thesis: verum

end;

then Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = (Sum F) + (Sum G) by RLVECT_1:58
.= (Sum F) + (0. L) by A48, A49, POLYNOM3:1
.= eval p,(x |^ i) by A36, RLVECT_1:def 7 ;
hence Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = eval p,(x |^ i) ; :: thesis: verum

end;

hence Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = eval p,(x |^ i) ; :: thesis: verum

end;

hence ((VM x,m) * (mConv p,m)) * (i + 1),1 = eval p,(x |^ i) by A3, A9, A10, MATRIX_3:def 4; :: thesis: verum

end;

hence (DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1 by A2, Def7; :: thesis: verum

end;

hence for i being Element of NAT st i < m holds
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1 ; :: thesis: verum