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=BaseG
ablsimpgd.2 ⊢φ→G∈Abel
Assertion ablsimpgd ⊢φ→G∈SimpGrp↔B∈ℙ

Proof

Step Hyp Ref Expression
1 ablsimpgd.1 ⊢B=BaseG
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∈ℙ