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 12 17 9	mulgnn0cld	$$⊢\phi \to \left(P-N\right)\underset{\dot{}}{·}X\in B$$
19	1 3 12 6 9	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{·}X\in B$$
20	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)$$
21	5 9 17 10 20	syl121anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(\left(P-N\right)\underset{\dot{}}{·}X\right)$$
22		eqid	$$⊢{+}_M={+}_M$$
23	1 2 22	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)$$
24	5 14 18 19 21 23	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)$$
25	1 22 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$$
26	12 19 25	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}{+}_M\left(N\underset{\dot{}}{·}X\right)=N\underset{\dot{}}{·}X$$
27	1 3 22	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)$$
28	12 17 6 9 27	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)$$
29	7	nn0cnd	$$⊢\phi \to P\in ℂ$$
30	6	nn0cnd	$$⊢\phi \to N\in ℂ$$
31	29 30	npcand	$$⊢\phi \to P-N+N=P$$
32	31	oveq1d	$$⊢\phi \to \left(P-N+N\right)\underset{\dot{}}{·}X=P\underset{\dot{}}{·}X$$
33	28 32	eqtr3d	$$⊢\phi \to \left(\left(P-N\right)\underset{\dot{}}{·}X\right){+}_M\left(N\underset{\dot{}}{·}X\right)=P\underset{\dot{}}{·}X$$
34	24 26 33	3brtr3d	$$⊢\phi \to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{·}X\right)$$