Metamath Proof Explorer


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 )