Detailed syntax breakdown of Definition df-zn
Step | Hyp | Ref
| Expression |
1 | | czn 20469 |
. 2
class
ℤ/nℤ |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | cn0 12090 |
. . 3
class
ℕ0 |
4 | | vz |
. . . 4
setvar 𝑧 |
5 | | zring 20435 |
. . . 4
class
ℤring |
6 | | vs |
. . . . 5
setvar 𝑠 |
7 | 4 | cv 1542 |
. . . . . 6
class 𝑧 |
8 | 2 | cv 1542 |
. . . . . . . . 9
class 𝑛 |
9 | 8 | csn 4541 |
. . . . . . . 8
class {𝑛} |
10 | | crsp 20208 |
. . . . . . . . 9
class
RSpan |
11 | 7, 10 | cfv 6380 |
. . . . . . . 8
class
(RSpan‘𝑧) |
12 | 9, 11 | cfv 6380 |
. . . . . . 7
class
((RSpan‘𝑧)‘{𝑛}) |
13 | | cqg 18539 |
. . . . . . 7
class
~QG |
14 | 7, 12, 13 | co 7213 |
. . . . . 6
class (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛})) |
15 | | cqus 17010 |
. . . . . 6
class
/s |
16 | 7, 14, 15 | co 7213 |
. . . . 5
class (𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) |
17 | 6 | cv 1542 |
. . . . . 6
class 𝑠 |
18 | | cnx 16744 |
. . . . . . . 8
class
ndx |
19 | | cple 16809 |
. . . . . . . 8
class
le |
20 | 18, 19 | cfv 6380 |
. . . . . . 7
class
(le‘ndx) |
21 | | vf |
. . . . . . . 8
setvar 𝑓 |
22 | | czrh 20466 |
. . . . . . . . . 10
class
ℤRHom |
23 | 17, 22 | cfv 6380 |
. . . . . . . . 9
class
(ℤRHom‘𝑠) |
24 | | cc0 10729 |
. . . . . . . . . . 11
class
0 |
25 | 8, 24 | wceq 1543 |
. . . . . . . . . 10
wff 𝑛 = 0 |
26 | | cz 12176 |
. . . . . . . . . 10
class
ℤ |
27 | | cfzo 13238 |
. . . . . . . . . . 11
class
..^ |
28 | 24, 8, 27 | co 7213 |
. . . . . . . . . 10
class
(0..^𝑛) |
29 | 25, 26, 28 | cif 4439 |
. . . . . . . . 9
class if(𝑛 = 0, ℤ, (0..^𝑛)) |
30 | 23, 29 | cres 5553 |
. . . . . . . 8
class
((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) |
31 | 21 | cv 1542 |
. . . . . . . . . 10
class 𝑓 |
32 | | cle 10868 |
. . . . . . . . . 10
class
≤ |
33 | 31, 32 | ccom 5555 |
. . . . . . . . 9
class (𝑓 ∘ ≤ ) |
34 | 31 | ccnv 5550 |
. . . . . . . . 9
class ◡𝑓 |
35 | 33, 34 | ccom 5555 |
. . . . . . . 8
class ((𝑓 ∘ ≤ ) ∘ ◡𝑓) |
36 | 21, 30, 35 | csb 3811 |
. . . . . . 7
class
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓) |
37 | 20, 36 | cop 4547 |
. . . . . 6
class
〈(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉 |
38 | | csts 16716 |
. . . . . 6
class
sSet |
39 | 17, 37, 38 | co 7213 |
. . . . 5
class (𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉) |
40 | 6, 16, 39 | csb 3811 |
. . . 4
class
⦋(𝑧
/s (𝑧
~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉) |
41 | 4, 5, 40 | csb 3811 |
. . 3
class
⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉) |
42 | 2, 3, 41 | cmpt 5135 |
. 2
class (𝑛 ∈ ℕ0
↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉)) |
43 | 1, 42 | wceq 1543 |
1
wff
ℤ/nℤ = (𝑛 ∈ ℕ0 ↦
⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉)) |