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 ) |
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 ) |