opprnsg

Description: Normal subgroups of the opposite ring are the same as the original normal subgroups. (Contributed by Thierry Arnoux, 13-Mar-2025)

		Ref	Expression
	Hypothesis	oppreqg.o	$⊢ O = {opp}_{r} (R)$
	Assertion	opprnsg	$⊢ NrmSGrp (R) = NrmSGrp (O)$

Step	Hyp	Ref	Expression
1		oppreqg.o	$⊢ O = {opp}_{r} (R)$
2	1	opprsubg	$⊢ SubGrp (R) = SubGrp (O)$
3	2	eleq2i	$⊢ g \in SubGrp (R) \leftrightarrow g \in SubGrp (O)$
4	3	anbi1i	$⊢ (g \in SubGrp (R) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x +_{R} y \in g \to y +_{R} x \in g)) \leftrightarrow (g \in SubGrp (O) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x +_{R} y \in g \to y +_{R} x \in g))$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ +_{R} = +_{R}$
7	5 6	isnsg2	$⊢ g \in NrmSGrp (R) \leftrightarrow (g \in SubGrp (R) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x +_{R} y \in g \to y +_{R} x \in g))$
8	1 5	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
9	1 6	oppradd	$⊢ +_{R} = +_{O}$
10	8 9	isnsg2	$⊢ g \in NrmSGrp (O) \leftrightarrow (g \in SubGrp (O) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x +_{R} y \in g \to y +_{R} x \in g))$
11	4 7 10	3bitr4i	$⊢ g \in NrmSGrp (R) \leftrightarrow g \in NrmSGrp (O)$
12	11	eqriv	$⊢ NrmSGrp (R) = NrmSGrp (O)$

Metamath Proof Explorer