Theorem ply1dg1rtn0

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

	Ref	Expression
Hypotheses	ply1dg1rt.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1dg1rt.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	ply1dg1rt.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	ply1dg1rt.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	ply1dg1rt.0	⊢ 0 = ( 0g ‘ 𝑅 )
	ply1dg1rtn0.r	⊢ ( 𝜑 → 𝑅 ∈ Field )
	ply1dg1rtn0.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
	ply1dg1rtn0.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 1 )
Assertion	ply1dg1rtn0	⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		ply1dg1rt.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1dg1rt.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
3		ply1dg1rt.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
4		ply1dg1rt.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
5		ply1dg1rt.0	⊢ 0 = ( 0g ‘ 𝑅 )
6		ply1dg1rtn0.r	⊢ ( 𝜑 → 𝑅 ∈ Field )
7		ply1dg1rtn0.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
8		ply1dg1rtn0.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 1 )
9		ovex	⊢ ( ( ( invg ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ( /r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 1 ) ) ∈ V
10	9	snid	⊢ ( ( ( invg ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ( /r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 1 ) ) ∈ { ( ( ( invg ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ( /r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 1 ) ) }
11		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
12		eqid	⊢ ( /r ‘ 𝑅 ) = ( /r ‘ 𝑅 )
13		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
14		eqid	⊢ ( ( coe1 ‘ 𝐺 ) ‘ 1 ) = ( ( coe1 ‘ 𝐺 ) ‘ 1 )
15		eqid	⊢ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) = ( ( coe1 ‘ 𝐺 ) ‘ 0 )
16		eqid	⊢ ( ( ( invg ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ( /r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 1 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ( /r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 1 ) )
17	1 2 3 4 5 6 7 8 11 12 13 14 15 16	ply1dg1rt	⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { ( ( ( invg ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ( /r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 1 ) ) } )
18	10 17	eleqtrrid	⊢ ( 𝜑 → ( ( ( invg ‘ 𝑅 ) ‘ ( ( coe1 ‘ 𝐺 ) ‘ 0 ) ) ( /r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 1 ) ) ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) )
19	18	ne0d	⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) ≠ ∅ )