Metamath Proof Explorer


Theorem tdeglem1OLD

Description: Obsolete version of tdeglem1 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)

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 tdeglem1OLD
|- ( 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 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 )