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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablsimpgd.2	⊢ ( 𝜑 → 𝐺 ∈ Abel )
Assertion	ablsimpgd	⊢ ( 𝜑 → ( 𝐺 ∈ SimpGrp ↔ ( ♯ ‘ 𝐵 ) ∈ ℙ ) )

Proof

Step	Hyp	Ref	Expression
1		ablsimpgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ablsimpgd.2	⊢ ( 𝜑 → 𝐺 ∈ Abel )
3	2	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ∈ SimpGrp ) → 𝐺 ∈ Abel )
4		simpr	⊢ ( ( 𝜑 ∧ 𝐺 ∈ SimpGrp ) → 𝐺 ∈ SimpGrp )
5	1 3 4	ablsimpgprmd	⊢ ( ( 𝜑 ∧ 𝐺 ∈ SimpGrp ) → ( ♯ ‘ 𝐵 ) ∈ ℙ )
6	2	ablgrpd	⊢ ( 𝜑 → 𝐺 ∈ Grp )
7	6	adantr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → 𝐺 ∈ Grp )
8		simpr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → ( ♯ ‘ 𝐵 ) ∈ ℙ )
9	1 7 8	prmgrpsimpgd	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → 𝐺 ∈ SimpGrp )
10	5 9	impbida	⊢ ( 𝜑 → ( 𝐺 ∈ SimpGrp ↔ ( ♯ ‘ 𝐵 ) ∈ ℙ ) )