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	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
2		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
3	1 2	istgp	⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ ( invg ‘ 𝐺 ) ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) ) )
4	3	simp1bi	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )