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 ‘ 𝑂 )