Metamath Proof Explorer


Theorem coe1mul4

Description: Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1mul3.s
|- Y = ( Poly1 ` R )
coe1mul3.t
|- .xb = ( .r ` Y )
coe1mul3.u
|- .x. = ( .r ` R )
coe1mul3.b
|- B = ( Base ` Y )
coe1mul3.d
|- D = ( deg1 ` R )
coe1mul4.z
|- .0. = ( 0g ` Y )
coe1mul4.r
|- ( ph -> R e. Ring )
coe1mul4.f1
|- ( ph -> F e. B )
coe1mul4.f2
|- ( ph -> F =/= .0. )
coe1mul4.g1
|- ( ph -> G e. B )
coe1mul4.g2
|- ( ph -> G =/= .0. )
Assertion coe1mul4
|- ( ph -> ( ( coe1 ` ( F .xb G ) ) ` ( ( D ` F ) + ( D ` G ) ) ) = ( ( ( coe1 ` F ) ` ( D ` F ) ) .x. ( ( coe1 ` G ) ` ( D ` G ) ) ) )

Proof

Step Hyp Ref Expression
1 coe1mul3.s
 |-  Y = ( Poly1 ` R )
2 coe1mul3.t
 |-  .xb = ( .r ` Y )
3 coe1mul3.u
 |-  .x. = ( .r ` R )
4 coe1mul3.b
 |-  B = ( Base ` Y )
5 coe1mul3.d
 |-  D = ( deg1 ` R )
6 coe1mul4.z
 |-  .0. = ( 0g ` Y )
7 coe1mul4.r
 |-  ( ph -> R e. Ring )
8 coe1mul4.f1
 |-  ( ph -> F e. B )
9 coe1mul4.f2
 |-  ( ph -> F =/= .0. )
10 coe1mul4.g1
 |-  ( ph -> G e. B )
11 coe1mul4.g2
 |-  ( ph -> G =/= .0. )
12 5 1 6 4 deg1nn0cl
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
13 7 8 9 12 syl3anc
 |-  ( ph -> ( D ` F ) e. NN0 )
14 13 nn0red
 |-  ( ph -> ( D ` F ) e. RR )
15 14 leidd
 |-  ( ph -> ( D ` F ) <_ ( D ` F ) )
16 5 1 6 4 deg1nn0cl
 |-  ( ( R e. Ring /\ G e. B /\ G =/= .0. ) -> ( D ` G ) e. NN0 )
17 7 10 11 16 syl3anc
 |-  ( ph -> ( D ` G ) e. NN0 )
18 17 nn0red
 |-  ( ph -> ( D ` G ) e. RR )
19 18 leidd
 |-  ( ph -> ( D ` G ) <_ ( D ` G ) )
20 1 2 3 4 5 7 8 13 15 10 17 19 coe1mul3
 |-  ( ph -> ( ( coe1 ` ( F .xb G ) ) ` ( ( D ` F ) + ( D ` G ) ) ) = ( ( ( coe1 ` F ) ` ( D ` F ) ) .x. ( ( coe1 ` G ) ` ( D ` G ) ) ) )