Metamath Proof Explorer

Theorem ringrng

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

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

Proof

Step	Hyp	Ref	Expression
1		ringabl	$⊢ R \in Ring \to R \in Abel$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
4		eqid	$⊢ +_{R} = +_{R}$
5		eqid	$⊢ \cdot_{R} = \cdot_{R}$
6	2 3 4 5	isring	$⊢ R \in Ring \leftrightarrow (R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))$
7		simpl	$⊢ (R \in Abel \land (R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))) \to R \in Abel$
8		mndsgrp	$⊢ {mulGrp}_{R} \in Mnd \to {mulGrp}_{R} \in Smgrp$
9	8	3ad2ant2	$⊢ (R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))) \to {mulGrp}_{R} \in Smgrp$
10	9	adantl	$⊢ (R \in Abel \land (R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))) \to {mulGrp}_{R} \in Smgrp$
11		simpr3	$⊢ (R \in Abel \land (R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))) \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))$
12	2 3 4 5	isrng	$⊢ R \in Rng \leftrightarrow (R \in Abel \land {mulGrp}_{R} \in Smgrp \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))$
13	7 10 11 12	syl3anbrc	$⊢ (R \in Abel \land (R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))) \to R \in Rng$
14	13	ex	$⊢ R \in Abel \to ((R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))) \to R \in Rng)$
15	6 14	biimtrid	$⊢ R \in Abel \to (R \in Ring \to R \in Rng)$
16	1 15	mpcom	$⊢ R \in Ring \to R \in Rng$