ogrpinvlt

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 = {Base}_{G}$
	ogrpinvlt.1	$⊢ \underset{˙}{<} = <_{G}$
	ogrpinvlt.2	$⊢ I = {inv}_{g} (G)$
Assertion	ogrpinvlt	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow I (Y) \underset{˙}{<} I (X))$

Proof

Step	Hyp	Ref	Expression
1		ogrpinvlt.0	$⊢ B = {Base}_{G}$
2		ogrpinvlt.1	$⊢ \underset{˙}{<} = <_{G}$
3		ogrpinvlt.2	$⊢ I = {inv}_{g} (G)$
4		simp1l	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to G \in oGrp$
5		simp2	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to X \in B$
6		simp3	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to Y \in B$
7		ogrpgrp	$⊢ G \in oGrp \to G \in Grp$
8	4 7	syl	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to G \in Grp$
9	1 3	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to I (Y) \in B$
10	8 6 9	syl2anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to I (Y) \in B$
11		eqid	$⊢ +_{G} = +_{G}$
12	1 2 11	ogrpaddltbi	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land I (Y) \in B)) \to (X \underset{˙}{<} Y \leftrightarrow (X +_{G} I (Y)) \underset{˙}{<} (Y +_{G} I (Y)))$
13	4 5 6 10 12	syl13anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X +_{G} I (Y)) \underset{˙}{<} (Y +_{G} I (Y)))$
14		eqid	$⊢ 0_{G} = 0_{G}$
15	1 11 14 3	grprinv	$⊢ (G \in Grp \land Y \in B) \to Y +_{G} I (Y) = 0_{G}$
16	8 6 15	syl2anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to Y +_{G} I (Y) = 0_{G}$
17	16	breq2d	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to ((X +_{G} I (Y)) \underset{˙}{<} (Y +_{G} I (Y)) \leftrightarrow (X +_{G} I (Y)) \underset{˙}{<} 0_{G})$
18		simp1r	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to {opp}_{𝑔} (G) \in oGrp$
19	1 11	grpcl	$⊢ (G \in Grp \land X \in B \land I (Y) \in B) \to X +_{G} I (Y) \in B$
20	8 5 10 19	syl3anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to X +_{G} I (Y) \in B$
21	1 14	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
22	4 7 21	3syl	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to 0_{G} \in B$
23	1 3	grpinvcl	$⊢ (G \in Grp \land X \in B) \to I (X) \in B$
24	8 5 23	syl2anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to I (X) \in B$
25	1 2 11 4 18 20 22 24	ogrpaddltrbid	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to ((X +_{G} I (Y)) \underset{˙}{<} 0_{G} \leftrightarrow (I (X) +_{G} (X +_{G} I (Y))) \underset{˙}{<} (I (X) +_{G} 0_{G}))$
26	13 17 25	3bitrd	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (I (X) +_{G} (X +_{G} I (Y))) \underset{˙}{<} (I (X) +_{G} 0_{G}))$
27	1 11 14 3	grplinv	$⊢ (G \in Grp \land X \in B) \to I (X) +_{G} X = 0_{G}$
28	8 5 27	syl2anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to I (X) +_{G} X = 0_{G}$
29	28	oveq1d	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to (I (X) +_{G} X) +_{G} I (Y) = 0_{G} +_{G} I (Y)$
30	1 11	grpass	$⊢ (G \in Grp \land (I (X) \in B \land X \in B \land I (Y) \in B)) \to (I (X) +_{G} X) +_{G} I (Y) = I (X) +_{G} (X +_{G} I (Y))$
31	8 24 5 10 30	syl13anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to (I (X) +_{G} X) +_{G} I (Y) = I (X) +_{G} (X +_{G} I (Y))$
32	1 11 14	grplid	$⊢ (G \in Grp \land I (Y) \in B) \to 0_{G} +_{G} I (Y) = I (Y)$
33	8 10 32	syl2anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to 0_{G} +_{G} I (Y) = I (Y)$
34	29 31 33	3eqtr3d	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to I (X) +_{G} (X +_{G} I (Y)) = I (Y)$
35	1 11 14	grprid	$⊢ (G \in Grp \land I (X) \in B) \to I (X) +_{G} 0_{G} = I (X)$
36	8 24 35	syl2anc	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to I (X) +_{G} 0_{G} = I (X)$
37	34 36	breq12d	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to ((I (X) +_{G} (X +_{G} I (Y))) \underset{˙}{<} (I (X) +_{G} 0_{G}) \leftrightarrow I (Y) \underset{˙}{<} I (X))$
38	26 37	bitrd	$⊢ ((G \in oGrp \land {opp}_{𝑔} (G) \in oGrp) \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow I (Y) \underset{˙}{<} I (X))$

Metamath Proof Explorer

Theorem ogrpinvlt

Proof