Metamath Proof Explorer

Theorem deg1mul3

Description: Degree of multiplication of a polynomial on the left by a nonzero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Jul-2019)

Ref Expression
Hypotheses deg1mul3.d 
|- D = ( deg1 ` R )
deg1mul3.p 
|- P = ( Poly1 ` R )
deg1mul3.e 
|- E = ( RLReg ` R )
deg1mul3.b 
|- B = ( Base ` P )
deg1mul3.t 
|- .x. = ( .r ` P )
deg1mul3.a 
|- A = ( algSc ` P )
Assertion deg1mul3 
|- ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) = ( D ` G ) )

Proof

Step Hyp Ref Expression
1 deg1mul3.d 
 |-  D = ( deg1 ` R )
2 deg1mul3.p 
 |-  P = ( Poly1 ` R )
3 deg1mul3.e 
 |-  E = ( RLReg ` R )
4 deg1mul3.b 
 |-  B = ( Base ` P )
5 deg1mul3.t 
 |-  .x. = ( .r ` P )
6 deg1mul3.a 
 |-  A = ( algSc ` P )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 3 7 rrgss 
 |-  E C_ ( Base ` R )
9 8 sseli 
 |-  ( F e. E -> F e. ( Base ` R ) )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 2 4 7 6 5 10 coe1sclmul 
 |-  ( ( R e. Ring /\ F e. ( Base ` R ) /\ G e. B ) -> ( coe1 ` ( ( A ` F ) .x. G ) ) = ( ( NN0 X. { F } ) oF ( .r ` R ) ( coe1 ` G ) ) )
12 9 11 syl3an2 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( coe1 ` ( ( A ` F ) .x. G ) ) = ( ( NN0 X. { F } ) oF ( .r ` R ) ( coe1 ` G ) ) )
13 12 oveq1d 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) = ( ( ( NN0 X. { F } ) oF ( .r ` R ) ( coe1 ` G ) ) supp ( 0g ` R ) ) )
14 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
15 nn0ex 
 |-  NN0 e. _V
16 15 a1i 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> NN0 e. _V )
17 simp1 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> R e. Ring )
18 simp2 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> F e. E )
19 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
20 19 4 2 7 coe1f 
 |-  ( G e. B -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
21 20 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
22 3 7 10 14 16 17 18 21 rrgsupp 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( ( ( NN0 X. { F } ) oF ( .r ` R ) ( coe1 ` G ) ) supp ( 0g ` R ) ) = ( ( coe1 ` G ) supp ( 0g ` R ) ) )
23 13 22 eqtrd 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) = ( ( coe1 ` G ) supp ( 0g ` R ) ) )
24 23 supeq1d 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> sup ( ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) , RR* , < ) = sup ( ( ( coe1 ` G ) supp ( 0g ` R ) ) , RR* , < ) )
25 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
26 25 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> P e. Ring )
27 2 6 7 4 ply1sclf 
 |-  ( R e. Ring -> A : ( Base ` R ) --> B )
28 27 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> A : ( Base ` R ) --> B )
29 9 3ad2ant2 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> F e. ( Base ` R ) )
30 28 29 ffvelcdmd 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( A ` F ) e. B )
31 simp3 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> G e. B )
32 4 5 ringcl 
 |-  ( ( P e. Ring /\ ( A ` F ) e. B /\ G e. B ) -> ( ( A ` F ) .x. G ) e. B )
33 26 30 31 32 syl3anc 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( ( A ` F ) .x. G ) e. B )
34 eqid 
 |-  ( coe1 ` ( ( A ` F ) .x. G ) ) = ( coe1 ` ( ( A ` F ) .x. G ) )
35 1 2 4 14 34 deg1val 
 |-  ( ( ( A ` F ) .x. G ) e. B -> ( D ` ( ( A ` F ) .x. G ) ) = sup ( ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) , RR* , < ) )
36 33 35 syl 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) = sup ( ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) , RR* , < ) )
37 1 2 4 14 19 deg1val 
 |-  ( G e. B -> ( D ` G ) = sup ( ( ( coe1 ` G ) supp ( 0g ` R ) ) , RR* , < ) )
38 37 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( D ` G ) = sup ( ( ( coe1 ` G ) supp ( 0g ` R ) ) , RR* , < ) )
39 24 36 38 3eqtr4d 
 |-  ( ( R e. Ring /\ F e. E /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) = ( D ` G ) )