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	|- P = ( Poly1 ` R )
	ply1dg1rt.u	|- U = ( Base ` P )
	ply1dg1rt.o	|- O = ( eval1 ` R )
	ply1dg1rt.d	|- D = ( deg1 ` R )
	ply1dg1rt.0	|- .0. = ( 0g ` R )
	ply1dg1rtn0.r	|- ( ph -> R e. Field )
	ply1dg1rtn0.g	|- ( ph -> G e. U )
	ply1dg1rtn0.1	|- ( ph -> ( D ` G ) = 1 )
Assertion	ply1dg1rtn0	|- ( ph -> ( `' ( O ` G ) " { .0. } ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		ply1dg1rt.p	|- P = ( Poly1 ` R )
2		ply1dg1rt.u	|- U = ( Base ` P )
3		ply1dg1rt.o	|- O = ( eval1 ` R )
4		ply1dg1rt.d	|- D = ( deg1 ` R )
5		ply1dg1rt.0	|- .0. = ( 0g ` R )
6		ply1dg1rtn0.r	|- ( ph -> R e. Field )
7		ply1dg1rtn0.g	|- ( ph -> G e. U )
8		ply1dg1rtn0.1	|- ( ph -> ( D ` G ) = 1 )
9		ovex	|- ( ( ( invg ` R ) ` ( ( coe1 ` G ) ` 0 ) ) ( /r ` R ) ( ( coe1 ` G ) ` 1 ) ) e. _V
10	9	snid	|- ( ( ( invg ` R ) ` ( ( coe1 ` G ) ` 0 ) ) ( /r ` R ) ( ( coe1 ` G ) ` 1 ) ) e. { ( ( ( invg ` R ) ` ( ( coe1 ` G ) ` 0 ) ) ( /r ` R ) ( ( coe1 ` G ) ` 1 ) ) }
11		eqid	|- ( invg ` R ) = ( invg ` R )
12		eqid	|- ( /r ` R ) = ( /r ` R )
13		eqid	|- ( coe1 ` G ) = ( coe1 ` G )
14		eqid	|- ( ( coe1 ` G ) ` 1 ) = ( ( coe1 ` G ) ` 1 )
15		eqid	|- ( ( coe1 ` G ) ` 0 ) = ( ( coe1 ` G ) ` 0 )
16		eqid	|- ( ( ( invg ` R ) ` ( ( coe1 ` G ) ` 0 ) ) ( /r ` R ) ( ( coe1 ` G ) ` 1 ) ) = ( ( ( invg ` R ) ` ( ( coe1 ` G ) ` 0 ) ) ( /r ` R ) ( ( coe1 ` G ) ` 1 ) )
17	1 2 3 4 5 6 7 8 11 12 13 14 15 16	ply1dg1rt	|- ( ph -> ( `' ( O ` G ) " { .0. } ) = { ( ( ( invg ` R ) ` ( ( coe1 ` G ) ` 0 ) ) ( /r ` R ) ( ( coe1 ` G ) ` 1 ) ) } )
18	10 17	eleqtrrid	|- ( ph -> ( ( ( invg ` R ) ` ( ( coe1 ` G ) ` 0 ) ) ( /r ` R ) ( ( coe1 ` G ) ` 1 ) ) e. ( `' ( O ` G ) " { .0. } ) )
19	18	ne0d	|- ( ph -> ( `' ( O ` G ) " { .0. } ) =/= (/) )