This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑂 = ( oppg ‘ 𝐺 )
Assertion oppgsubg ( SubGrp ‘ 𝐺 ) = ( SubGrp ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppggic.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
2 subgrcl ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
3 subgrcl ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝑂 ) → 𝑂 ∈ Grp )
4 1 oppggrpb ⊢ ( 𝐺 ∈ Grp ↔ 𝑂 ∈ Grp )
5 3 4 sylibr ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝑂 ) → 𝐺 ∈ Grp )
6 1 oppgsubm ⊢ ( SubMnd ‘ 𝐺 ) = ( SubMnd ‘ 𝑂 )
7 6 eleq2i ⊢ ( 𝑥 ∈ ( SubMnd ‘ 𝐺 ) ↔ 𝑥 ∈ ( SubMnd ‘ 𝑂 ) )
8 7 a1i ⊢ ( 𝐺 ∈ Grp → ( 𝑥 ∈ ( SubMnd ‘ 𝐺 ) ↔ 𝑥 ∈ ( SubMnd ‘ 𝑂 ) ) )
9 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
10 1 9 oppginv ⊢ ( 𝐺 ∈ Grp → ( invg ‘ 𝐺 ) = ( invg ‘ 𝑂 ) )
11 10 fveq1d ⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) = ( ( invg ‘ 𝑂 ) ‘ 𝑦 ) )
12 11 eleq1d ⊢ ( 𝐺 ∈ Grp → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑥 ↔ ( ( invg ‘ 𝑂 ) ‘ 𝑦 ) ∈ 𝑥 ) )
13 12 ralbidv ⊢ ( 𝐺 ∈ Grp → ( ∀ 𝑦 ∈ 𝑥 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝑥 ( ( invg ‘ 𝑂 ) ‘ 𝑦 ) ∈ 𝑥 ) )
14 8 13 anbi12d ⊢ ( 𝐺 ∈ Grp → ( ( 𝑥 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑥 ) ↔ ( 𝑥 ∈ ( SubMnd ‘ 𝑂 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( invg ‘ 𝑂 ) ‘ 𝑦 ) ∈ 𝑥 ) ) )
15 9 issubg3 ⊢ ( 𝐺 ∈ Grp → ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑥 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑥 ) ) )
16 eqid ⊢ ( invg ‘ 𝑂 ) = ( invg ‘ 𝑂 )
17 16 issubg3 ⊢ ( 𝑂 ∈ Grp → ( 𝑥 ∈ ( SubGrp ‘ 𝑂 ) ↔ ( 𝑥 ∈ ( SubMnd ‘ 𝑂 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( invg ‘ 𝑂 ) ‘ 𝑦 ) ∈ 𝑥 ) ) )
18 4 17 sylbi ⊢ ( 𝐺 ∈ Grp → ( 𝑥 ∈ ( SubGrp ‘ 𝑂 ) ↔ ( 𝑥 ∈ ( SubMnd ‘ 𝑂 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( invg ‘ 𝑂 ) ‘ 𝑦 ) ∈ 𝑥 ) ) )
19 14 15 18 3bitr4d ⊢ ( 𝐺 ∈ Grp → ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑥 ∈ ( SubGrp ‘ 𝑂 ) ) )
20 2 5 19 pm5.21nii ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑥 ∈ ( SubGrp ‘ 𝑂 ) )
21 20 eqriv ⊢ ( SubGrp ‘ 𝐺 ) = ( SubGrp ‘ 𝑂 )