Step | Hyp | Ref
| Expression |
1 | | eqidd 2611 |
. 2
⊢ (𝑁 ∈ ℕ →
(Base‘𝐺) =
(Base‘𝐺)) |
2 | | eqidd 2611 |
. 2
⊢ (𝑁 ∈ ℕ →
(+g‘𝐺) =
(+g‘𝐺)) |
3 | | dchrabl.g |
. . . 4
⊢ 𝐺 = (DChr‘𝑁) |
4 | | eqid 2610 |
. . . 4
⊢
(ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) |
5 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | | eqid 2610 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
7 | | simp2 1055 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑥 ∈ (Base‘𝐺)) |
8 | | simp3 1056 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑦 ∈ (Base‘𝐺)) |
9 | 3, 4, 5, 6, 7, 8 | dchrmulcl 24774 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
10 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘(ℤ/nℤ‘𝑁)) ∈ V |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) →
(Base‘(ℤ/nℤ‘𝑁)) ∈ V) |
12 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(ℤ/nℤ‘𝑁)) |
13 | 3, 4, 5, 12, 7 | dchrf 24767 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑥:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
14 | 13 | 3adant3r3 1268 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
15 | 3, 4, 5, 12, 8 | dchrf 24767 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑦:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
16 | 15 | 3adant3r3 1268 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
17 | | simpr3 1062 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧 ∈ (Base‘𝐺)) |
18 | 3, 4, 5, 12, 17 | dchrf 24767 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
19 | | mulass 9903 |
. . . . . . 7
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝑎 · 𝑏) · 𝑐) = (𝑎 · (𝑏 · 𝑐))) |
20 | 19 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ)) → ((𝑎 · 𝑏) · 𝑐) = (𝑎 · (𝑏 · 𝑐))) |
21 | 11, 14, 16, 18, 20 | caofass 6829 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥 ∘𝑓 · 𝑦) ∘𝑓
· 𝑧) = (𝑥 ∘𝑓
· (𝑦
∘𝑓 · 𝑧))) |
22 | | simpr1 1060 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥 ∈ (Base‘𝐺)) |
23 | | simpr2 1061 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺)) |
24 | 3, 4, 5, 6, 22, 23 | dchrmul 24773 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘𝑓 · 𝑦)) |
25 | 24 | oveq1d 6564 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∘𝑓 · 𝑧) = ((𝑥 ∘𝑓 · 𝑦) ∘𝑓
· 𝑧)) |
26 | 3, 4, 5, 6, 23, 17 | dchrmul 24773 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘𝑓 · 𝑧)) |
27 | 26 | oveq2d 6565 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥 ∘𝑓 · (𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘𝑓 · (𝑦 ∘𝑓
· 𝑧))) |
28 | 21, 25, 27 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∘𝑓 · 𝑧) = (𝑥 ∘𝑓 · (𝑦(+g‘𝐺)𝑧))) |
29 | 9 | 3adant3r3 1268 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
30 | 3, 4, 5, 6, 29, 17 | dchrmul 24773 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = ((𝑥(+g‘𝐺)𝑦) ∘𝑓 · 𝑧)) |
31 | 3, 4, 5, 6, 23, 17 | dchrmulcl 24774 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) |
32 | 3, 4, 5, 6, 22, 31 | dchrmul 24773 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘𝑓 · (𝑦(+g‘𝐺)𝑧))) |
33 | 28, 30, 32 | 3eqtr4d 2654 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
34 | | eqid 2610 |
. . . 4
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Unit‘(ℤ/nℤ‘𝑁)) |
35 | | eqid 2610 |
. . . 4
⊢ (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0)) = (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0)) |
36 | | id 22 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
37 | 3, 4, 5, 12, 34, 35, 36 | dchr1cl 24776 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0)) ∈ (Base‘𝐺)) |
38 | | simpr 476 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥 ∈ (Base‘𝐺)) |
39 | 3, 4, 5, 12, 34, 35, 6, 38 | dchrmulid2 24777 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0))(+g‘𝐺)𝑥) = 𝑥) |
40 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0)) = (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0)) |
41 | 3, 4, 5, 12, 34, 35, 6, 38, 40 | dchrinvcl 24778 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0)) ∈ (Base‘𝐺) ∧ ((𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0))(+g‘𝐺)𝑥) = (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0)))) |
42 | 41 | simpld 474 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0)) ∈ (Base‘𝐺)) |
43 | 41 | simprd 478 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0))(+g‘𝐺)𝑥) = (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0))) |
44 | 1, 2, 9, 33, 37, 39, 42, 43 | isgrpd 17267 |
. 2
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Grp) |
45 | 10 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) →
(Base‘(ℤ/nℤ‘𝑁)) ∈ V) |
46 | | mulcom 9901 |
. . . . 5
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 · 𝑏) = (𝑏 · 𝑎)) |
47 | 46 | adantl 481 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ)) → (𝑎 · 𝑏) = (𝑏 · 𝑎)) |
48 | 45, 13, 15, 47 | caofcom 6827 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥 ∘𝑓 · 𝑦) = (𝑦 ∘𝑓 · 𝑥)) |
49 | 3, 4, 5, 6, 7, 8 | dchrmul 24773 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘𝑓 · 𝑦)) |
50 | 3, 4, 5, 6, 8, 7 | dchrmul 24773 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑥) = (𝑦 ∘𝑓 · 𝑥)) |
51 | 48, 49, 50 | 3eqtr4d 2654 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
52 | 1, 2, 44, 51 | isabld 18029 |
1
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |