omndmul3

Description: In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018)

	Ref	Expression
Hypotheses	omndmul.0	$⊢ B = {Base}_{M}$
	omndmul.1	$⊢ \underset{˙}{\leq} = \leq_{M}$
	omndmul3.m	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	omndmul3.0	$⊢ \underset{˙}{0} = 0_{M}$
	omndmul3.o	$⊢ φ \to M \in oMnd$
	omndmul3.1	$⊢ φ \to N \in ℕ_{0}$
	omndmul3.2	$⊢ φ \to P \in ℕ_{0}$
	omndmul3.3	$⊢ φ \to N \leq P$
	omndmul3.4	$⊢ φ \to X \in B$
	omndmul3.5	$⊢ φ \to \underset{˙}{0} \underset{˙}{\leq} X$
Assertion	omndmul3	$⊢ φ \to (N \underset{˙}{\cdot} X) \underset{˙}{\leq} (P \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		omndmul.0	$⊢ B = {Base}_{M}$
2		omndmul.1	$⊢ \underset{˙}{\leq} = \leq_{M}$
3		omndmul3.m	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
4		omndmul3.0	$⊢ \underset{˙}{0} = 0_{M}$
5		omndmul3.o	$⊢ φ \to M \in oMnd$
6		omndmul3.1	$⊢ φ \to N \in ℕ_{0}$
7		omndmul3.2	$⊢ φ \to P \in ℕ_{0}$
8		omndmul3.3	$⊢ φ \to N \leq P$
9		omndmul3.4	$⊢ φ \to X \in B$
10		omndmul3.5	$⊢ φ \to \underset{˙}{0} \underset{˙}{\leq} X$
11		omndmnd	$⊢ M \in oMnd \to M \in Mnd$
12	5 11	syl	$⊢ φ \to M \in Mnd$
13	1 4	mndidcl	$⊢ M \in Mnd \to \underset{˙}{0} \in B$
14	12 13	syl	$⊢ φ \to \underset{˙}{0} \in B$
15		nn0sub	$⊢ (N \in ℕ_{0} \land P \in ℕ_{0}) \to (N \leq P \leftrightarrow P - N \in ℕ_{0})$
16	15	biimpa	$⊢ ((N \in ℕ_{0} \land P \in ℕ_{0}) \land N \leq P) \to P - N \in ℕ_{0}$
17	6 7 8 16	syl21anc	$⊢ φ \to P - N \in ℕ_{0}$
18	1 3 12 17 9	mulgnn0cld	$⊢ φ \to (P - N) \underset{˙}{\cdot} X \in B$
19	1 3 12 6 9	mulgnn0cld	$⊢ φ \to N \underset{˙}{\cdot} X \in B$
20	1 2 3 4	omndmul2	$⊢ (M \in oMnd \land (X \in B \land P - N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} ((P - N) \underset{˙}{\cdot} X)$
21	5 9 17 10 20	syl121anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{\leq} ((P - N) \underset{˙}{\cdot} X)$
22		eqid	$⊢ +_{M} = +_{M}$
23	1 2 22	omndadd	$⊢ (M \in oMnd \land (\underset{˙}{0} \in B \land (P - N) \underset{˙}{\cdot} X \in B \land N \underset{˙}{\cdot} X \in B) \land \underset{˙}{0} \underset{˙}{\leq} ((P - N) \underset{˙}{\cdot} X)) \to (\underset{˙}{0} +_{M} (N \underset{˙}{\cdot} X)) \underset{˙}{\leq} (((P - N) \underset{˙}{\cdot} X) +_{M} (N \underset{˙}{\cdot} X))$
24	5 14 18 19 21 23	syl131anc	$⊢ φ \to (\underset{˙}{0} +_{M} (N \underset{˙}{\cdot} X)) \underset{˙}{\leq} (((P - N) \underset{˙}{\cdot} X) +_{M} (N \underset{˙}{\cdot} X))$
25	1 22 4	mndlid	$⊢ (M \in Mnd \land N \underset{˙}{\cdot} X \in B) \to \underset{˙}{0} +_{M} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
26	12 19 25	syl2anc	$⊢ φ \to \underset{˙}{0} +_{M} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
27	1 3 22	mulgnn0dir	$⊢ (M \in Mnd \land (P - N \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (P - N + N) \underset{˙}{\cdot} X = ((P - N) \underset{˙}{\cdot} X) +_{M} (N \underset{˙}{\cdot} X)$
28	12 17 6 9 27	syl13anc	$⊢ φ \to (P - N + N) \underset{˙}{\cdot} X = ((P - N) \underset{˙}{\cdot} X) +_{M} (N \underset{˙}{\cdot} X)$
29	7	nn0cnd	$⊢ φ \to P \in ℂ$
30	6	nn0cnd	$⊢ φ \to N \in ℂ$
31	29 30	npcand	$⊢ φ \to P - N + N = P$
32	31	oveq1d	$⊢ φ \to (P - N + N) \underset{˙}{\cdot} X = P \underset{˙}{\cdot} X$
33	28 32	eqtr3d	$⊢ φ \to ((P - N) \underset{˙}{\cdot} X) +_{M} (N \underset{˙}{\cdot} X) = P \underset{˙}{\cdot} X$
34	24 26 33	3brtr3d	$⊢ φ \to (N \underset{˙}{\cdot} X) \underset{˙}{\leq} (P \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem omndmul3

Proof