Metamath Proof Explorer


Theorem plycj

Description: The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on ( *z ) independently of z .) (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plycj.2 G = * F *
plycj.3 φ x S x S
plycj.4 φ F Poly S
Assertion plycj φ G Poly S

Proof

Step Hyp Ref Expression
1 plycj.2 G = * F *
2 plycj.3 φ x S x S
3 plycj.4 φ F Poly S
4 eqid deg F = deg F
5 eqid coeff F = coeff F
6 4 1 5 plycjlem F Poly S G = z k = 0 deg F * coeff F k z k
7 3 6 syl φ G = z k = 0 deg F * coeff F k z k
8 plybss F Poly S S
9 3 8 syl φ S
10 0cnd φ 0
11 10 snssd φ 0
12 9 11 unssd φ S 0
13 dgrcl F Poly S deg F 0
14 3 13 syl φ deg F 0
15 5 coef F Poly S coeff F : 0 S 0
16 3 15 syl φ coeff F : 0 S 0
17 elfznn0 k 0 deg F k 0
18 fvco3 coeff F : 0 S 0 k 0 * coeff F k = coeff F k
19 16 17 18 syl2an φ k 0 deg F * coeff F k = coeff F k
20 ffvelcdm coeff F : 0 S 0 k 0 coeff F k S 0
21 16 17 20 syl2an φ k 0 deg F coeff F k S 0
22 2 ralrimiva φ x S x S
23 fveq2 x = coeff F k x = coeff F k
24 23 eleq1d x = coeff F k x S coeff F k S
25 24 rspccv x S x S coeff F k S coeff F k S
26 22 25 syl φ coeff F k S coeff F k S
27 elsni coeff F k 0 coeff F k = 0
28 27 fveq2d coeff F k 0 coeff F k = 0
29 cj0 0 = 0
30 28 29 eqtrdi coeff F k 0 coeff F k = 0
31 fvex coeff F k V
32 31 elsn coeff F k 0 coeff F k = 0
33 30 32 sylibr coeff F k 0 coeff F k 0
34 33 a1i φ coeff F k 0 coeff F k 0
35 26 34 orim12d φ coeff F k S coeff F k 0 coeff F k S coeff F k 0
36 elun coeff F k S 0 coeff F k S coeff F k 0
37 elun coeff F k S 0 coeff F k S coeff F k 0
38 35 36 37 3imtr4g φ coeff F k S 0 coeff F k S 0
39 38 adantr φ k 0 deg F coeff F k S 0 coeff F k S 0
40 21 39 mpd φ k 0 deg F coeff F k S 0
41 19 40 eqeltrd φ k 0 deg F * coeff F k S 0
42 12 14 41 elplyd φ z k = 0 deg F * coeff F k z k Poly S 0
43 7 42 eqeltrd φ G Poly S 0
44 plyun0 Poly S 0 = Poly S
45 43 44 eleqtrdi φ G Poly S