Metamath Proof Explorer

Theorem deg1ldgn

Description: An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1z.d 
|- D = ( deg1 ` R )
deg1z.p 
|- P = ( Poly1 ` R )
deg1z.z 
|- .0. = ( 0g ` P )
deg1nn0cl.b 
|- B = ( Base ` P )
deg1ldg.y 
|- Y = ( 0g ` R )
deg1ldg.a 
|- A = ( coe1 ` F )
deg1ldgn.r 
|- ( ph -> R e. Ring )
deg1ldgn.f 
|- ( ph -> F e. B )
deg1ldgn.x 
|- ( ph -> X e. NN0 )
deg1ldgn.e 
|- ( ph -> ( A ` X ) = Y )
Assertion deg1ldgn 
|- ( ph -> ( D ` F ) =/= X )

Proof

Step Hyp Ref Expression
1 deg1z.d 
 |-  D = ( deg1 ` R )
2 deg1z.p 
 |-  P = ( Poly1 ` R )
3 deg1z.z 
 |-  .0. = ( 0g ` P )
4 deg1nn0cl.b 
 |-  B = ( Base ` P )
5 deg1ldg.y 
 |-  Y = ( 0g ` R )
6 deg1ldg.a 
 |-  A = ( coe1 ` F )
7 deg1ldgn.r 
 |-  ( ph -> R e. Ring )
8 deg1ldgn.f 
 |-  ( ph -> F e. B )
9 deg1ldgn.x 
 |-  ( ph -> X e. NN0 )
10 deg1ldgn.e 
 |-  ( ph -> ( A ` X ) = Y )
11 fveq2 
 |-  ( ( D ` F ) = X -> ( A ` ( D ` F ) ) = ( A ` X ) )
12 11 adantl 
 |-  ( ( ph /\ ( D ` F ) = X ) -> ( A ` ( D ` F ) ) = ( A ` X ) )
13 7 adantr 
 |-  ( ( ph /\ ( D ` F ) = X ) -> R e. Ring )
14 8 adantr 
 |-  ( ( ph /\ ( D ` F ) = X ) -> F e. B )
15 eleq1a 
 |-  ( X e. NN0 -> ( ( D ` F ) = X -> ( D ` F ) e. NN0 ) )
16 9 15 syl 
 |-  ( ph -> ( ( D ` F ) = X -> ( D ` F ) e. NN0 ) )
17 16 imp 
 |-  ( ( ph /\ ( D ` F ) = X ) -> ( D ` F ) e. NN0 )
18 1 2 3 4 deg1nn0clb 
 |-  ( ( R e. Ring /\ F e. B ) -> ( F =/= .0. <-> ( D ` F ) e. NN0 ) )
19 7 8 18 syl2anc 
 |-  ( ph -> ( F =/= .0. <-> ( D ` F ) e. NN0 ) )
20 19 adantr 
 |-  ( ( ph /\ ( D ` F ) = X ) -> ( F =/= .0. <-> ( D ` F ) e. NN0 ) )
21 17 20 mpbird 
 |-  ( ( ph /\ ( D ` F ) = X ) -> F =/= .0. )
22 1 2 3 4 5 6 deg1ldg 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= Y )
23 13 14 21 22 syl3anc 
 |-  ( ( ph /\ ( D ` F ) = X ) -> ( A ` ( D ` F ) ) =/= Y )
24 12 23 eqnetrrd 
 |-  ( ( ph /\ ( D ` F ) = X ) -> ( A ` X ) =/= Y )
25 24 ex 
 |-  ( ph -> ( ( D ` F ) = X -> ( A ` X ) =/= Y ) )
26 25 necon2d 
 |-  ( ph -> ( ( A ` X ) = Y -> ( D ` F ) =/= X ) )
27 10 26 mpd 
 |-  ( ph -> ( D ` F ) =/= X )