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 )