omndadd2d

Description: In a commutative left ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 30-Jan-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$
	omndadd2d.c	$⊢ φ \to M \in CMnd$
Assertion	omndadd2d	$⊢ φ \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		omndadd2d.c	$⊢ φ \to M \in CMnd$
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 Z \in B \land Y \in B) \to Z \underset{˙}{+} Y \in B$
20	16 8 7 19	syl3anc	$⊢ φ \to Z \underset{˙}{+} Y \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 Z \underset{˙}{+} Y \in B \land Z \underset{˙}{+} W \in B)$
24	1 2 3	omndadd	$⊢ (M \in oMnd \land (X \in B \land Z \in B \land Y \in B) \land X \underset{˙}{\leq} Z) \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} Y)$
25	4 6 8 7 9 24	syl131anc	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} Y)$
26	1 2 3	omndadd	$⊢ (M \in oMnd \land (Y \in B \land W \in B \land Z \in B) \land Y \underset{˙}{\leq} W) \to (Y \underset{˙}{+} Z) \underset{˙}{\leq} (W \underset{˙}{+} Z)$
27	4 7 5 8 10 26	syl131anc	$⊢ φ \to (Y \underset{˙}{+} Z) \underset{˙}{\leq} (W \underset{˙}{+} Z)$
28	1 3	cmncom	$⊢ (M \in CMnd \land Y \in B \land Z \in B) \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
29	11 7 8 28	syl3anc	$⊢ φ \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
30	1 3	cmncom	$⊢ (M \in CMnd \land W \in B \land Z \in B) \to W \underset{˙}{+} Z = Z \underset{˙}{+} W$
31	11 5 8 30	syl3anc	$⊢ φ \to W \underset{˙}{+} Z = Z \underset{˙}{+} W$
32	27 29 31	3brtr3d	$⊢ φ \to (Z \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W)$
33	1 2	postr	$⊢ (M \in Poset \land (X \underset{˙}{+} Y \in B \land Z \underset{˙}{+} Y \in B \land Z \underset{˙}{+} W \in B)) \to (((X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} Y) \land (Z \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W)) \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W))$
34	33	imp	$⊢ ((M \in Poset \land (X \underset{˙}{+} Y \in B \land Z \underset{˙}{+} Y \in B \land Z \underset{˙}{+} W \in B)) \land ((X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} Y) \land (Z \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W))) \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W)$
35	14 23 25 32 34	syl22anc	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\leq} (Z \underset{˙}{+} W)$

Metamath Proof Explorer

Theorem omndadd2d

Proof