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 |
|
ffvelrn |
⊢ ( ( ℎ : { ∅ } ⟶ ℕ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 ℎ ) ) |