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 29925
 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 29923 . 2 class oRing
2 vz . . . . . . . . . . . . 13 setvar 𝑧
32cv 1522 . . . . . . . . . . . 12 class 𝑧
4 va . . . . . . . . . . . . 13 setvar 𝑎
54cv 1522 . . . . . . . . . . . 12 class 𝑎
6 vl . . . . . . . . . . . . 13 setvar 𝑙
76cv 1522 . . . . . . . . . . . 12 class 𝑙
83, 5, 7wbr 4685 . . . . . . . . . . 11 wff 𝑧𝑙𝑎
9 vb . . . . . . . . . . . . 13 setvar 𝑏
109cv 1522 . . . . . . . . . . . 12 class 𝑏
113, 10, 7wbr 4685 . . . . . . . . . . 11 wff 𝑧𝑙𝑏
128, 11wa 383 . . . . . . . . . 10 wff (𝑧𝑙𝑎𝑧𝑙𝑏)
13 vt . . . . . . . . . . . . 13 setvar 𝑡
1413cv 1522 . . . . . . . . . . . 12 class 𝑡
155, 10, 14co 6690 . . . . . . . . . . 11 class (𝑎𝑡𝑏)
163, 15, 7wbr 4685 . . . . . . . . . 10 wff 𝑧𝑙(𝑎𝑡𝑏)
1712, 16wi 4 . . . . . . . . 9 wff ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
18 vv . . . . . . . . . 10 setvar 𝑣
1918cv 1522 . . . . . . . . 9 class 𝑣
2017, 9, 19wral 2941 . . . . . . . 8 wff 𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
2120, 4, 19wral 2941 . . . . . . 7 wff 𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
22 vr . . . . . . . . 9 setvar 𝑟
2322cv 1522 . . . . . . . 8 class 𝑟
24 cple 15995 . . . . . . . 8 class le
2523, 24cfv 5926 . . . . . . 7 class (le‘𝑟)
2621, 6, 25wsbc 3468 . . . . . 6 wff [(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
27 cmulr 15989 . . . . . . 7 class .r
2823, 27cfv 5926 . . . . . 6 class (.r𝑟)
2926, 13, 28wsbc 3468 . . . . 5 wff [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
30 c0g 16147 . . . . . 6 class 0g
3123, 30cfv 5926 . . . . 5 class (0g𝑟)
3229, 2, 31wsbc 3468 . . . 4 wff [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
33 cbs 15904 . . . . 5 class Base
3423, 33cfv 5926 . . . 4 class (Base‘𝑟)
3532, 18, 34wsbc 3468 . . 3 wff [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
36 crg 18593 . . . 4 class Ring
37 cogrp 29826 . . . 4 class oGrp
3836, 37cin 3606 . . 3 class (Ring ∩ oGrp)
3935, 22, 38crab 2945 . 2 class {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
401, 39wceq 1523 1 wff oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
 Colors of variables: wff setvar class This definition is referenced by:  isorng  29927
 Copyright terms: Public domain W3C validator