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 𝐴 = { 𝑚 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑚 “ ℕ ) ∈ Fin }
tdeglem.h 𝐻 = ( 𝐴 ↦ ( ℂfld Σg ) )
Assertion tdeglem1OLD ( 𝐼𝑉𝐻 : 𝐴 ⟶ ℕ0 )

Proof

Step Hyp Ref Expression
1 tdeglem.a 𝐴 = { 𝑚 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑚 “ ℕ ) ∈ Fin }
2 tdeglem.h 𝐻 = ( 𝐴 ↦ ( ℂfld Σg ) )
3 cnfld0 0 = ( 0g ‘ ℂfld )
4 cnring fld ∈ Ring
5 ringcmn ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
6 4 5 mp1i ( ( 𝐼𝑉𝐴 ) → ℂfld ∈ CMnd )
7 simpl ( ( 𝐼𝑉𝐴 ) → 𝐼𝑉 )
8 nn0subm 0 ∈ ( SubMnd ‘ ℂfld )
9 8 a1i ( ( 𝐼𝑉𝐴 ) → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
10 1 psrbagfOLD ( ( 𝐼𝑉𝐴 ) → : 𝐼 ⟶ ℕ0 )
11 1 psrbagfsuppOLD ( ( 𝐴𝐼𝑉 ) → finSupp 0 )
12 11 ancoms ( ( 𝐼𝑉𝐴 ) → finSupp 0 )
13 3 6 7 9 10 12 gsumsubmcl ( ( 𝐼𝑉𝐴 ) → ( ℂfld Σg ) ∈ ℕ0 )
14 13 2 fmptd ( 𝐼𝑉𝐻 : 𝐴 ⟶ ℕ0 )