Metamath Proof Explorer

Theorem fta1lem

Description: Lemma for fta1 . (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses fta1.1 ⊢ R = F -1 0
fta1.2 ⊢ φ → D ∈ ℕ 0
fta1.3 ⊢ φ → F ∈ Poly ⁡ ℂ ∖ 0 𝑝
fta1.4 ⊢ φ → deg ⁡ F = D + 1
fta1.5 ⊢ φ → A ∈ F -1 0
fta1.6 ⊢ φ → ∀ g ∈ Poly ⁡ ℂ ∖ 0 𝑝 deg ⁡ g = D → g -1 0 ∈ Fin ∧ g -1 0 ≤ deg ⁡ g
Assertion fta1lem ⊢ φ → R ∈ Fin ∧ R ≤ deg ⁡ F

Proof

Step Hyp Ref Expression
1 fta1.1 ⊢ R = F -1 0
2 fta1.2 ⊢ φ → D ∈ ℕ 0
3 fta1.3 ⊢ φ → F ∈ Poly ⁡ ℂ ∖ 0 𝑝
4 fta1.4 ⊢ φ → deg ⁡ F = D + 1
5 fta1.5 ⊢ φ → A ∈ F -1 0
6 fta1.6 ⊢ φ → ∀ g ∈ Poly ⁡ ℂ ∖ 0 𝑝 deg ⁡ g = D → g -1 0 ∈ Fin ∧ g -1 0 ≤ deg ⁡ g
7 eldifsn ⊢ F ∈ Poly ⁡ ℂ ∖ 0 𝑝 ↔ F ∈ Poly ⁡ ℂ ∧ F ≠ 0 𝑝
8 3 7 sylib ⊢ φ → F ∈ Poly ⁡ ℂ ∧ F ≠ 0 𝑝
9 8 simpld ⊢ φ → F ∈ Poly ⁡ ℂ
10 plyf ⊢ F ∈ Poly ⁡ ℂ → F : ℂ ⟶ ℂ
11 ffn ⊢ F : ℂ ⟶ ℂ → F Fn ℂ
12 fniniseg ⊢ F Fn ℂ → A ∈ F -1 0 ↔ A ∈ ℂ ∧ F ⁡ A = 0
13 9 10 11 12 4syl ⊢ φ → A ∈ F -1 0 ↔ A ∈ ℂ ∧ F ⁡ A = 0
14 5 13 mpbid ⊢ φ → A ∈ ℂ ∧ F ⁡ A = 0
15 14 simpld ⊢ φ → A ∈ ℂ
16 14 simprd ⊢ φ → F ⁡ A = 0
17 eqid ⊢ X p − f ℂ × A = X p − f ℂ × A
18 17 facth ⊢ F ∈ Poly ⁡ ℂ ∧ A ∈ ℂ ∧ F ⁡ A = 0 → F = X p − f ℂ × A × f F quot X p − f ℂ × A
19 9 15 16 18 syl3anc ⊢ φ → F = X p − f ℂ × A × f F quot X p − f ℂ × A
20 19 cnveqd ⊢ φ → F -1 = X p − f ℂ × A × f F quot X p − f ℂ × A -1
21 20 imaeq1d ⊢ φ → F -1 0 = X p − f ℂ × A × f F quot X p − f ℂ × A -1 0
22 cnex ⊢ ℂ ∈ V
23 22 a1i ⊢ φ → ℂ ∈ V
24 ssid ⊢ ℂ ⊆ ℂ
25 ax-1cn ⊢ 1 ∈ ℂ
26 plyid ⊢ ℂ ⊆ ℂ ∧ 1 ∈ ℂ → X p ∈ Poly ⁡ ℂ
27 24 25 26 mp2an ⊢ X p ∈ Poly ⁡ ℂ
28 plyconst ⊢ ℂ ⊆ ℂ ∧ A ∈ ℂ → ℂ × A ∈ Poly ⁡ ℂ
29 24 15 28 sylancr ⊢ φ → ℂ × A ∈ Poly ⁡ ℂ
30 plysubcl ⊢ X p ∈ Poly ⁡ ℂ ∧ ℂ × A ∈ Poly ⁡ ℂ → X p − f ℂ × A ∈ Poly ⁡ ℂ
31 27 29 30 sylancr ⊢ φ → X p − f ℂ × A ∈ Poly ⁡ ℂ
32 plyf ⊢ X p − f ℂ × A ∈ Poly ⁡ ℂ → X p − f ℂ × A : ℂ ⟶ ℂ
33 31 32 syl ⊢ φ → X p − f ℂ × A : ℂ ⟶ ℂ
34 17 plyremlem ⊢ A ∈ ℂ → X p − f ℂ × A ∈ Poly ⁡ ℂ ∧ deg ⁡ X p − f ℂ × A = 1 ∧ X p − f ℂ × A -1 0 = A
35 15 34 syl ⊢ φ → X p − f ℂ × A ∈ Poly ⁡ ℂ ∧ deg ⁡ X p − f ℂ × A = 1 ∧ X p − f ℂ × A -1 0 = A
36 35 simp2d ⊢ φ → deg ⁡ X p − f ℂ × A = 1
37 ax-1ne0 ⊢ 1 ≠ 0
38 37 a1i ⊢ φ → 1 ≠ 0
39 36 38 eqnetrd ⊢ φ → deg ⁡ X p − f ℂ × A ≠ 0
40 fveq2 ⊢ X p − f ℂ × A = 0 𝑝 → deg ⁡ X p − f ℂ × A = deg ⁡ 0 𝑝
41 dgr0 ⊢ deg ⁡ 0 𝑝 = 0
42 40 41 eqtrdi ⊢ X p − f ℂ × A = 0 𝑝 → deg ⁡ X p − f ℂ × A = 0
43 42 necon3i ⊢ deg ⁡ X p − f ℂ × A ≠ 0 → X p − f ℂ × A ≠ 0 𝑝
44 39 43 syl ⊢ φ → X p − f ℂ × A ≠ 0 𝑝
45 quotcl2 ⊢ F ∈ Poly ⁡ ℂ ∧ X p − f ℂ × A ∈ Poly ⁡ ℂ ∧ X p − f ℂ × A ≠ 0 𝑝 → F quot X p − f ℂ × A ∈ Poly ⁡ ℂ
46 9 31 44 45 syl3anc ⊢ φ → F quot X p − f ℂ × A ∈ Poly ⁡ ℂ
47 plyf ⊢ F quot X p − f ℂ × A ∈ Poly ⁡ ℂ → F quot X p − f ℂ × A : ℂ ⟶ ℂ
48 46 47 syl ⊢ φ → F quot X p − f ℂ × A : ℂ ⟶ ℂ
49 ofmulrt ⊢ ℂ ∈ V ∧ X p − f ℂ × A : ℂ ⟶ ℂ ∧ F quot X p − f ℂ × A : ℂ ⟶ ℂ → X p − f ℂ × A × f F quot X p − f ℂ × A -1 0 = X p − f ℂ × A -1 0 ∪ F quot X p − f ℂ × A -1 0
50 23 33 48 49 syl3anc ⊢ φ → X p − f ℂ × A × f F quot X p − f ℂ × A -1 0 = X p − f ℂ × A -1 0 ∪ F quot X p − f ℂ × A -1 0
51 35 simp3d ⊢ φ → X p − f ℂ × A -1 0 = A
52 51 uneq1d ⊢ φ → X p − f ℂ × A -1 0 ∪ F quot X p − f ℂ × A -1 0 = A ∪ F quot X p − f ℂ × A -1 0
53 21 50 52 3eqtrd ⊢ φ → F -1 0 = A ∪ F quot X p − f ℂ × A -1 0
54 uncom ⊢ F quot X p − f ℂ × A -1 0 ∪ A = A ∪ F quot X p − f ℂ × A -1 0
55 53 1 54 3eqtr4g ⊢ φ → R = F quot X p − f ℂ × A -1 0 ∪ A
56 25 a1i ⊢ φ → 1 ∈ ℂ
57 dgrcl ⊢ F quot X p − f ℂ × A ∈ Poly ⁡ ℂ → deg ⁡ F quot X p − f ℂ × A ∈ ℕ 0
58 46 57 syl ⊢ φ → deg ⁡ F quot X p − f ℂ × A ∈ ℕ 0
59 58 nn0cnd ⊢ φ → deg ⁡ F quot X p − f ℂ × A ∈ ℂ
60 2 nn0cnd ⊢ φ → D ∈ ℂ
61 addcom ⊢ 1 ∈ ℂ ∧ D ∈ ℂ → 1 + D = D + 1
62 25 60 61 sylancr ⊢ φ → 1 + D = D + 1
63 19 fveq2d ⊢ φ → deg ⁡ F = deg ⁡ X p − f ℂ × A × f F quot X p − f ℂ × A
64 8 simprd ⊢ φ → F ≠ 0 𝑝
65 19 eqcomd ⊢ φ → X p − f ℂ × A × f F quot X p − f ℂ × A = F
66 0cnd ⊢ φ → 0 ∈ ℂ
67 mul01 ⊢ x ∈ ℂ → x ⋅ 0 = 0
68 67 adantl ⊢ φ ∧ x ∈ ℂ → x ⋅ 0 = 0
69 23 33 66 66 68 caofid1 ⊢ φ → X p − f ℂ × A × f ℂ × 0 = ℂ × 0
70 df-0p ⊢ 0 𝑝 = ℂ × 0
71 70 oveq2i ⊢ X p − f ℂ × A × f 0 𝑝 = X p − f ℂ × A × f ℂ × 0
72 69 71 70 3eqtr4g ⊢ φ → X p − f ℂ × A × f 0 𝑝 = 0 𝑝
73 64 65 72 3netr4d ⊢ φ → X p − f ℂ × A × f F quot X p − f ℂ × A ≠ X p − f ℂ × A × f 0 𝑝
74 oveq2 ⊢ F quot X p − f ℂ × A = 0 𝑝 → X p − f ℂ × A × f F quot X p − f ℂ × A = X p − f ℂ × A × f 0 𝑝
75 74 necon3i ⊢ X p − f ℂ × A × f F quot X p − f ℂ × A ≠ X p − f ℂ × A × f 0 𝑝 → F quot X p − f ℂ × A ≠ 0 𝑝
76 73 75 syl ⊢ φ → F quot X p − f ℂ × A ≠ 0 𝑝
77 eqid ⊢ deg ⁡ X p − f ℂ × A = deg ⁡ X p − f ℂ × A
78 eqid ⊢ deg ⁡ F quot X p − f ℂ × A = deg ⁡ F quot X p − f ℂ × A
79 77 78 dgrmul ⊢ X p − f ℂ × A ∈ Poly ⁡ ℂ ∧ X p − f ℂ × A ≠ 0 𝑝 ∧ F quot X p − f ℂ × A ∈ Poly ⁡ ℂ ∧ F quot X p − f ℂ × A ≠ 0 𝑝 → deg ⁡ X p − f ℂ × A × f F quot X p − f ℂ × A = deg ⁡ X p − f ℂ × A + deg ⁡ F quot X p − f ℂ × A
80 31 44 46 76 79 syl22anc ⊢ φ → deg ⁡ X p − f ℂ × A × f F quot X p − f ℂ × A = deg ⁡ X p − f ℂ × A + deg ⁡ F quot X p − f ℂ × A
81 63 4 80 3eqtr3d ⊢ φ → D + 1 = deg ⁡ X p − f ℂ × A + deg ⁡ F quot X p − f ℂ × A
82 36 oveq1d ⊢ φ → deg ⁡ X p − f ℂ × A + deg ⁡ F quot X p − f ℂ × A = 1 + deg ⁡ F quot X p − f ℂ × A
83 62 81 82 3eqtrrd ⊢ φ → 1 + deg ⁡ F quot X p − f ℂ × A = 1 + D
84 56 59 60 83 addcanad ⊢ φ → deg ⁡ F quot X p − f ℂ × A = D
85 fveqeq2 ⊢ g = F quot X p − f ℂ × A → deg ⁡ g = D ↔ deg ⁡ F quot X p − f ℂ × A = D
86 cnveq ⊢ g = F quot X p − f ℂ × A → g -1 = F quot X p − f ℂ × A -1
87 86 imaeq1d ⊢ g = F quot X p − f ℂ × A → g -1 0 = F quot X p − f ℂ × A -1 0
88 87 eleq1d ⊢ g = F quot X p − f ℂ × A → g -1 0 ∈ Fin ↔ F quot X p − f ℂ × A -1 0 ∈ Fin
89 87 fveq2d ⊢ g = F quot X p − f ℂ × A → g -1 0 = F quot X p − f ℂ × A -1 0
90 fveq2 ⊢ g = F quot X p − f ℂ × A → deg ⁡ g = deg ⁡ F quot X p − f ℂ × A
91 89 90 breq12d ⊢ g = F quot X p − f ℂ × A → g -1 0 ≤ deg ⁡ g ↔ F quot X p − f ℂ × A -1 0 ≤ deg ⁡ F quot X p − f ℂ × A
92 88 91 anbi12d ⊢ g = F quot X p − f ℂ × A → g -1 0 ∈ Fin ∧ g -1 0 ≤ deg ⁡ g ↔ F quot X p − f ℂ × A -1 0 ∈ Fin ∧ F quot X p − f ℂ × A -1 0 ≤ deg ⁡ F quot X p − f ℂ × A
93 85 92 imbi12d ⊢ g = F quot X p − f ℂ × A → deg ⁡ g = D → g -1 0 ∈ Fin ∧ g -1 0 ≤ deg ⁡ g ↔ deg ⁡ F quot X p − f ℂ × A = D → F quot X p − f ℂ × A -1 0 ∈ Fin ∧ F quot X p − f ℂ × A -1 0 ≤ deg ⁡ F quot X p − f ℂ × A
94 eldifsn ⊢ F quot X p − f ℂ × A ∈ Poly ⁡ ℂ ∖ 0 𝑝 ↔ F quot X p − f ℂ × A ∈ Poly ⁡ ℂ ∧ F quot X p − f ℂ × A ≠ 0 𝑝
95 46 76 94 sylanbrc ⊢ φ → F quot X p − f ℂ × A ∈ Poly ⁡ ℂ ∖ 0 𝑝
96 93 6 95 rspcdva ⊢ φ → deg ⁡ F quot X p − f ℂ × A = D → F quot X p − f ℂ × A -1 0 ∈ Fin ∧ F quot X p − f ℂ × A -1 0 ≤ deg ⁡ F quot X p − f ℂ × A
97 84 96 mpd ⊢ φ → F quot X p − f ℂ × A -1 0 ∈ Fin ∧ F quot X p − f ℂ × A -1 0 ≤ deg ⁡ F quot X p − f ℂ × A
98 97 simpld ⊢ φ → F quot X p − f ℂ × A -1 0 ∈ Fin
99 snfi ⊢ A ∈ Fin
100 unfi ⊢ F quot X p − f ℂ × A -1 0 ∈ Fin ∧ A ∈ Fin → F quot X p − f ℂ × A -1 0 ∪ A ∈ Fin
101 98 99 100 sylancl ⊢ φ → F quot X p − f ℂ × A -1 0 ∪ A ∈ Fin
102 55 101 eqeltrd ⊢ φ → R ∈ Fin
103 55 fveq2d ⊢ φ → R = F quot X p − f ℂ × A -1 0 ∪ A
104 hashcl ⊢ F quot X p − f ℂ × A -1 0 ∪ A ∈ Fin → F quot X p − f ℂ × A -1 0 ∪ A ∈ ℕ 0
105 101 104 syl ⊢ φ → F quot X p − f ℂ × A -1 0 ∪ A ∈ ℕ 0
106 105 nn0red ⊢ φ → F quot X p − f ℂ × A -1 0 ∪ A ∈ ℝ
107 hashcl ⊢ F quot X p − f ℂ × A -1 0 ∈ Fin → F quot X p − f ℂ × A -1 0 ∈ ℕ 0
108 98 107 syl ⊢ φ → F quot X p − f ℂ × A -1 0 ∈ ℕ 0
109 108 nn0red ⊢ φ → F quot X p − f ℂ × A -1 0 ∈ ℝ
110 peano2re ⊢ F quot X p − f ℂ × A -1 0 ∈ ℝ → F quot X p − f ℂ × A -1 0 + 1 ∈ ℝ
111 109 110 syl ⊢ φ → F quot X p − f ℂ × A -1 0 + 1 ∈ ℝ
112 dgrcl ⊢ F ∈ Poly ⁡ ℂ → deg ⁡ F ∈ ℕ 0
113 9 112 syl ⊢ φ → deg ⁡ F ∈ ℕ 0
114 113 nn0red ⊢ φ → deg ⁡ F ∈ ℝ
115 hashun2 ⊢ F quot X p − f ℂ × A -1 0 ∈ Fin ∧ A ∈ Fin → F quot X p − f ℂ × A -1 0 ∪ A ≤ F quot X p − f ℂ × A -1 0 + A
116 98 99 115 sylancl ⊢ φ → F quot X p − f ℂ × A -1 0 ∪ A ≤ F quot X p − f ℂ × A -1 0 + A
117 hashsng ⊢ A ∈ ℂ → A = 1
118 15 117 syl ⊢ φ → A = 1
119 118 oveq2d ⊢ φ → F quot X p − f ℂ × A -1 0 + A = F quot X p − f ℂ × A -1 0 + 1
120 116 119 breqtrd ⊢ φ → F quot X p − f ℂ × A -1 0 ∪ A ≤ F quot X p − f ℂ × A -1 0 + 1
121 2 nn0red ⊢ φ → D ∈ ℝ
122 1red ⊢ φ → 1 ∈ ℝ
123 97 simprd ⊢ φ → F quot X p − f ℂ × A -1 0 ≤ deg ⁡ F quot X p − f ℂ × A
124 123 84 breqtrd ⊢ φ → F quot X p − f ℂ × A -1 0 ≤ D
125 109 121 122 124 leadd1dd ⊢ φ → F quot X p − f ℂ × A -1 0 + 1 ≤ D + 1
126 125 4 breqtrrd ⊢ φ → F quot X p − f ℂ × A -1 0 + 1 ≤ deg ⁡ F
127 106 111 114 120 126 letrd ⊢ φ → F quot X p − f ℂ × A -1 0 ∪ A ≤ deg ⁡ F
128 103 127 eqbrtrd ⊢ φ → R ≤ deg ⁡ F
129 102 128 jca ⊢ φ → R ∈ Fin ∧ R ≤ deg ⁡ F