# Metamath Proof Explorer

## Theorem cnfldnm

Description: The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion cnfldnm
`|- abs = ( norm ` CCfld )`

### Proof

Step Hyp Ref Expression
1 0cn
` |-  0 e. CC`
2 eqid
` |-  ( abs o. - ) = ( abs o. - )`
3 2 cnmetdval
` |-  ( ( x e. CC /\ 0 e. CC ) -> ( x ( abs o. - ) 0 ) = ( abs ` ( x - 0 ) ) )`
4 1 3 mpan2
` |-  ( x e. CC -> ( x ( abs o. - ) 0 ) = ( abs ` ( x - 0 ) ) )`
5 subid1
` |-  ( x e. CC -> ( x - 0 ) = x )`
6 5 fveq2d
` |-  ( x e. CC -> ( abs ` ( x - 0 ) ) = ( abs ` x ) )`
7 4 6 eqtrd
` |-  ( x e. CC -> ( x ( abs o. - ) 0 ) = ( abs ` x ) )`
8 7 mpteq2ia
` |-  ( x e. CC |-> ( x ( abs o. - ) 0 ) ) = ( x e. CC |-> ( abs ` x ) )`
9 eqid
` |-  ( norm ` CCfld ) = ( norm ` CCfld )`
10 cnfldbas
` |-  CC = ( Base ` CCfld )`
11 cnfld0
` |-  0 = ( 0g ` CCfld )`
12 cnfldds
` |-  ( abs o. - ) = ( dist ` CCfld )`
13 9 10 11 12 nmfval
` |-  ( norm ` CCfld ) = ( x e. CC |-> ( x ( abs o. - ) 0 ) )`
14 absf
` |-  abs : CC --> RR`
15 14 a1i
` |-  ( T. -> abs : CC --> RR )`
16 15 feqmptd
` |-  ( T. -> abs = ( x e. CC |-> ( abs ` x ) ) )`
17 16 mptru
` |-  abs = ( x e. CC |-> ( abs ` x ) )`
18 8 13 17 3eqtr4ri
` |-  abs = ( norm ` CCfld )`