let L be Field; :: thesis: for p, q being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m & emb (2 * m),L <> 0. L holds
((emb (2 * m),L) " ) * (DFT ((DFT p,x,(2 * m)) * (DFT q,x,(2 * m))),(x " ),(2 * m)) = p *' q
let p, q be Polynomial of L; :: thesis: for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m & emb (2 * m),L <> 0. L holds
((emb (2 * m),L) " ) * (DFT ((DFT p,x,(2 * m)) * (DFT q,x,(2 * m))),(x " ),(2 * m)) = p *' q
let m be Element of NAT ; :: thesis: ( m > 0 & len p <= m & len q <= m implies for x being Element of L st x is_primitive_root_of_degree 2 * m & emb (2 * m),L <> 0. L holds
((emb (2 * m),L) " ) * (DFT ((DFT p,x,(2 * m)) * (DFT q,x,(2 * m))),(x " ),(2 * m)) = p *' q )
assume A1: ( m > 0 & len p <= m & len q <= m ) ; :: thesis: for x being Element of L st x is_primitive_root_of_degree 2 * m & emb (2 * m),L <> 0. L holds
((emb (2 * m),L) " ) * (DFT ((DFT p,x,(2 * m)) * (DFT q,x,(2 * m))),(x " ),(2 * m)) = p *' q
let x be Element of L; :: thesis: ( x is_primitive_root_of_degree 2 * m & 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 )
assume A2: x is_primitive_root_of_degree 2 * m ; :: thesis: ( not emb (2 * m),L <> 0. L or ((emb (2 * m),L) " ) * (DFT ((DFT p,x,(2 * m)) * (DFT q,x,(2 * m))),(x " ),(2 * m)) = p *' q )
assume A3: emb (2 * m),L <> 0. L ; :: thesis: ((emb (2 * m),L) " ) * (DFT ((DFT p,x,(2 * m)) * (DFT q,x,(2 * m))),(x " ),(2 * m)) = p *' q
((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 22
.= p *' q by POLYNOM5:28 ;
hence ((emb (2 * m),L) " ) * (DFT ((DFT p,x,(2 * m)) * (DFT q,x,(2 * m))),(x " ),(2 * m)) = p *' q ; :: thesis: verum