Theorem mhpval

Description: Value of the "homogeneous polynomial" function. (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$$
	mhpval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	mhpval	$$⊢\phi \to H\left(N\right)=\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\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		mhpval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9	1 2 3 4 5 6 7	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 _{j\in {\mathbb{N}}_0}g\left(j\right)=n\right\}\right\}\right)$$
10		eqeq2	$$⊢n=N\to \left(\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=n\leftrightarrow \sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right)$$
11	10	rabbidv	$$⊢n=N\to \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=n\right\}=\left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}$$
12	11	sseq2d	$$⊢n=N\to \left(f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=n\right\}\leftrightarrow f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}\right)$$
13	12	rabbidv	$$⊢n=N\to \left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=n\right\}\right\}=\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}\right\}$$
14	13	adantl	$$⊢\left(\phi \wedge n=N\right)\to \left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=n\right\}\right\}=\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}\right\}$$
15	3	fvexi	$$⊢B\in \mathrm{V}$$
16	15	rabex	$$⊢\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}\right\}\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to \left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}\right\}\in \mathrm{V}$$
18	9 14 8 17	fvmptd	$$⊢\phi \to H\left(N\right)=\left\{f\in B|f\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}\right\}$$