Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (0...((𝑂‘𝐴) − 1)) ∈ Fin) |
2 | | odf1.1 |
. . . . . . . . . . . . 13
⊢ 𝑋 = (Base‘𝐺) |
3 | | odf1.3 |
. . . . . . . . . . . . 13
⊢ · =
(.g‘𝐺) |
4 | 2, 3 | mulgcl 17382 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ 𝑋) → (𝑥 · 𝐴) ∈ 𝑋) |
5 | 4 | 3expa 1257 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ) ∧ 𝐴 ∈ 𝑋) → (𝑥 · 𝐴) ∈ 𝑋) |
6 | 5 | an32s 842 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝐴) ∈ 𝑋) |
7 | 6 | adantlr 747 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝐴) ∈ 𝑋) |
8 | | odf1.4 |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) |
9 | 7, 8 | fmptd 6292 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → 𝐹:ℤ⟶𝑋) |
10 | | frn 5966 |
. . . . . . . 8
⊢ (𝐹:ℤ⟶𝑋 → ran 𝐹 ⊆ 𝑋) |
11 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝐺)
∈ V |
12 | 2, 11 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝑋 ∈ V |
13 | 12 | ssex 4730 |
. . . . . . . 8
⊢ (ran
𝐹 ⊆ 𝑋 → ran 𝐹 ∈ V) |
14 | 9, 10, 13 | 3syl 18 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → ran 𝐹 ∈ V) |
15 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0...((𝑂‘𝐴) − 1)) → 𝑦 ∈ ℤ) |
16 | 15 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → 𝑦 ∈ ℤ) |
17 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑦 · 𝐴) ∈ V |
18 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐴) = (𝑦 · 𝐴)) |
19 | 8, 18 | elrnmpt1s 5294 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℤ ∧ (𝑦 · 𝐴) ∈ V) → (𝑦 · 𝐴) ∈ ran 𝐹) |
20 | 16, 17, 19 | sylancl 693 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → (𝑦 · 𝐴) ∈ ran 𝐹) |
21 | 20 | ralrimiva 2949 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → ∀𝑦 ∈ (0...((𝑂‘𝐴) − 1))(𝑦 · 𝐴) ∈ ran 𝐹) |
22 | | zmodfz 12554 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑥 mod (𝑂‘𝐴)) ∈ (0...((𝑂‘𝐴) − 1))) |
23 | 22 | ancoms 468 |
. . . . . . . . . . . 12
⊢ (((𝑂‘𝐴) ∈ ℕ ∧ 𝑥 ∈ ℤ) → (𝑥 mod (𝑂‘𝐴)) ∈ (0...((𝑂‘𝐴) − 1))) |
24 | 23 | adantll 746 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 mod (𝑂‘𝐴)) ∈ (0...((𝑂‘𝐴) − 1))) |
25 | | simpllr 795 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → (𝑂‘𝐴) ∈ ℕ) |
26 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → 𝑥 ∈ ℤ) |
27 | 15 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → 𝑦 ∈ ℤ) |
28 | | moddvds 14829 |
. . . . . . . . . . . . . 14
⊢ (((𝑂‘𝐴) ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 mod (𝑂‘𝐴)) = (𝑦 mod (𝑂‘𝐴)) ↔ (𝑂‘𝐴) ∥ (𝑥 − 𝑦))) |
29 | 25, 26, 27, 28 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → ((𝑥 mod (𝑂‘𝐴)) = (𝑦 mod (𝑂‘𝐴)) ↔ (𝑂‘𝐴) ∥ (𝑥 − 𝑦))) |
30 | 27 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → 𝑦 ∈ ℝ) |
31 | 25 | nnrpd 11746 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → (𝑂‘𝐴) ∈
ℝ+) |
32 | | 0z 11265 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℤ |
33 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑂‘𝐴) ∈ ℕ → (𝑂‘𝐴) ∈ ℤ) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑂‘𝐴) ∈ ℤ) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑂‘𝐴) ∈ ℤ) |
36 | | elfzm11 12280 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℤ ∧ (𝑂‘𝐴) ∈ ℤ) → (𝑦 ∈ (0...((𝑂‘𝐴) − 1)) ↔ (𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < (𝑂‘𝐴)))) |
37 | 32, 35, 36 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑦 ∈ (0...((𝑂‘𝐴) − 1)) ↔ (𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < (𝑂‘𝐴)))) |
38 | 37 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → (𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < (𝑂‘𝐴))) |
39 | 38 | simp2d 1067 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → 0 ≤ 𝑦) |
40 | 38 | simp3d 1068 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → 𝑦 < (𝑂‘𝐴)) |
41 | | modid 12557 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℝ ∧ (𝑂‘𝐴) ∈ ℝ+) ∧ (0 ≤
𝑦 ∧ 𝑦 < (𝑂‘𝐴))) → (𝑦 mod (𝑂‘𝐴)) = 𝑦) |
42 | 30, 31, 39, 40, 41 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → (𝑦 mod (𝑂‘𝐴)) = 𝑦) |
43 | 42 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → ((𝑥 mod (𝑂‘𝐴)) = (𝑦 mod (𝑂‘𝐴)) ↔ (𝑥 mod (𝑂‘𝐴)) = 𝑦)) |
44 | | eqcom 2617 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 mod (𝑂‘𝐴)) = 𝑦 ↔ 𝑦 = (𝑥 mod (𝑂‘𝐴))) |
45 | 43, 44 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → ((𝑥 mod (𝑂‘𝐴)) = (𝑦 mod (𝑂‘𝐴)) ↔ 𝑦 = (𝑥 mod (𝑂‘𝐴)))) |
46 | | simp-4l 802 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → 𝐺 ∈ Grp) |
47 | | simp-4r 803 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → 𝐴 ∈ 𝑋) |
48 | | odf1.2 |
. . . . . . . . . . . . . . 15
⊢ 𝑂 = (od‘𝐺) |
49 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) |
50 | 2, 48, 3, 49 | odcong 17791 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑥 − 𝑦) ↔ (𝑥 · 𝐴) = (𝑦 · 𝐴))) |
51 | 46, 47, 26, 27, 50 | syl112anc 1322 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → ((𝑂‘𝐴) ∥ (𝑥 − 𝑦) ↔ (𝑥 · 𝐴) = (𝑦 · 𝐴))) |
52 | 29, 45, 51 | 3bitr3rd 298 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...((𝑂‘𝐴) − 1))) → ((𝑥 · 𝐴) = (𝑦 · 𝐴) ↔ 𝑦 = (𝑥 mod (𝑂‘𝐴)))) |
53 | 52 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ∀𝑦 ∈ (0...((𝑂‘𝐴) − 1))((𝑥 · 𝐴) = (𝑦 · 𝐴) ↔ 𝑦 = (𝑥 mod (𝑂‘𝐴)))) |
54 | | reu6i 3364 |
. . . . . . . . . . 11
⊢ (((𝑥 mod (𝑂‘𝐴)) ∈ (0...((𝑂‘𝐴) − 1)) ∧ ∀𝑦 ∈ (0...((𝑂‘𝐴) − 1))((𝑥 · 𝐴) = (𝑦 · 𝐴) ↔ 𝑦 = (𝑥 mod (𝑂‘𝐴)))) → ∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))(𝑥 · 𝐴) = (𝑦 · 𝐴)) |
55 | 24, 53, 54 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))(𝑥 · 𝐴) = (𝑦 · 𝐴)) |
56 | 55 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → ∀𝑥 ∈ ℤ ∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))(𝑥 · 𝐴) = (𝑦 · 𝐴)) |
57 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑥 · 𝐴) ∈ V |
58 | 57 | rgenw 2908 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
ℤ (𝑥 · 𝐴) ∈ V |
59 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 · 𝐴) → (𝑧 = (𝑦 · 𝐴) ↔ (𝑥 · 𝐴) = (𝑦 · 𝐴))) |
60 | 59 | reubidv 3103 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑥 · 𝐴) → (∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))𝑧 = (𝑦 · 𝐴) ↔ ∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))(𝑥 · 𝐴) = (𝑦 · 𝐴))) |
61 | 8, 60 | ralrnmpt 6276 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ℤ (𝑥 · 𝐴) ∈ V → (∀𝑧 ∈ ran 𝐹∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))𝑧 = (𝑦 · 𝐴) ↔ ∀𝑥 ∈ ℤ ∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))(𝑥 · 𝐴) = (𝑦 · 𝐴))) |
62 | 58, 61 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
ran 𝐹∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))𝑧 = (𝑦 · 𝐴) ↔ ∀𝑥 ∈ ℤ ∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))(𝑥 · 𝐴) = (𝑦 · 𝐴)) |
63 | 56, 62 | sylibr 223 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → ∀𝑧 ∈ ran 𝐹∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))𝑧 = (𝑦 · 𝐴)) |
64 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0...((𝑂‘𝐴) − 1)) ↦ (𝑦 · 𝐴)) = (𝑦 ∈ (0...((𝑂‘𝐴) − 1)) ↦ (𝑦 · 𝐴)) |
65 | 64 | f1ompt 6290 |
. . . . . . . 8
⊢ ((𝑦 ∈ (0...((𝑂‘𝐴) − 1)) ↦ (𝑦 · 𝐴)):(0...((𝑂‘𝐴) − 1))–1-1-onto→ran
𝐹 ↔ (∀𝑦 ∈ (0...((𝑂‘𝐴) − 1))(𝑦 · 𝐴) ∈ ran 𝐹 ∧ ∀𝑧 ∈ ran 𝐹∃!𝑦 ∈ (0...((𝑂‘𝐴) − 1))𝑧 = (𝑦 · 𝐴))) |
66 | 21, 63, 65 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑦 ∈ (0...((𝑂‘𝐴) − 1)) ↦ (𝑦 · 𝐴)):(0...((𝑂‘𝐴) − 1))–1-1-onto→ran
𝐹) |
67 | | f1oen2g 7858 |
. . . . . . 7
⊢
(((0...((𝑂‘𝐴) − 1)) ∈ Fin ∧ ran 𝐹 ∈ V ∧ (𝑦 ∈ (0...((𝑂‘𝐴) − 1)) ↦ (𝑦 · 𝐴)):(0...((𝑂‘𝐴) − 1))–1-1-onto→ran
𝐹) → (0...((𝑂‘𝐴) − 1)) ≈ ran 𝐹) |
68 | 1, 14, 66, 67 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (0...((𝑂‘𝐴) − 1)) ≈ ran 𝐹) |
69 | | enfi 8061 |
. . . . . 6
⊢
((0...((𝑂‘𝐴) − 1)) ≈ ran 𝐹 → ((0...((𝑂‘𝐴) − 1)) ∈ Fin ↔ ran 𝐹 ∈ Fin)) |
70 | 68, 69 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → ((0...((𝑂‘𝐴) − 1)) ∈ Fin ↔ ran 𝐹 ∈ Fin)) |
71 | 1, 70 | mpbid 221 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → ran 𝐹 ∈ Fin) |
72 | 71 | iftrued 4044 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → if(ran 𝐹 ∈ Fin, (#‘ran 𝐹), 0) = (#‘ran 𝐹)) |
73 | | fz01en 12240 |
. . . . . 6
⊢ ((𝑂‘𝐴) ∈ ℤ → (0...((𝑂‘𝐴) − 1)) ≈ (1...(𝑂‘𝐴))) |
74 | | ensym 7891 |
. . . . . 6
⊢
((0...((𝑂‘𝐴) − 1)) ≈ (1...(𝑂‘𝐴)) → (1...(𝑂‘𝐴)) ≈ (0...((𝑂‘𝐴) − 1))) |
75 | 34, 73, 74 | 3syl 18 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (1...(𝑂‘𝐴)) ≈ (0...((𝑂‘𝐴) − 1))) |
76 | | entr 7894 |
. . . . 5
⊢
(((1...(𝑂‘𝐴)) ≈ (0...((𝑂‘𝐴) − 1)) ∧ (0...((𝑂‘𝐴) − 1)) ≈ ran 𝐹) → (1...(𝑂‘𝐴)) ≈ ran 𝐹) |
77 | 75, 68, 76 | syl2anc 691 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (1...(𝑂‘𝐴)) ≈ ran 𝐹) |
78 | | fzfid 12634 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (1...(𝑂‘𝐴)) ∈ Fin) |
79 | | hashen 12997 |
. . . . 5
⊢
(((1...(𝑂‘𝐴)) ∈ Fin ∧ ran 𝐹 ∈ Fin) → ((#‘(1...(𝑂‘𝐴))) = (#‘ran 𝐹) ↔ (1...(𝑂‘𝐴)) ≈ ran 𝐹)) |
80 | 78, 71, 79 | syl2anc 691 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) →
((#‘(1...(𝑂‘𝐴))) = (#‘ran 𝐹) ↔ (1...(𝑂‘𝐴)) ≈ ran 𝐹)) |
81 | 77, 80 | mpbird 246 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) →
(#‘(1...(𝑂‘𝐴))) = (#‘ran 𝐹)) |
82 | | nnnn0 11176 |
. . . . 5
⊢ ((𝑂‘𝐴) ∈ ℕ → (𝑂‘𝐴) ∈
ℕ0) |
83 | 82 | adantl 481 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑂‘𝐴) ∈
ℕ0) |
84 | | hashfz1 12996 |
. . . 4
⊢ ((𝑂‘𝐴) ∈ ℕ0 →
(#‘(1...(𝑂‘𝐴))) = (𝑂‘𝐴)) |
85 | 83, 84 | syl 17 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) →
(#‘(1...(𝑂‘𝐴))) = (𝑂‘𝐴)) |
86 | 72, 81, 85 | 3eqtr2rd 2651 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑂‘𝐴) = if(ran 𝐹 ∈ Fin, (#‘ran 𝐹), 0)) |
87 | | simp3 1056 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑂‘𝐴) = 0) |
88 | 2, 48, 3, 8 | odinf 17803 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → ¬ ran 𝐹 ∈ Fin) |
89 | 88 | iffalsed 4047 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → if(ran 𝐹 ∈ Fin, (#‘ran 𝐹), 0) = 0) |
90 | 87, 89 | eqtr4d 2647 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑂‘𝐴) = if(ran 𝐹 ∈ Fin, (#‘ran 𝐹), 0)) |
91 | 90 | 3expa 1257 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑂‘𝐴) = 0) → (𝑂‘𝐴) = if(ran 𝐹 ∈ Fin, (#‘ran 𝐹), 0)) |
92 | 2, 48 | odcl 17778 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈
ℕ0) |
93 | 92 | adantl 481 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈
ℕ0) |
94 | | elnn0 11171 |
. . 3
⊢ ((𝑂‘𝐴) ∈ ℕ0 ↔ ((𝑂‘𝐴) ∈ ℕ ∨ (𝑂‘𝐴) = 0)) |
95 | 93, 94 | sylib 207 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((𝑂‘𝐴) ∈ ℕ ∨ (𝑂‘𝐴) = 0)) |
96 | 86, 91, 95 | mpjaodan 823 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = if(ran 𝐹 ∈ Fin, (#‘ran 𝐹), 0)) |