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 ( ∈ ( ℕ0m 1o ) ↦ ( ‘ ∅ ) ) = ( ∈ ( ℕ0m 1o ) ↦ ( ℂfld Σg ) )

Proof

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