Metamath Proof Explorer

Theorem cnngp

Description: The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion cnngp 
|- CCfld e. NrmGrp

Proof

Step Hyp Ref Expression
1 cnring 
 |-  CCfld e. Ring
2 ringgrp 
 |-  ( CCfld e. Ring -> CCfld e. Grp )
3 1 2 ax-mp 
 |-  CCfld e. Grp
4 cnfldms 
 |-  CCfld e. MetSp
5 ssid 
 |-  ( abs o. - ) C_ ( abs o. - )
6 cnfldnm 
 |-  abs = ( norm ` CCfld )
7 cnfldsub 
 |-  - = ( -g ` CCfld )
8 cnfldds 
 |-  ( abs o. - ) = ( dist ` CCfld )
9 6 7 8 isngp 
 |-  ( CCfld e. NrmGrp <-> ( CCfld e. Grp /\ CCfld e. MetSp /\ ( abs o. - ) C_ ( abs o. - ) ) )
10 3 4 5 9 mpbir3an 
 |-  CCfld e. NrmGrp