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 = ( Base ` G )
	ablsimpg1gend.2	|- .0. = ( 0g ` G )
	ablsimpg1gend.3	|- .x. = ( .g ` G )
	ablsimpg1gend.4	|- ( ph -> G e. Abel )
	ablsimpg1gend.5	|- ( ph -> G e. SimpGrp )
	ablsimpg1gend.6	|- ( ph -> A e. B )
	ablsimpg1gend.7	|- ( ph -> -. A = .0. )
	ablsimpg1gend.8	|- ( ph -> C e. B )
Assertion	ablsimpg1gend	|- ( ph -> E. n e. ZZ C = ( n .x. A ) )

Proof

Step	Hyp	Ref	Expression
1		ablsimpg1gend.1	|- B = ( Base ` G )
2		ablsimpg1gend.2	|- .0. = ( 0g ` G )
3		ablsimpg1gend.3	|- .x. = ( .g ` G )
4		ablsimpg1gend.4	|- ( ph -> G e. Abel )
5		ablsimpg1gend.5	|- ( ph -> G e. SimpGrp )
6		ablsimpg1gend.6	|- ( ph -> A e. B )
7		ablsimpg1gend.7	|- ( ph -> -. A = .0. )
8		ablsimpg1gend.8	|- ( ph -> C e. B )
9		eqid	|- ( n e. ZZ |-> ( n .x. A ) ) = ( n e. ZZ |-> ( n .x. A ) )
10	5	simpggrpd	|- ( ph -> G e. Grp )
11	1 3 9 10 6	cycsubgcld	|- ( ph -> ran ( n e. ZZ |-> ( n .x. A ) ) e. ( SubGrp ` G ) )
12	1 3 9 6	cycsubggend	|- ( ph -> A e. ran ( n e. ZZ |-> ( n .x. A ) ) )
13	1 2 4 5 11 12 7	ablsimpnosubgd	|- ( ph -> ran ( n e. ZZ |-> ( n .x. A ) ) = B )
14	8 13	eleqtrrd	|- ( ph -> C e. ran ( n e. ZZ |-> ( n .x. A ) ) )
15	9 14	elrnmpt2d	|- ( ph -> E. n e. ZZ C = ( n .x. A ) )