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=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.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	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.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		mhpvscacl.x	$$⊢\phi \to X\in K$$
8		mhpvscacl.f	$$⊢\phi \to F\in H\left(N\right)$$
9		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
10		eqid	$$⊢0_R=0_R$$
11		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\}$$
12		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
13	12 1 8	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
14	2 13 5	mpllmodd	$$⊢\phi \to P\in \mathrm{LMod}$$
15	7 4	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_R$$
16	2 13 5	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
17	16	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
18	15 17	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
19	1 2 9 13 5 6 8	mhpmpl	$$⊢\phi \to F\in {\mathrm{Base}}_P$$
20		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
21		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
22	9 20 3 21	lmodvscl	$$⊢\left(P\in \mathrm{LMod}\wedge X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge F\in {\mathrm{Base}}_P\right)\to X\underset{\dot{}}{·}F\in {\mathrm{Base}}_P$$
23	14 18 19 22	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}F\in {\mathrm{Base}}_P$$
24	2 4 9 11 23	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$$
25		eqid	$$⊢{\cdot }_R={\cdot }_R$$
26	7	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$$
27	19	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$$
28		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\}$$
29	28	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\}$$
30	2 3 4 9 25 11 26 27 29	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)$$
31	2 4 9 11 19	mplelf	$$⊢\phi \to F:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶K$$
32		ssidd	$$⊢\phi \to F\mathrm{supp}{0}_R\subseteq F\mathrm{supp}{0}_R$$
33		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
34	11 33	rabexd	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
35		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
36	31 32 34 35	suppssr	$$⊢\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$$
37	36	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$$
38	4 25 10	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to X{\cdot }_R{0}_R=0_R$$
39	5 7 38	syl2anc	$$⊢\phi \to X{\cdot }_R{0}_R=0_R$$
40	39	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$$
41	30 37 40	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$$
42	24 41	suppss	$$⊢\phi \to \left(X\underset{\dot{}}{·}F\right)\mathrm{supp}{0}_R\subseteq F\mathrm{supp}{0}_R$$
43	1 10 11 13 5 6 8	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\}$$
44	42 43	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\}$$
45	1 2 9 10 11 13 5 6 23 44	ismhp2	$$⊢\phi \to X\underset{\dot{}}{·}F\in H\left(N\right)$$