Theorem mhpfval

Description: Value of the "homogeneous polynomial" operator. (Contributed by Steven Nguyen, 25-Aug-2023)

	Ref	Expression
Hypotheses	mhpfval.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpfval.p	$$⊢P=I\mathrm{mPoly}R$$
	mhpfval.b	$$⊢B={\mathrm{Base}}_P$$
	mhpfval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	mhpfval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mhpfval.i	$$⊢\phi \to I\in V$$
	mhpfval.r	$$⊢\phi \to R\in W$$
Assertion	mhpfval	$$⊢\phi \to H=\left(n\in {\mathbb{N}}_0⟼\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhpfval.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpfval.p	$$⊢P=I\mathrm{mPoly}R$$
3		mhpfval.b	$$⊢B={\mathrm{Base}}_P$$
4		mhpfval.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		mhpfval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		mhpfval.i	$$⊢\phi \to I\in V$$
7		mhpfval.r	$$⊢\phi \to R\in W$$
8	6	elexd	$$⊢\phi \to I\in \mathrm{V}$$
9	7	elexd	$$⊢\phi \to R\in \mathrm{V}$$
10		oveq12	$$⊢\left(i=I\wedge r=R\right)\to i\mathrm{mPoly}r=I\mathrm{mPoly}R$$
11	10 2	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to i\mathrm{mPoly}r=P$$
12	11	fveq2d	$$⊢\left(i=I\wedge r=R\right)\to {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}={\mathrm{Base}}_P$$
13	12 3	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}=B$$
14		fveq2	$$⊢r=R\to 0_r=0_R$$
15	14 4	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
16	15	oveq2d	$$⊢r=R\to f\mathrm{supp}{0}_r=f\mathrm{supp}\underset{\dot{}}{0}$$
17	16	adantl	$$⊢\left(i=I\wedge r=R\right)\to f\mathrm{supp}{0}_r=f\mathrm{supp}\underset{\dot{}}{0}$$
18		oveq2	$$⊢i=I\to {{\mathbb{N}}_0}^i={{\mathbb{N}}_0}^I$$
19	18	rabeqdv	$$⊢i=I\to \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\}$$
20	19 5	eqtr4di	$$⊢i=I\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=D$$
21	20	rabeqdv	$$⊢i=I\to \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\}=\left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}$$
22	21	adantr	$$⊢\left(i=I\wedge r=R\right)\to \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\}=\left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}$$
23	17 22	sseq12d	$$⊢\left(i=I\wedge r=R\right)\to \left(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\}\leftrightarrow f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right)$$
24	13 23	rabeqbidv	$$⊢\left(i=I\wedge r=R\right)\to \left\{f\in {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}|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\}\right\}=\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}$$
25	24	mpteq2dv	$$⊢\left(i=I\wedge r=R\right)\to \left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}|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\}\right\}\right)=\left(n\in {\mathbb{N}}_0⟼\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)$$
26		df-mhp	$$⊢\mathrm{mHomP}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}|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\}\right\}\right)\right)$$
27		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
28	27	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)\in \mathrm{V}$$
29	25 26 28	ovmpoa	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to I\mathrm{mHomP}R=\left(n\in {\mathbb{N}}_0⟼\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)$$
30	8 9 29	syl2anc	$$⊢\phi \to I\mathrm{mHomP}R=\left(n\in {\mathbb{N}}_0⟼\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)$$
31	1 30	eqtrid	$$⊢\phi \to H=\left(n\in {\mathbb{N}}_0⟼\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)$$