Theorem zring0

Description: The neutral 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 )