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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	omndmul.1	⊢ ≤ = ( le ‘ 𝑀 )
	omndmul3.m	⊢ · = ( .g ‘ 𝑀 )
	omndmul3.0	⊢ 0 = ( 0g ‘ 𝑀 )
	omndmul3.o	⊢ ( 𝜑 → 𝑀 ∈ oMnd )
	omndmul3.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	omndmul3.2	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
	omndmul3.3	⊢ ( 𝜑 → 𝑁 ≤ 𝑃 )
	omndmul3.4	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	omndmul3.5	⊢ ( 𝜑 → 0 ≤ 𝑋 )
Assertion	omndmul3	⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ≤ ( 𝑃 · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		omndmul.0	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		omndmul.1	⊢ ≤ = ( le ‘ 𝑀 )
3		omndmul3.m	⊢ · = ( .g ‘ 𝑀 )
4		omndmul3.0	⊢ 0 = ( 0g ‘ 𝑀 )
5		omndmul3.o	⊢ ( 𝜑 → 𝑀 ∈ oMnd )
6		omndmul3.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7		omndmul3.2	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
8		omndmul3.3	⊢ ( 𝜑 → 𝑁 ≤ 𝑃 )
9		omndmul3.4	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
10		omndmul3.5	⊢ ( 𝜑 → 0 ≤ 𝑋 )
11		omndmnd	⊢ ( 𝑀 ∈ oMnd → 𝑀 ∈ Mnd )
12	5 11	syl	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
13	1 4	mndidcl	⊢ ( 𝑀 ∈ Mnd → 0 ∈ 𝐵 )
14	12 13	syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
15		nn0sub	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑃 ↔ ( 𝑃 − 𝑁 ) ∈ ℕ0 ) )
16	15	biimpa	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑃 ) → ( 𝑃 − 𝑁 ) ∈ ℕ0 )
17	6 7 8 16	syl21anc	⊢ ( 𝜑 → ( 𝑃 − 𝑁 ) ∈ ℕ0 )
18	1 3	mulgnn0cl	⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑃 − 𝑁 ) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑃 − 𝑁 ) · 𝑋 ) ∈ 𝐵 )
19	12 17 9 18	syl3anc	⊢ ( 𝜑 → ( ( 𝑃 − 𝑁 ) · 𝑋 ) ∈ 𝐵 )
20	1 3	mulgnn0cl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
21	12 6 9 20	syl3anc	⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
22	1 2 3 4	omndmul2	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑃 − 𝑁 ) ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ ( ( 𝑃 − 𝑁 ) · 𝑋 ) )
23	5 9 17 10 22	syl121anc	⊢ ( 𝜑 → 0 ≤ ( ( 𝑃 − 𝑁 ) · 𝑋 ) )
24		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
25	1 2 24	omndadd	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ ( ( 𝑃 − 𝑁 ) · 𝑋 ) ∈ 𝐵 ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) ∧ 0 ≤ ( ( 𝑃 − 𝑁 ) · 𝑋 ) ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) ≤ ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) )
26	5 14 19 21 23 25	syl131anc	⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) ≤ ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) )
27	1 24 4	mndlid	⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
28	12 21 27	syl2anc	⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
29	1 3 24	mulgnn0dir	⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝑃 − 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑃 − 𝑁 ) + 𝑁 ) · 𝑋 ) = ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) )
30	12 17 6 9 29	syl13anc	⊢ ( 𝜑 → ( ( ( 𝑃 − 𝑁 ) + 𝑁 ) · 𝑋 ) = ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) )
31	7	nn0cnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
32	6	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
33	31 32	npcand	⊢ ( 𝜑 → ( ( 𝑃 − 𝑁 ) + 𝑁 ) = 𝑃 )
34	33	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑃 − 𝑁 ) + 𝑁 ) · 𝑋 ) = ( 𝑃 · 𝑋 ) )
35	30 34	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) = ( 𝑃 · 𝑋 ) )
36	26 28 35	3brtr3d	⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ≤ ( 𝑃 · 𝑋 ) )