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 ⊢ φ → G ∈ Abel
ablsimpgcygd.2 ⊢ φ → G ∈ SimpGrp
Assertion ablsimpgcygd ⊢ φ → G ∈ CycGrp

Proof

Step Hyp Ref Expression
1 ablsimpgcygd.1 ⊢ φ → G ∈ Abel
2 ablsimpgcygd.2 ⊢ φ → G ∈ SimpGrp
3 eqid ⊢ Base G = Base G
4 eqid ⊢ 0 G = 0 G
5 3 4 2 simpgnideld ⊢ φ → ∃ x ∈ Base G ¬ x = 0 G
6 eqid ⊢ ⋅ G = ⋅ G
7 2 simpggrpd ⊢ φ → G ∈ Grp
8 7 adantr ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G → G ∈ Grp
9 simprl ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G → x ∈ Base G
10 1 ad2antrr ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G ∧ y ∈ Base G → G ∈ Abel
11 2 ad2antrr ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G ∧ y ∈ Base G → G ∈ SimpGrp
12 simplrl ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G ∧ y ∈ Base G → x ∈ Base G
13 simplrr ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G ∧ y ∈ Base G → ¬ x = 0 G
14 simpr ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G ∧ y ∈ Base G → y ∈ Base G
15 3 4 6 10 11 12 13 14 ablsimpg1gend ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G ∧ y ∈ Base G → ∃ z ∈ ℤ y = z ⋅ G x
16 3 6 8 9 15 iscygd ⊢ φ ∧ x ∈ Base G ∧ ¬ x = 0 G → G ∈ CycGrp
17 5 16 rexlimddv ⊢ φ → G ∈ CycGrp