| Step |
Hyp |
Ref |
Expression |
| 1 |
|
deg1mul.1 |
|- D = ( deg1 ` R ) |
| 2 |
|
deg1mul.2 |
|- P = ( Poly1 ` R ) |
| 3 |
|
deg1mul.3 |
|- B = ( Base ` P ) |
| 4 |
|
deg1mul.4 |
|- .x. = ( .r ` P ) |
| 5 |
|
deg1mul.5 |
|- .0. = ( 0g ` P ) |
| 6 |
|
deg1mul.6 |
|- ( ph -> R e. Domn ) |
| 7 |
|
deg1mul.7 |
|- ( ph -> F e. B ) |
| 8 |
|
deg1mul.8 |
|- ( ph -> F =/= .0. ) |
| 9 |
|
deg1mul.9 |
|- ( ph -> G e. B ) |
| 10 |
|
deg1mul.10 |
|- ( ph -> G =/= .0. ) |
| 11 |
|
eqid |
|- ( RLReg ` R ) = ( RLReg ` R ) |
| 12 |
|
domnring |
|- ( R e. Domn -> R e. Ring ) |
| 13 |
6 12
|
syl |
|- ( ph -> R e. Ring ) |
| 14 |
1 2 5 3
|
deg1nn0cl |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 ) |
| 15 |
13 7 8 14
|
syl3anc |
|- ( ph -> ( D ` F ) e. NN0 ) |
| 16 |
|
eqid |
|- ( coe1 ` F ) = ( coe1 ` F ) |
| 17 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
| 18 |
16 3 2 17
|
coe1fvalcl |
|- ( ( F e. B /\ ( D ` F ) e. NN0 ) -> ( ( coe1 ` F ) ` ( D ` F ) ) e. ( Base ` R ) ) |
| 19 |
7 15 18
|
syl2anc |
|- ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) e. ( Base ` R ) ) |
| 20 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
| 21 |
1 2 5 3 20 16
|
deg1ldg |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( ( coe1 ` F ) ` ( D ` F ) ) =/= ( 0g ` R ) ) |
| 22 |
13 7 8 21
|
syl3anc |
|- ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) =/= ( 0g ` R ) ) |
| 23 |
17 11 20
|
domnrrg |
|- ( ( R e. Domn /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. ( Base ` R ) /\ ( ( coe1 ` F ) ` ( D ` F ) ) =/= ( 0g ` R ) ) -> ( ( coe1 ` F ) ` ( D ` F ) ) e. ( RLReg ` R ) ) |
| 24 |
6 19 22 23
|
syl3anc |
|- ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) e. ( RLReg ` R ) ) |
| 25 |
1 2 11 3 4 5 13 7 8 24 9 10
|
deg1mul2 |
|- ( ph -> ( D ` ( F .x. G ) ) = ( ( D ` F ) + ( D ` G ) ) ) |