Description: Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023) Remove sethood hypothesis. (Revised by SN, 18-May-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mhpvscacl.h | |
|
mhpvscacl.p | |
||
mhpvscacl.t | |
||
mhpvscacl.k | |
||
mhpvscacl.r | |
||
mhpvscacl.n | |
||
mhpvscacl.x | |
||
mhpvscacl.f | |
||
Assertion | mhpvscacl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mhpvscacl.h | |
|
2 | mhpvscacl.p | |
|
3 | mhpvscacl.t | |
|
4 | mhpvscacl.k | |
|
5 | mhpvscacl.r | |
|
6 | mhpvscacl.n | |
|
7 | mhpvscacl.x | |
|
8 | mhpvscacl.f | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | reldmmhp | |
|
13 | 12 1 8 | elfvov1 | |
14 | 2 13 5 | mpllmodd | |
15 | 7 4 | eleqtrdi | |
16 | 2 13 5 | mplsca | |
17 | 16 | fveq2d | |
18 | 15 17 | eleqtrd | |
19 | 1 2 9 13 5 6 8 | mhpmpl | |
20 | eqid | |
|
21 | eqid | |
|
22 | 9 20 3 21 | lmodvscl | |
23 | 14 18 19 22 | syl3anc | |
24 | 2 4 9 11 23 | mplelf | |
25 | eqid | |
|
26 | 7 | adantr | |
27 | 19 | adantr | |
28 | eldifi | |
|
29 | 28 | adantl | |
30 | 2 3 4 9 25 11 26 27 29 | mplvscaval | |
31 | 2 4 9 11 19 | mplelf | |
32 | ssidd | |
|
33 | ovexd | |
|
34 | 11 33 | rabexd | |
35 | fvexd | |
|
36 | 31 32 34 35 | suppssr | |
37 | 36 | oveq2d | |
38 | 4 25 10 | ringrz | |
39 | 5 7 38 | syl2anc | |
40 | 39 | adantr | |
41 | 30 37 40 | 3eqtrd | |
42 | 24 41 | suppss | |
43 | 1 10 11 13 5 6 8 | mhpdeg | |
44 | 42 43 | sstrd | |
45 | 1 2 9 10 11 13 5 6 23 44 | ismhp2 | |