| Step | Hyp | Ref
| Expression |
| 1 | | 1nprm 16716 |
. . . 4
⊢ ¬ 1
∈ ℙ |
| 2 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ 𝐵 ⊆
{(0g‘𝐺)})
→ 𝐵 ⊆
{(0g‘𝐺)}) |
| 3 | | cygctb.1 |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐺) |
| 4 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 5 | 3, 4 | grpidcl 18983 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
| 6 | 5 | snssd 4809 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
{(0g‘𝐺)}
⊆ 𝐵) |
| 7 | 6 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ 𝐵 ⊆
{(0g‘𝐺)})
→ {(0g‘𝐺)} ⊆ 𝐵) |
| 8 | 2, 7 | eqssd 4001 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ 𝐵 ⊆
{(0g‘𝐺)})
→ 𝐵 =
{(0g‘𝐺)}) |
| 9 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ 𝐵 ⊆
{(0g‘𝐺)})
→ (♯‘𝐵) =
(♯‘{(0g‘𝐺)})) |
| 10 | | fvex 6919 |
. . . . . . . 8
⊢
(0g‘𝐺) ∈ V |
| 11 | | hashsng 14408 |
. . . . . . . 8
⊢
((0g‘𝐺) ∈ V →
(♯‘{(0g‘𝐺)}) = 1) |
| 12 | 10, 11 | ax-mp 5 |
. . . . . . 7
⊢
(♯‘{(0g‘𝐺)}) = 1 |
| 13 | 9, 12 | eqtrdi 2793 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ 𝐵 ⊆
{(0g‘𝐺)})
→ (♯‘𝐵) =
1) |
| 14 | | simplr 769 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ 𝐵 ⊆
{(0g‘𝐺)})
→ (♯‘𝐵)
∈ ℙ) |
| 15 | 13, 14 | eqeltrrd 2842 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ 𝐵 ⊆
{(0g‘𝐺)})
→ 1 ∈ ℙ) |
| 16 | 15 | ex 412 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) → (𝐵 ⊆
{(0g‘𝐺)}
→ 1 ∈ ℙ)) |
| 17 | 1, 16 | mtoi 199 |
. . 3
⊢ ((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) → ¬ 𝐵
⊆ {(0g‘𝐺)}) |
| 18 | | nss 4048 |
. . 3
⊢ (¬
𝐵 ⊆
{(0g‘𝐺)}
↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ {(0g‘𝐺)})) |
| 19 | 17, 18 | sylib 218 |
. 2
⊢ ((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ {(0g‘𝐺)})) |
| 20 | | eqid 2737 |
. . 3
⊢
(od‘𝐺) =
(od‘𝐺) |
| 21 | | simpll 767 |
. . 3
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ 𝐺 ∈
Grp) |
| 22 | | simprl 771 |
. . 3
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ 𝑥 ∈ 𝐵) |
| 23 | | simprr 773 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ ¬ 𝑥 ∈
{(0g‘𝐺)}) |
| 24 | 20, 4, 3 | odeq1 19578 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → (((od‘𝐺)‘𝑥) = 1 ↔ 𝑥 = (0g‘𝐺))) |
| 25 | 21, 22, 24 | syl2anc 584 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ (((od‘𝐺)‘𝑥) = 1 ↔ 𝑥 = (0g‘𝐺))) |
| 26 | | velsn 4642 |
. . . . . 6
⊢ (𝑥 ∈
{(0g‘𝐺)}
↔ 𝑥 =
(0g‘𝐺)) |
| 27 | 25, 26 | bitr4di 289 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ (((od‘𝐺)‘𝑥) = 1 ↔ 𝑥 ∈ {(0g‘𝐺)})) |
| 28 | 23, 27 | mtbird 325 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ ¬ ((od‘𝐺)‘𝑥) = 1) |
| 29 | | prmnn 16711 |
. . . . . . . . . 10
⊢
((♯‘𝐵)
∈ ℙ → (♯‘𝐵) ∈ ℕ) |
| 30 | 29 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ (♯‘𝐵)
∈ ℕ) |
| 31 | 30 | nnnn0d 12587 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ (♯‘𝐵)
∈ ℕ0) |
| 32 | 3 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
| 33 | | hashclb 14397 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔
(♯‘𝐵) ∈
ℕ0)) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐵 ∈ Fin ↔
(♯‘𝐵) ∈
ℕ0) |
| 35 | 31, 34 | sylibr 234 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ 𝐵 ∈
Fin) |
| 36 | 3, 20 | oddvds2 19584 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵)) |
| 37 | 21, 35, 22, 36 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵)) |
| 38 | | simplr 769 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ (♯‘𝐵)
∈ ℙ) |
| 39 | 3, 20 | odcl2 19583 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ) |
| 40 | 21, 35, 22, 39 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ ((od‘𝐺)‘𝑥) ∈ ℕ) |
| 41 | | dvdsprime 16724 |
. . . . . . 7
⊢
(((♯‘𝐵)
∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ (((od‘𝐺)‘𝑥) = (♯‘𝐵) ∨ ((od‘𝐺)‘𝑥) = 1))) |
| 42 | 38, 40, 41 | syl2anc 584 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ (((od‘𝐺)‘𝑥) = (♯‘𝐵) ∨ ((od‘𝐺)‘𝑥) = 1))) |
| 43 | 37, 42 | mpbid 232 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ (((od‘𝐺)‘𝑥) = (♯‘𝐵) ∨ ((od‘𝐺)‘𝑥) = 1)) |
| 44 | 43 | ord 865 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ (¬ ((od‘𝐺)‘𝑥) = (♯‘𝐵) → ((od‘𝐺)‘𝑥) = 1)) |
| 45 | 28, 44 | mt3d 148 |
. . 3
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ ((od‘𝐺)‘𝑥) = (♯‘𝐵)) |
| 46 | 3, 20, 21, 22, 45 | iscygodd 19906 |
. 2
⊢ (((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) ∧ (𝑥 ∈
𝐵 ∧ ¬ 𝑥 ∈
{(0g‘𝐺)}))
→ 𝐺 ∈
CycGrp) |
| 47 | 19, 46 | exlimddv 1935 |
1
⊢ ((𝐺 ∈ Grp ∧
(♯‘𝐵) ∈
ℙ) → 𝐺 ∈
CycGrp) |