Step | Hyp | Ref
| Expression |
1 | | eqid 2740 |
. . 3
⊢
(Base‘𝐺) =
(Base‘𝐺) |
2 | | eqid 2740 |
. . 3
⊢
(.g‘𝐺) = (.g‘𝐺) |
3 | 1, 2 | iscyg3 19484 |
. 2
⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ ∃𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥))) |
4 | | eqidd 2741 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → (Base‘𝐺) = (Base‘𝐺)) |
5 | | eqidd 2741 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → (+g‘𝐺) = (+g‘𝐺)) |
6 | | simpll 764 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → 𝐺 ∈ Grp) |
7 | | eqeq1 2744 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (𝑦 = (𝑛(.g‘𝐺)𝑥) ↔ 𝑎 = (𝑛(.g‘𝐺)𝑥))) |
8 | 7 | rexbidv 3228 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → (∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥) ↔ ∃𝑛 ∈ ℤ 𝑎 = (𝑛(.g‘𝐺)𝑥))) |
9 | | oveq1 7278 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑛(.g‘𝐺)𝑥) = (𝑚(.g‘𝐺)𝑥)) |
10 | 9 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝑎 = (𝑛(.g‘𝐺)𝑥) ↔ 𝑎 = (𝑚(.g‘𝐺)𝑥))) |
11 | 10 | cbvrexv 3387 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℤ 𝑎 = (𝑛(.g‘𝐺)𝑥) ↔ ∃𝑚 ∈ ℤ 𝑎 = (𝑚(.g‘𝐺)𝑥)) |
12 | 8, 11 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑦 = 𝑎 → (∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥) ↔ ∃𝑚 ∈ ℤ 𝑎 = (𝑚(.g‘𝐺)𝑥))) |
13 | 12 | rspccv 3558 |
. . . . . . 7
⊢
(∀𝑦 ∈
(Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥) → (𝑎 ∈ (Base‘𝐺) → ∃𝑚 ∈ ℤ 𝑎 = (𝑚(.g‘𝐺)𝑥))) |
14 | 13 | adantl 482 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → (𝑎 ∈ (Base‘𝐺) → ∃𝑚 ∈ ℤ 𝑎 = (𝑚(.g‘𝐺)𝑥))) |
15 | | eqeq1 2744 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → (𝑦 = (𝑛(.g‘𝐺)𝑥) ↔ 𝑏 = (𝑛(.g‘𝐺)𝑥))) |
16 | 15 | rexbidv 3228 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → (∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥) ↔ ∃𝑛 ∈ ℤ 𝑏 = (𝑛(.g‘𝐺)𝑥))) |
17 | 16 | rspccv 3558 |
. . . . . . 7
⊢
(∀𝑦 ∈
(Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥) → (𝑏 ∈ (Base‘𝐺) → ∃𝑛 ∈ ℤ 𝑏 = (𝑛(.g‘𝐺)𝑥))) |
18 | 17 | adantl 482 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → (𝑏 ∈ (Base‘𝐺) → ∃𝑛 ∈ ℤ 𝑏 = (𝑛(.g‘𝐺)𝑥))) |
19 | | reeanv 3295 |
. . . . . . . 8
⊢
(∃𝑚 ∈
ℤ ∃𝑛 ∈
ℤ (𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ 𝑏 = (𝑛(.g‘𝐺)𝑥)) ↔ (∃𝑚 ∈ ℤ 𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ ∃𝑛 ∈ ℤ 𝑏 = (𝑛(.g‘𝐺)𝑥))) |
20 | | zcn 12324 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℂ) |
21 | 20 | ad2antrl 725 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → 𝑚 ∈ ℂ) |
22 | | zcn 12324 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
23 | 22 | ad2antll 726 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → 𝑛 ∈ ℂ) |
24 | 21, 23 | addcomd 11177 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝑚 + 𝑛) = (𝑛 + 𝑚)) |
25 | 24 | oveq1d 7286 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑚 + 𝑛)(.g‘𝐺)𝑥) = ((𝑛 + 𝑚)(.g‘𝐺)𝑥)) |
26 | | simpll 764 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → 𝐺 ∈ Grp) |
27 | | simprl 768 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → 𝑚 ∈ ℤ) |
28 | | simprr 770 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → 𝑛 ∈ ℤ) |
29 | | simplr 766 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → 𝑥 ∈ (Base‘𝐺)) |
30 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢
(+g‘𝐺) = (+g‘𝐺) |
31 | 1, 2, 30 | mulgdir 18733 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ (Base‘𝐺))) → ((𝑚 + 𝑛)(.g‘𝐺)𝑥) = ((𝑚(.g‘𝐺)𝑥)(+g‘𝐺)(𝑛(.g‘𝐺)𝑥))) |
32 | 26, 27, 28, 29, 31 | syl13anc 1371 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑚 + 𝑛)(.g‘𝐺)𝑥) = ((𝑚(.g‘𝐺)𝑥)(+g‘𝐺)(𝑛(.g‘𝐺)𝑥))) |
33 | 1, 2, 30 | mulgdir 18733 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑥 ∈ (Base‘𝐺))) → ((𝑛 + 𝑚)(.g‘𝐺)𝑥) = ((𝑛(.g‘𝐺)𝑥)(+g‘𝐺)(𝑚(.g‘𝐺)𝑥))) |
34 | 26, 28, 27, 29, 33 | syl13anc 1371 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑛 + 𝑚)(.g‘𝐺)𝑥) = ((𝑛(.g‘𝐺)𝑥)(+g‘𝐺)(𝑚(.g‘𝐺)𝑥))) |
35 | 25, 32, 34 | 3eqtr3d 2788 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑚(.g‘𝐺)𝑥)(+g‘𝐺)(𝑛(.g‘𝐺)𝑥)) = ((𝑛(.g‘𝐺)𝑥)(+g‘𝐺)(𝑚(.g‘𝐺)𝑥))) |
36 | | oveq12 7280 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ 𝑏 = (𝑛(.g‘𝐺)𝑥)) → (𝑎(+g‘𝐺)𝑏) = ((𝑚(.g‘𝐺)𝑥)(+g‘𝐺)(𝑛(.g‘𝐺)𝑥))) |
37 | | oveq12 7280 |
. . . . . . . . . . . 12
⊢ ((𝑏 = (𝑛(.g‘𝐺)𝑥) ∧ 𝑎 = (𝑚(.g‘𝐺)𝑥)) → (𝑏(+g‘𝐺)𝑎) = ((𝑛(.g‘𝐺)𝑥)(+g‘𝐺)(𝑚(.g‘𝐺)𝑥))) |
38 | 37 | ancoms 459 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ 𝑏 = (𝑛(.g‘𝐺)𝑥)) → (𝑏(+g‘𝐺)𝑎) = ((𝑛(.g‘𝐺)𝑥)(+g‘𝐺)(𝑚(.g‘𝐺)𝑥))) |
39 | 36, 38 | eqeq12d 2756 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ 𝑏 = (𝑛(.g‘𝐺)𝑥)) → ((𝑎(+g‘𝐺)𝑏) = (𝑏(+g‘𝐺)𝑎) ↔ ((𝑚(.g‘𝐺)𝑥)(+g‘𝐺)(𝑛(.g‘𝐺)𝑥)) = ((𝑛(.g‘𝐺)𝑥)(+g‘𝐺)(𝑚(.g‘𝐺)𝑥)))) |
40 | 35, 39 | syl5ibrcom 246 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ 𝑏 = (𝑛(.g‘𝐺)𝑥)) → (𝑎(+g‘𝐺)𝑏) = (𝑏(+g‘𝐺)𝑎))) |
41 | 40 | rexlimdvva 3225 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ 𝑏 = (𝑛(.g‘𝐺)𝑥)) → (𝑎(+g‘𝐺)𝑏) = (𝑏(+g‘𝐺)𝑎))) |
42 | 19, 41 | syl5bir 242 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) → ((∃𝑚 ∈ ℤ 𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ ∃𝑛 ∈ ℤ 𝑏 = (𝑛(.g‘𝐺)𝑥)) → (𝑎(+g‘𝐺)𝑏) = (𝑏(+g‘𝐺)𝑎))) |
43 | 42 | adantr 481 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → ((∃𝑚 ∈ ℤ 𝑎 = (𝑚(.g‘𝐺)𝑥) ∧ ∃𝑛 ∈ ℤ 𝑏 = (𝑛(.g‘𝐺)𝑥)) → (𝑎(+g‘𝐺)𝑏) = (𝑏(+g‘𝐺)𝑎))) |
44 | 14, 18, 43 | syl2and 608 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → ((𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → (𝑎(+g‘𝐺)𝑏) = (𝑏(+g‘𝐺)𝑎))) |
45 | 44 | 3impib 1115 |
. . . 4
⊢ ((((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → (𝑎(+g‘𝐺)𝑏) = (𝑏(+g‘𝐺)𝑎)) |
46 | 4, 5, 6, 45 | isabld 19398 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) ∧ ∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → 𝐺 ∈ Abel) |
47 | 46 | r19.29an 3219 |
. 2
⊢ ((𝐺 ∈ Grp ∧ ∃𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)∃𝑛 ∈ ℤ 𝑦 = (𝑛(.g‘𝐺)𝑥)) → 𝐺 ∈ Abel) |
48 | 3, 47 | sylbi 216 |
1
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel) |