ogrpaddltbi

Description: In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018)

	Ref	Expression
Hypotheses	ogrpaddlt.0	$⊢ B = {Base}_{G}$
	ogrpaddlt.1	$⊢ \underset{˙}{<} = <_{G}$
	ogrpaddlt.2	$⊢ \underset{˙}{+} = +_{G}$
Assertion	ogrpaddltbi	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z))$

Proof

Step	Hyp	Ref	Expression
1		ogrpaddlt.0	$⊢ B = {Base}_{G}$
2		ogrpaddlt.1	$⊢ \underset{˙}{<} = <_{G}$
3		ogrpaddlt.2	$⊢ \underset{˙}{+} = +_{G}$
4	1 2 3	ogrpaddlt	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)$
5	4	3expa	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{<} Y) \to (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)$
6		simpll	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to G \in oGrp$
7		ogrpgrp	$⊢ G \in oGrp \to G \in Grp$
8	6 7	syl	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to G \in Grp$
9		simplr1	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to X \in B$
10		simplr3	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to Z \in B$
11	1 3	grpcl	$⊢ (G \in Grp \land X \in B \land Z \in B) \to X \underset{˙}{+} Z \in B$
12	8 9 10 11	syl3anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to X \underset{˙}{+} Z \in B$
13		simplr2	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to Y \in B$
14	1 3	grpcl	$⊢ (G \in Grp \land Y \in B \land Z \in B) \to Y \underset{˙}{+} Z \in B$
15	8 13 10 14	syl3anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to Y \underset{˙}{+} Z \in B$
16		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
17	1 16	grpinvcl	$⊢ (G \in Grp \land Z \in B) \to {inv}_{g} (G) (Z) \in B$
18	8 10 17	syl2anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to {inv}_{g} (G) (Z) \in B$
19		simpr	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)$
20	1 2 3	ogrpaddlt	$⊢ (G \in oGrp \land (X \underset{˙}{+} Z \in B \land Y \underset{˙}{+} Z \in B \land {inv}_{g} (G) (Z) \in B) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to ((X \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z)) \underset{˙}{<} ((Y \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z))$
21	6 12 15 18 19 20	syl131anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to ((X \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z)) \underset{˙}{<} ((Y \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z))$
22	1 3	grpass	$⊢ (G \in Grp \land (X \in B \land Z \in B \land {inv}_{g} (G) (Z) \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z) = X \underset{˙}{+} (Z \underset{˙}{+} {inv}_{g} (G) (Z))$
23	8 9 10 18 22	syl13anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to (X \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z) = X \underset{˙}{+} (Z \underset{˙}{+} {inv}_{g} (G) (Z))$
24		eqid	$⊢ 0_{G} = 0_{G}$
25	1 3 24 16	grprinv	$⊢ (G \in Grp \land Z \in B) \to Z \underset{˙}{+} {inv}_{g} (G) (Z) = 0_{G}$
26	8 10 25	syl2anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to Z \underset{˙}{+} {inv}_{g} (G) (Z) = 0_{G}$
27	26	oveq2d	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to X \underset{˙}{+} (Z \underset{˙}{+} {inv}_{g} (G) (Z)) = X \underset{˙}{+} 0_{G}$
28	1 3 24	grprid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} 0_{G} = X$
29	8 9 28	syl2anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to X \underset{˙}{+} 0_{G} = X$
30	23 27 29	3eqtrd	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to (X \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z) = X$
31	1 3	grpass	$⊢ (G \in Grp \land (Y \in B \land Z \in B \land {inv}_{g} (G) (Z) \in B)) \to (Y \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z) = Y \underset{˙}{+} (Z \underset{˙}{+} {inv}_{g} (G) (Z))$
32	8 13 10 18 31	syl13anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to (Y \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z) = Y \underset{˙}{+} (Z \underset{˙}{+} {inv}_{g} (G) (Z))$
33	26	oveq2d	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to Y \underset{˙}{+} (Z \underset{˙}{+} {inv}_{g} (G) (Z)) = Y \underset{˙}{+} 0_{G}$
34	1 3 24	grprid	$⊢ (G \in Grp \land Y \in B) \to Y \underset{˙}{+} 0_{G} = Y$
35	8 13 34	syl2anc	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to Y \underset{˙}{+} 0_{G} = Y$
36	32 33 35	3eqtrd	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to (Y \underset{˙}{+} Z) \underset{˙}{+} {inv}_{g} (G) (Z) = Y$
37	21 30 36	3brtr3d	$⊢ ((G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \land (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z)) \to X \underset{˙}{<} Y$
38	5 37	impbida	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{+} Z) \underset{˙}{<} (Y \underset{˙}{+} Z))$

Metamath Proof Explorer

Theorem ogrpaddltbi

Proof