Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
omndmul.1 ⊢ ≤ = ( le ‘ 𝑀 )
omndmul.2 ⊢ · = ( .g ‘ 𝑀 )
omndmul.o ⊢ ( 𝜑 → 𝑀 ∈ oMnd )
omndmul.c ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
omndmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
omndmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
omndmul.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
omndmul.l ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
Assertion omndmul ( 𝜑 → ( 𝑁 · 𝑋 ) ≤ ( 𝑁 · 𝑌 ) )

Proof

Step Hyp Ref Expression
1 omndmul.0 ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 omndmul.1 ⊢ ≤ = ( le ‘ 𝑀 )
3 omndmul.2 ⊢ · = ( .g ‘ 𝑀 )
4 omndmul.o ⊢ ( 𝜑 → 𝑀 ∈ oMnd )
5 omndmul.c ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
6 omndmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 omndmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 omndmul.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 omndmul.l ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
10 oveq1 ⊢ ( 𝑚 = 0 → ( 𝑚 · 𝑋 ) = ( 0 · 𝑋 ) )
11 oveq1 ⊢ ( 𝑚 = 0 → ( 𝑚 · 𝑌 ) = ( 0 · 𝑌 ) )
12 10 11 breq12d ⊢ ( 𝑚 = 0 → ( ( 𝑚 · 𝑋 ) ≤ ( 𝑚 · 𝑌 ) ↔ ( 0 · 𝑋 ) ≤ ( 0 · 𝑌 ) ) )
13 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 · 𝑋 ) = ( 𝑛 · 𝑋 ) )
14 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 · 𝑌 ) = ( 𝑛 · 𝑌 ) )
15 13 14 breq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 · 𝑋 ) ≤ ( 𝑚 · 𝑌 ) ↔ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) )
16 oveq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 · 𝑋 ) = ( ( 𝑛 + 1 ) · 𝑋 ) )
17 oveq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 · 𝑌 ) = ( ( 𝑛 + 1 ) · 𝑌 ) )
18 16 17 breq12d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑚 · 𝑋 ) ≤ ( 𝑚 · 𝑌 ) ↔ ( ( 𝑛 + 1 ) · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑌 ) ) )
19 oveq1 ⊢ ( 𝑚 = 𝑁 → ( 𝑚 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
20 oveq1 ⊢ ( 𝑚 = 𝑁 → ( 𝑚 · 𝑌 ) = ( 𝑁 · 𝑌 ) )
21 19 20 breq12d ⊢ ( 𝑚 = 𝑁 → ( ( 𝑚 · 𝑋 ) ≤ ( 𝑚 · 𝑌 ) ↔ ( 𝑁 · 𝑋 ) ≤ ( 𝑁 · 𝑌 ) ) )
22 omndtos ⊢ ( 𝑀 ∈ oMnd → 𝑀 ∈ Toset )
23 tospos ⊢ ( 𝑀 ∈ Toset → 𝑀 ∈ Poset )
24 4 22 23 3syl ⊢ ( 𝜑 → 𝑀 ∈ Poset )
25 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
26 1 25 3 mulg0 ⊢ ( 𝑌 ∈ 𝐵 → ( 0 · 𝑌 ) = ( 0g ‘ 𝑀 ) )
27 7 26 syl ⊢ ( 𝜑 → ( 0 · 𝑌 ) = ( 0g ‘ 𝑀 ) )
28 omndmnd ⊢ ( 𝑀 ∈ oMnd → 𝑀 ∈ Mnd )
29 1 25 mndidcl ⊢ ( 𝑀 ∈ Mnd → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
30 4 28 29 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
31 27 30 eqeltrd ⊢ ( 𝜑 → ( 0 · 𝑌 ) ∈ 𝐵 )
32 1 2 posref ⊢ ( ( 𝑀 ∈ Poset ∧ ( 0 · 𝑌 ) ∈ 𝐵 ) → ( 0 · 𝑌 ) ≤ ( 0 · 𝑌 ) )
33 24 31 32 syl2anc ⊢ ( 𝜑 → ( 0 · 𝑌 ) ≤ ( 0 · 𝑌 ) )
34 1 25 3 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝑀 ) )
35 34 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝑀 ) )
36 26 adantl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 0 · 𝑌 ) = ( 0g ‘ 𝑀 ) )
37 35 36 eqtr4d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( 0 · 𝑌 ) )
38 37 breq1d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 0 · 𝑋 ) ≤ ( 0 · 𝑌 ) ↔ ( 0 · 𝑌 ) ≤ ( 0 · 𝑌 ) ) )
39 6 7 38 syl2anc ⊢ ( 𝜑 → ( ( 0 · 𝑋 ) ≤ ( 0 · 𝑌 ) ↔ ( 0 · 𝑌 ) ≤ ( 0 · 𝑌 ) ) )
40 33 39 mpbird ⊢ ( 𝜑 → ( 0 · 𝑋 ) ≤ ( 0 · 𝑌 ) )
41 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
42 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → 𝑀 ∈ oMnd )
43 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → 𝑌 ∈ 𝐵 )
44 42 28 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → 𝑀 ∈ Mnd )
45 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → 𝑛 ∈ ℕ0 )
46 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → 𝑋 ∈ 𝐵 )
47 1 3 mulgnn0cl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
48 44 45 46 47 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
49 1 3 mulgnn0cl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑛 · 𝑌 ) ∈ 𝐵 )
50 44 45 43 49 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → ( 𝑛 · 𝑌 ) ∈ 𝐵 )
51 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) )
52 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → 𝑋 ≤ 𝑌 )
53 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → 𝑀 ∈ CMnd )
54 1 2 41 42 43 48 46 50 51 52 53 omndadd2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → ( ( 𝑛 · 𝑋 ) ( +g ‘ 𝑀 ) 𝑋 ) ≤ ( ( 𝑛 · 𝑌 ) ( +g ‘ 𝑀 ) 𝑌 ) )
55 1 3 41 mulgnn0p1 ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑛 + 1 ) · 𝑋 ) = ( ( 𝑛 · 𝑋 ) ( +g ‘ 𝑀 ) 𝑋 ) )
56 44 45 46 55 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → ( ( 𝑛 + 1 ) · 𝑋 ) = ( ( 𝑛 · 𝑋 ) ( +g ‘ 𝑀 ) 𝑋 ) )
57 1 3 41 mulgnn0p1 ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑛 + 1 ) · 𝑌 ) = ( ( 𝑛 · 𝑌 ) ( +g ‘ 𝑀 ) 𝑌 ) )
58 44 45 43 57 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → ( ( 𝑛 + 1 ) · 𝑌 ) = ( ( 𝑛 · 𝑌 ) ( +g ‘ 𝑀 ) 𝑌 ) )
59 54 56 58 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( 𝑛 · 𝑌 ) ) → ( ( 𝑛 + 1 ) · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑌 ) )
60 12 15 18 21 40 59 nn0indd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 𝑋 ) ≤ ( 𝑁 · 𝑌 ) )
61 8 60 mpdan ⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ≤ ( 𝑁 · 𝑌 ) )