ogrpsub

Description: In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	ogrpsub.0	$⊢ B = {Base}_{G}$
	ogrpsub.1	$⊢ \underset{˙}{\leq} = \leq_{G}$
	ogrpsub.2	$⊢ \underset{˙}{-} = -_{G}$
Assertion	ogrpsub	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to (X \underset{˙}{-} Z) \underset{˙}{\leq} (Y \underset{˙}{-} Z)$

Proof

Step	Hyp	Ref	Expression
1		ogrpsub.0	$⊢ B = {Base}_{G}$
2		ogrpsub.1	$⊢ \underset{˙}{\leq} = \leq_{G}$
3		ogrpsub.2	$⊢ \underset{˙}{-} = -_{G}$
4		isogrp	$⊢ G \in oGrp \leftrightarrow (G \in Grp \land G \in oMnd)$
5	4	simprbi	$⊢ G \in oGrp \to G \in oMnd$
6	5	3ad2ant1	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to G \in oMnd$
7		simp21	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to X \in B$
8		simp22	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to Y \in B$
9		ogrpgrp	$⊢ G \in oGrp \to G \in Grp$
10	9	3ad2ant1	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to G \in Grp$
11		simp23	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to Z \in B$
12		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
13	1 12	grpinvcl	$⊢ (G \in Grp \land Z \in B) \to {inv}_{g} (G) (Z) \in B$
14	10 11 13	syl2anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to {inv}_{g} (G) (Z) \in B$
15		simp3	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y$
16		eqid	$⊢ +_{G} = +_{G}$
17	1 2 16	omndadd	$⊢ (G \in oMnd \land (X \in B \land Y \in B \land {inv}_{g} (G) (Z) \in B) \land X \underset{˙}{\leq} Y) \to (X +_{G} {inv}_{g} (G) (Z)) \underset{˙}{\leq} (Y +_{G} {inv}_{g} (G) (Z))$
18	6 7 8 14 15 17	syl131anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to (X +_{G} {inv}_{g} (G) (Z)) \underset{˙}{\leq} (Y +_{G} {inv}_{g} (G) (Z))$
19	1 16 12 3	grpsubval	$⊢ (X \in B \land Z \in B) \to X \underset{˙}{-} Z = X +_{G} {inv}_{g} (G) (Z)$
20	7 11 19	syl2anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{-} Z = X +_{G} {inv}_{g} (G) (Z)$
21	1 16 12 3	grpsubval	$⊢ (Y \in B \land Z \in B) \to Y \underset{˙}{-} Z = Y +_{G} {inv}_{g} (G) (Z)$
22	8 11 21	syl2anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to Y \underset{˙}{-} Z = Y +_{G} {inv}_{g} (G) (Z)$
23	18 20 22	3brtr4d	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to (X \underset{˙}{-} Z) \underset{˙}{\leq} (Y \underset{˙}{-} Z)$

Metamath Proof Explorer

Theorem ogrpsub

Proof