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 ‘ 𝑟 ) / 𝑙 ] ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ( ( 𝑧 𝑙 𝑎 ∧ 𝑧 𝑙 𝑏 ) → 𝑧 𝑙 ( 𝑎 𝑡 𝑏 ) ) }