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 12 17 9	mulgnn0cld	⊢ ( 𝜑 → ( ( 𝑃 − 𝑁 ) · 𝑋 ) ∈ 𝐵 )
19	1 3 12 6 9	mulgnn0cld	⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
20	1 2 3 4	omndmul2	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑃 − 𝑁 ) ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ ( ( 𝑃 − 𝑁 ) · 𝑋 ) )
21	5 9 17 10 20	syl121anc	⊢ ( 𝜑 → 0 ≤ ( ( 𝑃 − 𝑁 ) · 𝑋 ) )
22		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
23	1 2 22	omndadd	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ ( ( 𝑃 − 𝑁 ) · 𝑋 ) ∈ 𝐵 ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) ∧ 0 ≤ ( ( 𝑃 − 𝑁 ) · 𝑋 ) ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) ≤ ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) )
24	5 14 18 19 21 23	syl131anc	⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) ≤ ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) )
25	1 22 4	mndlid	⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
26	12 19 25	syl2anc	⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
27	1 3 22	mulgnn0dir	⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝑃 − 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑃 − 𝑁 ) + 𝑁 ) · 𝑋 ) = ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) )
28	12 17 6 9 27	syl13anc	⊢ ( 𝜑 → ( ( ( 𝑃 − 𝑁 ) + 𝑁 ) · 𝑋 ) = ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) )
29	7	nn0cnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
30	6	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
31	29 30	npcand	⊢ ( 𝜑 → ( ( 𝑃 − 𝑁 ) + 𝑁 ) = 𝑃 )
32	31	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑃 − 𝑁 ) + 𝑁 ) · 𝑋 ) = ( 𝑃 · 𝑋 ) )
33	28 32	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝑃 − 𝑁 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑁 · 𝑋 ) ) = ( 𝑃 · 𝑋 ) )
34	24 26 33	3brtr3d	⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ≤ ( 𝑃 · 𝑋 ) )