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

Metamath Proof Explorer

Definition df-orng

Description: Define class of all ordered rings. An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Assertion df-orng ⊢ oRing = r ∈ Ring ∩ oGrp | [˙Base r / v]˙ [˙0 r / z]˙ [˙⋅ r / t]˙ [˙≤ r / l]˙ ∀ a ∈ v ∀ b ∈ v z l a ∧ z l b → z l a t b

Detailed syntax breakdown

Step Hyp Ref Expression
0 corng class oRing
1 vr setvar r
2 crg class Ring
3 cogrp class oGrp
4 2 3 cin class Ring ∩ oGrp
5 cbs class Base
6 1 cv setvar r
7 6 5 cfv class Base r
8 vv setvar v
9 c0g class 0 𝑔
10 6 9 cfv class 0 r
11 vz setvar z
12 cmulr class ⋅ 𝑟
13 6 12 cfv class ⋅ r
14 vt setvar t
15 cple class le
16 6 15 cfv class ≤ r
17 vl setvar l
18 va setvar a
19 8 cv setvar v
20 vb setvar b
21 11 cv setvar z
22 17 cv setvar l
23 18 cv setvar a
24 21 23 22 wbr wff z l a
25 20 cv setvar b
26 21 25 22 wbr wff z l b
27 24 26 wa wff z l a ∧ z l b
28 14 cv setvar t
29 23 25 28 co class a t b
30 21 29 22 wbr wff z l a t b
31 27 30 wi wff z l a ∧ z l b → z l a t b
32 31 20 19 wral wff ∀ b ∈ v z l a ∧ z l b → z l a t b
33 32 18 19 wral wff ∀ a ∈ v ∀ b ∈ v z l a ∧ z l b → z l a t b
34 33 17 16 wsbc wff [˙≤ r / l]˙ ∀ a ∈ v ∀ b ∈ v z l a ∧ z l b → z l a t b
35 34 14 13 wsbc wff [˙⋅ r / t]˙ [˙≤ r / l]˙ ∀ a ∈ v ∀ b ∈ v z l a ∧ z l b → z l a t b
36 35 11 10 wsbc wff [˙0 r / z]˙ [˙⋅ r / t]˙ [˙≤ r / l]˙ ∀ a ∈ v ∀ b ∈ v z l a ∧ z l b → z l a t b
37 36 8 7 wsbc wff [˙Base r / v]˙ [˙0 r / z]˙ [˙⋅ r / t]˙ [˙≤ r / l]˙ ∀ a ∈ v ∀ b ∈ v z l a ∧ z l b → z l a t b
38 37 1 4 crab class r ∈ Ring ∩ oGrp | [˙Base r / v]˙ [˙0 r / z]˙ [˙⋅ r / t]˙ [˙≤ r / l]˙ ∀ a ∈ v ∀ b ∈ v z l a ∧ z l b → z l a t b
39 0 38 wceq wff oRing = r ∈ Ring ∩ oGrp | [˙Base r / v]˙ [˙0 r / z]˙ [˙⋅ r / t]˙ [˙≤ r / l]˙ ∀ a ∈ v ∀ b ∈ v z l a ∧ z l b → z l a t b