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 holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (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 holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (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 holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) )
assume that
A1: m > 0 and
A2: ( len p <= m & len q <= m ) ; :: thesis: 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)
let x be Element of L; :: thesis: ( x is_primitive_root_of_degree 2 * m implies DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) )
assume A3: x is_primitive_root_of_degree 2 * m ; :: thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
per cases ( len p = 0 or len q = 0 or ( len p <> 0 & len q <> 0 ) ) ;
suppose A4: ( len p = 0 or len q = 0 ) ; :: thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
per cases ( len p = 0 or len q = 0 ) by A4;
suppose len p = 0 ; :: thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
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 DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by Th33; :: thesis: verum
end;
suppose len q = 0 ; :: thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
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 DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by Th33; :: thesis: verum
end;
end;
end;
suppose A5: ( len p <> 0 & len q <> 0 ) ; :: thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)
set v1 = VM (x,(2 * m));
set 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
((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i
proof
let i be Nat; :: thesis: ( i < 2 * m implies ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i )
i in NAT by ORDINAL1:def 12;
hence ( i < 2 * m implies ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i ) by A7, Th41; :: thesis: verum
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 (VM ((x "),(2 * m))) = 2 * m by MATRIX_0:24
.= len (VM (x,(2 * m))) by MATRIX_0:24 ;
A11: m + m <> 0 by A1;
A12: (VM ((x "),(2 * m))) * (VM (x,(2 * m))) = (VM (x,(2 * m))) * (VM ((x "),(2 * m))) by A3, Th40
.= (emb ((2 * m),L)) * (1. (L,(2 * m))) by A3, Th39 ;
A13: now :: thesis: for u9 being object st u9 in dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) holds
(aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . u9 = ((emb ((2 * m),L)) * (p *' q)) . u9
let u9 be object ; :: thesis: ( u9 in dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) implies (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1 )
assume u9 in dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) ; :: thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1
then reconsider u = u9 as Element of NAT by FUNCT_2:def 1;
per cases ( u < 2 * m or 2 * m <= u ) ;
suppose A14: u < 2 * m ; :: thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1
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 ;
:: thesis: verum
end;
suppose A18: 2 * m <= u ; :: thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1
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 ;
:: thesis: verum
end;
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 (VM (x,(2 * m))) by MATRIX_0:24 ;
then A21: len ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) = len (VM (x,(2 * m))) by MATRIX_3:def 4
.= 2 * m by MATRIX_0:24 ;
width ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) = width (mConv ((p *' q),(2 * m))) by A20, MATRIX_3:def 4
.= 1 by A11, Th28 ;
then (VM (x,(2 * m))) * (mConv ((p *' q),(2 * m))) is Matrix of 2 * m,1,L by A11, A21, MATRIX_0:20;
then aConv ((VM ((x "),(2 * m))) * (mConv ((DFT ((p *' q),x,(2 * m))),(2 * m)))) = aConv ((VM ((x "),(2 * m))) * ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m))))) by A11, A8, Th29
.= aConv (((VM ((x "),(2 * m))) * (VM (x,(2 * m)))) * (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 DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by A11, A9, A19, Th42; :: thesis: verum
end;
end;