Step |
Hyp |
Ref |
Expression |
1 |
|
odcl.1 |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
odcl.2 |
⊢ 𝑂 = ( od ‘ 𝐺 ) |
3 |
|
odid.3 |
⊢ · = ( .g ‘ 𝐺 ) |
4 |
|
odid.4 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
5 |
1 2 3 4
|
mndodcong |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) |
6 |
5
|
biimpd |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) |
7 |
6
|
3expia |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) ) |
8 |
7
|
3impa |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) ) |
9 |
|
nn0z |
⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ ) |
10 |
|
nn0z |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ ) |
11 |
|
zsubcl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ ) |
12 |
9 10 11
|
syl2an |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 − 𝑁 ) ∈ ℤ ) |
13 |
12
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑀 − 𝑁 ) ∈ ℤ ) |
14 |
|
0dvds |
⊢ ( ( 𝑀 − 𝑁 ) ∈ ℤ → ( 0 ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 − 𝑁 ) = 0 ) ) |
15 |
13 14
|
syl |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 − 𝑁 ) = 0 ) ) |
16 |
|
nn0cn |
⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ ) |
17 |
|
nn0cn |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ ) |
18 |
|
subeq0 |
⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 − 𝑁 ) = 0 ↔ 𝑀 = 𝑁 ) ) |
19 |
16 17 18
|
syl2an |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 − 𝑁 ) = 0 ↔ 𝑀 = 𝑁 ) ) |
20 |
19
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 − 𝑁 ) = 0 ↔ 𝑀 = 𝑁 ) ) |
21 |
|
oveq1 |
⊢ ( 𝑀 = 𝑁 → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) |
22 |
20 21
|
syl6bi |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 − 𝑁 ) = 0 → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) |
23 |
15 22
|
sylbid |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 ∥ ( 𝑀 − 𝑁 ) → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) |
24 |
|
breq1 |
⊢ ( ( 𝑂 ‘ 𝐴 ) = 0 → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ 0 ∥ ( 𝑀 − 𝑁 ) ) ) |
25 |
24
|
imbi1d |
⊢ ( ( 𝑂 ‘ 𝐴 ) = 0 → ( ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ↔ ( 0 ∥ ( 𝑀 − 𝑁 ) → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) ) |
26 |
23 25
|
syl5ibrcom |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) ) |
27 |
1 2
|
odcl |
⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ) |
28 |
27
|
3ad2ant2 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ) |
29 |
|
elnn0 |
⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) ) |
30 |
28 29
|
sylib |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) ) |
31 |
8 26 30
|
mpjaod |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) → ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) ) |