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

Metamath Proof Explorer

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