ablsimpgcygd

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

Step	Hyp	Ref	Expression
1		ablsimpgcygd.1	$⊢ φ \to G \in Abel$
2		ablsimpgcygd.2	$⊢ φ \to G \in SimpGrp$
3		eqid	$⊢ {Base}_{G} = {Base}_{G}$
4		eqid	$⊢ 0_{G} = 0_{G}$
5	3 4 2	simpgnideld	$⊢ φ \to \exists x \in {Base}_{G} \neg x = 0_{G}$
6		eqid	$⊢ \cdot_{G} = \cdot_{G}$
7	2	simpggrpd	$⊢ φ \to G \in Grp$
8	7	adantr	$⊢ (φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \to G \in Grp$
9		simprl	$⊢ (φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \to x \in {Base}_{G}$
10	1	ad2antrr	$⊢ ((φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \land y \in {Base}_{G}) \to G \in Abel$
11	2	ad2antrr	$⊢ ((φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \land y \in {Base}_{G}) \to G \in SimpGrp$
12		simplrl	$⊢ ((φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \land y \in {Base}_{G}) \to x \in {Base}_{G}$
13		simplrr	$⊢ ((φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \land y \in {Base}_{G}) \to \neg x = 0_{G}$
14		simpr	$⊢ ((φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \land y \in {Base}_{G}) \to y \in {Base}_{G}$
15	3 4 6 10 11 12 13 14	ablsimpg1gend	$⊢ ((φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \land y \in {Base}_{G}) \to \exists z \in ℤ y = z \cdot_{G} x$
16	3 6 8 9 15	iscygd	$⊢ (φ \land (x \in {Base}_{G} \land \neg x = 0_{G})) \to G \in CycGrp$
17	5 16	rexlimddv	$⊢ φ \to G \in CycGrp$

Metamath Proof Explorer