# Metamath Proof Explorer

## Theorem ablsimpgcygd

Description: An abelian simple group is cyclic. (Contributed by Rohan Ridenour, 3-Aug-2023) (Proof shortened by Rohan Ridenour, 31-Oct-2023)

Ref Expression
Hypotheses ablsimpgcygd.1 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
ablsimpgcygd.2 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
Assertion ablsimpgcygd ${⊢}{\phi }\to {G}\in \mathrm{CycGrp}$

### Proof

Step Hyp Ref Expression
1 ablsimpgcygd.1 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
2 ablsimpgcygd.2 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
3 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
4 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
5 3 4 2 simpgnideld ${⊢}{\phi }\to \exists {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}¬{x}={0}_{{G}}$
6 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
7 2 simpggrpd ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
8 7 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\to {G}\in \mathrm{Grp}$
9 simprl ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\to {x}\in {\mathrm{Base}}_{{G}}$
10 1 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {G}\in \mathrm{Abel}$
11 2 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {G}\in \mathrm{SimpGrp}$
12 simplrl ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {x}\in {\mathrm{Base}}_{{G}}$
13 simplrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to ¬{x}={0}_{{G}}$
14 simpr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {y}\in {\mathrm{Base}}_{{G}}$
15 3 4 6 10 11 12 13 14 ablsimpg1gend ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to \exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}{y}={z}{\cdot }_{{G}}{x}$
16 3 6 8 9 15 iscygd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge ¬{x}={0}_{{G}}\right)\right)\to {G}\in \mathrm{CycGrp}$
17 5 16 rexlimddv ${⊢}{\phi }\to {G}\in \mathrm{CycGrp}$