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 0 I | m -1 Fin
tdeglem.h H = h A fld h
Assertion tdeglem1OLD I V H : A 0

Proof

Step Hyp Ref Expression
1 tdeglem.a A = m 0 I | m -1 Fin
2 tdeglem.h H = h A fld h
3 cnfld0 0 = 0 fld
4 cnring fld Ring
5 ringcmn fld Ring fld CMnd
6 4 5 mp1i I V h A fld CMnd
7 simpl I V h A I V
8 nn0subm 0 SubMnd fld
9 8 a1i I V h A 0 SubMnd fld
10 1 psrbagfOLD I V h A h : I 0
11 1 psrbagfsuppOLD h A I V finSupp 0 h
12 11 ancoms I V h A finSupp 0 h
13 3 6 7 9 10 12 gsumsubmcl I V h A fld h 0
14 13 2 fmptd I V H : A 0