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 = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
	tdeglem.h	|- H = ( h e. A |-> ( CCfld gsum h ) )
Assertion	tdeglem1	|- ( I e. V -> 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	|- ( ( I e. V /\ h e. A ) -> CCfld e. CMnd )
7		simpl	|- ( ( I e. V /\ h e. A ) -> I e. V )
8		nn0subm	|- NN0 e. ( SubMnd ` CCfld )
9	8	a1i	|- ( ( I e. V /\ h e. A ) -> NN0 e. ( SubMnd ` CCfld ) )
10	1	psrbagf	|- ( ( I e. V /\ h e. A ) -> h : I --> NN0 )
11	1	psrbagfsupp	|- ( ( h e. A /\ I e. V ) -> h finSupp 0 )
12	11	ancoms	|- ( ( I e. V /\ h e. A ) -> h finSupp 0 )
13	3 6 7 9 10 12	gsumsubmcl	|- ( ( I e. V /\ h e. A ) -> ( CCfld gsum h ) e. NN0 )
14	13 2	fmptd	|- ( I e. V -> H : A --> NN0 )