This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zring0

Description: The zero element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zring0 0 = ( 0g ‘ ℤring )

Proof

Step Hyp Ref Expression
1 cncrng ⊢ ℂfld ∈ CRing
2 crngring ⊢ ( ℂfld ∈ CRing → ℂfld ∈ Ring )
3 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
4 1 2 3 mp2b ⊢ ℂfld ∈ Mnd
5 0z ⊢ 0 ∈ ℤ
6 zsscn ⊢ ℤ ⊆ ℂ
7 df-zring ⊢ ℤring = ( ℂfld ↾s ℤ )
8 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
9 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
10 7 8 9 ress0g ⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ ℤ ∧ ℤ ⊆ ℂ ) → 0 = ( 0g ‘ ℤring ) )
11 4 5 6 10 mp3an ⊢ 0 = ( 0g ‘ ℤring )