Proof of Theorem cyggenod
Step | Hyp | Ref
| Expression |
1 | | iscyg.1 |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
2 | | iscyg.2 |
. . 3
⊢ · =
(.g‘𝐺) |
3 | | iscyg3.e |
. . 3
⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} |
4 | 1, 2, 3 | iscyggen 18282 |
. 2
⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵)) |
5 | | simplr 792 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → 𝐵 ∈ Fin) |
6 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℤ) → 𝐺 ∈ Grp) |
7 | | simpr 477 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ) |
8 | | simplr 792 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℤ) → 𝑋 ∈ 𝐵) |
9 | 1, 2 | mulgcl 17559 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑛 · 𝑋) ∈ 𝐵) |
10 | 6, 7, 8, 9 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℤ) → (𝑛 · 𝑋) ∈ 𝐵) |
11 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) |
12 | 10, 11 | fmptd 6385 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)):ℤ⟶𝐵) |
13 | | frn 6053 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)):ℤ⟶𝐵 → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ⊆ 𝐵) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ⊆ 𝐵) |
15 | | ssfi 8180 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ⊆ 𝐵) → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ∈ Fin) |
16 | 5, 14, 15 | syl2anc 693 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ∈ Fin) |
17 | | hashen 13135 |
. . . . 5
⊢ ((ran
(𝑛 ∈ ℤ ↦
(𝑛 · 𝑋)) ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋))) = (#‘𝐵) ↔ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ≈ 𝐵)) |
18 | 16, 5, 17 | syl2anc 693 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → ((#‘ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋))) = (#‘𝐵) ↔ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ≈ 𝐵)) |
19 | | cyggenod.o |
. . . . . . . 8
⊢ 𝑂 = (od‘𝐺) |
20 | 1, 19, 2, 11 | dfod2 17981 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑂‘𝑋) = if(ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ∈ Fin, (#‘ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋))), 0)) |
21 | 20 | adantlr 751 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → (𝑂‘𝑋) = if(ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ∈ Fin, (#‘ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋))), 0)) |
22 | 16 | iftrued 4094 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → if(ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ∈ Fin, (#‘ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋))), 0) = (#‘ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)))) |
23 | 21, 22 | eqtr2d 2657 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → (#‘ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋))) = (𝑂‘𝑋)) |
24 | 23 | eqeq1d 2624 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → ((#‘ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋))) = (#‘𝐵) ↔ (𝑂‘𝑋) = (#‘𝐵))) |
25 | | fisseneq 8171 |
. . . . . . 7
⊢ ((𝐵 ∈ Fin ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ⊆ 𝐵 ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ≈ 𝐵) → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵) |
26 | 25 | 3expia 1267 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ⊆ 𝐵) → (ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ≈ 𝐵 → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵)) |
27 | | enrefg 7987 |
. . . . . . . 8
⊢ (𝐵 ∈ Fin → 𝐵 ≈ 𝐵) |
28 | 27 | adantr 481 |
. . . . . . 7
⊢ ((𝐵 ∈ Fin ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ⊆ 𝐵) → 𝐵 ≈ 𝐵) |
29 | | breq1 4656 |
. . . . . . 7
⊢ (ran
(𝑛 ∈ ℤ ↦
(𝑛 · 𝑋)) = 𝐵 → (ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ≈ 𝐵 ↔ 𝐵 ≈ 𝐵)) |
30 | 28, 29 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ⊆ 𝐵) → (ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵 → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ≈ 𝐵)) |
31 | 26, 30 | impbid 202 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ⊆ 𝐵) → (ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ≈ 𝐵 ↔ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵)) |
32 | 5, 14, 31 | syl2anc 693 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → (ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) ≈ 𝐵 ↔ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵)) |
33 | 18, 24, 32 | 3bitr3rd 299 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) ∧ 𝑋 ∈ 𝐵) → (ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵 ↔ (𝑂‘𝑋) = (#‘𝐵))) |
34 | 33 | pm5.32da 673 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) → ((𝑋 ∈ 𝐵 ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵) ↔ (𝑋 ∈ 𝐵 ∧ (𝑂‘𝑋) = (#‘𝐵)))) |
35 | 4, 34 | syl5bb 272 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ (𝑂‘𝑋) = (#‘𝐵)))) |