Metamath Proof Explorer

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 ` ZZring ) = ( abs |` ZZ )

Proof

Step Hyp Ref Expression
1 cnring 
 |-  CCfld e. Ring
2 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
3 1 2 ax-mp 
 |-  CCfld e. Mnd
4 0z 
 |-  0 e. ZZ
5 zsscn 
 |-  ZZ C_ CC
6 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
7 cnfldbas 
 |-  CC = ( Base ` CCfld )
8 cnfld0 
 |-  0 = ( 0g ` CCfld )
9 cnfldnm 
 |-  abs = ( norm ` CCfld )
10 6 7 8 9 ressnm 
 |-  ( ( CCfld e. Mnd /\ 0 e. ZZ /\ ZZ C_ CC ) -> ( abs |` ZZ ) = ( norm ` ZZring ) )
11 10 eqcomd 
 |-  ( ( CCfld e. Mnd /\ 0 e. ZZ /\ ZZ C_ CC ) -> ( norm ` ZZring ) = ( abs |` ZZ ) )
12 3 4 5 11 mp3an 
 |-  ( norm ` ZZring ) = ( abs |` ZZ )