# Metamath Proof Explorer

## Theorem ablsimpg1gend

Description: An abelian simple group is generated by any non-identity element. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses ablsimpg1gend.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
ablsimpg1gend.2
ablsimpg1gend.3
ablsimpg1gend.4 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
ablsimpg1gend.5 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
ablsimpg1gend.6 ${⊢}{\phi }\to {A}\in {B}$
ablsimpg1gend.7
ablsimpg1gend.8 ${⊢}{\phi }\to {C}\in {B}$
Assertion ablsimpg1gend

### Proof

Step Hyp Ref Expression
1 ablsimpg1gend.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 ablsimpg1gend.2
3 ablsimpg1gend.3
4 ablsimpg1gend.4 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
5 ablsimpg1gend.5 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
6 ablsimpg1gend.6 ${⊢}{\phi }\to {A}\in {B}$
7 ablsimpg1gend.7
8 ablsimpg1gend.8 ${⊢}{\phi }\to {C}\in {B}$
9 eqid
10 5 simpggrpd ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
11 1 3 9 10 6 cycsubgcld
12 1 3 9 6 cycsubggend
13 1 2 4 5 11 12 7 ablsimpnosubgd
14 8 13 eleqtrrd
15 9 14 elrnmpt2d