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