Metamath Proof Explorer

Theorem orngring

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

Ref Expression
Assertion orngring ⊢ R ∈ oRing → R ∈ Ring

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base R = Base R
2 eqid ⊢ 0 R = 0 R
3 eqid ⊢ ⋅ R = ⋅ R
4 eqid ⊢ ≤ R = ≤ R
5 1 2 3 4 isorng ⊢ R ∈ oRing ↔ R ∈ Ring ∧ R ∈ oGrp ∧ ∀ a ∈ Base R ∀ b ∈ Base R 0 R ≤ R a ∧ 0 R ≤ R b → 0 R ≤ R a ⋅ R b
6 5 simp1bi ⊢ R ∈ oRing → R ∈ Ring