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	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
	tgpinv.5	⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion	grpinvhmeo	⊢ ( 𝐺 ∈ TopGrp → 𝐼 ∈ ( 𝐽 Homeo 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		tgpcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2		tgpinv.5	⊢ 𝐼 = ( invg ‘ 𝐺 )
3	1 2	tgpinv	⊢ ( 𝐺 ∈ TopGrp → 𝐼 ∈ ( 𝐽 Cn 𝐽 ) )
4		tgpgrp	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6	5 2	grpinvcnv	⊢ ( 𝐺 ∈ Grp → ◡ 𝐼 = 𝐼 )
7	4 6	syl	⊢ ( 𝐺 ∈ TopGrp → ◡ 𝐼 = 𝐼 )
8	7 3	eqeltrd	⊢ ( 𝐺 ∈ TopGrp → ◡ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) )
9		ishmeo	⊢ ( 𝐼 ∈ ( 𝐽 Homeo 𝐽 ) ↔ ( 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ∧ ◡ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
10	3 8 9	sylanbrc	⊢ ( 𝐺 ∈ TopGrp → 𝐼 ∈ ( 𝐽 Homeo 𝐽 ) )