Metamath Proof Explorer

Theorem deg1mul

Description: Degree of multiplication of two nonzero polynomials in a domain. (Contributed by metakunt, 6-May-2025)

Ref Expression
Hypotheses deg1mul.1 
|- D = ( deg1 ` R )
deg1mul.2 
|- P = ( Poly1 ` R )
deg1mul.3 
|- B = ( Base ` P )
deg1mul.4 
|- .x. = ( .r ` P )
deg1mul.5 
|- .0. = ( 0g ` P )
deg1mul.6 
|- ( ph -> R e. Domn )
deg1mul.7 
|- ( ph -> F e. B )
deg1mul.8 
|- ( ph -> F =/= .0. )
deg1mul.9 
|- ( ph -> G e. B )
deg1mul.10 
|- ( ph -> G =/= .0. )
Assertion deg1mul 
|- ( ph -> ( D ` ( F .x. G ) ) = ( ( D ` F ) + ( D ` G ) ) )

Proof

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