Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-orng Structured version   Visualization version   GIF version

Definition df-orng 30127
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.)
Assertion
Ref Expression
df-orng oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
Distinct variable group:   𝑎,𝑏,𝑙,𝑟,𝑡,𝑣,𝑧

Detailed syntax breakdown of Definition df-orng
StepHypRef Expression
1 corng 30125 . 2 class oRing
2 vz . . . . . . . . . . . . 13 setvar 𝑧
32cv 1631 . . . . . . . . . . . 12 class 𝑧
4 va . . . . . . . . . . . . 13 setvar 𝑎
54cv 1631 . . . . . . . . . . . 12 class 𝑎
6 vl . . . . . . . . . . . . 13 setvar 𝑙
76cv 1631 . . . . . . . . . . . 12 class 𝑙
83, 5, 7wbr 4804 . . . . . . . . . . 11 wff 𝑧𝑙𝑎
9 vb . . . . . . . . . . . . 13 setvar 𝑏
109cv 1631 . . . . . . . . . . . 12 class 𝑏
113, 10, 7wbr 4804 . . . . . . . . . . 11 wff 𝑧𝑙𝑏
128, 11wa 383 . . . . . . . . . 10 wff (𝑧𝑙𝑎𝑧𝑙𝑏)
13 vt . . . . . . . . . . . . 13 setvar 𝑡
1413cv 1631 . . . . . . . . . . . 12 class 𝑡
155, 10, 14co 6814 . . . . . . . . . . 11 class (𝑎𝑡𝑏)
163, 15, 7wbr 4804 . . . . . . . . . 10 wff 𝑧𝑙(𝑎𝑡𝑏)
1712, 16wi 4 . . . . . . . . 9 wff ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
18 vv . . . . . . . . . 10 setvar 𝑣
1918cv 1631 . . . . . . . . 9 class 𝑣
2017, 9, 19wral 3050 . . . . . . . 8 wff 𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
2120, 4, 19wral 3050 . . . . . . 7 wff 𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
22 vr . . . . . . . . 9 setvar 𝑟
2322cv 1631 . . . . . . . 8 class 𝑟
24 cple 16170 . . . . . . . 8 class le
2523, 24cfv 6049 . . . . . . 7 class (le‘𝑟)
2621, 6, 25wsbc 3576 . . . . . 6 wff [(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
27 cmulr 16164 . . . . . . 7 class .r
2823, 27cfv 6049 . . . . . 6 class (.r𝑟)
2926, 13, 28wsbc 3576 . . . . 5 wff [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
30 c0g 16322 . . . . . 6 class 0g
3123, 30cfv 6049 . . . . 5 class (0g𝑟)
3229, 2, 31wsbc 3576 . . . 4 wff [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
33 cbs 16079 . . . . 5 class Base
3423, 33cfv 6049 . . . 4 class (Base‘𝑟)
3532, 18, 34wsbc 3576 . . 3 wff [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
36 crg 18767 . . . 4 class Ring
37 cogrp 30028 . . . 4 class oGrp
3836, 37cin 3714 . . 3 class (Ring ∩ oGrp)
3935, 22, 38crab 3054 . 2 class {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
401, 39wceq 1632 1 wff oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
Colors of variables: wff setvar class
This definition is referenced by:  isorng  30129
  Copyright terms: Public domain W3C validator