Theorem ogrpinv0le

Description: In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018)

	Ref	Expression
Hypotheses	ogrpsub.0	$$⊢B={\mathrm{Base}}_G$$
	ogrpsub.1	$$⊢\underset{\dot{}}{\le }={\le }_G$$
	ogrpinv.2	$$⊢I={inv}_g\left(G\right)$$
	ogrpinv.3	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	ogrpinv0le	$$⊢\left(G\in \mathrm{oGrp}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\leftrightarrow I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ogrpsub.0	$$⊢B={\mathrm{Base}}_G$$
2		ogrpsub.1	$$⊢\underset{\dot{}}{\le }={\le }_G$$
3		ogrpinv.2	$$⊢I={inv}_g\left(G\right)$$
4		ogrpinv.3	$$⊢\underset{\dot{}}{0}=0_G$$
5		isogrp	$$⊢G\in \mathrm{oGrp}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{oMnd}\right)$$
6	5	simprbi	$$⊢G\in \mathrm{oGrp}\to G\in \mathrm{oMnd}$$
7	6	ad2antrr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to G\in \mathrm{oMnd}$$
8		omndmnd	$$⊢G\in \mathrm{oMnd}\to G\in \mathrm{Mnd}$$
9	1 4	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
10	7 8 9	3syl	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to \underset{\dot{}}{0}\in B$$
11		simplr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to X\in B$$
12		ogrpgrp	$$⊢G\in \mathrm{oGrp}\to G\in \mathrm{Grp}$$
13	12	ad2antrr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to G\in \mathrm{Grp}$$
14	1 3	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to I\left(X\right)\in B$$
15	13 11 14	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to I\left(X\right)\in B$$
16		simpr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }X$$
17		eqid	$$⊢{+}_G={+}_G$$
18	1 2 17	omndadd	$$⊢\left(G\in \mathrm{oMnd}\wedge \left(\underset{\dot{}}{0}\in B\wedge X\in B\wedge I\left(X\right)\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to \left(\underset{\dot{}}{0}{+}_{G}I\left(X\right)\right)\underset{\dot{}}{\le }\left(X{+}_{G}I\left(X\right)\right)$$
19	7 10 11 15 16 18	syl131anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to \left(\underset{\dot{}}{0}{+}_{G}I\left(X\right)\right)\underset{\dot{}}{\le }\left(X{+}_{G}I\left(X\right)\right)$$
20	1 17 4	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge I\left(X\right)\in B\right)\to \underset{\dot{}}{0}{+}_{G}I\left(X\right)=I\left(X\right)$$
21	13 15 20	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to \underset{\dot{}}{0}{+}_{G}I\left(X\right)=I\left(X\right)$$
22	1 17 4 3	grprinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X{+}_{G}I\left(X\right)=\underset{\dot{}}{0}$$
23	13 11 22	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to X{+}_{G}I\left(X\right)=\underset{\dot{}}{0}$$
24	19 21 23	3brtr3d	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}$$
25	6	ad2antrr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to G\in \mathrm{oMnd}$$
26	12	ad2antrr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to G\in \mathrm{Grp}$$
27		simplr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to X\in B$$
28	26 27 14	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to I\left(X\right)\in B$$
29	25 8 9	3syl	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\in B$$
30		simpr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}$$
31	1 2 17	omndadd	$$⊢\left(G\in \mathrm{oMnd}\wedge \left(I\left(X\right)\in B\wedge \underset{\dot{}}{0}\in B\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to \left(I\left(X\right){+}_{G}X\right)\underset{\dot{}}{\le }\left(\underset{\dot{}}{0}{+}_{G}X\right)$$
32	25 28 29 27 30 31	syl131anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to \left(I\left(X\right){+}_{G}X\right)\underset{\dot{}}{\le }\left(\underset{\dot{}}{0}{+}_{G}X\right)$$
33	1 17 4 3	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to I\left(X\right){+}_{G}X=\underset{\dot{}}{0}$$
34	26 27 33	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to I\left(X\right){+}_{G}X=\underset{\dot{}}{0}$$
35	1 17 4	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \underset{\dot{}}{0}{+}_{G}X=X$$
36	26 27 35	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}{+}_{G}X=X$$
37	32 34 36	3brtr3d	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }X$$
38	24 37	impbida	$$⊢\left(G\in \mathrm{oGrp}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\leftrightarrow I\left(X\right)\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)$$