Theorem mhpvscacl

Description: Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

	Ref	Expression
Hypotheses	mhpvscacl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpvscacl.p	$$⊢P=I\mathrm{mPoly}R$$
	mhpvscacl.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	mhpvscacl.k	$$⊢K={\mathrm{Base}}_R$$
	mhpvscacl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mhpvscacl.x	$$⊢\phi \to X\in K$$
	mhpvscacl.f	$$⊢\phi \to F\in H\left(N\right)$$
Assertion	mhpvscacl	$$⊢\phi \to X\underset{\dot{}}{·}F\in H\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhpvscacl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpvscacl.p	$$⊢P=I\mathrm{mPoly}R$$
3		mhpvscacl.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
4		mhpvscacl.k	$$⊢K={\mathrm{Base}}_R$$
5		mhpvscacl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		mhpvscacl.x	$$⊢\phi \to X\in K$$
7		mhpvscacl.f	$$⊢\phi \to F\in H\left(N\right)$$
8		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
9		eqid	$$⊢0_R=0_R$$
10		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
11		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
12	11 1 7	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
13	1 7	mhprcl	$$⊢\phi \to N\in {\mathbb{N}}_0$$
14		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
15		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
16	2 12 5	mpllmodd	$$⊢\phi \to P\in \mathrm{LMod}$$
17	6 4	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_R$$
18	2 12 5	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
19	18	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
20	17 19	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
21	1 2 8 7	mhpmpl	$$⊢\phi \to F\in {\mathrm{Base}}_P$$
22	8 14 3 15 16 20 21	lmodvscld	$$⊢\phi \to X\underset{\dot{}}{·}F\in {\mathrm{Base}}_P$$
23	2 4 8 10 22	mplelf	$$⊢\phi \to \left(X\underset{\dot{}}{·}F\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶K$$
24		eqid	$$⊢{\cdot }_R={\cdot }_R$$
25	6	adantr	$$⊢\left(\phi \wedge k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\right)\to X\in K$$
26	21	adantr	$$⊢\left(\phi \wedge k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\right)\to F\in {\mathrm{Base}}_P$$
27		eldifi	$$⊢k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\to k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
28	27	adantl	$$⊢\left(\phi \wedge k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\right)\to k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
29	2 3 4 8 24 10 25 26 28	mplvscaval	$$⊢\left(\phi \wedge k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\right)\to \left(X\underset{\dot{}}{·}F\right)\left(k\right)=X{\cdot }_{R}F\left(k\right)$$
30	2 4 8 10 21	mplelf	$$⊢\phi \to F:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶K$$
31		ssidd	$$⊢\phi \to F\mathrm{supp}{0}_R\subseteq F\mathrm{supp}{0}_R$$
32		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
33	30 31 7 32	suppssrg	$$⊢\left(\phi \wedge k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\right)\to F\left(k\right)=0_R$$
34	33	oveq2d	$$⊢\left(\phi \wedge k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\right)\to X{\cdot }_{R}F\left(k\right)=X{\cdot }_R{0}_R$$
35	4 24 9 5 6	ringrzd	$$⊢\phi \to X{\cdot }_R{0}_R=0_R$$
36	35	adantr	$$⊢\left(\phi \wedge k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\right)\to X{\cdot }_R{0}_R=0_R$$
37	29 34 36	3eqtrd	$$⊢\left(\phi \wedge k\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus {supp}_{0_R}\left(F\right)\right)\right)\to \left(X\underset{\dot{}}{·}F\right)\left(k\right)=0_R$$
38	23 37	suppss	$$⊢\phi \to \left(X\underset{\dot{}}{·}F\right)\mathrm{supp}{0}_R\subseteq F\mathrm{supp}{0}_R$$
39	1 9 10 7	mhpdeg	$$⊢\phi \to F\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
40	38 39	sstrd	$$⊢\phi \to \left(X\underset{\dot{}}{·}F\right)\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
41	1 2 8 9 10 12 5 13 22 40	ismhp2	$$⊢\phi \to X\underset{\dot{}}{·}F\in H\left(N\right)$$