Metamath Proof Explorer


Theorem iscygd

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

Ref Expression
Hypotheses iscyg.1 B = Base G
iscyg.2 · ˙ = G
iscygd.3 φ G Grp
iscygd.4 φ X B
iscygd.5 φ y B n y = n · ˙ X
Assertion iscygd φ G CycGrp

Proof

Step Hyp Ref Expression
1 iscyg.1 B = Base G
2 iscyg.2 · ˙ = G
3 iscygd.3 φ G Grp
4 iscygd.4 φ X B
5 iscygd.5 φ y B n y = n · ˙ X
6 5 ralrimiva φ y B n y = n · ˙ X
7 eqid x B | ran n n · ˙ x = B = x B | ran n n · ˙ x = B
8 1 2 7 iscyggen2 G Grp X x B | ran n n · ˙ x = B X B y B n y = n · ˙ X
9 3 8 syl φ X x B | ran n n · ˙ x = B X B y B n y = n · ˙ X
10 4 6 9 mpbir2and φ X x B | ran n n · ˙ x = B
11 10 ne0d φ x B | ran n n · ˙ x = B
12 1 2 7 iscyg2 G CycGrp G Grp x B | ran n n · ˙ x = B
13 3 11 12 sylanbrc φ G CycGrp