| 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)) |