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 
|- CCfld e. TopGrp

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 cnfldtps 
 |-  CCfld e. TopSp
5 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
6 5 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
7 cnfldsub 
 |-  - = ( -g ` CCfld )
8 5 7 istgp2 
 |-  ( CCfld e. TopGrp <-> ( CCfld e. Grp /\ CCfld e. TopSp /\ - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) ) )
9 3 4 6 8 mpbir3an 
 |-  CCfld e. TopGrp