Metamath Proof Explorer

Theorem deg1le0eq0

Description: A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl . (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses deg1sclb.d 
|- D = ( deg1 ` R )
deg1sclb.p 
|- P = ( Poly1 ` R )
deg1sclb.z 
|- .0. = ( 0g ` R )
deg1sclb.1 
|- B = ( Base ` P )
deg1sclb.2 
|- O = ( 0g ` P )
deg1sclb.3 
|- ( ph -> R e. Ring )
deg1sclb.4 
|- ( ph -> F e. B )
deg1sclb.5 
|- ( ph -> ( D ` F ) <_ 0 )
Assertion deg1le0eq0 
|- ( ph -> ( F = O <-> ( ( coe1 ` F ) ` 0 ) = .0. ) )

Proof

Step Hyp Ref Expression
1 deg1sclb.d 
 |-  D = ( deg1 ` R )
2 deg1sclb.p 
 |-  P = ( Poly1 ` R )
3 deg1sclb.z 
 |-  .0. = ( 0g ` R )
4 deg1sclb.1 
 |-  B = ( Base ` P )
5 deg1sclb.2 
 |-  O = ( 0g ` P )
6 deg1sclb.3 
 |-  ( ph -> R e. Ring )
7 deg1sclb.4 
 |-  ( ph -> F e. B )
8 deg1sclb.5 
 |-  ( ph -> ( D ` F ) <_ 0 )
9 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
10 1 2 4 9 deg1le0 
 |-  ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) <_ 0 <-> F = ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) ) )
11 10 biimpa 
 |-  ( ( ( R e. Ring /\ F e. B ) /\ ( D ` F ) <_ 0 ) -> F = ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) )
12 6 7 8 11 syl21anc 
 |-  ( ph -> F = ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) )
13 12 adantr 
 |-  ( ( ph /\ F = O ) -> F = ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) )
14 simpr 
 |-  ( ( ph /\ F = O ) -> F = O )
15 13 14 eqtr3d 
 |-  ( ( ph /\ F = O ) -> ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) = O )
16 6 adantr 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) =/= .0. ) -> R e. Ring )
17 0nn0 
 |-  0 e. NN0
18 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 18 4 2 19 coe1fvalcl 
 |-  ( ( F e. B /\ 0 e. NN0 ) -> ( ( coe1 ` F ) ` 0 ) e. ( Base ` R ) )
21 7 17 20 sylancl 
 |-  ( ph -> ( ( coe1 ` F ) ` 0 ) e. ( Base ` R ) )
22 21 adantr 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) =/= .0. ) -> ( ( coe1 ` F ) ` 0 ) e. ( Base ` R ) )
23 simpr 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) =/= .0. ) -> ( ( coe1 ` F ) ` 0 ) =/= .0. )
24 2 9 3 5 19 ply1scln0 
 |-  ( ( R e. Ring /\ ( ( coe1 ` F ) ` 0 ) e. ( Base ` R ) /\ ( ( coe1 ` F ) ` 0 ) =/= .0. ) -> ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) =/= O )
25 16 22 23 24 syl3anc 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) =/= .0. ) -> ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) =/= O )
26 25 ex 
 |-  ( ph -> ( ( ( coe1 ` F ) ` 0 ) =/= .0. -> ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) =/= O ) )
27 26 necon4d 
 |-  ( ph -> ( ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) = O -> ( ( coe1 ` F ) ` 0 ) = .0. ) )
28 27 imp 
 |-  ( ( ph /\ ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) = O ) -> ( ( coe1 ` F ) ` 0 ) = .0. )
29 15 28 syldan 
 |-  ( ( ph /\ F = O ) -> ( ( coe1 ` F ) ` 0 ) = .0. )
30 12 adantr 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) = .0. ) -> F = ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) )
31 simpr 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) = .0. ) -> ( ( coe1 ` F ) ` 0 ) = .0. )
32 31 fveq2d 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) = .0. ) -> ( ( algSc ` P ) ` ( ( coe1 ` F ) ` 0 ) ) = ( ( algSc ` P ) ` .0. ) )
33 2 9 3 5 6 ply1ascl0 
 |-  ( ph -> ( ( algSc ` P ) ` .0. ) = O )
34 33 adantr 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) = .0. ) -> ( ( algSc ` P ) ` .0. ) = O )
35 30 32 34 3eqtrd 
 |-  ( ( ph /\ ( ( coe1 ` F ) ` 0 ) = .0. ) -> F = O )
36 29 35 impbida 
 |-  ( ph -> ( F = O <-> ( ( coe1 ` F ) ` 0 ) = .0. ) )