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 
|- O = ( oppR ` R )
Assertion opprnsg 
|- ( NrmSGrp ` R ) = ( NrmSGrp ` O )

Proof

Step Hyp Ref Expression
1 oppreqg.o 
 |-  O = ( oppR ` R )
2 1 opprsubg 
 |-  ( SubGrp ` R ) = ( SubGrp ` O )
3 2 eleq2i 
 |-  ( g e. ( SubGrp ` R ) <-> g e. ( SubGrp ` O ) )
4 3 anbi1i 
 |-  ( ( g e. ( SubGrp ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) e. g -> ( y ( +g ` R ) x ) e. g ) ) <-> ( g e. ( SubGrp ` O ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) e. g -> ( y ( +g ` R ) x ) e. g ) ) )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( +g ` R ) = ( +g ` R )
7 5 6 isnsg2 
 |-  ( g e. ( NrmSGrp ` R ) <-> ( g e. ( SubGrp ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) e. g -> ( y ( +g ` R ) x ) e. g ) ) )
8 1 5 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
9 1 6 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
10 8 9 isnsg2 
 |-  ( g e. ( NrmSGrp ` O ) <-> ( g e. ( SubGrp ` O ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) e. g -> ( y ( +g ` R ) x ) e. g ) ) )
11 4 7 10 3bitr4i 
 |-  ( g e. ( NrmSGrp ` R ) <-> g e. ( NrmSGrp ` O ) )
12 11 eqriv 
 |-  ( NrmSGrp ` R ) = ( NrmSGrp ` O )