Theorem ringrng

Description: A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Assertion	ringrng	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Rng}$$

Proof

Step	Hyp	Ref	Expression
1		ringabl	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Abel}$$
2		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
3		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
4		eqid	$$⊢{+}_R={+}_R$$
5		eqid	$$⊢{\cdot }_R={\cdot }_R$$
6	2 3 4 5	isring	$$⊢R\in \mathrm{Ring}\leftrightarrow \left(R\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x{\cdot }_R\left(y{+}_{R}z\right)=\left(x{\cdot }_{R}y\right){+}_R\left(x{\cdot }_{R}z\right)\wedge \left(x{+}_{R}y\right){\cdot }_{R}z=\left(x{\cdot }_{R}z\right){+}_R\left(y{\cdot }_{R}z\right)\right)\right)$$
7		simpl	$$⊢\left(R\in \mathrm{Abel}\wedge \left(R\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x{\cdot }_R\left(y{+}_{R}z\right)=\left(x{\cdot }_{R}y\right){+}_R\left(x{\cdot }_{R}z\right)\wedge \left(x{+}_{R}y\right){\cdot }_{R}z=\left(x{\cdot }_{R}z\right){+}_R\left(y{\cdot }_{R}z\right)\right)\right)\right)\to R\in \mathrm{Abel}$$
8		mndsgrp	Could not format ( ( mulGrp ` R ) e. Mnd -> ( mulGrp ` R ) e. Smgrp ) : No typesetting found for |- ( ( mulGrp ` R ) e. Mnd -> ( mulGrp ` R ) e. Smgrp ) with typecode |-
9	8	3ad2ant2	Could not format ( ( R e. Grp /\ ( mulGrp ` R ) e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) -> ( mulGrp ` R ) e. Smgrp ) : No typesetting found for |- ( ( R e. Grp /\ ( mulGrp ` R ) e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) -> ( mulGrp ` R ) e. Smgrp ) with typecode |-
10	9	adantl	Could not format ( ( R e. Abel /\ ( R e. Grp /\ ( mulGrp ` R ) e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) ) -> ( mulGrp ` R ) e. Smgrp ) : No typesetting found for |- ( ( R e. Abel /\ ( R e. Grp /\ ( mulGrp ` R ) e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) ) -> ( mulGrp ` R ) e. Smgrp ) with typecode |-
11		simpr3	$$⊢\left(R\in \mathrm{Abel}\wedge \left(R\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x{\cdot }_R\left(y{+}_{R}z\right)=\left(x{\cdot }_{R}y\right){+}_R\left(x{\cdot }_{R}z\right)\wedge \left(x{+}_{R}y\right){\cdot }_{R}z=\left(x{\cdot }_{R}z\right){+}_R\left(y{\cdot }_{R}z\right)\right)\right)\right)\to \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x{\cdot }_R\left(y{+}_{R}z\right)=\left(x{\cdot }_{R}y\right){+}_R\left(x{\cdot }_{R}z\right)\wedge \left(x{+}_{R}y\right){\cdot }_{R}z=\left(x{\cdot }_{R}z\right){+}_R\left(y{\cdot }_{R}z\right)\right)$$
12	2 3 4 5	isrng	Could not format ( R e. Rng <-> ( R e. Abel /\ ( mulGrp ` R ) e. Smgrp /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) ) : No typesetting found for |- ( R e. Rng <-> ( R e. Abel /\ ( mulGrp ` R ) e. Smgrp /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) ) with typecode |-
13	7 10 11 12	syl3anbrc	$$⊢\left(R\in \mathrm{Abel}\wedge \left(R\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x{\cdot }_R\left(y{+}_{R}z\right)=\left(x{\cdot }_{R}y\right){+}_R\left(x{\cdot }_{R}z\right)\wedge \left(x{+}_{R}y\right){\cdot }_{R}z=\left(x{\cdot }_{R}z\right){+}_R\left(y{\cdot }_{R}z\right)\right)\right)\right)\to R\in \mathrm{Rng}$$
14	13	ex	$$⊢R\in \mathrm{Abel}\to \left(\left(R\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\left(x{\cdot }_R\left(y{+}_{R}z\right)=\left(x{\cdot }_{R}y\right){+}_R\left(x{\cdot }_{R}z\right)\wedge \left(x{+}_{R}y\right){\cdot }_{R}z=\left(x{\cdot }_{R}z\right){+}_R\left(y{\cdot }_{R}z\right)\right)\right)\to R\in \mathrm{Rng}\right)$$
15	6 14	syl5bi	$$⊢R\in \mathrm{Abel}\to \left(R\in \mathrm{Ring}\to R\in \mathrm{Rng}\right)$$
16	1 15	mpcom	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Rng}$$