Step | Hyp | Ref
| Expression |
1 | | iscyg.1 |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
2 | | iscyg.2 |
. . . . 5
⊢ · =
(.g‘𝐺) |
3 | | iscyg3.e |
. . . . 5
⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} |
4 | 1, 2, 3 | iscyggen2 19265 |
. . . 4
⊢ (𝐺 ∈ Grp → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋)))) |
5 | 4 | simprbda 502 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ 𝐵) |
6 | | cyggeninv.n |
. . . 4
⊢ 𝑁 = (invg‘𝐺) |
7 | 1, 6 | grpinvcl 18415 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵) |
8 | 5, 7 | syldan 594 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → (𝑁‘𝑋) ∈ 𝐵) |
9 | 4 | simplbda 503 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋)) |
10 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑛 · 𝑋) = (𝑚 · 𝑋)) |
11 | 10 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑦 = (𝑛 · 𝑋) ↔ 𝑦 = (𝑚 · 𝑋))) |
12 | 11 | cbvrexvw 3359 |
. . . . 5
⊢
(∃𝑛 ∈
ℤ 𝑦 = (𝑛 · 𝑋) ↔ ∃𝑚 ∈ ℤ 𝑦 = (𝑚 · 𝑋)) |
13 | | znegcl 12212 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℤ → -𝑚 ∈
ℤ) |
14 | 13 | adantl 485 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → -𝑚 ∈ ℤ) |
15 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℤ) |
16 | 15 | zcnd 12283 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℂ) |
17 | 16 | negnegd 11180 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → --𝑚 = 𝑚) |
18 | 17 | oveq1d 7228 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → (--𝑚 · 𝑋) = (𝑚 · 𝑋)) |
19 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → 𝐺 ∈ Grp) |
20 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → 𝑋 ∈ 𝐵) |
21 | 1, 2, 6 | mulgneg2 18525 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ -𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (--𝑚 · 𝑋) = (-𝑚 · (𝑁‘𝑋))) |
22 | 19, 14, 20, 21 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → (--𝑚 · 𝑋) = (-𝑚 · (𝑁‘𝑋))) |
23 | 18, 22 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → (𝑚 · 𝑋) = (-𝑚 · (𝑁‘𝑋))) |
24 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑛 = -𝑚 → (𝑛 · (𝑁‘𝑋)) = (-𝑚 · (𝑁‘𝑋))) |
25 | 24 | rspceeqv 3552 |
. . . . . . . 8
⊢ ((-𝑚 ∈ ℤ ∧ (𝑚 · 𝑋) = (-𝑚 · (𝑁‘𝑋))) → ∃𝑛 ∈ ℤ (𝑚 · 𝑋) = (𝑛 · (𝑁‘𝑋))) |
26 | 14, 23, 25 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → ∃𝑛 ∈ ℤ (𝑚 · 𝑋) = (𝑛 · (𝑁‘𝑋))) |
27 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = (𝑚 · 𝑋) → (𝑦 = (𝑛 · (𝑁‘𝑋)) ↔ (𝑚 · 𝑋) = (𝑛 · (𝑁‘𝑋)))) |
28 | 27 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑦 = (𝑚 · 𝑋) → (∃𝑛 ∈ ℤ 𝑦 = (𝑛 · (𝑁‘𝑋)) ↔ ∃𝑛 ∈ ℤ (𝑚 · 𝑋) = (𝑛 · (𝑁‘𝑋)))) |
29 | 26, 28 | syl5ibrcom 250 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℤ) → (𝑦 = (𝑚 · 𝑋) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · (𝑁‘𝑋)))) |
30 | 29 | rexlimdva 3203 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) → (∃𝑚 ∈ ℤ 𝑦 = (𝑚 · 𝑋) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · (𝑁‘𝑋)))) |
31 | 12, 30 | syl5bi 245 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) ∧ 𝑦 ∈ 𝐵) → (∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · (𝑁‘𝑋)))) |
32 | 31 | ralimdva 3100 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → (∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋) → ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · (𝑁‘𝑋)))) |
33 | 9, 32 | mpd 15 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · (𝑁‘𝑋))) |
34 | 1, 2, 3 | iscyggen2 19265 |
. . 3
⊢ (𝐺 ∈ Grp → ((𝑁‘𝑋) ∈ 𝐸 ↔ ((𝑁‘𝑋) ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · (𝑁‘𝑋))))) |
35 | 34 | adantr 484 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → ((𝑁‘𝑋) ∈ 𝐸 ↔ ((𝑁‘𝑋) ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · (𝑁‘𝑋))))) |
36 | 8, 33, 35 | mpbir2and 713 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → (𝑁‘𝑋) ∈ 𝐸) |