Metamath Proof Explorer


Theorem iscyg

Description: Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses iscyg.1 B = Base G
iscyg.2 · ˙ = G
Assertion iscyg G CycGrp G Grp x B ran n n · ˙ x = B

Proof

Step Hyp Ref Expression
1 iscyg.1 B = Base G
2 iscyg.2 · ˙ = G
3 fveq2 g = G Base g = Base G
4 3 1 eqtr4di g = G Base g = B
5 fveq2 g = G g = G
6 5 2 eqtr4di g = G g = · ˙
7 6 oveqd g = G n g x = n · ˙ x
8 7 mpteq2dv g = G n n g x = n n · ˙ x
9 8 rneqd g = G ran n n g x = ran n n · ˙ x
10 9 4 eqeq12d g = G ran n n g x = Base g ran n n · ˙ x = B
11 4 10 rexeqbidv g = G x Base g ran n n g x = Base g x B ran n n · ˙ x = B
12 df-cyg CycGrp = g Grp | x Base g ran n n g x = Base g
13 11 12 elrab2 G CycGrp G Grp x B ran n n · ˙ x = B