ply1dg1rtn0

Description: Polynomials of degree 1 over a field always have some roots. (Contributed by Thierry Arnoux, 8-Jun-2025)

Step	Hyp	Ref	Expression
1		ply1dg1rt.p	$⊢ P = {Poly}_{1} (R)$
2		ply1dg1rt.u	$⊢ U = {Base}_{P}$
3		ply1dg1rt.o	$⊢ O = {eval}_{1} (R)$
4		ply1dg1rt.d	$⊢ D = \deg_{1} (R)$
5		ply1dg1rt.0	$⊢ \underset{˙}{0} = 0_{R}$
6		ply1dg1rtn0.r	$⊢ φ \to R \in Field$
7		ply1dg1rtn0.g	$⊢ φ \to G \in U$
8		ply1dg1rtn0.1	$⊢ φ \to D (G) = 1$
9		ovex	$⊢ {inv}_{g} (R) ({coe}_{1} (G) (0)) /_{r} (R) {coe}_{1} (G) (1) \in V$
10	9	snid	$⊢ {inv}_{g} (R) ({coe}_{1} (G) (0)) /_{r} (R) {coe}_{1} (G) (1) \in \{{inv}_{g} (R) ({coe}_{1} (G) (0)) /_{r} (R) {coe}_{1} (G) (1)\}$
11		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
12		eqid	$⊢ /_{r} (R) = /_{r} (R)$
13		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
14		eqid	$⊢ {coe}_{1} (G) (1) = {coe}_{1} (G) (1)$
15		eqid	$⊢ {coe}_{1} (G) (0) = {coe}_{1} (G) (0)$
16		eqid	$⊢ {inv}_{g} (R) ({coe}_{1} (G) (0)) /_{r} (R) {coe}_{1} (G) (1) = {inv}_{g} (R) ({coe}_{1} (G) (0)) /_{r} (R) {coe}_{1} (G) (1)$
17	1 2 3 4 5 6 7 8 11 12 13 14 15 16	ply1dg1rt	$⊢ φ \to {O (G)}^{-1} [\{\underset{˙}{0}\}] = \{{inv}_{g} (R) ({coe}_{1} (G) (0)) /_{r} (R) {coe}_{1} (G) (1)\}$
18	10 17	eleqtrrid	$⊢ φ \to {inv}_{g} (R) ({coe}_{1} (G) (0)) /_{r} (R) {coe}_{1} (G) (1) \in {O (G)}^{-1} [\{\underset{˙}{0}\}]$
19	18	ne0d	$⊢ φ \to {O (G)}^{-1} [\{\underset{˙}{0}\}] \neq \emptyset$

Metamath Proof Explorer