| 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 ) |