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 = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
	tdeglem.h	|- H = ( h e. A |-> ( CCfld gsum h ) )
Assertion	tdeglem1	|- H : A --> NN0

Proof

Step	Hyp	Ref	Expression
1		tdeglem.a	|- A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
2		tdeglem.h	|- H = ( h e. A |-> ( CCfld gsum h ) )
3		cnfld0	|- 0 = ( 0g ` CCfld )
4		cnring	|- CCfld e. Ring
5		ringcmn	|- ( CCfld e. Ring -> CCfld e. CMnd )
6	4 5	mp1i	|- ( h e. A -> CCfld e. CMnd )
7		id	|- ( h e. A -> h e. A )
8	1	psrbagf	|- ( h e. A -> h : I --> NN0 )
9	8	ffnd	|- ( h e. A -> h Fn I )
10	7 9	fndmexd	|- ( h e. A -> I e. _V )
11		nn0subm	|- NN0 e. ( SubMnd ` CCfld )
12	11	a1i	|- ( h e. A -> NN0 e. ( SubMnd ` CCfld ) )
13	1	psrbagfsupp	|- ( h e. A -> h finSupp 0 )
14	3 6 10 12 8 13	gsumsubmcl	|- ( h e. A -> ( CCfld gsum h ) e. NN0 )
15	2 14	fmpti	|- H : A --> NN0