This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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