Theorem tgpgrp

Description: A topological group is a group. (Contributed by FL, 18-Apr-2010) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	tgpgrp	$$⊢G\in \mathrm{TopGrp}\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left(G\right)=\mathrm{TopOpen}\left(G\right)$$
2		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
3	1 2	istgp	$$⊢G\in \mathrm{TopGrp}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{TopMnd}\wedge {inv}_g\left(G\right)\in \left(\mathrm{TopOpen}\left(G\right)\mathrm{Cn}\mathrm{TopOpen}\left(G\right)\right)\right)$$
4	3	simp1bi	$$⊢G\in \mathrm{TopGrp}\to G\in \mathrm{Grp}$$