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

Metamath Proof Explorer

Theorem cygabl

Description: A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016) (Proof shortened by AV, 20-Jan-2024)

Ref Expression
Assertion cygabl ( 𝐺 ∈ CycGrp → 𝐺 ∈ Abel )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
3 1 2 iscyg3 ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
4 eqidd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
5 eqidd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) )
6 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) → 𝐺 ∈ Grp )
7 oveq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) = ( 𝑖 ( .g ‘ 𝐺 ) 𝑥 ) )
8 7 eqeq2d ⊢ ( 𝑛 = 𝑖 → ( 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ↔ 𝑦 = ( 𝑖 ( .g ‘ 𝐺 ) 𝑥 ) ) )
9 8 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ↔ ∃ 𝑖 ∈ ℤ 𝑦 = ( 𝑖 ( .g ‘ 𝐺 ) 𝑥 ) )
10 9 biimpi ⊢ ( ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) → ∃ 𝑖 ∈ ℤ 𝑦 = ( 𝑖 ( .g ‘ 𝐺 ) 𝑥 ) )
11 10 ralimi ⊢ ( ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) → ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑖 ∈ ℤ 𝑦 = ( 𝑖 ( .g ‘ 𝐺 ) 𝑥 ) )
12 11 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑖 ∈ ℤ 𝑦 = ( 𝑖 ( .g ‘ 𝐺 ) 𝑥 ) )
13 12 3ad2ant1 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑖 ∈ ℤ 𝑦 = ( 𝑖 ( .g ‘ 𝐺 ) 𝑥 ) )
14 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) → 𝐺 ∈ Grp )
15 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
16 15 anim1ci ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) → ( ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
17 df-3an ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ↔ ( ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
18 16 17 sylibr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) → ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
19 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
20 1 2 19 mulgdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑚 + 𝑛 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
21 14 18 20 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) → ( ( 𝑚 + 𝑛 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
22 21 ralrimivva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ∀ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ℤ ( ( 𝑚 + 𝑛 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
23 22 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) → ∀ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ℤ ( ( 𝑚 + 𝑛 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
24 23 3ad2ant1 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → ∀ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ℤ ( ( 𝑚 + 𝑛 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
25 simp2 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → 𝑎 ∈ ( Base ‘ 𝐺 ) )
26 simp3 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → 𝑏 ∈ ( Base ‘ 𝐺 ) )
27 zsscn ⊢ ℤ ⊆ ℂ
28 27 a1i ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → ℤ ⊆ ℂ )
29 13 24 25 26 28 cyccom ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝐺 ) 𝑎 ) )
30 4 5 6 29 isabld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) → 𝐺 ∈ Abel )
31 30 r19.29an ⊢ ( ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) → 𝐺 ∈ Abel )
32 3 31 sylbi ⊢ ( 𝐺 ∈ CycGrp → 𝐺 ∈ Abel )