Theorem grpinvhmeo

Description: The inverse function in a topological group is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	tgpcn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
	tgpinv.5	$$⊢I={inv}_g\left(G\right)$$
Assertion	grpinvhmeo	$$⊢G\in \mathrm{TopGrp}\to I\in \left(J\mathrm{Homeo}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgpcn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
2		tgpinv.5	$$⊢I={inv}_g\left(G\right)$$
3	1 2	tgpinv	$$⊢G\in \mathrm{TopGrp}\to I\in \left(J\mathrm{Cn}J\right)$$
4		tgpgrp	$$⊢G\in \mathrm{TopGrp}\to G\in \mathrm{Grp}$$
5		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
6	5 2	grpinvcnv	$$⊢G\in \mathrm{Grp}\to I^{-1}=I$$
7	4 6	syl	$$⊢G\in \mathrm{TopGrp}\to I^{-1}=I$$
8	7 3	eqeltrd	$$⊢G\in \mathrm{TopGrp}\to I^{-1}\in \left(J\mathrm{Cn}J\right)$$
9		ishmeo	$$⊢I\in \left(J\mathrm{Homeo}J\right)\leftrightarrow \left(I\in \left(J\mathrm{Cn}J\right)\wedge I^{-1}\in \left(J\mathrm{Cn}J\right)\right)$$
10	3 8 9	sylanbrc	$$⊢G\in \mathrm{TopGrp}\to I\in \left(J\mathrm{Homeo}J\right)$$