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 = { 𝑟 ∈ ( Ring ∩ oGrp ) ∣ [ ( Base ‘ 𝑟 ) / 𝑣 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] [ ( le ‘ 𝑟 ) / 𝑙 ] ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 corng ⊢ oRing
1 vr ⊢ 𝑟
2 crg ⊢ Ring
3 cogrp ⊢ oGrp
4 2 3 cin ⊢ ( Ring ∩ oGrp )
5 cbs ⊢ Base
6 1 cv ⊢ 𝑟
7 6 5 cfv ⊢ ( Base ‘ 𝑟 )
8 vv ⊢ 𝑣
9 c0g ⊢ 0g
10 6 9 cfv ⊢ ( 0g ‘ 𝑟 )
11 vz ⊢ 𝑧
12 cmulr ⊢ .r
13 6 12 cfv ⊢ ( .r ‘ 𝑟 )
14 vt ⊢ 𝑡
15 cple ⊢ le
16 6 15 cfv ⊢ ( le ‘ 𝑟 )
17 vl ⊢ 𝑙
18 va ⊢ 𝑎
19 8 cv ⊢ 𝑣
20 vb ⊢ 𝑏
21 11 cv ⊢ 𝑧
22 17 cv ⊢ 𝑙
23 18 cv ⊢ 𝑎
24 21 23 22 wbr ⊢ 𝑧 𝑙 𝑎
25 20 cv ⊢ 𝑏
26 21 25 22 wbr ⊢ 𝑧 𝑙 𝑏
27 24 26 wa ⊢ ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 )
28 14 cv ⊢ 𝑡
29 23 25 28 co ⊢ ( 𝑎 𝑡 𝑏 )
30 21 29 22 wbr ⊢ 𝑧 𝑙 ( 𝑎 𝑡 𝑏 )
31 27 30 wi ⊢ ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) )
32 31 20 19 wral ⊢ ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) )
33 32 18 19 wral ⊢ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) )
34 33 17 16 wsbc ⊢ [ ( le ‘ 𝑟 ) / 𝑙 ] ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) )
35 34 14 13 wsbc ⊢ [ ( .r ‘ 𝑟 ) / 𝑡 ] [ ( le ‘ 𝑟 ) / 𝑙 ] ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) )
36 35 11 10 wsbc ⊢ [ ( 0g ‘ 𝑟 ) / 𝑧 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] [ ( le ‘ 𝑟 ) / 𝑙 ] ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) )
37 36 8 7 wsbc ⊢ [ ( Base ‘ 𝑟 ) / 𝑣 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] [ ( le ‘ 𝑟 ) / 𝑙 ] ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) )
38 37 1 4 crab ⊢ { 𝑟 ∈ ( Ring ∩ oGrp ) ∣ [ ( Base ‘ 𝑟 ) / 𝑣 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] [ ( le ‘ 𝑟 ) / 𝑙 ] ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) ) }
39 0 38 wceq ⊢ oRing = { 𝑟 ∈ ( Ring ∩ oGrp ) ∣ [ ( Base ‘ 𝑟 ) / 𝑣 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] [ ( le ‘ 𝑟 ) / 𝑙 ] ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) ) }