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
|
psrbagfOLD |
|- ( ( I e. V /\ h e. A ) -> h : I --> NN0 ) |
11 |
1
|
psrbagfsuppOLD |
|- ( ( 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 ) |