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 ⊢ A = m ∈ ℕ 0 I | m -1 ℕ ∈ Fin
tdeglem.h ⊢ H = h ∈ A ⟼ ∑ ℂ fld h
Assertion tdeglem1 ⊢ 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 ⊢ h ∈ A → ℂ fld ∈ CMnd
7 id ⊢ h ∈ A → h ∈ A
8 1 psrbagf ⊢ h ∈ A → h : I ⟶ ℕ 0
9 8 ffnd ⊢ h ∈ A → h Fn I
10 7 9 fndmexd ⊢ h ∈ A → I ∈ V
11 nn0subm ⊢ ℕ 0 ∈ SubMnd ⁡ ℂ fld
12 11 a1i ⊢ h ∈ A → ℕ 0 ∈ SubMnd ⁡ ℂ fld
13 1 psrbagfsupp ⊢ h ∈ A → finSupp 0 ⁡ h
14 3 6 10 12 8 13 gsumsubmcl ⊢ h ∈ A → ∑ ℂ fld h ∈ ℕ 0
15 2 14 fmpti ⊢ H : A ⟶ ℕ 0