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 
|- 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. } ) =/= (/) )