Metamath Proof Explorer

Theorem tdeglem2

Description: Simplification of total degree for the univariate case. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Assertion tdeglem2 ⊢ h ∈ ℕ 0 1 𝑜 ⟼ h ⁡ ∅ = h ∈ ℕ 0 1 𝑜 ⟼ ∑ ℂ fld h

Proof

Step Hyp Ref Expression
1 elmapi ⊢ h ∈ ℕ 0 ∅ → h : ∅ ⟶ ℕ 0
2 1 feqmptd ⊢ h ∈ ℕ 0 ∅ → h = x ∈ ∅ ⟼ h ⁡ x
3 2 oveq2d ⊢ h ∈ ℕ 0 ∅ → ∑ ℂ fld h = ∑ ℂ fld x ∈ ∅ h ⁡ x
4 cnring ⊢ ℂ fld ∈ Ring
5 ringmnd ⊢ ℂ fld ∈ Ring → ℂ fld ∈ Mnd
6 4 5 mp1i ⊢ h ∈ ℕ 0 ∅ → ℂ fld ∈ Mnd
7 0ex ⊢ ∅ ∈ V
8 7 a1i ⊢ h ∈ ℕ 0 ∅ → ∅ ∈ V
9 7 snid ⊢ ∅ ∈ ∅
10 ffvelrn ⊢ h : ∅ ⟶ ℕ 0 ∧ ∅ ∈ ∅ → h ⁡ ∅ ∈ ℕ 0
11 1 9 10 sylancl ⊢ h ∈ ℕ 0 ∅ → h ⁡ ∅ ∈ ℕ 0
12 11 nn0cnd ⊢ h ∈ ℕ 0 ∅ → h ⁡ ∅ ∈ ℂ
13 cnfldbas ⊢ ℂ = Base ℂ fld
14 fveq2 ⊢ x = ∅ → h ⁡ x = h ⁡ ∅
15 13 14 gsumsn ⊢ ℂ fld ∈ Mnd ∧ ∅ ∈ V ∧ h ⁡ ∅ ∈ ℂ → ∑ ℂ fld x ∈ ∅ h ⁡ x = h ⁡ ∅
16 6 8 12 15 syl3anc ⊢ h ∈ ℕ 0 ∅ → ∑ ℂ fld x ∈ ∅ h ⁡ x = h ⁡ ∅
17 3 16 eqtrd ⊢ h ∈ ℕ 0 ∅ → ∑ ℂ fld h = h ⁡ ∅
18 df1o2 ⊢ 1 𝑜 = ∅
19 18 oveq2i ⊢ ℕ 0 1 𝑜 = ℕ 0 ∅
20 17 19 eleq2s ⊢ h ∈ ℕ 0 1 𝑜 → ∑ ℂ fld h = h ⁡ ∅
21 20 eqcomd ⊢ h ∈ ℕ 0 1 𝑜 → h ⁡ ∅ = ∑ ℂ fld h
22 21 mpteq2ia ⊢ h ∈ ℕ 0 1 𝑜 ⟼ h ⁡ ∅ = h ∈ ℕ 0 1 𝑜 ⟼ ∑ ℂ fld h