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	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{TopGrp}$$

Proof

Step	Hyp	Ref	Expression
1		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
2		ringgrp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
3	1 2	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
4		cnfldtps	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}$$
5		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6	5	subcn	$$⊢-\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
7		cnfldsub	$$⊢-={-}_{{ℂ}_{\mathrm{fld}}}$$
8	5 7	istgp2	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{TopGrp}\leftrightarrow \left({ℂ}_{\mathrm{fld}}\in \mathrm{Grp}\wedge {ℂ}_{\mathrm{fld}}\in \mathrm{TopSp}\wedge -\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)$$
9	3 4 6 8	mpbir3an	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{TopGrp}$$