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 10
.= p *' q by POLYNOM5:27 ;
hence ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q ; :: thesis: verum