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=m0I|m-1Fin
tdeglem.h H=hAfldh
Assertion tdeglem1OLD IVH:A0

Proof

Step Hyp Ref Expression
1 tdeglem.a A=m0I|m-1Fin
2 tdeglem.h H=hAfldh
3 cnfld0 0=0fld
4 cnring fldRing
5 ringcmn fldRingfldCMnd
6 4 5 mp1i IVhAfldCMnd
7 simpl IVhAIV
8 nn0subm 0SubMndfld
9 8 a1i IVhA0SubMndfld
10 1 psrbagfOLD IVhAh:I0
11 1 psrbagfsuppOLD hAIVfinSupp0h
12 11 ancoms IVhAfinSupp0h
13 3 6 7 9 10 12 gsumsubmcl IVhAfldh0
14 13 2 fmptd IVH:A0