Description: Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | plycj.1 | |
|
plycj.2 | |
||
coecj.3 | |
||
Assertion | coecj | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | plycj.1 | |
|
2 | plycj.2 | |
|
3 | coecj.3 | |
|
4 | cjcl | |
|
5 | 4 | adantl | |
6 | plyssc | |
|
7 | 6 | sseli | |
8 | 1 2 5 7 | plycj | |
9 | dgrcl | |
|
10 | 1 9 | eqeltrid | |
11 | cjf | |
|
12 | 3 | coef3 | |
13 | fco | |
|
14 | 11 12 13 | sylancr | |
15 | fvco3 | |
|
16 | 12 15 | sylan | |
17 | cj0 | |
|
18 | 17 | eqcomi | |
19 | 18 | a1i | |
20 | 16 19 | eqeq12d | |
21 | 12 | ffvelrnda | |
22 | 0cnd | |
|
23 | cj11 | |
|
24 | 21 22 23 | syl2anc | |
25 | 20 24 | bitrd | |
26 | 25 | necon3bid | |
27 | 3 1 | dgrub2 | |
28 | plyco0 | |
|
29 | 10 12 28 | syl2anc | |
30 | 27 29 | mpbid | |
31 | 30 | r19.21bi | |
32 | 26 31 | sylbid | |
33 | 32 | ralrimiva | |
34 | plyco0 | |
|
35 | 10 14 34 | syl2anc | |
36 | 33 35 | mpbird | |
37 | 1 2 3 | plycjlem | |
38 | 8 10 14 36 37 | coeeq | |