Theorem zringnm

Description: The norm (function) for a ring of integers is the absolute value function (restricted to the integers). (Contributed by AV, 13-Jun-2019)

	Ref	Expression
Assertion	zringnm	$$⊢\mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)={\mathrm{abs}\upharpoonright }_{\mathbb{Z}}$$

Proof

Step	Hyp	Ref	Expression
1		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
2		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
3	1 2	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
4		0z	$$⊢0\in \mathbb{Z}$$
5		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
6		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
7		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
8		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
9		cnfldnm	$$⊢\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$
10	6 7 8 9	ressnm	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in \mathbb{Z}\wedge \mathbb{Z}\subseteq ℂ\right)\to {\mathrm{abs}\upharpoonright }_{\mathbb{Z}}=\mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
11	10	eqcomd	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in \mathbb{Z}\wedge \mathbb{Z}\subseteq ℂ\right)\to \mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)={\mathrm{abs}\upharpoonright }_{\mathbb{Z}}$$
12	3 4 5 11	mp3an	$$⊢\mathrm{norm}\left({\mathbb{Z}}_{\mathrm{ring}}\right)={\mathrm{abs}\upharpoonright }_{\mathbb{Z}}$$