Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  deg1mul3 Unicode version

Theorem deg1mul3 19716
 Description: Degree of multiplication of a polynomial on the left by a non-zero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.)
Hypotheses
Ref Expression
deg1mul3.d deg1
deg1mul3.p Poly1
deg1mul3.e RLReg
deg1mul3.b
deg1mul3.t
deg1mul3.a algSc
Assertion
Ref Expression
deg1mul3

Proof of Theorem deg1mul3
StepHypRef Expression
1 deg1mul3.e . . . . . . . . 9 RLReg
2 eqid 2366 . . . . . . . . 9
31, 2rrgss 16243 . . . . . . . 8
43sseli 3262 . . . . . . 7
5 deg1mul3.p . . . . . . . 8 Poly1
6 deg1mul3.b . . . . . . . 8
7 deg1mul3.a . . . . . . . 8 algSc
8 deg1mul3.t . . . . . . . 8
9 eqid 2366 . . . . . . . 8
105, 6, 2, 7, 8, 9coe1sclmul 16568 . . . . . . 7 coe1 coe1
114, 10syl3an2 1217 . . . . . 6 coe1 coe1
1211cnveqd 4960 . . . . 5 coe1 coe1
1312imaeq1d 5114 . . . 4 coe1 coe1
14 eqid 2366 . . . . 5
15 nn0ex 10120 . . . . . 6
1615a1i 10 . . . . 5
17 simp1 956 . . . . 5
18 simp2 957 . . . . 5
19 eqid 2366 . . . . . . 7 coe1 coe1
2019, 6, 5, 2coe1f 16502 . . . . . 6 coe1
21203ad2ant3 979 . . . . 5 coe1
221, 2, 9, 14, 16, 17, 18, 21rrgsupp 16242 . . . 4 coe1 coe1
2313, 22eqtrd 2398 . . 3 coe1 coe1
2423supeq1d 7346 . 2 coe1 coe1
255ply1rng 16536 . . . . 5
26253ad2ant1 977 . . . 4
275, 7, 2, 6ply1sclf 16571 . . . . . 6
28273ad2ant1 977 . . . . 5
2943ad2ant2 978 . . . . 5
30 ffvelrn 5770 . . . . 5
3128, 29, 30syl2anc 642 . . . 4
32 simp3 958 . . . 4
336, 8rngcl 15564 . . . 4
3426, 31, 32, 33syl3anc 1183 . . 3
35 deg1mul3.d . . . 4 deg1
36 eqid 2366 . . . 4 coe1 coe1
3735, 5, 6, 14, 36deg1val 19697 . . 3 coe1
3834, 37syl 15 . 2 coe1
3935, 5, 6, 14, 19deg1val 19697 . . 3 coe1