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=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$

Proof

Step	Hyp	Ref	Expression
1		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
2		crngring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
3		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
4	1 2 3	mp2b	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
5		0z	$$⊢0\in \mathbb{Z}$$
6		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
7		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
8		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
9		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
10	7 8 9	ress0g	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in \mathbb{Z}\wedge \mathbb{Z}\subseteq ℂ\right)\to 0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
11	4 5 6 10	mp3an	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$