Theorem ogrpinv0lt

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

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

Proof

Step	Hyp	Ref	Expression
1		ogrpinvlt.0	$$⊢B={\mathrm{Base}}_G$$
2		ogrpinvlt.1	$$⊢\underset{\dot{}}{<}={<}_G$$
3		ogrpinvlt.2	$$⊢I={inv}_g\left(G\right)$$
4		ogrpinv0lt.3	$$⊢\underset{\dot{}}{0}=0_G$$
5		simpll	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to G\in \mathrm{oGrp}$$
6		ogrpgrp	$$⊢G\in \mathrm{oGrp}\to G\in \mathrm{Grp}$$
7	5 6	syl	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to G\in \mathrm{Grp}$$
8	1 4	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
9	7 8	syl	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \underset{\dot{}}{0}\in B$$
10		simplr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to X\in B$$
11	1 3	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to I\left(X\right)\in B$$
12	7 10 11	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to I\left(X\right)\in B$$
13		simpr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
14		eqid	$$⊢{+}_G={+}_G$$
15	1 2 14	ogrpaddlt	$$⊢\left(G\in \mathrm{oGrp}\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{}}{<}X\right)\to \left(\underset{\dot{}}{0}{+}_{G}I\left(X\right)\right)\underset{\dot{}}{<}\left(X{+}_{G}I\left(X\right)\right)$$
16	5 9 10 12 13 15	syl131anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \left(\underset{\dot{}}{0}{+}_{G}I\left(X\right)\right)\underset{\dot{}}{<}\left(X{+}_{G}I\left(X\right)\right)$$
17	1 14 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)$$
18	7 12 17	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \underset{\dot{}}{0}{+}_{G}I\left(X\right)=I\left(X\right)$$
19	1 14 4 3	grprinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X{+}_{G}I\left(X\right)=\underset{\dot{}}{0}$$
20	7 10 19	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to X{+}_{G}I\left(X\right)=\underset{\dot{}}{0}$$
21	16 18 20	3brtr3d	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}$$
22		simpll	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to G\in \mathrm{oGrp}$$
23	22 6	syl	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to G\in \mathrm{Grp}$$
24		simplr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to X\in B$$
25	23 24 11	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to I\left(X\right)\in B$$
26	22 6 8	3syl	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\in B$$
27		simpr	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}$$
28	1 2 14	ogrpaddlt	$$⊢\left(G\in \mathrm{oGrp}\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{}}{<}\underset{\dot{}}{0}\right)\to \left(I\left(X\right){+}_{G}X\right)\underset{\dot{}}{<}\left(\underset{\dot{}}{0}{+}_{G}X\right)$$
29	22 25 26 24 27 28	syl131anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to \left(I\left(X\right){+}_{G}X\right)\underset{\dot{}}{<}\left(\underset{\dot{}}{0}{+}_{G}X\right)$$
30	1 14 4 3	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to I\left(X\right){+}_{G}X=\underset{\dot{}}{0}$$
31	23 24 30	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to I\left(X\right){+}_{G}X=\underset{\dot{}}{0}$$
32	1 14 4	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \underset{\dot{}}{0}{+}_{G}X=X$$
33	23 24 32	syl2anc	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}{+}_{G}X=X$$
34	29 31 33	3brtr3d	$$⊢\left(\left(G\in \mathrm{oGrp}\wedge X\in B\right)\wedge I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
35	21 34	impbida	$$⊢\left(G\in \mathrm{oGrp}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\leftrightarrow I\left(X\right)\underset{\dot{}}{<}\underset{\dot{}}{0}\right)$$