Metamath Proof Explorer

Theorem fta1g

Description: The one-sided fundamental theorem of algebra. A polynomial of degree n has at most n roots. Unlike the real fundamental theorem fta , which is only true in CC and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses fta1g.p ⊢P=Poly1⁡R
fta1g.b ⊢B=BaseP
fta1g.d ⊢D=deg1⁡R
fta1g.o ⊢O=eval1⁡R
fta1g.w ⊢W=0R
fta1g.z ⊢0˙=0P
fta1g.1 ⊢φ→R∈IDomn
fta1g.2 ⊢φ→F∈B
fta1g.3 ⊢φ→F≠0˙
Assertion fta1g ⊢φ→O⁡F-1W≤D⁡F

Proof

Step Hyp Ref Expression
1 fta1g.p ⊢P=Poly1⁡R
2 fta1g.b ⊢B=BaseP
3 fta1g.d ⊢D=deg1⁡R
4 fta1g.o ⊢O=eval1⁡R
5 fta1g.w ⊢W=0R
6 fta1g.z ⊢0˙=0P
7 fta1g.1 ⊢φ→R∈IDomn
8 fta1g.2 ⊢φ→F∈B
9 fta1g.3 ⊢φ→F≠0˙
10 eqid ⊢D⁡F=D⁡F
11 fveqeq2 ⊢f=F→D⁡f=D⁡F↔D⁡F=D⁡F
12 fveq2 ⊢f=F→O⁡f=O⁡F
13 12 cnveqd ⊢f=F→O⁡f-1=O⁡F-1
14 13 imaeq1d ⊢f=F→O⁡f-1W=O⁡F-1W
15 14 fveq2d ⊢f=F→O⁡f-1W=O⁡F-1W
16 fveq2 ⊢f=F→D⁡f=D⁡F
17 15 16 breq12d ⊢f=F→O⁡f-1W≤D⁡f↔O⁡F-1W≤D⁡F
18 11 17 imbi12d ⊢f=F→D⁡f=D⁡F→O⁡f-1W≤D⁡f↔D⁡F=D⁡F→O⁡F-1W≤D⁡F
19 isidom ⊢R∈IDomn↔R∈CRing∧R∈Domn
20 19 simplbi ⊢R∈IDomn→R∈CRing
21 crngring ⊢R∈CRing→R∈Ring
22 7 20 21 3syl ⊢φ→R∈Ring
23 3 1 6 2 deg1nn0cl ⊢R∈Ring∧F∈B∧F≠0˙→D⁡F∈ℕ0
24 22 8 9 23 syl3anc ⊢φ→D⁡F∈ℕ0
25 eqeq2 ⊢x=0→D⁡f=x↔D⁡f=0
26 25 imbi1d ⊢x=0→D⁡f=x→O⁡f-1W≤D⁡f↔D⁡f=0→O⁡f-1W≤D⁡f
27 26 ralbidv ⊢x=0→∀f∈BD⁡f=x→O⁡f-1W≤D⁡f↔∀f∈BD⁡f=0→O⁡f-1W≤D⁡f
28 27 imbi2d ⊢x=0→R∈IDomn→∀f∈BD⁡f=x→O⁡f-1W≤D⁡f↔R∈IDomn→∀f∈BD⁡f=0→O⁡f-1W≤D⁡f
29 eqeq2 ⊢x=d→D⁡f=x↔D⁡f=d
30 29 imbi1d ⊢x=d→D⁡f=x→O⁡f-1W≤D⁡f↔D⁡f=d→O⁡f-1W≤D⁡f
31 30 ralbidv ⊢x=d→∀f∈BD⁡f=x→O⁡f-1W≤D⁡f↔∀f∈BD⁡f=d→O⁡f-1W≤D⁡f
32 31 imbi2d ⊢x=d→R∈IDomn→∀f∈BD⁡f=x→O⁡f-1W≤D⁡f↔R∈IDomn→∀f∈BD⁡f=d→O⁡f-1W≤D⁡f
33 eqeq2 ⊢x=d+1→D⁡f=x↔D⁡f=d+1
34 33 imbi1d ⊢x=d+1→D⁡f=x→O⁡f-1W≤D⁡f↔D⁡f=d+1→O⁡f-1W≤D⁡f
35 34 ralbidv ⊢x=d+1→∀f∈BD⁡f=x→O⁡f-1W≤D⁡f↔∀f∈BD⁡f=d+1→O⁡f-1W≤D⁡f
36 35 imbi2d ⊢x=d+1→R∈IDomn→∀f∈BD⁡f=x→O⁡f-1W≤D⁡f↔R∈IDomn→∀f∈BD⁡f=d+1→O⁡f-1W≤D⁡f
37 eqeq2 ⊢x=D⁡F→D⁡f=x↔D⁡f=D⁡F
38 37 imbi1d ⊢x=D⁡F→D⁡f=x→O⁡f-1W≤D⁡f↔D⁡f=D⁡F→O⁡f-1W≤D⁡f
39 38 ralbidv ⊢x=D⁡F→∀f∈BD⁡f=x→O⁡f-1W≤D⁡f↔∀f∈BD⁡f=D⁡F→O⁡f-1W≤D⁡f
40 39 imbi2d ⊢x=D⁡F→R∈IDomn→∀f∈BD⁡f=x→O⁡f-1W≤D⁡f↔R∈IDomn→∀f∈BD⁡f=D⁡F→O⁡f-1W≤D⁡f
41 simprr ⊢R∈IDomn∧f∈B∧D⁡f=0→D⁡f=0
42 0nn0 ⊢0∈ℕ0
43 41 42 eqeltrdi ⊢R∈IDomn∧f∈B∧D⁡f=0→D⁡f∈ℕ0
44 20 21 syl ⊢R∈IDomn→R∈Ring
45 simpl ⊢f∈B∧D⁡f=0→f∈B
46 3 1 6 2 deg1nn0clb ⊢R∈Ring∧f∈B→f≠0˙↔D⁡f∈ℕ0
47 44 45 46 syl2an ⊢R∈IDomn∧f∈B∧D⁡f=0→f≠0˙↔D⁡f∈ℕ0
48 43 47 mpbird ⊢R∈IDomn∧f∈B∧D⁡f=0→f≠0˙
49 simplrr ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→D⁡f=0
50 0le0 ⊢0≤0
51 49 50 eqbrtrdi ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→D⁡f≤0
52 44 ad2antrr ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→R∈Ring
53 simplrl ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→f∈B
54 eqid ⊢algSc⁡P=algSc⁡P
55 3 1 2 54 deg1le0 ⊢R∈Ring∧f∈B→D⁡f≤0↔f=algSc⁡P⁡coe1⁡f⁡0
56 52 53 55 syl2anc ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→D⁡f≤0↔f=algSc⁡P⁡coe1⁡f⁡0
57 51 56 mpbid ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→f=algSc⁡P⁡coe1⁡f⁡0
58 57 fveq2d ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→O⁡f=O⁡algSc⁡P⁡coe1⁡f⁡0
59 20 adantr ⊢R∈IDomn∧f∈B∧D⁡f=0→R∈CRing
60 59 adantr ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→R∈CRing
61 eqid ⊢coe1⁡f=coe1⁡f
62 eqid ⊢BaseR=BaseR
63 61 2 1 62 coe1f ⊢f∈B→coe1⁡f:ℕ0⟶BaseR
64 53 63 syl ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→coe1⁡f:ℕ0⟶BaseR
65 ffvelcdm ⊢coe1⁡f:ℕ0⟶BaseR∧0∈ℕ0→coe1⁡f⁡0∈BaseR
66 64 42 65 sylancl ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→coe1⁡f⁡0∈BaseR
67 4 1 62 54 evl1sca ⊢R∈CRing∧coe1⁡f⁡0∈BaseR→O⁡algSc⁡P⁡coe1⁡f⁡0=BaseR×coe1⁡f⁡0
68 60 66 67 syl2anc ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→O⁡algSc⁡P⁡coe1⁡f⁡0=BaseR×coe1⁡f⁡0
69 58 68 eqtrd ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→O⁡f=BaseR×coe1⁡f⁡0
70 69 fveq1d ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→O⁡f⁡x=BaseR×coe1⁡f⁡0⁡x
71 eqid ⊢R↑𝑠BaseR=R↑𝑠BaseR
72 eqid ⊢BaseR↑𝑠BaseR=BaseR↑𝑠BaseR
73 simpl ⊢R∈IDomn∧f∈B∧D⁡f=0→R∈IDomn
74 fvexd ⊢R∈IDomn∧f∈B∧D⁡f=0→BaseR∈V
75 4 1 71 62 evl1rhm ⊢R∈CRing→O∈PRingHomR↑𝑠BaseR
76 2 72 rhmf ⊢O∈PRingHomR↑𝑠BaseR→O:B⟶BaseR↑𝑠BaseR
77 59 75 76 3syl ⊢R∈IDomn∧f∈B∧D⁡f=0→O:B⟶BaseR↑𝑠BaseR
78 simprl ⊢R∈IDomn∧f∈B∧D⁡f=0→f∈B
79 77 78 ffvelcdmd ⊢R∈IDomn∧f∈B∧D⁡f=0→O⁡f∈BaseR↑𝑠BaseR
80 71 62 72 73 74 79 pwselbas ⊢R∈IDomn∧f∈B∧D⁡f=0→O⁡f:BaseR⟶BaseR
81 ffn ⊢O⁡f:BaseR⟶BaseR→O⁡fFnBaseR
82 fniniseg ⊢O⁡fFnBaseR→x∈O⁡f-1W↔x∈BaseR∧O⁡f⁡x=W
83 80 81 82 3syl ⊢R∈IDomn∧f∈B∧D⁡f=0→x∈O⁡f-1W↔x∈BaseR∧O⁡f⁡x=W
84 83 simplbda ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→O⁡f⁡x=W
85 83 simprbda ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→x∈BaseR
86 fvex ⊢coe1⁡f⁡0∈V
87 86 fvconst2 ⊢x∈BaseR→BaseR×coe1⁡f⁡0⁡x=coe1⁡f⁡0
88 85 87 syl ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→BaseR×coe1⁡f⁡0⁡x=coe1⁡f⁡0
89 70 84 88 3eqtr3rd ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→coe1⁡f⁡0=W
90 89 fveq2d ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→algSc⁡P⁡coe1⁡f⁡0=algSc⁡P⁡W
91 1 54 5 6 ply1scl0 ⊢R∈Ring→algSc⁡P⁡W=0˙
92 52 91 syl ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→algSc⁡P⁡W=0˙
93 57 90 92 3eqtrd ⊢R∈IDomn∧f∈B∧D⁡f=0∧x∈O⁡f-1W→f=0˙
94 93 ex ⊢R∈IDomn∧f∈B∧D⁡f=0→x∈O⁡f-1W→f=0˙
95 94 necon3ad ⊢R∈IDomn∧f∈B∧D⁡f=0→f≠0˙→¬x∈O⁡f-1W
96 48 95 mpd ⊢R∈IDomn∧f∈B∧D⁡f=0→¬x∈O⁡f-1W
97 96 eq0rdv ⊢R∈IDomn∧f∈B∧D⁡f=0→O⁡f-1W=∅
98 97 fveq2d ⊢R∈IDomn∧f∈B∧D⁡f=0→O⁡f-1W=∅
99 hash0 ⊢∅=0
100 98 99 eqtrdi ⊢R∈IDomn∧f∈B∧D⁡f=0→O⁡f-1W=0
101 50 41 breqtrrid ⊢R∈IDomn∧f∈B∧D⁡f=0→0≤D⁡f
102 100 101 eqbrtrd ⊢R∈IDomn∧f∈B∧D⁡f=0→O⁡f-1W≤D⁡f
103 102 expr ⊢R∈IDomn∧f∈B→D⁡f=0→O⁡f-1W≤D⁡f
104 103 ralrimiva ⊢R∈IDomn→∀f∈BD⁡f=0→O⁡f-1W≤D⁡f
105 fveqeq2 ⊢f=g→D⁡f=d↔D⁡g=d
106 fveq2 ⊢f=g→O⁡f=O⁡g
107 106 cnveqd ⊢f=g→O⁡f-1=O⁡g-1
108 107 imaeq1d ⊢f=g→O⁡f-1W=O⁡g-1W
109 108 fveq2d ⊢f=g→O⁡f-1W=O⁡g-1W
110 fveq2 ⊢f=g→D⁡f=D⁡g
111 109 110 breq12d ⊢f=g→O⁡f-1W≤D⁡f↔O⁡g-1W≤D⁡g
112 105 111 imbi12d ⊢f=g→D⁡f=d→O⁡f-1W≤D⁡f↔D⁡g=d→O⁡g-1W≤D⁡g
113 112 cbvralvw ⊢∀f∈BD⁡f=d→O⁡f-1W≤D⁡f↔∀g∈BD⁡g=d→O⁡g-1W≤D⁡g
114 simprr ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→D⁡f=d+1
115 peano2nn0 ⊢d∈ℕ0→d+1∈ℕ0
116 115 ad2antlr ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→d+1∈ℕ0
117 114 116 eqeltrd ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→D⁡f∈ℕ0
118 117 nn0ge0d ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→0≤D⁡f
119 fveq2 ⊢O⁡f-1W=∅→O⁡f-1W=∅
120 119 99 eqtrdi ⊢O⁡f-1W=∅→O⁡f-1W=0
121 120 breq1d ⊢O⁡f-1W=∅→O⁡f-1W≤D⁡f↔0≤D⁡f
122 118 121 syl5ibrcom ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→O⁡f-1W=∅→O⁡f-1W≤D⁡f
123 122 a1dd ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→O⁡f-1W=∅→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→O⁡f-1W≤D⁡f
124 n0 ⊢O⁡f-1W≠∅↔∃xx∈O⁡f-1W
125 simplll ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1∧x∈O⁡f-1W∧∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→R∈IDomn
126 simplrl ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1∧x∈O⁡f-1W∧∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→f∈B
127 eqid ⊢var1⁡R=var1⁡R
128 eqid ⊢-P=-P
129 eqid ⊢var1⁡R-PalgSc⁡P⁡x=var1⁡R-PalgSc⁡P⁡x
130 simpllr ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1∧x∈O⁡f-1W∧∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→d∈ℕ0
131 simplrr ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1∧x∈O⁡f-1W∧∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→D⁡f=d+1
132 simprl ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1∧x∈O⁡f-1W∧∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→x∈O⁡f-1W
133 simprr ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1∧x∈O⁡f-1W∧∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g
134 1 2 3 4 5 6 125 126 62 127 128 54 129 130 131 132 133 fta1glem2 ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1∧x∈O⁡f-1W∧∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→O⁡f-1W≤D⁡f
135 134 exp32 ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→x∈O⁡f-1W→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→O⁡f-1W≤D⁡f
136 135 exlimdv ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→∃xx∈O⁡f-1W→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→O⁡f-1W≤D⁡f
137 124 136 biimtrid ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→O⁡f-1W≠∅→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→O⁡f-1W≤D⁡f
138 123 137 pm2.61dne ⊢R∈IDomn∧d∈ℕ0∧f∈B∧D⁡f=d+1→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→O⁡f-1W≤D⁡f
139 138 expr ⊢R∈IDomn∧d∈ℕ0∧f∈B→D⁡f=d+1→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→O⁡f-1W≤D⁡f
140 139 com23 ⊢R∈IDomn∧d∈ℕ0∧f∈B→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→D⁡f=d+1→O⁡f-1W≤D⁡f
141 140 ralrimdva ⊢R∈IDomn∧d∈ℕ0→∀g∈BD⁡g=d→O⁡g-1W≤D⁡g→∀f∈BD⁡f=d+1→O⁡f-1W≤D⁡f
142 113 141 biimtrid ⊢R∈IDomn∧d∈ℕ0→∀f∈BD⁡f=d→O⁡f-1W≤D⁡f→∀f∈BD⁡f=d+1→O⁡f-1W≤D⁡f
143 142 expcom ⊢d∈ℕ0→R∈IDomn→∀f∈BD⁡f=d→O⁡f-1W≤D⁡f→∀f∈BD⁡f=d+1→O⁡f-1W≤D⁡f
144 143 a2d ⊢d∈ℕ0→R∈IDomn→∀f∈BD⁡f=d→O⁡f-1W≤D⁡f→R∈IDomn→∀f∈BD⁡f=d+1→O⁡f-1W≤D⁡f
145 28 32 36 40 104 144 nn0ind ⊢D⁡F∈ℕ0→R∈IDomn→∀f∈BD⁡f=D⁡F→O⁡f-1W≤D⁡f
146 24 7 145 sylc ⊢φ→∀f∈BD⁡f=D⁡F→O⁡f-1W≤D⁡f
147 18 146 8 rspcdva ⊢φ→D⁡F=D⁡F→O⁡F-1W≤D⁡F
148 10 147 mpi ⊢φ→O⁡F-1W≤D⁡F