# Metamath Proof Explorer

## Theorem plyremlem

Description: Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis plyrem.1 ${⊢}{G}={X}^{p}{-}_{f}\left(ℂ×\left\{{A}\right\}\right)$
Assertion plyremlem ${⊢}{A}\in ℂ\to \left({G}\in \mathrm{Poly}\left(ℂ\right)\wedge \mathrm{deg}\left({G}\right)=1\wedge {{G}}^{-1}\left[\left\{0\right\}\right]=\left\{{A}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 plyrem.1 ${⊢}{G}={X}^{p}{-}_{f}\left(ℂ×\left\{{A}\right\}\right)$
2 ssid ${⊢}ℂ\subseteq ℂ$
3 ax-1cn ${⊢}1\in ℂ$
4 plyid ${⊢}\left(ℂ\subseteq ℂ\wedge 1\in ℂ\right)\to {X}^{p}\in \mathrm{Poly}\left(ℂ\right)$
5 2 3 4 mp2an ${⊢}{X}^{p}\in \mathrm{Poly}\left(ℂ\right)$
6 plyconst ${⊢}\left(ℂ\subseteq ℂ\wedge {A}\in ℂ\right)\to ℂ×\left\{{A}\right\}\in \mathrm{Poly}\left(ℂ\right)$
7 2 6 mpan ${⊢}{A}\in ℂ\to ℂ×\left\{{A}\right\}\in \mathrm{Poly}\left(ℂ\right)$
8 plysubcl ${⊢}\left({X}^{p}\in \mathrm{Poly}\left(ℂ\right)\wedge ℂ×\left\{{A}\right\}\in \mathrm{Poly}\left(ℂ\right)\right)\to {X}^{p}{-}_{f}\left(ℂ×\left\{{A}\right\}\right)\in \mathrm{Poly}\left(ℂ\right)$
9 5 7 8 sylancr ${⊢}{A}\in ℂ\to {X}^{p}{-}_{f}\left(ℂ×\left\{{A}\right\}\right)\in \mathrm{Poly}\left(ℂ\right)$
10 1 9 eqeltrid ${⊢}{A}\in ℂ\to {G}\in \mathrm{Poly}\left(ℂ\right)$
11 negcl ${⊢}{A}\in ℂ\to -{A}\in ℂ$
12 addcom ${⊢}\left(-{A}\in ℂ\wedge {z}\in ℂ\right)\to -{A}+{z}={z}+\left(-{A}\right)$
13 11 12 sylan ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to -{A}+{z}={z}+\left(-{A}\right)$
14 negsub ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to {z}+\left(-{A}\right)={z}-{A}$
15 14 ancoms ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to {z}+\left(-{A}\right)={z}-{A}$
16 13 15 eqtrd ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to -{A}+{z}={z}-{A}$
17 16 mpteq2dva ${⊢}{A}\in ℂ\to \left({z}\in ℂ⟼-{A}+{z}\right)=\left({z}\in ℂ⟼{z}-{A}\right)$
18 cnex ${⊢}ℂ\in \mathrm{V}$
19 18 a1i ${⊢}{A}\in ℂ\to ℂ\in \mathrm{V}$
20 negex ${⊢}-{A}\in \mathrm{V}$
21 20 a1i ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to -{A}\in \mathrm{V}$
22 simpr ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to {z}\in ℂ$
23 fconstmpt ${⊢}ℂ×\left\{-{A}\right\}=\left({z}\in ℂ⟼-{A}\right)$
24 23 a1i ${⊢}{A}\in ℂ\to ℂ×\left\{-{A}\right\}=\left({z}\in ℂ⟼-{A}\right)$
25 df-idp ${⊢}{X}^{p}={\mathrm{I}↾}_{ℂ}$
26 mptresid ${⊢}{\mathrm{I}↾}_{ℂ}=\left({z}\in ℂ⟼{z}\right)$
27 25 26 eqtri ${⊢}{X}^{p}=\left({z}\in ℂ⟼{z}\right)$
28 27 a1i ${⊢}{A}\in ℂ\to {X}^{p}=\left({z}\in ℂ⟼{z}\right)$
29 19 21 22 24 28 offval2 ${⊢}{A}\in ℂ\to \left(ℂ×\left\{-{A}\right\}\right){+}_{f}{X}^{p}=\left({z}\in ℂ⟼-{A}+{z}\right)$
30 simpl ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to {A}\in ℂ$
31 fconstmpt ${⊢}ℂ×\left\{{A}\right\}=\left({z}\in ℂ⟼{A}\right)$
32 31 a1i ${⊢}{A}\in ℂ\to ℂ×\left\{{A}\right\}=\left({z}\in ℂ⟼{A}\right)$
33 19 22 30 28 32 offval2 ${⊢}{A}\in ℂ\to {X}^{p}{-}_{f}\left(ℂ×\left\{{A}\right\}\right)=\left({z}\in ℂ⟼{z}-{A}\right)$
34 17 29 33 3eqtr4d ${⊢}{A}\in ℂ\to \left(ℂ×\left\{-{A}\right\}\right){+}_{f}{X}^{p}={X}^{p}{-}_{f}\left(ℂ×\left\{{A}\right\}\right)$
35 34 1 syl6eqr ${⊢}{A}\in ℂ\to \left(ℂ×\left\{-{A}\right\}\right){+}_{f}{X}^{p}={G}$
36 35 fveq2d ${⊢}{A}\in ℂ\to \mathrm{deg}\left(\left(ℂ×\left\{-{A}\right\}\right){+}_{f}{X}^{p}\right)=\mathrm{deg}\left({G}\right)$
37 plyconst ${⊢}\left(ℂ\subseteq ℂ\wedge -{A}\in ℂ\right)\to ℂ×\left\{-{A}\right\}\in \mathrm{Poly}\left(ℂ\right)$
38 2 11 37 sylancr ${⊢}{A}\in ℂ\to ℂ×\left\{-{A}\right\}\in \mathrm{Poly}\left(ℂ\right)$
39 5 a1i ${⊢}{A}\in ℂ\to {X}^{p}\in \mathrm{Poly}\left(ℂ\right)$
40 0dgr ${⊢}-{A}\in ℂ\to \mathrm{deg}\left(ℂ×\left\{-{A}\right\}\right)=0$
41 11 40 syl ${⊢}{A}\in ℂ\to \mathrm{deg}\left(ℂ×\left\{-{A}\right\}\right)=0$
42 0lt1 ${⊢}0<1$
43 41 42 eqbrtrdi ${⊢}{A}\in ℂ\to \mathrm{deg}\left(ℂ×\left\{-{A}\right\}\right)<1$
44 eqid ${⊢}\mathrm{deg}\left(ℂ×\left\{-{A}\right\}\right)=\mathrm{deg}\left(ℂ×\left\{-{A}\right\}\right)$
45 dgrid ${⊢}\mathrm{deg}\left({X}^{p}\right)=1$
46 45 eqcomi ${⊢}1=\mathrm{deg}\left({X}^{p}\right)$
47 44 46 dgradd2 ${⊢}\left(ℂ×\left\{-{A}\right\}\in \mathrm{Poly}\left(ℂ\right)\wedge {X}^{p}\in \mathrm{Poly}\left(ℂ\right)\wedge \mathrm{deg}\left(ℂ×\left\{-{A}\right\}\right)<1\right)\to \mathrm{deg}\left(\left(ℂ×\left\{-{A}\right\}\right){+}_{f}{X}^{p}\right)=1$
48 38 39 43 47 syl3anc ${⊢}{A}\in ℂ\to \mathrm{deg}\left(\left(ℂ×\left\{-{A}\right\}\right){+}_{f}{X}^{p}\right)=1$
49 36 48 eqtr3d ${⊢}{A}\in ℂ\to \mathrm{deg}\left({G}\right)=1$
50 1 33 syl5eq ${⊢}{A}\in ℂ\to {G}=\left({z}\in ℂ⟼{z}-{A}\right)$
51 50 fveq1d ${⊢}{A}\in ℂ\to {G}\left({z}\right)=\left({z}\in ℂ⟼{z}-{A}\right)\left({z}\right)$
52 51 adantr ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to {G}\left({z}\right)=\left({z}\in ℂ⟼{z}-{A}\right)\left({z}\right)$
53 ovex ${⊢}{z}-{A}\in \mathrm{V}$
54 eqid ${⊢}\left({z}\in ℂ⟼{z}-{A}\right)=\left({z}\in ℂ⟼{z}-{A}\right)$
55 54 fvmpt2 ${⊢}\left({z}\in ℂ\wedge {z}-{A}\in \mathrm{V}\right)\to \left({z}\in ℂ⟼{z}-{A}\right)\left({z}\right)={z}-{A}$
56 22 53 55 sylancl ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to \left({z}\in ℂ⟼{z}-{A}\right)\left({z}\right)={z}-{A}$
57 52 56 eqtrd ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to {G}\left({z}\right)={z}-{A}$
58 57 eqeq1d ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to \left({G}\left({z}\right)=0↔{z}-{A}=0\right)$
59 subeq0 ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to \left({z}-{A}=0↔{z}={A}\right)$
60 59 ancoms ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to \left({z}-{A}=0↔{z}={A}\right)$
61 58 60 bitrd ${⊢}\left({A}\in ℂ\wedge {z}\in ℂ\right)\to \left({G}\left({z}\right)=0↔{z}={A}\right)$
62 61 pm5.32da ${⊢}{A}\in ℂ\to \left(\left({z}\in ℂ\wedge {G}\left({z}\right)=0\right)↔\left({z}\in ℂ\wedge {z}={A}\right)\right)$
63 plyf ${⊢}{G}\in \mathrm{Poly}\left(ℂ\right)\to {G}:ℂ⟶ℂ$
64 ffn ${⊢}{G}:ℂ⟶ℂ\to {G}Fnℂ$
65 fniniseg ${⊢}{G}Fnℂ\to \left({z}\in {{G}}^{-1}\left[\left\{0\right\}\right]↔\left({z}\in ℂ\wedge {G}\left({z}\right)=0\right)\right)$
66 10 63 64 65 4syl ${⊢}{A}\in ℂ\to \left({z}\in {{G}}^{-1}\left[\left\{0\right\}\right]↔\left({z}\in ℂ\wedge {G}\left({z}\right)=0\right)\right)$
67 eleq1a ${⊢}{A}\in ℂ\to \left({z}={A}\to {z}\in ℂ\right)$
68 67 pm4.71rd ${⊢}{A}\in ℂ\to \left({z}={A}↔\left({z}\in ℂ\wedge {z}={A}\right)\right)$
69 62 66 68 3bitr4d ${⊢}{A}\in ℂ\to \left({z}\in {{G}}^{-1}\left[\left\{0\right\}\right]↔{z}={A}\right)$
70 velsn ${⊢}{z}\in \left\{{A}\right\}↔{z}={A}$
71 69 70 syl6bbr ${⊢}{A}\in ℂ\to \left({z}\in {{G}}^{-1}\left[\left\{0\right\}\right]↔{z}\in \left\{{A}\right\}\right)$
72 71 eqrdv ${⊢}{A}\in ℂ\to {{G}}^{-1}\left[\left\{0\right\}\right]=\left\{{A}\right\}$
73 10 49 72 3jca ${⊢}{A}\in ℂ\to \left({G}\in \mathrm{Poly}\left(ℂ\right)\wedge \mathrm{deg}\left({G}\right)=1\wedge {{G}}^{-1}\left[\left\{0\right\}\right]=\left\{{A}\right\}\right)$