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 syl6bb ⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .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 )