Metamath Proof Explorer

Theorem subrngringnsg

Description: A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025)

Ref Expression
Assertion subrngringnsg 
|- ( A e. ( SubRng ` R ) -> A e. ( NrmSGrp ` R ) )

Proof

Step Hyp Ref Expression
1 subrngsubg 
 |-  ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) )
2 subrngrcl 
 |-  ( A e. ( SubRng ` R ) -> R e. Rng )
3 rngabl 
 |-  ( R e. Rng -> R e. Abel )
4 2 3 syl 
 |-  ( A e. ( SubRng ` R ) -> R e. Abel )
5 4 3anim1i 
 |-  ( ( A e. ( SubRng ` R ) /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) )
6 5 3expb 
 |-  ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( +g ` R ) = ( +g ` R )
9 7 8 ablcom 
 |-  ( ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( +g ` R ) y ) = ( y ( +g ` R ) x ) )
10 6 9 syl 
 |-  ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) = ( y ( +g ` R ) x ) )
11 10 eleq1d 
 |-  ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( +g ` R ) y ) e. A <-> ( y ( +g ` R ) x ) e. A ) )
12 11 biimpd 
 |-  ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( +g ` R ) y ) e. A -> ( y ( +g ` R ) x ) e. A ) )
13 12 ralrimivva 
 |-  ( A e. ( SubRng ` R ) -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) e. A -> ( y ( +g ` R ) x ) e. A ) )
14 7 8 isnsg2 
 |-  ( A e. ( NrmSGrp ` R ) <-> ( A e. ( SubGrp ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) e. A -> ( y ( +g ` R ) x ) e. A ) ) )
15 1 13 14 sylanbrc 
 |-  ( A e. ( SubRng ` R ) -> A e. ( NrmSGrp ` R ) )