isorng

Description: An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018)

	Ref	Expression
Hypotheses	isorng.0	$⊢ B = {Base}_{R}$
	isorng.1	$⊢ \underset{˙}{0} = 0_{R}$
	isorng.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	isorng.3	$⊢ \underset{˙}{\leq} = \leq_{R}$
Assertion	isorng	$⊢ R \in oRing \leftrightarrow (R \in Ring \land R \in oGrp \land \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$

Proof

Step	Hyp	Ref	Expression
1		isorng.0	$⊢ B = {Base}_{R}$
2		isorng.1	$⊢ \underset{˙}{0} = 0_{R}$
3		isorng.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		isorng.3	$⊢ \underset{˙}{\leq} = \leq_{R}$
5		elin	$⊢ R \in (Ring \cap oGrp) \leftrightarrow (R \in Ring \land R \in oGrp)$
6	5	anbi1i	$⊢ (R \in (Ring \cap oGrp) \land \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b))) \leftrightarrow ((R \in Ring \land R \in oGrp) \land \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$
7		fvexd	$⊢ r = R \to \cdot_{r} \in V$
8		simpr	$⊢ (r = R \land t = \cdot_{r}) \to t = \cdot_{r}$
9		simpl	$⊢ (r = R \land t = \cdot_{r}) \to r = R$
10	9	fveq2d	$⊢ (r = R \land t = \cdot_{r}) \to \cdot_{r} = \cdot_{R}$
11	10 3	eqtr4di	$⊢ (r = R \land t = \cdot_{r}) \to \cdot_{r} = \underset{˙}{\cdot}$
12	8 11	eqtrd	$⊢ (r = R \land t = \cdot_{r}) \to t = \underset{˙}{\cdot}$
13	12	oveqd	$⊢ (r = R \land t = \cdot_{r}) \to a t b = a \underset{˙}{\cdot} b$
14	13	breq2d	$⊢ (r = R \land t = \cdot_{r}) \to (\underset{˙}{0} l (a t b) \leftrightarrow \underset{˙}{0} l (a \underset{˙}{\cdot} b))$
15	14	imbi2d	$⊢ (r = R \land t = \cdot_{r}) \to (((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)) \leftrightarrow ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a \underset{˙}{\cdot} b)))$
16	15	2ralbidv	$⊢ (r = R \land t = \cdot_{r}) \to (\forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)) \leftrightarrow \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a \underset{˙}{\cdot} b)))$
17	16	sbcbidv	$⊢ (r = R \land t = \cdot_{r}) \to (\underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)) \leftrightarrow \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a \underset{˙}{\cdot} b)))$
18	7 17	sbcied	$⊢ r = R \to (\underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)) \leftrightarrow \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a \underset{˙}{\cdot} b)))$
19		fvexd	$⊢ r = R \to {Base}_{r} \in V$
20		simpr	$⊢ (r = R \land v = {Base}_{r}) \to v = {Base}_{r}$
21		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
22	21 1	eqtr4di	$⊢ r = R \to {Base}_{r} = B$
23	22	adantr	$⊢ (r = R \land v = {Base}_{r}) \to {Base}_{r} = B$
24	20 23	eqtrd	$⊢ (r = R \land v = {Base}_{r}) \to v = B$
25		raleq	$⊢ v = B \to (\forall b \in v ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \forall b \in B ((z l a \land z l b) \to z l (a t b)))$
26	25	raleqbi1dv	$⊢ v = B \to (\forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)))$
27	24 26	syl	$⊢ (r = R \land v = {Base}_{r}) \to (\forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)))$
28	27	sbcbidv	$⊢ (r = R \land v = {Base}_{r}) \to (\underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)))$
29	28	sbcbidv	$⊢ (r = R \land v = {Base}_{r}) \to (\underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)))$
30	29	sbcbidv	$⊢ (r = R \land v = {Base}_{r}) \to (\underset{˙}{[} 0_{r} / z \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \underset{˙}{[} 0_{r} / z \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)))$
31	19 30	sbcied	$⊢ r = R \to (\underset{˙}{[} {Base}_{r} / v \underset{˙}{]} \underset{˙}{[} 0_{r} / z \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \underset{˙}{[} 0_{r} / z \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)))$
32		fvexd	$⊢ r = R \to 0_{r} \in V$
33		simpr	$⊢ (r = R \land z = 0_{r}) \to z = 0_{r}$
34		fveq2	$⊢ r = R \to 0_{r} = 0_{R}$
35	34 2	eqtr4di	$⊢ r = R \to 0_{r} = \underset{˙}{0}$
36	35	adantr	$⊢ (r = R \land z = 0_{r}) \to 0_{r} = \underset{˙}{0}$
37	33 36	eqtrd	$⊢ (r = R \land z = 0_{r}) \to z = \underset{˙}{0}$
38	37	breq1d	$⊢ (r = R \land z = 0_{r}) \to (z l a \leftrightarrow \underset{˙}{0} l a)$
39	37	breq1d	$⊢ (r = R \land z = 0_{r}) \to (z l b \leftrightarrow \underset{˙}{0} l b)$
40	38 39	anbi12d	$⊢ (r = R \land z = 0_{r}) \to ((z l a \land z l b) \leftrightarrow (\underset{˙}{0} l a \land \underset{˙}{0} l b))$
41	37	breq1d	$⊢ (r = R \land z = 0_{r}) \to (z l (a t b) \leftrightarrow \underset{˙}{0} l (a t b))$
42	40 41	imbi12d	$⊢ (r = R \land z = 0_{r}) \to (((z l a \land z l b) \to z l (a t b)) \leftrightarrow ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)))$
43	42	2ralbidv	$⊢ (r = R \land z = 0_{r}) \to (\forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)))$
44	43	sbcbidv	$⊢ (r = R \land z = 0_{r}) \to (\underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)))$
45	44	sbcbidv	$⊢ (r = R \land z = 0_{r}) \to (\underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)))$
46	32 45	sbcied	$⊢ r = R \to (\underset{˙}{[} 0_{r} / z \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)))$
47	31 46	bitr2d	$⊢ r = R \to (\underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a t b)) \leftrightarrow \underset{˙}{[} {Base}_{r} / v \underset{˙}{]} \underset{˙}{[} 0_{r} / z \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b)))$
48		fvexd	$⊢ r = R \to \leq_{r} \in V$
49		simpr	$⊢ (r = R \land l = \leq_{r}) \to l = \leq_{r}$
50		simpl	$⊢ (r = R \land l = \leq_{r}) \to r = R$
51	50	fveq2d	$⊢ (r = R \land l = \leq_{r}) \to \leq_{r} = \leq_{R}$
52	51 4	eqtr4di	$⊢ (r = R \land l = \leq_{r}) \to \leq_{r} = \underset{˙}{\leq}$
53	49 52	eqtrd	$⊢ (r = R \land l = \leq_{r}) \to l = \underset{˙}{\leq}$
54	53	breqd	$⊢ (r = R \land l = \leq_{r}) \to (\underset{˙}{0} l a \leftrightarrow \underset{˙}{0} \underset{˙}{\leq} a)$
55	53	breqd	$⊢ (r = R \land l = \leq_{r}) \to (\underset{˙}{0} l b \leftrightarrow \underset{˙}{0} \underset{˙}{\leq} b)$
56	54 55	anbi12d	$⊢ (r = R \land l = \leq_{r}) \to ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \leftrightarrow (\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b))$
57	53	breqd	$⊢ (r = R \land l = \leq_{r}) \to (\underset{˙}{0} l (a \underset{˙}{\cdot} b) \leftrightarrow \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b))$
58	56 57	imbi12d	$⊢ (r = R \land l = \leq_{r}) \to (((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a \underset{˙}{\cdot} b)) \leftrightarrow ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$
59	58	2ralbidv	$⊢ (r = R \land l = \leq_{r}) \to (\forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a \underset{˙}{\cdot} b)) \leftrightarrow \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$
60	48 59	sbcied	$⊢ r = R \to (\underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in B \forall b \in B ((\underset{˙}{0} l a \land \underset{˙}{0} l b) \to \underset{˙}{0} l (a \underset{˙}{\cdot} b)) \leftrightarrow \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$
61	18 47 60	3bitr3d	$⊢ r = R \to (\underset{˙}{[} {Base}_{r} / v \underset{˙}{]} \underset{˙}{[} 0_{r} / z \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b)) \leftrightarrow \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$
62		df-orng	$⊢ oRing = \{r \in (Ring \cap oGrp) \| \underset{˙}{[} {Base}_{r} / v \underset{˙}{]} \underset{˙}{[} 0_{r} / z \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} \leq_{r} / l \underset{˙}{]} \forall a \in v \forall b \in v ((z l a \land z l b) \to z l (a t b))\}$
63	61 62	elrab2	$⊢ R \in oRing \leftrightarrow (R \in (Ring \cap oGrp) \land \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$
64		df-3an	$⊢ (R \in Ring \land R \in oGrp \land \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b))) \leftrightarrow ((R \in Ring \land R \in oGrp) \land \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$
65	6 63 64	3bitr4i	$⊢ R \in oRing \leftrightarrow (R \in Ring \land R \in oGrp \land \forall a \in B \forall b \in B ((\underset{˙}{0} \underset{˙}{\leq} a \land \underset{˙}{0} \underset{˙}{\leq} b) \to \underset{˙}{0} \underset{˙}{\leq} (a \underset{˙}{\cdot} b)))$

Metamath Proof Explorer

Theorem isorng

Proof