Metamath Proof Explorer

Theorem oppgsubg

Description: Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis oppggic.o ⊢ O = opp 𝑔 ⁡ G
Assertion oppgsubg ⊢ SubGrp ⁡ G = SubGrp ⁡ O

Proof

Step Hyp Ref Expression
1 oppggic.o ⊢ O = opp 𝑔 ⁡ G
2 subgrcl ⊢ x ∈ SubGrp ⁡ G → G ∈ Grp
3 subgrcl ⊢ x ∈ SubGrp ⁡ O → O ∈ Grp
4 1 oppggrpb ⊢ G ∈ Grp ↔ O ∈ Grp
5 3 4 sylibr ⊢ x ∈ SubGrp ⁡ O → G ∈ Grp
6 1 oppgsubm ⊢ SubMnd ⁡ G = SubMnd ⁡ O
7 6 eleq2i ⊢ x ∈ SubMnd ⁡ G ↔ x ∈ SubMnd ⁡ O
8 7 a1i ⊢ G ∈ Grp → x ∈ SubMnd ⁡ G ↔ x ∈ SubMnd ⁡ O
9 eqid ⊢ inv g ⁡ G = inv g ⁡ G
10 1 9 oppginv ⊢ G ∈ Grp → inv g ⁡ G = inv g ⁡ O
11 10 fveq1d ⊢ G ∈ Grp → inv g ⁡ G ⁡ y = inv g ⁡ O ⁡ y
12 11 eleq1d ⊢ G ∈ Grp → inv g ⁡ G ⁡ y ∈ x ↔ inv g ⁡ O ⁡ y ∈ x
13 12 ralbidv ⊢ G ∈ Grp → ∀ y ∈ x inv g ⁡ G ⁡ y ∈ x ↔ ∀ y ∈ x inv g ⁡ O ⁡ y ∈ x
14 8 13 anbi12d ⊢ G ∈ Grp → x ∈ SubMnd ⁡ G ∧ ∀ y ∈ x inv g ⁡ G ⁡ y ∈ x ↔ x ∈ SubMnd ⁡ O ∧ ∀ y ∈ x inv g ⁡ O ⁡ y ∈ x
15 9 issubg3 ⊢ G ∈ Grp → x ∈ SubGrp ⁡ G ↔ x ∈ SubMnd ⁡ G ∧ ∀ y ∈ x inv g ⁡ G ⁡ y ∈ x
16 eqid ⊢ inv g ⁡ O = inv g ⁡ O
17 16 issubg3 ⊢ O ∈ Grp → x ∈ SubGrp ⁡ O ↔ x ∈ SubMnd ⁡ O ∧ ∀ y ∈ x inv g ⁡ O ⁡ y ∈ x
18 4 17 sylbi ⊢ G ∈ Grp → x ∈ SubGrp ⁡ O ↔ x ∈ SubMnd ⁡ O ∧ ∀ y ∈ x inv g ⁡ O ⁡ y ∈ x
19 14 15 18 3bitr4d ⊢ G ∈ Grp → x ∈ SubGrp ⁡ G ↔ x ∈ SubGrp ⁡ O
20 2 5 19 pm5.21nii ⊢ x ∈ SubGrp ⁡ G ↔ x ∈ SubGrp ⁡ O
21 20 eqriv ⊢ SubGrp ⁡ G = SubGrp ⁡ O