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