Theorem cycsubggend

Description: The cyclic subgroup generated by A includes its generator. Although this theorem holds for any class G , the definition of F is only meaningful if G is a group. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	cycsubggend.1	|- B = ( Base ` G )
	cycsubggend.2	|- .x. = ( .g ` G )
	cycsubggend.3	|- F = ( n e. ZZ |-> ( n .x. A ) )
	cycsubggend.4	|- ( ph -> A e. B )
Assertion	cycsubggend	|- ( ph -> A e. ran F )

Proof

Step	Hyp	Ref	Expression
1		cycsubggend.1	|- B = ( Base ` G )
2		cycsubggend.2	|- .x. = ( .g ` G )
3		cycsubggend.3	|- F = ( n e. ZZ |-> ( n .x. A ) )
4		cycsubggend.4	|- ( ph -> A e. B )
5		1zzd	|- ( ph -> 1 e. ZZ )
6		simpr	|- ( ( ph /\ n = 1 ) -> n = 1 )
7	6	oveq1d	|- ( ( ph /\ n = 1 ) -> ( n .x. A ) = ( 1 .x. A ) )
8	4	adantr	|- ( ( ph /\ n = 1 ) -> A e. B )
9	1 2	mulg1	|- ( A e. B -> ( 1 .x. A ) = A )
10	8 9	syl	|- ( ( ph /\ n = 1 ) -> ( 1 .x. A ) = A )
11	7 10	eqtr2d	|- ( ( ph /\ n = 1 ) -> A = ( n .x. A ) )
12	3 5 4 11	elrnmptdv	|- ( ph -> A e. ran F )