let L be Field; :: thesis: for p being Polynomial of L

for m being Nat st 0 < m & len p <= m holds

for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

let p be Polynomial of L; :: thesis: for m being Nat st 0 < m & len p <= m holds

for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

let m be Nat; :: thesis: ( 0 < m & len p <= m implies for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) )

assume that

A1: 0 < m and

A2: len p <= m ; :: thesis: for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

let x be Element of L; :: thesis: DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

A3: m in NAT by ORDINAL1:def 12;

.= dom (aConv ((VM (x,m)) * (mConv (p,m)))) by FUNCT_2:def 1 ;

hence DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) by A4, FUNCT_1:2; :: thesis: verum

for m being Nat st 0 < m & len p <= m holds

for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

let p be Polynomial of L; :: thesis: for m being Nat st 0 < m & len p <= m holds

for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

let m be Nat; :: thesis: ( 0 < m & len p <= m implies for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) )

assume that

A1: 0 < m and

A2: len p <= m ; :: thesis: for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

let x be Element of L; :: thesis: DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

A3: m in NAT by ORDINAL1:def 12;

A4: now :: thesis: for u9 being object st u9 in dom (DFT (p,x,m)) holds

(DFT (p,x,m)) . u9 = (aConv ((VM (x,m)) * (mConv (p,m)))) . u9

dom (DFT (p,x,m)) =
NAT
by FUNCT_2:def 1
(DFT (p,x,m)) . u9 = (aConv ((VM (x,m)) * (mConv (p,m)))) . u9

let u9 be object ; :: thesis: ( u9 in dom (DFT (p,x,m)) implies (DFT (p,x,m)) . b_{1} = (aConv ((VM (x,m)) * (mConv (p,m)))) . b_{1} )

assume u9 in dom (DFT (p,x,m)) ; :: thesis: (DFT (p,x,m)) . b_{1} = (aConv ((VM (x,m)) * (mConv (p,m)))) . b_{1}

then reconsider u = u9 as Element of NAT by FUNCT_2:def 1;

end;assume u9 in dom (DFT (p,x,m)) ; :: thesis: (DFT (p,x,m)) . b

then reconsider u = u9 as Element of NAT by FUNCT_2:def 1;

per cases
( u < m or m <= u )
;

end;

suppose A5:
u < m
; :: thesis: (DFT (p,x,m)) . b_{1} = (aConv ((VM (x,m)) * (mConv (p,m)))) . b_{1}

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 ; :: thesis: verum

end;.= 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 ; :: thesis: verum

suppose A7:
m <= u
; :: thesis: (DFT (p,x,m)) . b_{1} = (aConv ((VM (x,m)) * (mConv (p,m)))) . b_{1}

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 ; :: thesis: verum

end;.= 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 ; :: thesis: verum

.= dom (aConv ((VM (x,m)) * (mConv (p,m)))) by FUNCT_2:def 1 ;

hence DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) by A4, FUNCT_1:2; :: thesis: verum