omndadd2rd

Description: In a left- and right- ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 2-May-2018)

	Ref	Expression
Hypotheses	omndadd.0	$⊢ B = {Base}_{M}$
	omndadd.1	$⊢ \underset{˙}{\leq} = \leq_{M}$
	omndadd.2	$⊢ \underset{˙}{+} = +_{M}$
	omndadd2d.m	$⊢ φ \to M \in oMnd$
	omndadd2d.w	$⊢ φ \to W \in B$
	omndadd2d.x	$⊢ φ \to X \in B$
	omndadd2d.y	$⊢ φ \to Y \in B$
	omndadd2d.z	$⊢ φ \to Z \in B$
	omndadd2d.1	$⊢ φ \to X \underset{˙}{\leq} Z$
	omndadd2d.2	$⊢ φ \to Y \underset{˙}{\leq} W$
	omndadd2rd.c	$⊢ φ \to {opp}_{𝑔} (M) \in oMnd$
Assertion	omndadd2rd	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W)$

Proof

Step	Hyp	Ref	Expression
1		omndadd.0	$⊢ B = {Base}_{M}$
2		omndadd.1	$⊢ \underset{˙}{\leq} = \leq_{M}$
3		omndadd.2	$⊢ \underset{˙}{+} = +_{M}$
4		omndadd2d.m	$⊢ φ \to M \in oMnd$
5		omndadd2d.w	$⊢ φ \to W \in B$
6		omndadd2d.x	$⊢ φ \to X \in B$
7		omndadd2d.y	$⊢ φ \to Y \in B$
8		omndadd2d.z	$⊢ φ \to Z \in B$
9		omndadd2d.1	$⊢ φ \to X \underset{˙}{\leq} Z$
10		omndadd2d.2	$⊢ φ \to Y \underset{˙}{\leq} W$
11		omndadd2rd.c	$⊢ φ \to {opp}_{𝑔} (M) \in oMnd$
12		omndtos	$⊢ M \in oMnd \to M \in Toset$
13		tospos	$⊢ M \in Toset \to M \in Poset$
14	4 12 13	3syl	$⊢ φ \to M \in Poset$
15		omndmnd	$⊢ M \in oMnd \to M \in Mnd$
16	4 15	syl	$⊢ φ \to M \in Mnd$
17	1 3	mndcl	$⊢ (M \in Mnd \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
18	16 6 7 17	syl3anc	$⊢ φ \to X \underset{˙}{+} Y \in B$
19	1 3	mndcl	$⊢ (M \in Mnd \land X \in B \land W \in B) \to X \underset{˙}{+} W \in B$
20	16 6 5 19	syl3anc	$⊢ φ \to X \underset{˙}{+} W \in B$
21	1 3	mndcl	$⊢ (M \in Mnd \land Z \in B \land W \in B) \to Z \underset{˙}{+} W \in B$
22	16 8 5 21	syl3anc	$⊢ φ \to Z \underset{˙}{+} W \in B$
23	18 20 22	3jca	$⊢ φ \to (X \underset{˙}{+} Y \in B \land X \underset{˙}{+} W \in B \land Z \underset{˙}{+} W \in B)$
24	1 2 3	omndaddr	$⊢ ({opp}_{𝑔} (M) \in oMnd \land (Y \in B \land W \in B \land X \in B) \land Y \underset{˙}{\leq} W) \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (X \underset{˙}{+} W)$
25	11 7 5 6 10 24	syl131anc	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (X \underset{˙}{+} W)$
26	1 2 3	omndadd	$⊢ (M \in oMnd \land (X \in B \land Z \in B \land W \in B) \land X \underset{˙}{\leq} Z) \to (X \underset{˙}{+} W) \underset{˙}{\leq} (Z \underset{˙}{+} W)$
27	4 6 8 5 9 26	syl131anc	$⊢ φ \to (X \underset{˙}{+} W) \underset{˙}{\leq} (Z \underset{˙}{+} W)$
28	1 2	postr	$⊢ (M \in Poset \land (X \underset{˙}{+} Y \in B \land X \underset{˙}{+} W \in B \land Z \underset{˙}{+} W \in B)) \to (((X \underset{˙}{+} Y) \underset{˙}{\leq} (X \underset{˙}{+} W) \land (X \underset{˙}{+} W) \underset{˙}{\leq} (Z \underset{˙}{+} W)) \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W))$
29	28	imp	$⊢ ((M \in Poset \land (X \underset{˙}{+} Y \in B \land X \underset{˙}{+} W \in B \land Z \underset{˙}{+} W \in B)) \land ((X \underset{˙}{+} Y) \underset{˙}{\leq} (X \underset{˙}{+} W) \land (X \underset{˙}{+} W) \underset{˙}{\leq} (Z \underset{˙}{+} W))) \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W)$
30	14 23 25 27 29	syl22anc	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W)$

Metamath Proof Explorer

Theorem omndadd2rd

Proof