| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ (♯‘𝐵) = 1) →
(♯‘𝐵) =
1) | 
| 2 |  | ablsimpgprmd.3 | . . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ SimpGrp) | 
| 3 | 2 | simpggrpd 20116 | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 4 |  | ablsimpgprmd.1 | . . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) | 
| 5 |  | eqid 2736 | . . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 6 | 4, 5 | grpidcl 18984 | . . . . . . 7
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) | 
| 7 | 3, 6 | syl 17 | . . . . . 6
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐵) | 
| 8 | 7 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (♯‘𝐵) = 1) →
(0g‘𝐺)
∈ 𝐵) | 
| 9 |  | ablsimpgprmd.2 | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Abel) | 
| 10 | 4, 9, 2 | ablsimpgfind 20131 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ Fin) | 
| 11 | 10 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (♯‘𝐵) = 1) → 𝐵 ∈ Fin) | 
| 12 | 1, 8, 11 | hash1elsn 14411 | . . . 4
⊢ ((𝜑 ∧ (♯‘𝐵) = 1) → 𝐵 = {(0g‘𝐺)}) | 
| 13 | 2 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (♯‘𝐵) = 1) → 𝐺 ∈ SimpGrp) | 
| 14 | 4, 5, 13 | simpgntrivd 20119 | . . . 4
⊢ ((𝜑 ∧ (♯‘𝐵) = 1) → ¬ 𝐵 = {(0g‘𝐺)}) | 
| 15 | 12, 14 | pm2.65da 816 | . . 3
⊢ (𝜑 → ¬ (♯‘𝐵) = 1) | 
| 16 | 4, 3, 10 | hashfingrpnn 18991 | . . . . 5
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ) | 
| 17 |  | elnn1uz2 12968 | . . . . 5
⊢
((♯‘𝐵)
∈ ℕ ↔ ((♯‘𝐵) = 1 ∨ (♯‘𝐵) ∈
(ℤ≥‘2))) | 
| 18 | 16, 17 | sylib 218 | . . . 4
⊢ (𝜑 → ((♯‘𝐵) = 1 ∨ (♯‘𝐵) ∈
(ℤ≥‘2))) | 
| 19 | 18 | ord 864 | . . 3
⊢ (𝜑 → (¬
(♯‘𝐵) = 1
→ (♯‘𝐵)
∈ (ℤ≥‘2))) | 
| 20 | 15, 19 | mpd 15 | . 2
⊢ (𝜑 → (♯‘𝐵) ∈
(ℤ≥‘2)) | 
| 21 | 9, 2 | ablsimpgcygd 20127 | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ CycGrp) | 
| 22 | 21 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) → 𝐺 ∈ CycGrp) | 
| 23 |  | simp3 1138 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) → 𝑦 ∥ (♯‘𝐵)) | 
| 24 | 10 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) → 𝐵 ∈ Fin) | 
| 25 |  | simp2 1137 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) → 𝑦 ∈ ℕ) | 
| 26 | 4, 22, 23, 24, 25 | fincygsubgodexd 20134 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) → ∃𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝑦) | 
| 27 |  | simpl1 1191 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → 𝜑) | 
| 28 | 27, 2 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → 𝐺 ∈ SimpGrp) | 
| 29 |  | simprl 770 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → 𝑥 ∈ (SubGrp‘𝐺)) | 
| 30 |  | ablnsg 19866 | . . . . . . . . 9
⊢ (𝐺 ∈ Abel →
(NrmSGrp‘𝐺) =
(SubGrp‘𝐺)) | 
| 31 | 27, 9, 30 | 3syl 18 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → (NrmSGrp‘𝐺) = (SubGrp‘𝐺)) | 
| 32 | 29, 31 | eleqtrrd 2843 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → 𝑥 ∈ (NrmSGrp‘𝐺)) | 
| 33 | 4, 5, 28, 32 | simpgnsgeqd 20122 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → (𝑥 = {(0g‘𝐺)} ∨ 𝑥 = 𝐵)) | 
| 34 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = {(0g‘𝐺)}) → 𝑥 = {(0g‘𝐺)}) | 
| 35 | 34 | fveq2d 6909 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = {(0g‘𝐺)}) → (♯‘𝑥) =
(♯‘{(0g‘𝐺)})) | 
| 36 |  | simplrr 777 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = {(0g‘𝐺)}) → (♯‘𝑥) = 𝑦) | 
| 37 | 5 | fvexi 6919 | . . . . . . . . . 10
⊢
(0g‘𝐺) ∈ V | 
| 38 |  | hashsng 14409 | . . . . . . . . . 10
⊢
((0g‘𝐺) ∈ V →
(♯‘{(0g‘𝐺)}) = 1) | 
| 39 | 37, 38 | mp1i 13 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = {(0g‘𝐺)}) →
(♯‘{(0g‘𝐺)}) = 1) | 
| 40 | 35, 36, 39 | 3eqtr3d 2784 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = {(0g‘𝐺)}) → 𝑦 = 1) | 
| 41 | 40 | ex 412 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → (𝑥 = {(0g‘𝐺)} → 𝑦 = 1)) | 
| 42 |  | simplrr 777 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = 𝐵) → (♯‘𝑥) = 𝑦) | 
| 43 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) | 
| 44 | 43 | fveq2d 6909 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = 𝐵) → (♯‘𝑥) = (♯‘𝐵)) | 
| 45 | 42, 44 | eqtr3d 2778 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) ∧ 𝑥 = 𝐵) → 𝑦 = (♯‘𝐵)) | 
| 46 | 45 | ex 412 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → (𝑥 = 𝐵 → 𝑦 = (♯‘𝐵))) | 
| 47 | 41, 46 | orim12d 966 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → ((𝑥 = {(0g‘𝐺)} ∨ 𝑥 = 𝐵) → (𝑦 = 1 ∨ 𝑦 = (♯‘𝐵)))) | 
| 48 | 33, 47 | mpd 15 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) ∧ (𝑥 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑥) = 𝑦)) → (𝑦 = 1 ∨ 𝑦 = (♯‘𝐵))) | 
| 49 | 26, 48 | rexlimddv 3160 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ 𝑦 ∥ (♯‘𝐵)) → (𝑦 = 1 ∨ 𝑦 = (♯‘𝐵))) | 
| 50 | 49 | 3exp 1119 | . . 3
⊢ (𝜑 → (𝑦 ∈ ℕ → (𝑦 ∥ (♯‘𝐵) → (𝑦 = 1 ∨ 𝑦 = (♯‘𝐵))))) | 
| 51 | 50 | ralrimiv 3144 | . 2
⊢ (𝜑 → ∀𝑦 ∈ ℕ (𝑦 ∥ (♯‘𝐵) → (𝑦 = 1 ∨ 𝑦 = (♯‘𝐵)))) | 
| 52 |  | isprm2 16720 | . 2
⊢
((♯‘𝐵)
∈ ℙ ↔ ((♯‘𝐵) ∈ (ℤ≥‘2)
∧ ∀𝑦 ∈
ℕ (𝑦 ∥
(♯‘𝐵) →
(𝑦 = 1 ∨ 𝑦 = (♯‘𝐵))))) | 
| 53 | 20, 51, 52 | sylanbrc 583 | 1
⊢ (𝜑 → (♯‘𝐵) ∈
ℙ) |