Theorem orngogrp

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

	Ref	Expression
Assertion	orngogrp	⊢ ( 𝑅 ∈ oRing → 𝑅 ∈ oGrp )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
3		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
4		eqid	⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
5	1 2 3 4	isorng	⊢ ( 𝑅 ∈ oRing ↔ ( 𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑅 ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( ( 0g ‘ 𝑅 ) ( le ‘ 𝑅 ) 𝑎 ∧ ( 0g ‘ 𝑅 ) ( le ‘ 𝑅 ) 𝑏 ) → ( 0g ‘ 𝑅 ) ( le ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ) )
6	5	simp2bi	⊢ ( 𝑅 ∈ oRing → 𝑅 ∈ oGrp )