Theorem 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={\mathrm{Base}}_R$$
	isorng.1	$$⊢\underset{\dot{}}{0}=0_R$$
	isorng.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isorng.3	$$⊢\underset{\dot{}}{\le }={\le }_R$$
Assertion	isorng	$$⊢R\in \mathrm{oRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge R\in \mathrm{oGrp}\wedge \forall a\in B\forall b\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }a\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(a\underset{\dot{}}{·}b\right)\right)\right)$$

Proof

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