Theorem zzsnm

Description: The norm of the ring of the integers. (Contributed by Thierry Arnoux, 8-Nov-2017) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Assertion	zzsnm	⊢ ( 𝑀 ∈ ℤ → ( abs ‘ 𝑀 ) = ( ( norm ‘ ℤring ) ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		fvres	⊢ ( 𝑀 ∈ ℤ → ( ( abs ↾ ℤ ) ‘ 𝑀 ) = ( abs ‘ 𝑀 ) )
2		zringnm	⊢ ( norm ‘ ℤring ) = ( abs ↾ ℤ )
3	2	eqcomi	⊢ ( abs ↾ ℤ ) = ( norm ‘ ℤring )
4	3	fveq1i	⊢ ( ( abs ↾ ℤ ) ‘ 𝑀 ) = ( ( norm ‘ ℤring ) ‘ 𝑀 )
5	1 4	eqtr3di	⊢ ( 𝑀 ∈ ℤ → ( abs ‘ 𝑀 ) = ( ( norm ‘ ℤring ) ‘ 𝑀 ) )