Metamath Proof Explorer

Theorem prmsimpcyc

Description: A group of prime order is cyclic if and only if it is simple. This is the first family of finite simple groups. (Contributed by Thierry Arnoux, 21-Sep-2023)

Ref Expression
Hypothesis prmsimpcyc.1 ⊢ B = Base G
Assertion prmsimpcyc ⊢ B ∈ ℙ → G ∈ SimpGrp ↔ G ∈ CycGrp

Proof

Step Hyp Ref Expression
1 prmsimpcyc.1 ⊢ B = Base G
2 simpggrp ⊢ G ∈ SimpGrp → G ∈ Grp
3 id ⊢ B ∈ ℙ → B ∈ ℙ
4 1 prmcyg ⊢ G ∈ Grp ∧ B ∈ ℙ → G ∈ CycGrp
5 2 3 4 syl2anr ⊢ B ∈ ℙ ∧ G ∈ SimpGrp → G ∈ CycGrp
6 cyggrp ⊢ G ∈ CycGrp → G ∈ Grp
7 6 adantl ⊢ B ∈ ℙ ∧ G ∈ CycGrp → G ∈ Grp
8 simpl ⊢ B ∈ ℙ ∧ G ∈ CycGrp → B ∈ ℙ
9 1 7 8 prmgrpsimpgd ⊢ B ∈ ℙ ∧ G ∈ CycGrp → G ∈ SimpGrp
10 5 9 impbida ⊢ B ∈ ℙ → G ∈ SimpGrp ↔ G ∈ CycGrp