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	⊢ ( norm ‘ ℤring ) = ( abs ↾ ℤ )

Proof

Step	Hyp	Ref	Expression
1		cnring	⊢ ℂfld ∈ Ring
2		ringmnd	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
3	1 2	ax-mp	⊢ ℂfld ∈ Mnd
4		0z	⊢ 0 ∈ ℤ
5		zsscn	⊢ ℤ ⊆ ℂ
6		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
7		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
8		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
9		cnfldnm	⊢ abs = ( norm ‘ ℂfld )
10	6 7 8 9	ressnm	⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ ℤ ∧ ℤ ⊆ ℂ ) → ( abs ↾ ℤ ) = ( norm ‘ ℤring ) )
11	10	eqcomd	⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ ℤ ∧ ℤ ⊆ ℂ ) → ( norm ‘ ℤring ) = ( abs ↾ ℤ ) )
12	3 4 5 11	mp3an	⊢ ( norm ‘ ℤring ) = ( abs ↾ ℤ )