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 ℂ × A
Assertion plyremlem ⊢ A ∈ ℂ → G ∈ Poly ⁡ ℂ ∧ deg ⁡ G = 1 ∧ G -1 0 = A

Proof

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