Definition df-mhp

Description: Define the subspaces of order- n homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmhp	$$class\mathrm{mHomP}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		vn	$$setvarn$$
5		cn0	$$class{\mathbb{N}}_0$$
6		vf	$$setvarf$$
7		cbs	$$class\mathrm{Base}$$
8	1	cv	$$setvari$$
9		cmpl	$$class\mathrm{mPoly}$$
10	3	cv	$$setvarr$$
11	8 10 9	co	$$class\left(i\mathrm{mPoly}r\right)$$
12	11 7	cfv	$$class{\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}$$
13	6	cv	$$setvarf$$
14		csupp	$$class\mathrm{supp}$$
15		c0g	$$class{0}_{𝑔}$$
16	10 15	cfv	$$class{0}_r$$
17	13 16 14	co	$$class{supp}_{0_r}\left(f\right)$$
18		vg	$$setvarg$$
19		vh	$$setvarh$$
20		cmap	$$class{\uparrow }_{𝑚}$$
21	5 8 20	co	$$class\left({{\mathbb{N}}_0}^i\right)$$
22	19	cv	$$setvarh$$
23	22	ccnv	$$class{h}^{-1}$$
24		cn	$$class\mathbb{N}$$
25	23 24	cima	$$class{h}^{-1}\left[\mathbb{N}\right]$$
26		cfn	$$class\mathrm{Fin}$$
27	25 26	wcel	$$wff{h}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
28	27 19 21	crab	$$class\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
29		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
30		cress	$$class{\upharpoonright }_{𝑠}$$
31	29 5 30	co	$$class\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)$$
32		cgsu	$$class{\Sigma }_{𝑔}$$
33	18	cv	$$setvarg$$
34	31 33 32	co	$$class\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},g\right)$$
35	4	cv	$$setvarn$$
36	34 35	wceq	$$wff{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n$$
37	36 18 28	crab	$$class\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\}$$
38	17 37	wss	$$wfff\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\}$$
39	38 6 12	crab	$$class\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\}$$
40	4 5 39	cmpt	$$class\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)$$
41	1 3 2 2 40	cmpo	$$class\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)$$
42	0 41	wceq	$$wff\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)$$