Theorem tdeglem1

Description: Functionality of the total degree helper function. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

	Ref	Expression
Hypotheses	tdeglem.a	$$⊢A=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	tdeglem.h	$$⊢H=\left(h\in A⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
Assertion	tdeglem1	$$⊢I\in V\to H:A⟶{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		tdeglem.a	$$⊢A=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		tdeglem.h	$$⊢H=\left(h\in A⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
3		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
4		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
5		ringcmn	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
6	4 5	mp1i	$$⊢\left(I\in V\wedge h\in A\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
7		simpl	$$⊢\left(I\in V\wedge h\in A\right)\to I\in V$$
8		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
9	8	a1i	$$⊢\left(I\in V\wedge h\in A\right)\to {\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
10	1	psrbagf	$$⊢\left(I\in V\wedge h\in A\right)\to h:I⟶{\mathbb{N}}_0$$
11	1	psrbagfsupp	$$⊢\left(h\in A\wedge I\in V\right)\to {finSupp}_0\left(h\right)$$
12	11	ancoms	$$⊢\left(I\in V\wedge h\in A\right)\to {finSupp}_0\left(h\right)$$
13	3 6 7 9 10 12	gsumsubmcl	$$⊢\left(I\in V\wedge h\in A\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}h\in {\mathbb{N}}_0$$
14	13 2	fmptd	$$⊢I\in V\to H:A⟶{\mathbb{N}}_0$$