subrngringnsg

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

		Ref	Expression
	Assertion	subrngringnsg	$⊢ A \in SubRng (R) \to A \in NrmSGrp (R)$

Step	Hyp	Ref	Expression
1		subrngsubg	$⊢ A \in SubRng (R) \to A \in SubGrp (R)$
2		subrngrcl	$⊢ A \in SubRng (R) \to R \in Rng$
3		rngabl	$⊢ R \in Rng \to R \in Abel$
4	2 3	syl	$⊢ A \in SubRng (R) \to R \in Abel$
5	4	3anim1i	$⊢ (A \in SubRng (R) \land x \in {Base}_{R} \land y \in {Base}_{R}) \to (R \in Abel \land x \in {Base}_{R} \land y \in {Base}_{R})$
6	5	3expb	$⊢ (A \in SubRng (R) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to (R \in Abel \land x \in {Base}_{R} \land y \in {Base}_{R})$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8		eqid	$⊢ +_{R} = +_{R}$
9	7 8	ablcom	$⊢ (R \in Abel \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x +_{R} y = y +_{R} x$
10	6 9	syl	$⊢ (A \in SubRng (R) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x +_{R} y = y +_{R} x$
11	10	eleq1d	$⊢ (A \in SubRng (R) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to (x +_{R} y \in A \leftrightarrow y +_{R} x \in A)$
12	11	biimpd	$⊢ (A \in SubRng (R) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to (x +_{R} y \in A \to y +_{R} x \in A)$
13	12	ralrimivva	$⊢ A \in SubRng (R) \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x +_{R} y \in A \to y +_{R} x \in A)$
14	7 8	isnsg2	$⊢ A \in NrmSGrp (R) \leftrightarrow (A \in SubGrp (R) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x +_{R} y \in A \to y +_{R} x \in A))$
15	1 13 14	sylanbrc	$⊢ A \in SubRng (R) \to A \in NrmSGrp (R)$

Metamath Proof Explorer