Theorem mhpvscacl

Description: Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023)

	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.i	$$⊢\phi \to I\in V$$
	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.i	$$⊢\phi \to I\in V$$
6		mhpvscacl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		mhpvscacl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
8		mhpvscacl.x	$$⊢\phi \to X\in K$$
9		mhpvscacl.f	$$⊢\phi \to F\in H\left(N\right)$$
10		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
11		eqid	$$⊢0_R=0_R$$
12		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\}$$
13	2	mpllmod	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{LMod}$$
14	5 6 13	syl2anc	$$⊢\phi \to P\in \mathrm{LMod}$$
15	8 4	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_R$$
16	2 5 6	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 10 5 6 7 9	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	10 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 10 12 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	8	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 10 25 12 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 10 12 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	12 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 11	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to X{\cdot }_R{0}_R=0_R$$
39	6 8 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 11 12 5 6 7 9	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 10 11 12 5 6 7 23 44	ismhp2	$$⊢\phi \to X\underset{\dot{}}{·}F\in H\left(N\right)$$