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