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