Theorem 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={\mathrm{Base}}_M$$
	omndmul.1	$$⊢\underset{\dot{}}{\le }={\le }_M$$
	omndmul3.m	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
	omndmul3.0	$$⊢\underset{\dot{}}{0}=0_M$$
	omndmul3.o	$$⊢\phi \to M\in \mathrm{oMnd}$$
	omndmul3.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	omndmul3.2	$$⊢\phi \to P\in {\mathbb{N}}_0$$
	omndmul3.3	$$⊢\phi \to N\le P$$
	omndmul3.4	$$⊢\phi \to X\in B$$
	omndmul3.5	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }X$$
Assertion	omndmul3	$$⊢\phi \to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{·}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		omndmul.0	$$⊢B={\mathrm{Base}}_M$$
2		omndmul.1	$$⊢\underset{\dot{}}{\le }={\le }_M$$
3		omndmul3.m	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
4		omndmul3.0	$$⊢\underset{\dot{}}{0}=0_M$$
5		omndmul3.o	$$⊢\phi \to M\in \mathrm{oMnd}$$
6		omndmul3.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		omndmul3.2	$$⊢\phi \to P\in {\mathbb{N}}_0$$
8		omndmul3.3	$$⊢\phi \to N\le P$$
9		omndmul3.4	$$⊢\phi \to X\in B$$
10		omndmul3.5	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }X$$
11		omndmnd	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Mnd}$$
12	5 11	syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
13	1 4	mndidcl	$$⊢M\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
14	12 13	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
15		nn0sub	$$⊢\left(N\in {\mathbb{N}}_0\wedge P\in {\mathbb{N}}_0\right)\to \left(N\le P\leftrightarrow P-N\in {\mathbb{N}}_0\right)$$
16	15	biimpa	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge P\in {\mathbb{N}}_0\right)\wedge N\le P\right)\to P-N\in {\mathbb{N}}_0$$
17	6 7 8 16	syl21anc	$$⊢\phi \to P-N\in {\mathbb{N}}_0$$
18	1 3	mulgnn0cl	$$⊢\left(M\in \mathrm{Mnd}\wedge P-N\in {\mathbb{N}}_0\wedge X\in B\right)\to \left(P-N\right)\underset{\dot{}}{·}X\in B$$
19	12 17 9 18	syl3anc	$$⊢\phi \to \left(P-N\right)\underset{\dot{}}{·}X\in B$$
20	1 3	mulgnn0cl	$$⊢\left(M\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge X\in B\right)\to N\underset{\dot{}}{·}X\in B$$
21	12 6 9 20	syl3anc	$$⊢\phi \to N\underset{\dot{}}{·}X\in B$$
22	1 2 3 4	omndmul2	$$⊢\left(M\in \mathrm{oMnd}\wedge \left(X\in B\wedge P-N\in {\mathbb{N}}_0\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(\left(P-N\right)\underset{\dot{}}{·}X\right)$$
23	5 9 17 10 22	syl121anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(\left(P-N\right)\underset{\dot{}}{·}X\right)$$
24		eqid	$$⊢{+}_M={+}_M$$
25	1 2 24	omndadd	$$⊢\left(M\in \mathrm{oMnd}\wedge \left(\underset{\dot{}}{0}\in B\wedge \left(P-N\right)\underset{\dot{}}{·}X\in B\wedge N\underset{\dot{}}{·}X\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(\left(P-N\right)\underset{\dot{}}{·}X\right)\right)\to \left(\underset{\dot{}}{0}{+}_M\left(N\underset{\dot{}}{·}X\right)\right)\underset{\dot{}}{\le }\left(\left(\left(P-N\right)\underset{\dot{}}{·}X\right){+}_M\left(N\underset{\dot{}}{·}X\right)\right)$$
26	5 14 19 21 23 25	syl131anc	$$⊢\phi \to \left(\underset{\dot{}}{0}{+}_M\left(N\underset{\dot{}}{·}X\right)\right)\underset{\dot{}}{\le }\left(\left(\left(P-N\right)\underset{\dot{}}{·}X\right){+}_M\left(N\underset{\dot{}}{·}X\right)\right)$$
27	1 24 4	mndlid	$$⊢\left(M\in \mathrm{Mnd}\wedge N\underset{\dot{}}{·}X\in B\right)\to \underset{\dot{}}{0}{+}_M\left(N\underset{\dot{}}{·}X\right)=N\underset{\dot{}}{·}X$$
28	12 21 27	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}{+}_M\left(N\underset{\dot{}}{·}X\right)=N\underset{\dot{}}{·}X$$
29	1 3 24	mulgnn0dir	$$⊢\left(M\in \mathrm{Mnd}\wedge \left(P-N\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\wedge X\in B\right)\right)\to \left(P-N+N\right)\underset{\dot{}}{·}X=\left(\left(P-N\right)\underset{\dot{}}{·}X\right){+}_M\left(N\underset{\dot{}}{·}X\right)$$
30	12 17 6 9 29	syl13anc	$$⊢\phi \to \left(P-N+N\right)\underset{\dot{}}{·}X=\left(\left(P-N\right)\underset{\dot{}}{·}X\right){+}_M\left(N\underset{\dot{}}{·}X\right)$$
31	7	nn0cnd	$$⊢\phi \to P\in ℂ$$
32	6	nn0cnd	$$⊢\phi \to N\in ℂ$$
33	31 32	npcand	$$⊢\phi \to P-N+N=P$$
34	33	oveq1d	$$⊢\phi \to \left(P-N+N\right)\underset{\dot{}}{·}X=P\underset{\dot{}}{·}X$$
35	30 34	eqtr3d	$$⊢\phi \to \left(\left(P-N\right)\underset{\dot{}}{·}X\right){+}_M\left(N\underset{\dot{}}{·}X\right)=P\underset{\dot{}}{·}X$$
36	26 28 35	3brtr3d	$$⊢\phi \to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{·}X\right)$$