| Step | Hyp | Ref
| Expression |
| 1 | | cygctb.1 |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | eqid 2737 |
. . 3
⊢
(.g‘𝐺) = (.g‘𝐺) |
| 3 | | eqid 2737 |
. . 3
⊢ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} |
| 4 | 1, 2, 3 | iscyg2 19900 |
. 2
⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} ≠ ∅)) |
| 5 | | n0 4353 |
. . . 4
⊢ ({𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} ≠ ∅ ↔ ∃𝑦 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵}) |
| 6 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} ⊆ 𝐵 |
| 7 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵}) → 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵}) |
| 8 | 6, 7 | sselid 3981 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵}) → 𝑦 ∈ 𝐵) |
| 9 | | eqid 2737 |
. . . . . . . . 9
⊢
(od‘𝐺) =
(od‘𝐺) |
| 10 | 1, 2, 3, 9 | cyggenod2 19903 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵}) → ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) |
| 11 | 8, 10 | jca 511 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵}) → (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) |
| 12 | 11 | ex 412 |
. . . . . 6
⊢ (𝐺 ∈ Grp → (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} → (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0)))) |
| 13 | | cyggex.o |
. . . . . . . . . 10
⊢ 𝐸 = (gEx‘𝐺) |
| 14 | 1, 13 | gexcl 19598 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp → 𝐸 ∈
ℕ0) |
| 15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) → 𝐸 ∈
ℕ0) |
| 16 | | hashcl 14395 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
| 17 | 16 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) ∧ 𝐵 ∈ Fin) → (♯‘𝐵) ∈
ℕ0) |
| 18 | | 0nn0 12541 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
| 19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) ∧ ¬ 𝐵 ∈ Fin) → 0 ∈
ℕ0) |
| 20 | 17, 19 | ifclda 4561 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) → if(𝐵 ∈ Fin,
(♯‘𝐵), 0)
∈ ℕ0) |
| 21 | | breq2 5147 |
. . . . . . . . 9
⊢
((♯‘𝐵) =
if(𝐵 ∈ Fin,
(♯‘𝐵), 0)
→ (𝐸 ∥
(♯‘𝐵) ↔
𝐸 ∥ if(𝐵 ∈ Fin,
(♯‘𝐵),
0))) |
| 22 | | breq2 5147 |
. . . . . . . . 9
⊢ (0 =
if(𝐵 ∈ Fin,
(♯‘𝐵), 0)
→ (𝐸 ∥ 0 ↔
𝐸 ∥ if(𝐵 ∈ Fin,
(♯‘𝐵),
0))) |
| 23 | 1, 13 | gexdvds3 19608 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) → 𝐸 ∥ (♯‘𝐵)) |
| 24 | 23 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) ∧ 𝐵 ∈ Fin) → 𝐸 ∥ (♯‘𝐵)) |
| 25 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) ∧ ¬ 𝐵 ∈ Fin) → 𝐸 ∈
ℕ0) |
| 26 | | nn0z 12638 |
. . . . . . . . . 10
⊢ (𝐸 ∈ ℕ0
→ 𝐸 ∈
ℤ) |
| 27 | | dvds0 16309 |
. . . . . . . . . 10
⊢ (𝐸 ∈ ℤ → 𝐸 ∥ 0) |
| 28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) ∧ ¬ 𝐵 ∈ Fin) → 𝐸 ∥ 0) |
| 29 | 21, 22, 24, 28 | ifbothda 4564 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) → 𝐸 ∥ if(𝐵 ∈ Fin, (♯‘𝐵), 0)) |
| 30 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) → ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) |
| 31 | 1, 13, 9 | gexod 19604 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((od‘𝐺)‘𝑦) ∥ 𝐸) |
| 32 | 31 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) → ((od‘𝐺)‘𝑦) ∥ 𝐸) |
| 33 | 30, 32 | eqbrtrrd 5167 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) → if(𝐵 ∈ Fin,
(♯‘𝐵), 0)
∥ 𝐸) |
| 34 | | dvdseq 16351 |
. . . . . . . 8
⊢ (((𝐸 ∈ ℕ0
∧ if(𝐵 ∈ Fin,
(♯‘𝐵), 0)
∈ ℕ0) ∧ (𝐸 ∥ if(𝐵 ∈ Fin, (♯‘𝐵), 0) ∧ if(𝐵 ∈ Fin, (♯‘𝐵), 0) ∥ 𝐸)) → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) |
| 35 | 15, 20, 29, 33, 34 | syl22anc 839 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) |
| 36 | 35 | ex 412 |
. . . . . 6
⊢ (𝐺 ∈ Grp → ((𝑦 ∈ 𝐵 ∧ ((od‘𝐺)‘𝑦) = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) |
| 37 | 12, 36 | syld 47 |
. . . . 5
⊢ (𝐺 ∈ Grp → (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) |
| 38 | 37 | exlimdv 1933 |
. . . 4
⊢ (𝐺 ∈ Grp → (∃𝑦 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) |
| 39 | 5, 38 | biimtrid 242 |
. . 3
⊢ (𝐺 ∈ Grp → ({𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} ≠ ∅ → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0))) |
| 40 | 39 | imp 406 |
. 2
⊢ ((𝐺 ∈ Grp ∧ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)𝑥)) = 𝐵} ≠ ∅) → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) |
| 41 | 4, 40 | sylbi 217 |
1
⊢ (𝐺 ∈ CycGrp → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)) |