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