Description: Express a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mplmon2.p | |
|
mplmon2.v | |
||
mplmon2.d | |
||
mplmon2.o | |
||
mplmon2.z | |
||
mplmon2.b | |
||
mplmon2.i | |
||
mplmon2.r | |
||
mplmon2.k | |
||
mplmon2.x | |
||
Assertion | mplmon2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mplmon2.p | |
|
2 | mplmon2.v | |
|
3 | mplmon2.d | |
|
4 | mplmon2.o | |
|
5 | mplmon2.z | |
|
6 | mplmon2.b | |
|
7 | mplmon2.i | |
|
8 | mplmon2.r | |
|
9 | mplmon2.k | |
|
10 | mplmon2.x | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | 1 11 5 4 3 7 8 9 | mplmon | |
14 | 1 2 6 11 12 3 10 13 | mplvsca | |
15 | ovex | |
|
16 | 3 15 | rabex2 | |
17 | 16 | a1i | |
18 | 10 | adantr | |
19 | 4 | fvexi | |
20 | 5 | fvexi | |
21 | 19 20 | ifex | |
22 | 21 | a1i | |
23 | fconstmpt | |
|
24 | 23 | a1i | |
25 | eqidd | |
|
26 | 17 18 22 24 25 | offval2 | |
27 | oveq2 | |
|
28 | 27 | eqeq1d | |
29 | oveq2 | |
|
30 | 29 | eqeq1d | |
31 | 6 12 4 | ringridm | |
32 | 8 10 31 | syl2anc | |
33 | iftrue | |
|
34 | 33 | eqcomd | |
35 | 32 34 | sylan9eq | |
36 | 6 12 5 | ringrz | |
37 | 8 10 36 | syl2anc | |
38 | iffalse | |
|
39 | 38 | eqcomd | |
40 | 37 39 | sylan9eq | |
41 | 28 30 35 40 | ifbothda | |
42 | 41 | mpteq2dv | |
43 | 14 26 42 | 3eqtrd | |