Detailed syntax breakdown of Definition df-dchr
Step | Hyp | Ref
| Expression |
1 | | cdchr 26378 |
. 2
class
DChr |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | cn 11971 |
. . 3
class
ℕ |
4 | | vz |
. . . 4
setvar 𝑧 |
5 | 2 | cv 1538 |
. . . . 5
class 𝑛 |
6 | | czn 20702 |
. . . . 5
class
ℤ/nℤ |
7 | 5, 6 | cfv 6435 |
. . . 4
class
(ℤ/nℤ‘𝑛) |
8 | | vb |
. . . . 5
setvar 𝑏 |
9 | 4 | cv 1538 |
. . . . . . . . . 10
class 𝑧 |
10 | | cbs 16910 |
. . . . . . . . . 10
class
Base |
11 | 9, 10 | cfv 6435 |
. . . . . . . . 9
class
(Base‘𝑧) |
12 | | cui 19879 |
. . . . . . . . . 10
class
Unit |
13 | 9, 12 | cfv 6435 |
. . . . . . . . 9
class
(Unit‘𝑧) |
14 | 11, 13 | cdif 3885 |
. . . . . . . 8
class
((Base‘𝑧)
∖ (Unit‘𝑧)) |
15 | | cc0 10869 |
. . . . . . . . 9
class
0 |
16 | 15 | csn 4563 |
. . . . . . . 8
class
{0} |
17 | 14, 16 | cxp 5589 |
. . . . . . 7
class
(((Base‘𝑧)
∖ (Unit‘𝑧))
× {0}) |
18 | | vx |
. . . . . . . 8
setvar 𝑥 |
19 | 18 | cv 1538 |
. . . . . . 7
class 𝑥 |
20 | 17, 19 | wss 3888 |
. . . . . 6
wff
(((Base‘𝑧)
∖ (Unit‘𝑧))
× {0}) ⊆ 𝑥 |
21 | | cmgp 19718 |
. . . . . . . 8
class
mulGrp |
22 | 9, 21 | cfv 6435 |
. . . . . . 7
class
(mulGrp‘𝑧) |
23 | | ccnfld 20595 |
. . . . . . . 8
class
ℂfld |
24 | 23, 21 | cfv 6435 |
. . . . . . 7
class
(mulGrp‘ℂfld) |
25 | | cmhm 18426 |
. . . . . . 7
class
MndHom |
26 | 22, 24, 25 | co 7277 |
. . . . . 6
class
((mulGrp‘𝑧)
MndHom (mulGrp‘ℂfld)) |
27 | 20, 18, 26 | crab 3068 |
. . . . 5
class {𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} |
28 | | cnx 16892 |
. . . . . . . 8
class
ndx |
29 | 28, 10 | cfv 6435 |
. . . . . . 7
class
(Base‘ndx) |
30 | 8 | cv 1538 |
. . . . . . 7
class 𝑏 |
31 | 29, 30 | cop 4569 |
. . . . . 6
class
〈(Base‘ndx), 𝑏〉 |
32 | | cplusg 16960 |
. . . . . . . 8
class
+g |
33 | 28, 32 | cfv 6435 |
. . . . . . 7
class
(+g‘ndx) |
34 | | cmul 10874 |
. . . . . . . . 9
class
· |
35 | 34 | cof 7531 |
. . . . . . . 8
class
∘f · |
36 | 30, 30 | cxp 5589 |
. . . . . . . 8
class (𝑏 × 𝑏) |
37 | 35, 36 | cres 5593 |
. . . . . . 7
class (
∘f · ↾ (𝑏 × 𝑏)) |
38 | 33, 37 | cop 4569 |
. . . . . 6
class
〈(+g‘ndx), ( ∘f · ↾
(𝑏 × 𝑏))〉 |
39 | 31, 38 | cpr 4565 |
. . . . 5
class
{〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (
∘f · ↾ (𝑏 × 𝑏))〉} |
40 | 8, 27, 39 | csb 3833 |
. . . 4
class
⦋{𝑥
∈ ((mulGrp‘𝑧)
MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))〉} |
41 | 4, 7, 40 | csb 3833 |
. . 3
class
⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))〉} |
42 | 2, 3, 41 | cmpt 5159 |
. 2
class (𝑛 ∈ ℕ ↦
⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))〉}) |
43 | 1, 42 | wceq 1539 |
1
wff DChr =
(𝑛 ∈ ℕ ↦
⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom
(mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))〉}) |