Metamath Proof Explorer

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 ⊢ O = opp 𝑔 ⁡ G
Assertion oppgtgp ⊢ G ∈ TopGrp → O ∈ TopGrp

Proof

Step Hyp Ref Expression
1 oppgtmd.1 ⊢ O = opp 𝑔 ⁡ G
2 tgpgrp ⊢ G ∈ TopGrp → G ∈ Grp
3 1 oppggrp ⊢ G ∈ Grp → O ∈ Grp
4 2 3 syl ⊢ G ∈ TopGrp → O ∈ Grp
5 tgptmd ⊢ G ∈ TopGrp → G ∈ TopMnd
6 1 oppgtmd ⊢ G ∈ TopMnd → O ∈ TopMnd
7 5 6 syl ⊢ G ∈ TopGrp → O ∈ TopMnd
8 eqid ⊢ inv g ⁡ G = inv g ⁡ G
9 1 8 oppginv ⊢ G ∈ Grp → inv g ⁡ G = inv g ⁡ O
10 2 9 syl ⊢ G ∈ TopGrp → inv g ⁡ G = inv g ⁡ O
11 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
12 11 8 tgpinv ⊢ G ∈ TopGrp → inv g ⁡ G ∈ TopOpen ⁡ G Cn TopOpen ⁡ G
13 10 12 eqeltrrd ⊢ G ∈ TopGrp → inv g ⁡ O ∈ 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 ∈ TopGrp ↔ O ∈ Grp ∧ O ∈ TopMnd ∧ inv g ⁡ O ∈ TopOpen ⁡ G Cn TopOpen ⁡ G
17 4 7 13 16 syl3anbrc ⊢ G ∈ TopGrp → O ∈ TopGrp