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

Metamath Proof Explorer

Theorem subrngringnsg

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

Ref Expression
Assertion subrngringnsg ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝐴 ∈ ( NrmSGrp ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 subrngsubg ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) )
2 subrngrcl ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝑅 ∈ Rng )
3 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
4 2 3 syl ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝑅 ∈ Abel )
5 4 3anim1i ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
6 5 3expb ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑅 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
9 7 8 ablcom ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) )
10 6 9 syl ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) )
11 10 eleq1d ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐴 ↔ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝐴 ) )
12 11 biimpd ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐴 → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝐴 ) )
13 12 ralrimivva ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐴 → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝐴 ) )
14 7 8 isnsg2 ⊢ ( 𝐴 ∈ ( NrmSGrp ‘ 𝑅 ) ↔ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐴 → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝐴 ) ) )
15 1 13 14 sylanbrc ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝐴 ∈ ( NrmSGrp ‘ 𝑅 ) )