Theorem orngogrp

Description: An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018)

	Ref	Expression
Assertion	orngogrp	$$⊢R\in \mathrm{oRing}\to R\in \mathrm{oGrp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2		eqid	$$⊢0_R=0_R$$
3		eqid	$$⊢{\cdot }_R={\cdot }_R$$
4		eqid	$$⊢{\le }_R={\le }_R$$
5	1 2 3 4	isorng	$$⊢R\in \mathrm{oRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge R\in \mathrm{oGrp}\wedge \forall a\in {\mathrm{Base}}_R\forall b\in {\mathrm{Base}}_R\left(\left(0_R{\le }_{R}a\wedge 0_R{\le }_{R}b\right)\to 0_R{\le }_R\left(a{\cdot }_{R}b\right)\right)\right)$$
6	5	simp2bi	$$⊢R\in \mathrm{oRing}\to R\in \mathrm{oGrp}$$