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 ⊢ G ∈ CycGrp → G ∈ Abel

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base G = Base G
2 eqid ⊢ ⋅ G = ⋅ G
3 1 2 iscyg3 ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ ∃ x ∈ Base G ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x
4 eqidd ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → Base G = Base G
5 eqidd ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → + G = + G
6 simpll ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → G ∈ Grp
7 oveq1 ⊢ n = i → n ⋅ G x = i ⋅ G x
8 7 eqeq2d ⊢ n = i → y = n ⋅ G x ↔ y = i ⋅ G x
9 8 cbvrexvw ⊢ ∃ n ∈ ℤ y = n ⋅ G x ↔ ∃ i ∈ ℤ y = i ⋅ G x
10 9 biimpi ⊢ ∃ n ∈ ℤ y = n ⋅ G x → ∃ i ∈ ℤ y = i ⋅ G x
11 10 ralimi ⊢ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → ∀ y ∈ Base G ∃ i ∈ ℤ y = i ⋅ G x
12 11 adantl ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → ∀ y ∈ Base G ∃ i ∈ ℤ y = i ⋅ G x
13 12 3ad2ant1 ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x ∧ a ∈ Base G ∧ b ∈ Base G → ∀ y ∈ Base G ∃ i ∈ ℤ y = i ⋅ G x
14 simpll ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → G ∈ Grp
15 simpr ⊢ G ∈ Grp ∧ x ∈ Base G → x ∈ Base G
16 15 anim1ci ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m ∈ ℤ ∧ n ∈ ℤ ∧ x ∈ Base G
17 df-3an ⊢ m ∈ ℤ ∧ n ∈ ℤ ∧ x ∈ Base G ↔ m ∈ ℤ ∧ n ∈ ℤ ∧ x ∈ Base G
18 16 17 sylibr ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m ∈ ℤ ∧ n ∈ ℤ ∧ x ∈ Base G
19 eqid ⊢ + G = + G
20 1 2 19 mulgdir ⊢ G ∈ Grp ∧ m ∈ ℤ ∧ n ∈ ℤ ∧ x ∈ Base G → m + n ⋅ G x = m ⋅ G x + G n ⋅ G x
21 14 18 20 syl2anc ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m + n ⋅ G x = m ⋅ G x + G n ⋅ G x
22 21 ralrimivva ⊢ G ∈ Grp ∧ x ∈ Base G → ∀ m ∈ ℤ ∀ n ∈ ℤ m + n ⋅ G x = m ⋅ G x + G n ⋅ G x
23 22 adantr ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → ∀ m ∈ ℤ ∀ n ∈ ℤ m + n ⋅ G x = m ⋅ G x + G n ⋅ G x
24 23 3ad2ant1 ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x ∧ a ∈ Base G ∧ b ∈ Base G → ∀ m ∈ ℤ ∀ n ∈ ℤ m + n ⋅ G x = m ⋅ G x + G n ⋅ G x
25 simp2 ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x ∧ a ∈ Base G ∧ b ∈ Base G → a ∈ Base G
26 simp3 ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x ∧ a ∈ Base G ∧ b ∈ Base G → b ∈ Base G
27 zsscn ⊢ ℤ ⊆ ℂ
28 27 a1i ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x ∧ a ∈ Base G ∧ b ∈ Base G → ℤ ⊆ ℂ
29 13 24 25 26 28 cyccom ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x ∧ a ∈ Base G ∧ b ∈ Base G → a + G b = b + G a
30 4 5 6 29 isabld ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → G ∈ Abel
31 30 r19.29an ⊢ G ∈ Grp ∧ ∃ x ∈ Base G ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → G ∈ Abel
32 3 31 sylbi ⊢ G ∈ CycGrp → G ∈ Abel