Metamath Proof Explorer


Theorem mhpvscacl

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 H=ImHomPR
mhpvscacl.p P=ImPolyR
mhpvscacl.t ·˙=P
mhpvscacl.k K=BaseR
mhpvscacl.r φRRing
mhpvscacl.n φN0
mhpvscacl.x φXK
mhpvscacl.f φFHN
Assertion mhpvscacl φX·˙FHN

Proof

Step Hyp Ref Expression
1 mhpvscacl.h H=ImHomPR
2 mhpvscacl.p P=ImPolyR
3 mhpvscacl.t ·˙=P
4 mhpvscacl.k K=BaseR
5 mhpvscacl.r φRRing
6 mhpvscacl.n φN0
7 mhpvscacl.x φXK
8 mhpvscacl.f φFHN
9 eqid BaseP=BaseP
10 eqid 0R=0R
11 eqid h0I|h-1Fin=h0I|h-1Fin
12 reldmmhp ReldommHomP
13 12 1 8 elfvov1 φIV
14 2 13 5 mpllmodd φPLMod
15 7 4 eleqtrdi φXBaseR
16 2 13 5 mplsca φR=ScalarP
17 16 fveq2d φBaseR=BaseScalarP
18 15 17 eleqtrd φXBaseScalarP
19 1 2 9 13 5 6 8 mhpmpl φFBaseP
20 eqid ScalarP=ScalarP
21 eqid BaseScalarP=BaseScalarP
22 9 20 3 21 lmodvscl PLModXBaseScalarPFBasePX·˙FBaseP
23 14 18 19 22 syl3anc φX·˙FBaseP
24 2 4 9 11 23 mplelf φX·˙F:h0I|h-1FinK
25 eqid R=R
26 7 adantr φkh0I|h-1Finsupp0RFXK
27 19 adantr φkh0I|h-1Finsupp0RFFBaseP
28 eldifi kh0I|h-1Finsupp0RFkh0I|h-1Fin
29 28 adantl φkh0I|h-1Finsupp0RFkh0I|h-1Fin
30 2 3 4 9 25 11 26 27 29 mplvscaval φkh0I|h-1Finsupp0RFX·˙Fk=XRFk
31 2 4 9 11 19 mplelf φF:h0I|h-1FinK
32 ssidd φFsupp0RFsupp0R
33 ovexd φ0IV
34 11 33 rabexd φh0I|h-1FinV
35 fvexd φ0RV
36 31 32 34 35 suppssr φkh0I|h-1Finsupp0RFFk=0R
37 36 oveq2d φkh0I|h-1Finsupp0RFXRFk=XR0R
38 4 25 10 ringrz RRingXKXR0R=0R
39 5 7 38 syl2anc φXR0R=0R
40 39 adantr φkh0I|h-1Finsupp0RFXR0R=0R
41 30 37 40 3eqtrd φkh0I|h-1Finsupp0RFX·˙Fk=0R
42 24 41 suppss φX·˙Fsupp0RFsupp0R
43 1 10 11 13 5 6 8 mhpdeg φFsupp0Rgh0I|h-1Fin|fld𝑠0g=N
44 42 43 sstrd φX·˙Fsupp0Rgh0I|h-1Fin|fld𝑠0g=N
45 1 2 9 10 11 13 5 6 23 44 ismhp2 φX·˙FHN