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	$$⊢\underset{\dot{}}{0}=0_G$$
	ablsimpg1gend.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	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	$$⊢\phi \to \neg A=\underset{\dot{}}{0}$$
	ablsimpg1gend.8	$$⊢\phi \to C\in B$$
Assertion	ablsimpg1gend	$$⊢\phi \to \exists n\in \mathbb{Z}C=n\underset{\dot{}}{·}A$$

Proof

Step	Hyp	Ref	Expression
1		ablsimpg1gend.1	$$⊢B={\mathrm{Base}}_G$$
2		ablsimpg1gend.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		ablsimpg1gend.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
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	$$⊢\phi \to \neg A=\underset{\dot{}}{0}$$
8		ablsimpg1gend.8	$$⊢\phi \to C\in B$$
9		eqid	$$⊢\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)$$
10	5	simpggrpd	$$⊢\phi \to G\in \mathrm{Grp}$$
11	1 3 9 10 6	cycsubgcld	$$⊢\phi \to \mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)\in \mathrm{SubGrp}\left(G\right)$$
12	1 3 9 6	cycsubggend	$$⊢\phi \to A\in \mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)$$
13	1 2 4 5 11 12 7	ablsimpnosubgd	$$⊢\phi \to \mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)=B$$
14	8 13	eleqtrrd	$$⊢\phi \to C\in \mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)$$
15	9 14	elrnmpt2d	$$⊢\phi \to \exists n\in \mathbb{Z}C=n\underset{\dot{}}{·}A$$