Metamath Proof Explorer


Theorem coecj

Description: Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plycj.1 N=degF
plycj.2 G=*F*
coecj.3 A=coeffF
Assertion coecj FPolyScoeffG=*A

Proof

Step Hyp Ref Expression
1 plycj.1 N=degF
2 plycj.2 G=*F*
3 coecj.3 A=coeffF
4 cjcl xx
5 4 adantl FPolySxx
6 plyssc PolySPoly
7 6 sseli FPolySFPoly
8 1 2 5 7 plycj FPolySGPoly
9 dgrcl FPolySdegF0
10 1 9 eqeltrid FPolySN0
11 cjf *:
12 3 coef3 FPolySA:0
13 fco *:A:0*A:0
14 11 12 13 sylancr FPolyS*A:0
15 fvco3 A:0k0*Ak=Ak
16 12 15 sylan FPolySk0*Ak=Ak
17 cj0 0=0
18 17 eqcomi 0=0
19 18 a1i FPolySk00=0
20 16 19 eqeq12d FPolySk0*Ak=0Ak=0
21 12 ffvelrnda FPolySk0Ak
22 0cnd FPolySk00
23 cj11 Ak0Ak=0Ak=0
24 21 22 23 syl2anc FPolySk0Ak=0Ak=0
25 20 24 bitrd FPolySk0*Ak=0Ak=0
26 25 necon3bid FPolySk0*Ak0Ak0
27 3 1 dgrub2 FPolySAN+1=0
28 plyco0 N0A:0AN+1=0k0Ak0kN
29 10 12 28 syl2anc FPolySAN+1=0k0Ak0kN
30 27 29 mpbid FPolySk0Ak0kN
31 30 r19.21bi FPolySk0Ak0kN
32 26 31 sylbid FPolySk0*Ak0kN
33 32 ralrimiva FPolySk0*Ak0kN
34 plyco0 N0*A:0*AN+1=0k0*Ak0kN
35 10 14 34 syl2anc FPolyS*AN+1=0k0*Ak0kN
36 33 35 mpbird FPolyS*AN+1=0
37 1 2 3 plycjlem FPolySG=zk=0N*Akzk
38 8 10 14 36 37 coeeq FPolyScoeffG=*A