This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orngogrp

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

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

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ 0_{R} = 0_{R}$
3		eqid	$⊢ \cdot_{R} = \cdot_{R}$
4		eqid	$⊢ \leq_{R} = \leq_{R}$
5	1 2 3 4	isorng	$⊢ R \in oRing \leftrightarrow (R \in Ring \land R \in oGrp \land \forall a \in {Base}_{R} \forall b \in {Base}_{R} ((0_{R} \leq_{R} a \land 0_{R} \leq_{R} b) \to 0_{R} \leq_{R} (a \cdot_{R} b)))$
6	5	simp2bi	$⊢ R \in oRing \to R \in oGrp$