Theorem oppgtgp

Description: The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015)

	Ref	Expression
Hypothesis	oppgtmd.1	⊢ 𝑂 = ( oppg ‘ 𝐺 )
Assertion	oppgtgp	⊢ ( 𝐺 ∈ TopGrp → 𝑂 ∈ TopGrp )

Proof

Step	Hyp	Ref	Expression
1		oppgtmd.1	⊢ 𝑂 = ( oppg ‘ 𝐺 )
2		tgpgrp	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
3	1	oppggrp	⊢ ( 𝐺 ∈ Grp → 𝑂 ∈ Grp )
4	2 3	syl	⊢ ( 𝐺 ∈ TopGrp → 𝑂 ∈ Grp )
5		tgptmd	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
6	1	oppgtmd	⊢ ( 𝐺 ∈ TopMnd → 𝑂 ∈ TopMnd )
7	5 6	syl	⊢ ( 𝐺 ∈ TopGrp → 𝑂 ∈ TopMnd )
8		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
9	1 8	oppginv	⊢ ( 𝐺 ∈ Grp → ( invg ‘ 𝐺 ) = ( invg ‘ 𝑂 ) )
10	2 9	syl	⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) = ( invg ‘ 𝑂 ) )
11		eqid	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
12	11 8	tgpinv	⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) )
13	10 12	eqeltrrd	⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝑂 ) ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) )
14	1 11	oppgtopn	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝑂 )
15		eqid	⊢ ( invg ‘ 𝑂 ) = ( invg ‘ 𝑂 )
16	14 15	istgp	⊢ ( 𝑂 ∈ TopGrp ↔ ( 𝑂 ∈ Grp ∧ 𝑂 ∈ TopMnd ∧ ( invg ‘ 𝑂 ) ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) ) )
17	4 7 13 16	syl3anbrc	⊢ ( 𝐺 ∈ TopGrp → 𝑂 ∈ TopGrp )