Metamath Proof Explorer

Theorem cnfldtgp

Description: The complex numbers form a topological group under addition, with the standard topology induced by the absolute value metric. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion cnfldtgp ⊢ ℂ fld ∈ TopGrp

Proof

Step Hyp Ref Expression
1 cnring ⊢ ℂ fld ∈ Ring
2 ringgrp ⊢ ℂ fld ∈ Ring → ℂ fld ∈ Grp
3 1 2 ax-mp ⊢ ℂ fld ∈ Grp
4 cnfldtps ⊢ ℂ fld ∈ TopSp
5 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
6 5 subcn ⊢ − ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
7 cnfldsub ⊢ − = - ℂ fld
8 5 7 istgp2 ⊢ ℂ fld ∈ TopGrp ↔ ℂ fld ∈ Grp ∧ ℂ fld ∈ TopSp ∧ − ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
9 3 4 6 8 mpbir3an ⊢ ℂ fld ∈ TopGrp