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	|- ( ph -> G e. Abel )
Assertion	ablsimpgd	|- ( ph -> ( G e. SimpGrp <-> ( # ` B ) e. Prime ) )

Proof

Step	Hyp	Ref	Expression
1		ablsimpgd.1	|- B = ( Base ` G )
2		ablsimpgd.2	|- ( ph -> G e. Abel )
3	2	adantr	|- ( ( ph /\ G e. SimpGrp ) -> G e. Abel )
4		simpr	|- ( ( ph /\ G e. SimpGrp ) -> G e. SimpGrp )
5	1 3 4	ablsimpgprmd	|- ( ( ph /\ G e. SimpGrp ) -> ( # ` B ) e. Prime )
6	2	ablgrpd	|- ( ph -> G e. Grp )
7	6	adantr	|- ( ( ph /\ ( # ` B ) e. Prime ) -> G e. Grp )
8		simpr	|- ( ( ph /\ ( # ` B ) e. Prime ) -> ( # ` B ) e. Prime )
9	1 7 8	prmgrpsimpgd	|- ( ( ph /\ ( # ` B ) e. Prime ) -> G e. SimpGrp )
10	5 9	impbida	|- ( ph -> ( G e. SimpGrp <-> ( # ` B ) e. Prime ) )