Step | Hyp | Ref
| Expression |
1 | | eqidd 2772 |
. 2
⊢ (𝑁 ∈ ℕ →
(Base‘𝐺) =
(Base‘𝐺)) |
2 | | eqidd 2772 |
. 2
⊢ (𝑁 ∈ ℕ →
(+g‘𝐺) =
(+g‘𝐺)) |
3 | | dchrabl.g |
. . . 4
⊢ 𝐺 = (DChr‘𝑁) |
4 | | eqid 2771 |
. . . 4
⊢
(ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) |
5 | | eqid 2771 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | | eqid 2771 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
7 | | simp2 1118 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑥 ∈ (Base‘𝐺)) |
8 | | simp3 1119 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑦 ∈ (Base‘𝐺)) |
9 | 3, 4, 5, 6, 7, 8 | dchrmulcl 25542 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
10 | | fvexd 6511 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) →
(Base‘(ℤ/nℤ‘𝑁)) ∈ V) |
11 | | eqid 2771 |
. . . . . . . 8
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(ℤ/nℤ‘𝑁)) |
12 | 3, 4, 5, 11, 7 | dchrf 25535 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑥:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
13 | 12 | 3adant3r3 1165 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
14 | 3, 4, 5, 11, 8 | dchrf 25535 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑦:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
15 | 14 | 3adant3r3 1165 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
16 | | simpr3 1177 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧 ∈ (Base‘𝐺)) |
17 | 3, 4, 5, 11, 16 | dchrf 25535 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
18 | | mulass 10421 |
. . . . . . 7
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝑎 · 𝑏) · 𝑐) = (𝑎 · (𝑏 · 𝑐))) |
19 | 18 | adantl 474 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ)) → ((𝑎 · 𝑏) · 𝑐) = (𝑎 · (𝑏 · 𝑐))) |
20 | 10, 13, 15, 17, 19 | caofass 7259 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥 ∘𝑓 · 𝑦) ∘𝑓
· 𝑧) = (𝑥 ∘𝑓
· (𝑦
∘𝑓 · 𝑧))) |
21 | | simpr1 1175 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥 ∈ (Base‘𝐺)) |
22 | | simpr2 1176 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺)) |
23 | 3, 4, 5, 6, 21, 22 | dchrmul 25541 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘𝑓 · 𝑦)) |
24 | 23 | oveq1d 6989 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∘𝑓 · 𝑧) = ((𝑥 ∘𝑓 · 𝑦) ∘𝑓
· 𝑧)) |
25 | 3, 4, 5, 6, 22, 16 | dchrmul 25541 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘𝑓 · 𝑧)) |
26 | 25 | oveq2d 6990 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥 ∘𝑓 · (𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘𝑓 · (𝑦 ∘𝑓
· 𝑧))) |
27 | 20, 24, 26 | 3eqtr4d 2817 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∘𝑓 · 𝑧) = (𝑥 ∘𝑓 · (𝑦(+g‘𝐺)𝑧))) |
28 | 9 | 3adant3r3 1165 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
29 | 3, 4, 5, 6, 28, 16 | dchrmul 25541 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = ((𝑥(+g‘𝐺)𝑦) ∘𝑓 · 𝑧)) |
30 | 3, 4, 5, 6, 22, 16 | dchrmulcl 25542 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) |
31 | 3, 4, 5, 6, 21, 30 | dchrmul 25541 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘𝑓 · (𝑦(+g‘𝐺)𝑧))) |
32 | 27, 29, 31 | 3eqtr4d 2817 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
33 | | eqid 2771 |
. . . 4
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Unit‘(ℤ/nℤ‘𝑁)) |
34 | | eqid 2771 |
. . . 4
⊢ (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0)) = (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0)) |
35 | | id 22 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
36 | 3, 4, 5, 11, 33, 34, 35 | dchr1cl 25544 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0)) ∈ (Base‘𝐺)) |
37 | | simpr 477 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥 ∈ (Base‘𝐺)) |
38 | 3, 4, 5, 11, 33, 34, 6, 37 | dchrmulid2 25545 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0))(+g‘𝐺)𝑥) = 𝑥) |
39 | | eqid 2771 |
. . . . 5
⊢ (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0)) = (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0)) |
40 | 3, 4, 5, 11, 33, 34, 6, 37, 39 | dchrinvcl 25546 |
. . . 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)))) |
41 | 40 | simpld 487 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0)) ∈ (Base‘𝐺)) |
42 | 40 | simprd 488 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), (1 / (𝑥‘𝑘)), 0))(+g‘𝐺)𝑥) = (𝑘 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ if(𝑘 ∈
(Unit‘(ℤ/nℤ‘𝑁)), 1, 0))) |
43 | 1, 2, 9, 32, 36, 38, 41, 42 | isgrpd 17925 |
. 2
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Grp) |
44 | | fvexd 6511 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) →
(Base‘(ℤ/nℤ‘𝑁)) ∈ V) |
45 | | mulcom 10419 |
. . . . 5
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 · 𝑏) = (𝑏 · 𝑎)) |
46 | 45 | adantl 474 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ)) → (𝑎 · 𝑏) = (𝑏 · 𝑎)) |
47 | 44, 12, 14, 46 | caofcom 7257 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥 ∘𝑓 · 𝑦) = (𝑦 ∘𝑓 · 𝑥)) |
48 | 3, 4, 5, 6, 7, 8 | dchrmul 25541 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘𝑓 · 𝑦)) |
49 | 3, 4, 5, 6, 8, 7 | dchrmul 25541 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑥) = (𝑦 ∘𝑓 · 𝑥)) |
50 | 47, 48, 49 | 3eqtr4d 2817 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
51 | 1, 2, 43, 50 | isabld 18691 |
1
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |