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 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 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 A2: 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 A3: ( 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 A3;

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:8;
then A4: p *' q = 0_. L by POLYNOM3:35;
then A5: (emb (2 * m),L) * (p *' q) = 0_. L by POLYNOM5:29;
DFT (DFT (p *' q),x,(2 * m)),(x " ),(2 * m) = DFT (0_. L),(x " ),(2 * m) by A4, Th33;
hence DFT (DFT (p *' q),x,(2 * m)),(x " ),(2 * m) = (emb (2 * m),L) * (p *' q) by A5, 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:8;
then A6: p *' q = 0_. L by POLYNOM3:35;
then A7: (emb (2 * m),L) * (p *' q) = 0_. L by POLYNOM5:29;
DFT (DFT (p *' q),x,(2 * m)),(x " ),(2 * m) = DFT (0_. L),(x " ),(2 * m) by A6, Th33;
hence DFT (DFT (p *' q),x,(2 * m)),(x " ),(2 * m) = (emb (2 * m),L) * (p *' q) by A7, Th33; :: thesis: verum

end;

end;

end;

suppose ( len p <> 0 & len q <> 0 ) ; :: thesis: DFT (DFT (p *' q),x,(2 * m)),(x " ),(2 * m) = (emb (2 * m),L) * (p *' q)

then A8: ( len p > 0 & len q > 0 ) ;
A9: m + m <> 0 by A1;
then A10: 0 < 2 * m ;
set v1 = VM x,(2 * m);
set v2 = VM (x " ),(2 * m);
A11: width (VM (x " ),(2 * m)) = 2 * m by MATRIX_1:25
.= len (VM x,(2 * m)) by MATRIX_1:25 ;
A12: len (mConv (p *' q),(2 * m)) = 2 * m by A10, Th28
.= width (VM x,(2 * m)) by MATRIX_1:25 ;
A13: (VM (x " ),(2 * m)) * (VM x,(2 * m)) = (VM x,(2 * m)) * (VM (x " ),(2 * m)) by A2, A10, Th40
.= (emb (2 * m),L) * (1. L,(2 * m)) by A2, A10, Th39 ;
A14: len (DFT (p *' q),x,(2 * m)) <= 2 * m

proof

for i being Nat st i >= 2 * m holds
(DFT (p *' q),x,(2 * m)) . i = 0. L by Def7;
then 2 * m is_at_least_length_of DFT (p *' q),x,(2 * m) by ALGSEQ_1:def 3;
hence len (DFT (p *' q),x,(2 * m)) <= 2 * m by ALGSEQ_1:def 4; :: thesis: verum

end;

A15: len ((VM x,(2 * m)) * (mConv (p *' q),(2 * m))) = len (VM x,(2 * m)) by A12, MATRIX_3:def 4
.= 2 * m by MATRIX_1:25 ;
A16: width ((VM x,(2 * m)) * (mConv (p *' q),(2 * m))) = width (mConv (p *' q),(2 * m)) by A12, MATRIX_3:def 4
.= 1 by A10, Th28 ;
A17: len (p *' q) <= (len p) + (len q) by A8, Th9;
(len p) + (len q) <= m + m by A1, XREAL_1:9;
then A18: len (p *' q) <= 2 * m by A17, XXREAL_0:2;
A19: 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 13;
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 A18, Th41; :: thesis: verum

end;

(VM x,(2 * m)) * (mConv (p *' q),(2 * m)) is Matrix of 2 * m,1,L by A10, A15, A16, MATRIX_1:20;
then A20: 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 A10, A19, Th29
.= aConv (((VM (x " ),(2 * m)) * (VM x,(2 * m))) * (mConv (p *' q),(2 * m))) by A11, A12, MATRIX_3:35
.= aConv ((emb (2 * m),L) * ((1. L,(2 * m)) * (mConv (p *' q),(2 * m)))) by A10, A13, Th6
.= aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m))) by A1, Lm12 ;
aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m))) = (emb (2 * m),L) * (p *' q)

proof

A21: 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 ;

now

let u' be set ; :: thesis: ( u' in dom (aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m)))) implies (aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m)))) . b₁ = ((emb (2 * m),L) * (p *' q)) . b₁ )
assume u' in dom (aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m)))) ; :: thesis: (aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m)))) . b₁ = ((emb (2 * m),L) * (p *' q)) . b₁
then reconsider u = u' as Element of NAT by FUNCT_2:def 1;

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

suppose A22: u < 2 * m ; :: thesis: (aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m)))) . b₁ = ((emb (2 * m),L) * (p *' q)) . b₁

A23: len ((emb (2 * m),L) * (mConv (p *' q),(2 * m))) = len (mConv (p *' q),(2 * m)) by MATRIX_3:def 5
.= 2 * m by A10, Th28 ;
A24: [(u + 1),1] in Indices (mConv (p *' q),(2 * m))

proof

len (mConv (p *' q),(2 * m)) = 2 * m by A10, Th28;
then A25: dom (mConv (p *' q),(2 * m)) = Seg (2 * m) by FINSEQ_1:def 3;
A26: 0 + 1 <= u + 1 by XREAL_1:8;
u + 1 <= 2 * m by A22, NAT_1:13;
then A27: u + 1 in Seg (2 * m) by A26;
A28: Seg (width (mConv (p *' q),(2 * m))) = Seg 1 by A10, Th28;
1 in Seg 1 ;
hence [(u + 1),1] in Indices (mConv (p *' q),(2 * m)) by A25, A27, A28, ZFMISC_1:106; :: thesis: verum

end;

thus (aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m)))) . u' = ((emb (2 * m),L) * (mConv (p *' q),(2 * m))) * (u + 1),1 by A22, A23, Def5
.= (emb (2 * m),L) * ((mConv (p *' q),(2 * m)) * (u + 1),1) by A24, MATRIX_3:def 5
.= (emb (2 * m),L) * ((p *' q) . u) by A22, Th28
.= ((emb (2 * m),L) * (p *' q)) . u' by POLYNOM5:def 3 ; :: thesis: verum

end;

suppose A29: 2 * m <= u ; :: thesis: (aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m)))) . b₁ = ((emb (2 * m),L) * (p *' q)) . b₁

len ((emb (2 * m),L) * (mConv (p *' q),(2 * m))) = len (mConv (p *' q),(2 * m)) by MATRIX_3:def 5
.= 2 * m by A10, Th28 ;
hence (aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m)))) . u' = 0. L by A29, Def5
.= (emb (2 * m),L) * (0. L) by VECTSP_1:36
.= (emb (2 * m),L) * ((p *' q) . u) by A18, A29, ALGSEQ_1:22, XXREAL_0:2
.= ((emb (2 * m),L) * (p *' q)) . u' by POLYNOM5:def 3 ;
:: thesis: verum

end;

end;

end;

hence aConv ((emb (2 * m),L) * (mConv (p *' q),(2 * m))) = (emb (2 * m),L) * (p *' q) by A21, FUNCT_1:9; :: thesis: verum

end;

hence DFT (DFT (p *' q),x,(2 * m)),(x " ),(2 * m) = (emb (2 * m),L) * (p *' q) by A9, A14, A20, Th42; :: thesis: verum

end;

end;