Metamath Proof Explorer

Theorem fta1lem

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

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

Proof

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