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∈ℕ01𝑜⟼h⁡∅=h∈ℕ01𝑜⟼∑ℂfldh

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∅→∑ℂfldh=∑ℂfldx∈∅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 ffvelcdm ⊢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⁡∅∈ℂ→∑ℂfldx∈∅h⁡x=h⁡∅
16 6 8 12 15 syl3anc ⊢h∈ℕ0∅→∑ℂfldx∈∅h⁡x=h⁡∅
17 3 16 eqtrd ⊢h∈ℕ0∅→∑ℂfldh=h⁡∅
18 df1o2 ⊢1𝑜=∅
19 18 oveq2i ⊢ℕ01𝑜=ℕ0∅
20 17 19 eleq2s ⊢h∈ℕ01𝑜→∑ℂfldh=h⁡∅
21 20 eqcomd ⊢h∈ℕ01𝑜→h⁡∅=∑ℂfldh
22 21 mpteq2ia ⊢h∈ℕ01𝑜⟼h⁡∅=h∈ℕ01𝑜⟼∑ℂfldh