This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cyg

Description: Define a cyclic group, which is a group with an element x , called the generator of the group, such that all elements in the group are multiples of x . A generator is usually not unique. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion df-cyg CycGrp = { 𝑔 ∈ Grp ∣ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccyg ⊢ CycGrp
1 vg ⊢ 𝑔
2 cgrp ⊢ Grp
3 vx ⊢ 𝑥
4 cbs ⊢ Base
5 1 cv ⊢ 𝑔
6 5 4 cfv ⊢ ( Base ‘ 𝑔 )
7 vn ⊢ 𝑛
8 cz ⊢ ℤ
9 7 cv ⊢ 𝑛
10 cmg ⊢ .g
11 5 10 cfv ⊢ ( .g ‘ 𝑔 )
12 3 cv ⊢ 𝑥
13 9 12 11 co ⊢ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 )
14 7 8 13 cmpt ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) )
15 14 crn ⊢ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) )
16 15 6 wceq ⊢ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 )
17 16 3 6 wrex ⊢ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 )
18 17 1 2 crab ⊢ { 𝑔 ∈ Grp ∣ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 ) }
19 0 18 wceq ⊢ CycGrp = { 𝑔 ∈ Grp ∣ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 ) }