tdeglem2

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

		Ref	Expression
	Assertion	tdeglem2	⊢ ( ℎ ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ℎ ‘ ∅ ) ) = ( ℎ ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ℂ_fld Σ_g ℎ ) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ℎ : { ∅ } ⟶ ℕ₀ )
2	1	feqmptd	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ℎ = ( 𝑥 ∈ { ∅ } ↦ ( ℎ ‘ 𝑥 ) ) )
3	2	oveq2d	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ( ℂ_fld Σ_g ℎ ) = ( ℂ_fld Σ_g ( 𝑥 ∈ { ∅ } ↦ ( ℎ ‘ 𝑥 ) ) ) )
4		cnring	⊢ ℂ_fld ∈ Ring
5		ringmnd	⊢ ( ℂ_fld ∈ Ring → ℂ_fld ∈ Mnd )
6	4 5	mp1i	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ℂ_fld ∈ Mnd )
7		0ex	⊢ ∅ ∈ V
8	7	a1i	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ∅ ∈ V )
9	7	snid	⊢ ∅ ∈ { ∅ }
10		ffvelcdm	⊢ ( ( ℎ : { ∅ } ⟶ ℕ₀ ∧ ∅ ∈ { ∅ } ) → ( ℎ ‘ ∅ ) ∈ ℕ₀ )
11	1 9 10	sylancl	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ( ℎ ‘ ∅ ) ∈ ℕ₀ )
12	11	nn0cnd	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ( ℎ ‘ ∅ ) ∈ ℂ )
13		cnfldbas	⊢ ℂ = ( Base ‘ ℂ_fld )
14		fveq2	⊢ ( 𝑥 = ∅ → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ ∅ ) )
15	13 14	gsumsn	⊢ ( ( ℂ_fld ∈ Mnd ∧ ∅ ∈ V ∧ ( ℎ ‘ ∅ ) ∈ ℂ ) → ( ℂ_fld Σ_g ( 𝑥 ∈ { ∅ } ↦ ( ℎ ‘ 𝑥 ) ) ) = ( ℎ ‘ ∅ ) )
16	6 8 12 15	syl3anc	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ( ℂ_fld Σ_g ( 𝑥 ∈ { ∅ } ↦ ( ℎ ‘ 𝑥 ) ) ) = ( ℎ ‘ ∅ ) )
17	3 16	eqtrd	⊢ ( ℎ ∈ ( ℕ₀ ↑_m { ∅ } ) → ( ℂ_fld Σ_g ℎ ) = ( ℎ ‘ ∅ ) )
18		df1o2	⊢ 1_o = { ∅ }
19	18	oveq2i	⊢ ( ℕ₀ ↑_m 1_o ) = ( ℕ₀ ↑_m { ∅ } )
20	17 19	eleq2s	⊢ ( ℎ ∈ ( ℕ₀ ↑_m 1_o ) → ( ℂ_fld Σ_g ℎ ) = ( ℎ ‘ ∅ ) )
21	20	eqcomd	⊢ ( ℎ ∈ ( ℕ₀ ↑_m 1_o ) → ( ℎ ‘ ∅ ) = ( ℂ_fld Σ_g ℎ ) )
22	21	mpteq2ia	⊢ ( ℎ ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ℎ ‘ ∅ ) ) = ( ℎ ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ℂ_fld Σ_g ℎ ) )

Metamath Proof Explorer

Theorem tdeglem2

Proof