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 \in SubGrp (G) \to G \in Grp$
3		subgrcl	$⊢ x \in SubGrp (O) \to O \in Grp$
4	1	oppggrpb	$⊢ G \in Grp \leftrightarrow O \in Grp$
5	3 4	sylibr	$⊢ x \in SubGrp (O) \to G \in Grp$
6	1	oppgsubm	$⊢ SubMnd (G) = SubMnd (O)$
7	6	eleq2i	$⊢ x \in SubMnd (G) \leftrightarrow x \in SubMnd (O)$
8	7	a1i	$⊢ G \in Grp \to (x \in SubMnd (G) \leftrightarrow x \in SubMnd (O))$
9		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
10	1 9	oppginv	$⊢ G \in Grp \to {inv}_{g} (G) = {inv}_{g} (O)$
11	10	fveq1d	$⊢ G \in Grp \to {inv}_{g} (G) (y) = {inv}_{g} (O) (y)$
12	11	eleq1d	$⊢ G \in Grp \to ({inv}_{g} (G) (y) \in x \leftrightarrow {inv}_{g} (O) (y) \in x)$
13	12	ralbidv	$⊢ G \in Grp \to (\forall y \in x {inv}_{g} (G) (y) \in x \leftrightarrow \forall y \in x {inv}_{g} (O) (y) \in x)$
14	8 13	anbi12d	$⊢ G \in Grp \to ((x \in SubMnd (G) \land \forall y \in x {inv}_{g} (G) (y) \in x) \leftrightarrow (x \in SubMnd (O) \land \forall y \in x {inv}_{g} (O) (y) \in x))$
15	9	issubg3	$⊢ G \in Grp \to (x \in SubGrp (G) \leftrightarrow (x \in SubMnd (G) \land \forall y \in x {inv}_{g} (G) (y) \in x))$
16		eqid	$⊢ {inv}_{g} (O) = {inv}_{g} (O)$
17	16	issubg3	$⊢ O \in Grp \to (x \in SubGrp (O) \leftrightarrow (x \in SubMnd (O) \land \forall y \in x {inv}_{g} (O) (y) \in x))$
18	4 17	sylbi	$⊢ G \in Grp \to (x \in SubGrp (O) \leftrightarrow (x \in SubMnd (O) \land \forall y \in x {inv}_{g} (O) (y) \in x))$
19	14 15 18	3bitr4d	$⊢ G \in Grp \to (x \in SubGrp (G) \leftrightarrow x \in SubGrp (O))$
20	2 5 19	pm5.21nii	$⊢ x \in SubGrp (G) \leftrightarrow x \in SubGrp (O)$
21	20	eqriv	$⊢ SubGrp (G) = SubGrp (O)$

Metamath Proof Explorer

Theorem oppgsubg

Proof