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	⊢ − = ( -g ‘ ℂ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