Metamath Proof Explorer

Theorem cygablOLD

Description: Obsolete proof of cygabl as of 20-Jan-2024. A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion cygablOLD ⊢ 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 eqeq1 ⊢ y = a → y = n ⋅ G x ↔ a = n ⋅ G x
8 7 rexbidv ⊢ y = a → ∃ n ∈ ℤ y = n ⋅ G x ↔ ∃ n ∈ ℤ a = n ⋅ G x
9 oveq1 ⊢ n = m → n ⋅ G x = m ⋅ G x
10 9 eqeq2d ⊢ n = m → a = n ⋅ G x ↔ a = m ⋅ G x
11 10 cbvrexv ⊢ ∃ n ∈ ℤ a = n ⋅ G x ↔ ∃ m ∈ ℤ a = m ⋅ G x
12 8 11 bitrdi ⊢ y = a → ∃ n ∈ ℤ y = n ⋅ G x ↔ ∃ m ∈ ℤ a = m ⋅ G x
13 12 rspccv ⊢ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → a ∈ Base G → ∃ m ∈ ℤ a = m ⋅ G x
14 13 adantl ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → a ∈ Base G → ∃ m ∈ ℤ a = m ⋅ G x
15 eqeq1 ⊢ y = b → y = n ⋅ G x ↔ b = n ⋅ G x
16 15 rexbidv ⊢ y = b → ∃ n ∈ ℤ y = n ⋅ G x ↔ ∃ n ∈ ℤ b = n ⋅ G x
17 16 rspccv ⊢ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → b ∈ Base G → ∃ n ∈ ℤ b = n ⋅ G x
18 17 adantl ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → b ∈ Base G → ∃ n ∈ ℤ b = n ⋅ G x
19 reeanv ⊢ ∃ m ∈ ℤ ∃ n ∈ ℤ a = m ⋅ G x ∧ b = n ⋅ G x ↔ ∃ m ∈ ℤ a = m ⋅ G x ∧ ∃ n ∈ ℤ b = n ⋅ G x
20 zcn ⊢ m ∈ ℤ → m ∈ ℂ
21 20 ad2antrl ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m ∈ ℂ
22 zcn ⊢ n ∈ ℤ → n ∈ ℂ
23 22 ad2antll ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → n ∈ ℂ
24 21 23 addcomd ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m + n = n + m
25 24 oveq1d ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m + n ⋅ G x = n + m ⋅ G x
26 simpll ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → G ∈ Grp
27 simprl ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m ∈ ℤ
28 simprr ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → n ∈ ℤ
29 simplr ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → x ∈ Base G
30 eqid ⊢ + G = + G
31 1 2 30 mulgdir ⊢ G ∈ Grp ∧ m ∈ ℤ ∧ n ∈ ℤ ∧ x ∈ Base G → m + n ⋅ G x = m ⋅ G x + G n ⋅ G x
32 26 27 28 29 31 syl13anc ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m + n ⋅ G x = m ⋅ G x + G n ⋅ G x
33 1 2 30 mulgdir ⊢ G ∈ Grp ∧ n ∈ ℤ ∧ m ∈ ℤ ∧ x ∈ Base G → n + m ⋅ G x = n ⋅ G x + G m ⋅ G x
34 26 28 27 29 33 syl13anc ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → n + m ⋅ G x = n ⋅ G x + G m ⋅ G x
35 25 32 34 3eqtr3d ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → m ⋅ G x + G n ⋅ G x = n ⋅ G x + G m ⋅ G x
36 oveq12 ⊢ a = m ⋅ G x ∧ b = n ⋅ G x → a + G b = m ⋅ G x + G n ⋅ G x
37 oveq12 ⊢ b = n ⋅ G x ∧ a = m ⋅ G x → b + G a = n ⋅ G x + G m ⋅ G x
38 37 ancoms ⊢ a = m ⋅ G x ∧ b = n ⋅ G x → b + G a = n ⋅ G x + G m ⋅ G x
39 36 38 eqeq12d ⊢ a = m ⋅ G x ∧ b = n ⋅ G x → a + G b = b + G a ↔ m ⋅ G x + G n ⋅ G x = n ⋅ G x + G m ⋅ G x
40 35 39 syl5ibrcom ⊢ G ∈ Grp ∧ x ∈ Base G ∧ m ∈ ℤ ∧ n ∈ ℤ → a = m ⋅ G x ∧ b = n ⋅ G x → a + G b = b + G a
41 40 rexlimdvva ⊢ G ∈ Grp ∧ x ∈ Base G → ∃ m ∈ ℤ ∃ n ∈ ℤ a = m ⋅ G x ∧ b = n ⋅ G x → a + G b = b + G a
42 19 41 syl5bir ⊢ G ∈ Grp ∧ x ∈ Base G → ∃ m ∈ ℤ a = m ⋅ G x ∧ ∃ n ∈ ℤ b = n ⋅ G x → a + G b = b + G a
43 42 adantr ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → ∃ m ∈ ℤ a = m ⋅ G x ∧ ∃ n ∈ ℤ b = n ⋅ G x → a + G b = b + G a
44 14 18 43 syl2and ⊢ 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
45 44 3impib ⊢ 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
46 4 5 6 45 isabld ⊢ G ∈ Grp ∧ x ∈ Base G ∧ ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → G ∈ Abel
47 46 r19.29an ⊢ G ∈ Grp ∧ ∃ x ∈ Base G ∀ y ∈ Base G ∃ n ∈ ℤ y = n ⋅ G x → G ∈ Abel
48 3 47 sylbi ⊢ G ∈ CycGrp → G ∈ Abel