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

Theorem deg1mul3le 19502
 Description: Degree of multiplication of a polynomial on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.)
Hypotheses
Ref Expression
deg1mul3le.d deg1
deg1mul3le.p Poly1
deg1mul3le.k
deg1mul3le.b
deg1mul3le.t
deg1mul3le.a algSc
Assertion
Ref Expression
deg1mul3le

Proof of Theorem deg1mul3le
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 deg1mul3le.p . . . . . . . 8 Poly1
21ply1rng 16326 . . . . . . 7
323ad2ant1 976 . . . . . 6
4 deg1mul3le.a . . . . . . . . 9 algSc
5 deg1mul3le.k . . . . . . . . 9
6 deg1mul3le.b . . . . . . . . 9
71, 4, 5, 6ply1sclf 16361 . . . . . . . 8
873ad2ant1 976 . . . . . . 7
9 simp2 956 . . . . . . 7
10 ffvelrn 5663 . . . . . . 7
118, 9, 10syl2anc 642 . . . . . 6
12 simp3 957 . . . . . 6
13 deg1mul3le.t . . . . . . 7
146, 13rngcl 15354 . . . . . 6
153, 11, 12, 14syl3anc 1182 . . . . 5
16 eqid 2283 . . . . . 6 coe1 coe1
1716, 6, 1, 5coe1f 16292 . . . . 5 coe1
1815, 17syl 15 . . . 4 coe1
19 eldifi 3298 . . . . . 6 coe1
20 simpl1 958 . . . . . . 7
21 simpl2 959 . . . . . . 7
22 simpl3 960 . . . . . . 7
23 simpr 447 . . . . . . 7
24 eqid 2283 . . . . . . . 8
251, 6, 5, 4, 13, 24coe1sclmulfv 16359 . . . . . . 7 coe1 coe1
2620, 21, 22, 23, 25syl121anc 1187 . . . . . 6 coe1 coe1
2719, 26sylan2 460 . . . . 5 coe1 coe1 coe1
28 eqid 2283 . . . . . . . . 9 coe1 coe1
2928, 6, 1, 5coe1f 16292 . . . . . . . 8 coe1
30293ad2ant3 978 . . . . . . 7 coe1
31 ssid 3197 . . . . . . . 8 coe1 coe1
3231a1i 10 . . . . . . 7 coe1 coe1
3330, 32suppssr 5659 . . . . . 6 coe1 coe1
3433oveq2d 5874 . . . . 5 coe1 coe1
35 eqid 2283 . . . . . . . 8
365, 24, 35rngrz 15378 . . . . . . 7
37363adant3 975 . . . . . 6
3837adantr 451 . . . . 5 coe1
3927, 34, 383eqtrd 2319 . . . 4 coe1 coe1
4018, 39suppss 5658 . . 3 coe1 coe1
41 cnvimass 5033 . . . . 5 coe1 coe1
42 fdm 5393 . . . . . 6 coe1 coe1
4330, 42syl 15 . . . . 5 coe1
4441, 43syl5sseq 3226 . . . 4 coe1
45 nn0ssre 9969 . . . . 5
46 ressxr 8876 . . . . 5
4745, 46sstri 3188 . . . 4
4844, 47syl6ss 3191 . . 3 coe1
49 supxrss 10651 . . 3 coe1 coe1 coe1 coe1 coe1
5040, 48, 49syl2anc 642 . 2 coe1 coe1
51 deg1mul3le.d . . . 4 deg1
5251, 1, 6, 35, 16deg1val 19482 . . 3 coe1
5315, 52syl 15 . 2 coe1
5451, 1, 6, 35, 28deg1val 19482 . . 3 coe1