This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tdeglem1

Description: Functionality of the total degree helper function. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019) Remove sethood antecedent. (Revised by SN, 7-Aug-2024)

Ref Expression
Hypotheses tdeglem.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
tdeglem.h ⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
Assertion tdeglem1 𝐻 : 𝐴 ⟶ ℕ0

Proof

Step Hyp Ref Expression
1 tdeglem.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ 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 id ⊢ ( ℎ ∈ 𝐴 → ℎ ∈ 𝐴 )
8 1 psrbagf ⊢ ( ℎ ∈ 𝐴 → ℎ : 𝐼 ⟶ ℕ0 )
9 8 ffnd ⊢ ( ℎ ∈ 𝐴 → ℎ Fn 𝐼 )
10 7 9 fndmexd ⊢ ( ℎ ∈ 𝐴 → 𝐼 ∈ V )
11 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
12 11 a1i ⊢ ( ℎ ∈ 𝐴 → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
13 1 psrbagfsupp ⊢ ( ℎ ∈ 𝐴 → ℎ finSupp 0 )
14 3 6 10 12 8 13 gsumsubmcl ⊢ ( ℎ ∈ 𝐴 → ( ℂfld Σg ℎ ) ∈ ℕ0 )
15 2 14 fmpti ⊢ 𝐻 : 𝐴 ⟶ ℕ0