This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ≤ ( 𝑃 · 𝑋 ) )