# 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}={\mathrm{Base}}_{{G}}$
ablsimpgd.2 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
Assertion ablsimpgd ${⊢}{\phi }\to \left({G}\in \mathrm{SimpGrp}↔\left|{B}\right|\in ℙ\right)$

### Proof

Step Hyp Ref Expression
1 ablsimpgd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 ablsimpgd.2 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
3 2 adantr ${⊢}\left({\phi }\wedge {G}\in \mathrm{SimpGrp}\right)\to {G}\in \mathrm{Abel}$
4 simpr ${⊢}\left({\phi }\wedge {G}\in \mathrm{SimpGrp}\right)\to {G}\in \mathrm{SimpGrp}$
5 1 3 4 ablsimpgprmd ${⊢}\left({\phi }\wedge {G}\in \mathrm{SimpGrp}\right)\to \left|{B}\right|\in ℙ$
6 2 ablgrpd ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
7 6 adantr ${⊢}\left({\phi }\wedge \left|{B}\right|\in ℙ\right)\to {G}\in \mathrm{Grp}$
8 simpr ${⊢}\left({\phi }\wedge \left|{B}\right|\in ℙ\right)\to \left|{B}\right|\in ℙ$
9 1 7 8 prmgrpsimpgd ${⊢}\left({\phi }\wedge \left|{B}\right|\in ℙ\right)\to {G}\in \mathrm{SimpGrp}$
10 5 9 impbida ${⊢}{\phi }\to \left({G}\in \mathrm{SimpGrp}↔\left|{B}\right|\in ℙ\right)$