Theorem omndmul

Description: In a commutative ordered monoid, the ordering is compatible with group power. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	omndmul.0	$$⊢B={\mathrm{Base}}_M$$
	omndmul.1	$$⊢\underset{\dot{}}{\le }={\le }_M$$
	omndmul.2	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
	omndmul.o	$$⊢\phi \to M\in \mathrm{oMnd}$$
	omndmul.c	$$⊢\phi \to M\in \mathrm{CMnd}$$
	omndmul.x	$$⊢\phi \to X\in B$$
	omndmul.y	$$⊢\phi \to Y\in B$$
	omndmul.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	omndmul.l	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
Assertion	omndmul	$$⊢\phi \to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(N\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		omndmul.0	$$⊢B={\mathrm{Base}}_M$$
2		omndmul.1	$$⊢\underset{\dot{}}{\le }={\le }_M$$
3		omndmul.2	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
4		omndmul.o	$$⊢\phi \to M\in \mathrm{oMnd}$$
5		omndmul.c	$$⊢\phi \to M\in \mathrm{CMnd}$$
6		omndmul.x	$$⊢\phi \to X\in B$$
7		omndmul.y	$$⊢\phi \to Y\in B$$
8		omndmul.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9		omndmul.l	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
10		oveq1	$$⊢m=0\to m\underset{\dot{}}{·}X=0\underset{\dot{}}{·}X$$
11		oveq1	$$⊢m=0\to m\underset{\dot{}}{·}Y=0\underset{\dot{}}{·}Y$$
12	10 11	breq12d	$$⊢m=0\to \left(\left(m\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}Y\right)\leftrightarrow \left(0\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}Y\right)\right)$$
13		oveq1	$$⊢m=n\to m\underset{\dot{}}{·}X=n\underset{\dot{}}{·}X$$
14		oveq1	$$⊢m=n\to m\underset{\dot{}}{·}Y=n\underset{\dot{}}{·}Y$$
15	13 14	breq12d	$$⊢m=n\to \left(\left(m\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}Y\right)\leftrightarrow \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)$$
16		oveq1	$$⊢m=n+1\to m\underset{\dot{}}{·}X=\left(n+1\right)\underset{\dot{}}{·}X$$
17		oveq1	$$⊢m=n+1\to m\underset{\dot{}}{·}Y=\left(n+1\right)\underset{\dot{}}{·}Y$$
18	16 17	breq12d	$$⊢m=n+1\to \left(\left(m\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}Y\right)\leftrightarrow \left(\left(n+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}Y\right)\right)$$
19		oveq1	$$⊢m=N\to m\underset{\dot{}}{·}X=N\underset{\dot{}}{·}X$$
20		oveq1	$$⊢m=N\to m\underset{\dot{}}{·}Y=N\underset{\dot{}}{·}Y$$
21	19 20	breq12d	$$⊢m=N\to \left(\left(m\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}Y\right)\leftrightarrow \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(N\underset{\dot{}}{·}Y\right)\right)$$
22		omndtos	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Toset}$$
23		tospos	$$⊢M\in \mathrm{Toset}\to M\in \mathrm{Poset}$$
24	4 22 23	3syl	$$⊢\phi \to M\in \mathrm{Poset}$$
25		eqid	$$⊢0_M=0_M$$
26	1 25 3	mulg0	$$⊢Y\in B\to 0\underset{\dot{}}{·}Y=0_M$$
27	7 26	syl	$$⊢\phi \to 0\underset{\dot{}}{·}Y=0_M$$
28		omndmnd	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Mnd}$$
29	1 25	mndidcl	$$⊢M\in \mathrm{Mnd}\to 0_M\in B$$
30	4 28 29	3syl	$$⊢\phi \to 0_M\in B$$
31	27 30	eqeltrd	$$⊢\phi \to 0\underset{\dot{}}{·}Y\in B$$
32	1 2	posref	$$⊢\left(M\in \mathrm{Poset}\wedge 0\underset{\dot{}}{·}Y\in B\right)\to \left(0\underset{\dot{}}{·}Y\right)\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}Y\right)$$
33	24 31 32	syl2anc	$$⊢\phi \to \left(0\underset{\dot{}}{·}Y\right)\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}Y\right)$$
34	1 25 3	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{·}X=0_M$$
35	34	adantr	$$⊢\left(X\in B\wedge Y\in B\right)\to 0\underset{\dot{}}{·}X=0_M$$
36	26	adantl	$$⊢\left(X\in B\wedge Y\in B\right)\to 0\underset{\dot{}}{·}Y=0_M$$
37	35 36	eqtr4d	$$⊢\left(X\in B\wedge Y\in B\right)\to 0\underset{\dot{}}{·}X=0\underset{\dot{}}{·}Y$$
38	37	breq1d	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\left(0\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}Y\right)\leftrightarrow \left(0\underset{\dot{}}{·}Y\right)\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}Y\right)\right)$$
39	6 7 38	syl2anc	$$⊢\phi \to \left(\left(0\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}Y\right)\leftrightarrow \left(0\underset{\dot{}}{·}Y\right)\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}Y\right)\right)$$
40	33 39	mpbird	$$⊢\phi \to \left(0\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}Y\right)$$
41		eqid	$$⊢{+}_M={+}_M$$
42	4	ad2antrr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to M\in \mathrm{oMnd}$$
43	7	ad2antrr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to Y\in B$$
44	42 28	syl	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to M\in \mathrm{Mnd}$$
45		simplr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to n\in {\mathbb{N}}_0$$
46	6	ad2antrr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to X\in B$$
47	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$$
48	44 45 46 47	syl3anc	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to n\underset{\dot{}}{·}X\in B$$
49	1 3	mulgnn0cl	$$⊢\left(M\in \mathrm{Mnd}\wedge n\in {\mathbb{N}}_0\wedge Y\in B\right)\to n\underset{\dot{}}{·}Y\in B$$
50	44 45 43 49	syl3anc	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to n\underset{\dot{}}{·}Y\in B$$
51		simpr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)$$
52	9	ad2antrr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to X\underset{\dot{}}{\le }Y$$
53	5	ad2antrr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to M\in \mathrm{CMnd}$$
54	1 2 41 42 43 48 46 50 51 52 53	omndadd2d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to \left(\left(n\underset{\dot{}}{·}X\right){+}_{M}X\right)\underset{\dot{}}{\le }\left(\left(n\underset{\dot{}}{·}Y\right){+}_{M}Y\right)$$
55	1 3 41	mulgnn0p1	$$⊢\left(M\in \mathrm{Mnd}\wedge n\in {\mathbb{N}}_0\wedge X\in B\right)\to \left(n+1\right)\underset{\dot{}}{·}X=\left(n\underset{\dot{}}{·}X\right){+}_{M}X$$
56	44 45 46 55	syl3anc	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to \left(n+1\right)\underset{\dot{}}{·}X=\left(n\underset{\dot{}}{·}X\right){+}_{M}X$$
57	1 3 41	mulgnn0p1	$$⊢\left(M\in \mathrm{Mnd}\wedge n\in {\mathbb{N}}_0\wedge Y\in B\right)\to \left(n+1\right)\underset{\dot{}}{·}Y=\left(n\underset{\dot{}}{·}Y\right){+}_{M}Y$$
58	44 45 43 57	syl3anc	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to \left(n+1\right)\underset{\dot{}}{·}Y=\left(n\underset{\dot{}}{·}Y\right){+}_{M}Y$$
59	54 56 58	3brtr4d	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}Y\right)\right)\to \left(\left(n+1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}Y\right)$$
60	12 15 18 21 40 59	nn0indd	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\right)\to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(N\underset{\dot{}}{·}Y\right)$$
61	8 60	mpdan	$$⊢\phi \to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{\le }\left(N\underset{\dot{}}{·}Y\right)$$