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 · ˙ = G
cycsubggend.3 F = n n · ˙ A
cycsubggend.4 φ A B
Assertion cycsubggend φ A ran F

Proof

Step Hyp Ref Expression
1 cycsubggend.1 B = Base G
2 cycsubggend.2 · ˙ = G
3 cycsubggend.3 F = n n · ˙ A
4 cycsubggend.4 φ A B
5 1zzd φ 1
6 simpr φ n = 1 n = 1
7 6 oveq1d φ n = 1 n · ˙ A = 1 · ˙ A
8 4 adantr φ n = 1 A B
9 1 2 mulg1 A B 1 · ˙ A = A
10 8 9 syl φ n = 1 1 · ˙ A = A
11 7 10 eqtr2d φ n = 1 A = n · ˙ A
12 3 5 4 11 elrnmptdv φ A ran F