Step |
Hyp |
Ref |
Expression |
1 |
|
2zrng.e |
⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } |
2 |
|
2zrngbas.r |
⊢ 𝑅 = ( ℂfld ↾s 𝐸 ) |
3 |
|
cncrng |
⊢ ℂfld ∈ CRing |
4 |
|
crngring |
⊢ ( ℂfld ∈ CRing → ℂfld ∈ Ring ) |
5 |
|
ringmnd |
⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd ) |
6 |
3 4 5
|
mp2b |
⊢ ℂfld ∈ Mnd |
7 |
1
|
0even |
⊢ 0 ∈ 𝐸 |
8 |
|
ssrab2 |
⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ⊆ ℤ |
9 |
1 8
|
eqsstri |
⊢ 𝐸 ⊆ ℤ |
10 |
|
zsscn |
⊢ ℤ ⊆ ℂ |
11 |
9 10
|
sstri |
⊢ 𝐸 ⊆ ℂ |
12 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
13 |
|
cnfld0 |
⊢ 0 = ( 0g ‘ ℂfld ) |
14 |
2 12 13
|
ress0g |
⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ 𝐸 ∧ 𝐸 ⊆ ℂ ) → 0 = ( 0g ‘ 𝑅 ) ) |
15 |
6 7 11 14
|
mp3an |
⊢ 0 = ( 0g ‘ 𝑅 ) |