Theorem tdeglem2

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

	Ref	Expression
Assertion	tdeglem2	⊢ ( ℎ ∈ ( ℕ0 ↑m 1o ) ↦ ( ℎ ‘ ∅ ) ) = ( ℎ ∈ ( ℕ0 ↑m 1o ) ↦ ( ℂfld Σg ℎ ) )

Proof

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