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