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 = ( TopOpen ` G )
	tgpinv.5	|- I = ( invg ` G )
Assertion	grpinvhmeo	|- ( G e. TopGrp -> I e. ( J Homeo J ) )

Proof

Step	Hyp	Ref	Expression
1		tgpcn.j	|- J = ( TopOpen ` G )
2		tgpinv.5	|- I = ( invg ` G )
3	1 2	tgpinv	|- ( G e. TopGrp -> I e. ( J Cn J ) )
4		tgpgrp	|- ( G e. TopGrp -> G e. Grp )
5		eqid	|- ( Base ` G ) = ( Base ` G )
6	5 2	grpinvcnv	|- ( G e. Grp -> `' I = I )
7	4 6	syl	|- ( G e. TopGrp -> `' I = I )
8	7 3	eqeltrd	|- ( G e. TopGrp -> `' I e. ( J Cn J ) )
9		ishmeo	|- ( I e. ( J Homeo J ) <-> ( I e. ( J Cn J ) /\ `' I e. ( J Cn J ) ) )
10	3 8 9	sylanbrc	|- ( G e. TopGrp -> I e. ( J Homeo J ) )