Theorem subrngringnsg

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

	Ref	Expression
Assertion	subrngringnsg	Could not format assertion : No typesetting found for |- ( A e. ( SubRng ` R ) -> A e. ( NrmSGrp ` R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subrngsubg	Could not format ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) ) with typecode |-
2		subrngrcl	Could not format ( A e. ( SubRng ` R ) -> R e. Rng ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> R e. Rng ) with typecode |-
3		rngabl	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Abel}$$
4	2 3	syl	Could not format ( A e. ( SubRng ` R ) -> R e. Abel ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> R e. Abel ) with typecode |-
5	4	3anim1i	Could not format ( ( A e. ( SubRng ` R ) /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) with typecode |-
6	5	3expb	Could not format ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) with typecode |-
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8		eqid	$$⊢{+}_R={+}_R$$
9	7 8	ablcom	$$⊢\left(R\in \mathrm{Abel}\wedge x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\to x{+}_{R}y=y{+}_{R}x$$
10	6 9	syl	Could not format ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) = ( y ( +g ` R ) x ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) = ( y ( +g ` R ) x ) ) with typecode |-
11	10	eleq1d	Could not format ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( +g ` R ) y ) e. A <-> ( y ( +g ` R ) x ) e. A ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( +g ` R ) y ) e. A <-> ( y ( +g ` R ) x ) e. A ) ) with typecode |-
12	11	biimpd	Could not format ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( +g ` R ) y ) e. A -> ( y ( +g ` R ) x ) e. A ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( +g ` R ) y ) e. A -> ( y ( +g ` R ) x ) e. A ) ) with typecode |-
13	12	ralrimivva	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
14	7 8	isnsg2	$$⊢A\in \mathrm{NrmSGrp}\left(R\right)\leftrightarrow \left(A\in \mathrm{SubGrp}\left(R\right)\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\left(x{+}_{R}y\in A\to y{+}_{R}x\in A\right)\right)$$
15	1 13 14	sylanbrc	Could not format ( A e. ( SubRng ` R ) -> A e. ( NrmSGrp ` R ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> A e. ( NrmSGrp ` R ) ) with typecode |-