Theorem 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	⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion	opprnsg	⊢ ( NrmSGrp ‘ 𝑅 ) = ( NrmSGrp ‘ 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		oppreqg.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2	1	opprsubg	⊢ ( SubGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑂 )
3	2	eleq2i	⊢ ( 𝑔 ∈ ( SubGrp ‘ 𝑅 ) ↔ 𝑔 ∈ ( SubGrp ‘ 𝑂 ) )
4	3	anbi1i	⊢ ( ( 𝑔 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑔 → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝑔 ) ) ↔ ( 𝑔 ∈ ( SubGrp ‘ 𝑂 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑔 → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝑔 ) ) )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
7	5 6	isnsg2	⊢ ( 𝑔 ∈ ( NrmSGrp ‘ 𝑅 ) ↔ ( 𝑔 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑔 → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝑔 ) ) )
8	1 5	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
9	1 6	oppradd	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
10	8 9	isnsg2	⊢ ( 𝑔 ∈ ( NrmSGrp ‘ 𝑂 ) ↔ ( 𝑔 ∈ ( SubGrp ‘ 𝑂 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑔 → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝑔 ) ) )
11	4 7 10	3bitr4i	⊢ ( 𝑔 ∈ ( NrmSGrp ‘ 𝑅 ) ↔ 𝑔 ∈ ( NrmSGrp ‘ 𝑂 ) )
12	11	eqriv	⊢ ( NrmSGrp ‘ 𝑅 ) = ( NrmSGrp ‘ 𝑂 )