Metamath Proof Explorer

Theorem ablsimpgd

Description: An abelian group is simple if and only if its order is prime. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses ablsimpgd.1 ⊢ B = Base G
ablsimpgd.2 ⊢ φ → G ∈ Abel
Assertion ablsimpgd ⊢ φ → G ∈ SimpGrp ↔ B ∈ ℙ

Proof

Step Hyp Ref Expression
1 ablsimpgd.1 ⊢ B = Base G
2 ablsimpgd.2 ⊢ φ → G ∈ Abel
3 2 adantr ⊢ φ ∧ G ∈ SimpGrp → G ∈ Abel
4 simpr ⊢ φ ∧ G ∈ SimpGrp → G ∈ SimpGrp
5 1 3 4 ablsimpgprmd ⊢ φ ∧ G ∈ SimpGrp → B ∈ ℙ
6 2 ablgrpd ⊢ φ → G ∈ Grp
7 6 adantr ⊢ φ ∧ B ∈ ℙ → G ∈ Grp
8 simpr ⊢ φ ∧ B ∈ ℙ → B ∈ ℙ
9 1 7 8 prmgrpsimpgd ⊢ φ ∧ B ∈ ℙ → G ∈ SimpGrp
10 5 9 impbida ⊢ φ → G ∈ SimpGrp ↔ B ∈ ℙ