Metamath Proof Explorer

Theorem mndodconglem

Description: Lemma for mndodcong . (Contributed by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odid.3 ⊢ · = ( .g ‘ 𝐺 )
odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
mndodconglem.1 ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
mndodconglem.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
mndodconglem.3 ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
mndodconglem.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
mndodconglem.5 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
mndodconglem.6 ⊢ ( 𝜑 → 𝑀 < ( 𝑂 ‘ 𝐴 ) )
mndodconglem.7 ⊢ ( 𝜑 → 𝑁 < ( 𝑂 ‘ 𝐴 ) )
mndodconglem.8 ⊢ ( 𝜑 → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) )
Assertion mndodconglem ( ( 𝜑 ∧ 𝑀 ≤ 𝑁 ) → 𝑀 = 𝑁 )

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 mndodconglem.1 ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6 mndodconglem.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
7 mndodconglem.3 ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
8 mndodconglem.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
9 mndodconglem.5 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
10 mndodconglem.6 ⊢ ( 𝜑 → 𝑀 < ( 𝑂 ‘ 𝐴 ) )
11 mndodconglem.7 ⊢ ( 𝜑 → 𝑁 < ( 𝑂 ‘ 𝐴 ) )
12 mndodconglem.8 ⊢ ( 𝜑 → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) )
13 7 nnred ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
14 13 recnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℂ )
15 8 nn0red ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
16 15 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
17 9 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
18 17 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
19 14 16 18 addsubassd ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) − 𝑁 ) = ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) )
20 7 nnzd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
21 8 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
22 20 21 zaddcld ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) ∈ ℤ )
23 22 zred ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) ∈ ℝ )
24 nn0addge1 ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑂 ‘ 𝐴 ) ≤ ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) )
25 13 8 24 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ≤ ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) )
26 17 13 23 11 25 ltletrd ⊢ ( 𝜑 → 𝑁 < ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) )
27 9 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
28 znnsub ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) ∈ ℤ ) → ( 𝑁 < ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) ↔ ( ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) − 𝑁 ) ∈ ℕ ) )
29 27 22 28 syl2anc ⊢ ( 𝜑 → ( 𝑁 < ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) ↔ ( ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) − 𝑁 ) ∈ ℕ ) )
30 26 29 mpbid ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) + 𝑀 ) − 𝑁 ) ∈ ℕ )
31 19 30 eqeltrrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) ∈ ℕ )
32 14 16 18 addsub12d ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) = ( 𝑀 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) )
33 32 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) · 𝐴 ) = ( ( 𝑀 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) )
34 12 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) · 𝐴 ) ) = ( ( 𝑁 · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) · 𝐴 ) ) )
35 znnsub ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ) → ( 𝑁 < ( 𝑂 ‘ 𝐴 ) ↔ ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ∈ ℕ ) )
36 27 20 35 syl2anc ⊢ ( 𝜑 → ( 𝑁 < ( 𝑂 ‘ 𝐴 ) ↔ ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ∈ ℕ ) )
37 11 36 mpbid ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ∈ ℕ )
38 37 nnnn0d ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ∈ ℕ0 )
39 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
40 1 3 39 mulgnn0dir ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑀 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) = ( ( 𝑀 · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) · 𝐴 ) ) )
41 5 8 38 6 40 syl13anc ⊢ ( 𝜑 → ( ( 𝑀 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) = ( ( 𝑀 · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) · 𝐴 ) ) )
42 1 3 39 mulgnn0dir ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑁 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) = ( ( 𝑁 · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) · 𝐴 ) ) )
43 5 9 38 6 42 syl13anc ⊢ ( 𝜑 → ( ( 𝑁 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) = ( ( 𝑁 · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) · 𝐴 ) ) )
44 34 41 43 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑀 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) = ( ( 𝑁 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) )
45 18 14 pncan3d ⊢ ( 𝜑 → ( 𝑁 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) = ( 𝑂 ‘ 𝐴 ) )
46 45 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) = ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) )
47 1 2 3 4 odid ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
48 6 47 syl ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
49 46 48 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) = 0 )
50 44 49 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 + ( ( 𝑂 ‘ 𝐴 ) − 𝑁 ) ) · 𝐴 ) = 0 )
51 33 50 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) · 𝐴 ) = 0 )
52 1 2 3 4 odlem2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) ∈ ℕ ∧ ( ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) · 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) ) )
53 6 31 51 52 syl3anc ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) ) )
54 elfzle2 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) ) → ( 𝑂 ‘ 𝐴 ) ≤ ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) )
55 53 54 syl ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ≤ ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) )
56 21 27 zsubcld ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℤ )
57 56 zred ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℝ )
58 13 57 addge01d ⊢ ( 𝜑 → ( 0 ≤ ( 𝑀 − 𝑁 ) ↔ ( 𝑂 ‘ 𝐴 ) ≤ ( ( 𝑂 ‘ 𝐴 ) + ( 𝑀 − 𝑁 ) ) ) )
59 55 58 mpbird ⊢ ( 𝜑 → 0 ≤ ( 𝑀 − 𝑁 ) )
60 15 17 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 𝑀 − 𝑁 ) ↔ 𝑁 ≤ 𝑀 ) )
61 59 60 mpbid ⊢ ( 𝜑 → 𝑁 ≤ 𝑀 )
62 15 17 letri3d ⊢ ( 𝜑 → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
63 62 biimprd ⊢ ( 𝜑 → ( ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) → 𝑀 = 𝑁 ) )
64 61 63 mpan2d ⊢ ( 𝜑 → ( 𝑀 ≤ 𝑁 → 𝑀 = 𝑁 ) )
65 64 imp ⊢ ( ( 𝜑 ∧ 𝑀 ≤ 𝑁 ) → 𝑀 = 𝑁 )