This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnngp

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

Ref Expression
Assertion cnngp ⊢ ℂ fld ∈ NrmGrp

Proof

Step Hyp Ref Expression
1 cnring ⊢ ℂ fld ∈ Ring
2 ringgrp ⊢ ℂ fld ∈ Ring → ℂ fld ∈ Grp
3 1 2 ax-mp ⊢ ℂ fld ∈ Grp
4 cnfldms ⊢ ℂ fld ∈ MetSp
5 ssid ⊢ abs ∘ − ⊆ abs ∘ −
6 cnfldnm ⊢ abs = norm ⁡ ℂ fld
7 cnfldsub ⊢ − = - ℂ fld
8 cnfldds ⊢ abs ∘ − = dist ⁡ ℂ fld
9 6 7 8 isngp ⊢ ℂ fld ∈ NrmGrp ↔ ℂ fld ∈ Grp ∧ ℂ fld ∈ MetSp ∧ abs ∘ − ⊆ abs ∘ −
10 3 4 5 9 mpbir3an ⊢ ℂ fld ∈ NrmGrp