oppgtgp

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

		Ref	Expression
	Hypothesis	oppgtmd.1	$⊢ O = {opp}_{𝑔} (G)$
	Assertion	oppgtgp	$⊢ G \in TopGrp \to O \in TopGrp$

Step	Hyp	Ref	Expression
1		oppgtmd.1	$⊢ O = {opp}_{𝑔} (G)$
2		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
3	1	oppggrp	$⊢ G \in Grp \to O \in Grp$
4	2 3	syl	$⊢ G \in TopGrp \to O \in Grp$
5		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
6	1	oppgtmd	$⊢ G \in TopMnd \to O \in TopMnd$
7	5 6	syl	$⊢ G \in TopGrp \to O \in TopMnd$
8		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
9	1 8	oppginv	$⊢ G \in Grp \to {inv}_{g} (G) = {inv}_{g} (O)$
10	2 9	syl	$⊢ G \in TopGrp \to {inv}_{g} (G) = {inv}_{g} (O)$
11		eqid	$⊢ TopOpen (G) = TopOpen (G)$
12	11 8	tgpinv	$⊢ G \in TopGrp \to {inv}_{g} (G) \in (TopOpen (G) Cn TopOpen (G))$
13	10 12	eqeltrrd	$⊢ G \in TopGrp \to {inv}_{g} (O) \in (TopOpen (G) Cn TopOpen (G))$
14	1 11	oppgtopn	$⊢ TopOpen (G) = TopOpen (O)$
15		eqid	$⊢ {inv}_{g} (O) = {inv}_{g} (O)$
16	14 15	istgp	$⊢ O \in TopGrp \leftrightarrow (O \in Grp \land O \in TopMnd \land {inv}_{g} (O) \in (TopOpen (G) Cn TopOpen (G)))$
17	4 7 13 16	syl3anbrc	$⊢ G \in TopGrp \to O \in TopGrp$

Metamath Proof Explorer