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) Remove sethood antecedent. (Revised by SN, 7-Aug-2024)

	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	$$⊢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	$$⊢h\in A\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
7		id	$$⊢h\in A\to h\in A$$
8	1	psrbagf	$$⊢h\in A\to h:I⟶{\mathbb{N}}_0$$
9	8	ffnd	$$⊢h\in A\to hFnI$$
10	7 9	fndmexd	$$⊢h\in A\to I\in \mathrm{V}$$
11		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
12	11	a1i	$$⊢h\in A\to {\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
13	1	psrbagfsupp	$$⊢h\in A\to {finSupp}_0\left(h\right)$$
14	3 6 10 12 8 13	gsumsubmcl	$$⊢h\in A\to {\sum }_{{ℂ}_{\mathrm{fld}}}h\in {\mathbb{N}}_0$$
15	2 14	fmpti	$$⊢H:A⟶{\mathbb{N}}_0$$