This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
		ply1dg1rt.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
		ply1dg1rt.o	⊢ 𝑂 = ( eval₁ ‘ 𝑅 )
		ply1dg1rt.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
		ply1dg1rt.0	⊢ 0 = ( 0_g ‘ 𝑅 )
		ply1dg1rtn0.r	⊢ ( 𝜑 → 𝑅 ∈ Field )
		ply1dg1rtn0.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
		ply1dg1rtn0.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 1 )
	Assertion	ply1dg1rtn0	⊢ ( 𝜑 → ( ^◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) ≠ ∅ )

Proof

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