Step | Hyp | Ref
| Expression |
1 | | czn 21052 |
. 2
class
β€/nβ€ |
2 | | vn |
. . 3
setvar π |
3 | | cn0 12472 |
. . 3
class
β0 |
4 | | vz |
. . . 4
setvar π§ |
5 | | czring 21017 |
. . . 4
class
β€ring |
6 | | vs |
. . . . 5
setvar π |
7 | 4 | cv 1541 |
. . . . . 6
class π§ |
8 | 2 | cv 1541 |
. . . . . . . . 9
class π |
9 | 8 | csn 4629 |
. . . . . . . 8
class {π} |
10 | | crsp 20784 |
. . . . . . . . 9
class
RSpan |
11 | 7, 10 | cfv 6544 |
. . . . . . . 8
class
(RSpanβπ§) |
12 | 9, 11 | cfv 6544 |
. . . . . . 7
class
((RSpanβπ§)β{π}) |
13 | | cqg 19002 |
. . . . . . 7
class
~QG |
14 | 7, 12, 13 | co 7409 |
. . . . . 6
class (π§ ~QG
((RSpanβπ§)β{π})) |
15 | | cqus 17451 |
. . . . . 6
class
/s |
16 | 7, 14, 15 | co 7409 |
. . . . 5
class (π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) |
17 | 6 | cv 1541 |
. . . . . 6
class π |
18 | | cnx 17126 |
. . . . . . . 8
class
ndx |
19 | | cple 17204 |
. . . . . . . 8
class
le |
20 | 18, 19 | cfv 6544 |
. . . . . . 7
class
(leβndx) |
21 | | vf |
. . . . . . . 8
setvar π |
22 | | czrh 21049 |
. . . . . . . . . 10
class
β€RHom |
23 | 17, 22 | cfv 6544 |
. . . . . . . . 9
class
(β€RHomβπ ) |
24 | | cc0 11110 |
. . . . . . . . . . 11
class
0 |
25 | 8, 24 | wceq 1542 |
. . . . . . . . . 10
wff π = 0 |
26 | | cz 12558 |
. . . . . . . . . 10
class
β€ |
27 | | cfzo 13627 |
. . . . . . . . . . 11
class
..^ |
28 | 24, 8, 27 | co 7409 |
. . . . . . . . . 10
class
(0..^π) |
29 | 25, 26, 28 | cif 4529 |
. . . . . . . . 9
class if(π = 0, β€, (0..^π)) |
30 | 23, 29 | cres 5679 |
. . . . . . . 8
class
((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) |
31 | 21 | cv 1541 |
. . . . . . . . . 10
class π |
32 | | cle 11249 |
. . . . . . . . . 10
class
β€ |
33 | 31, 32 | ccom 5681 |
. . . . . . . . 9
class (π β β€ ) |
34 | 31 | ccnv 5676 |
. . . . . . . . 9
class β‘π |
35 | 33, 34 | ccom 5681 |
. . . . . . . 8
class ((π β β€ ) β β‘π) |
36 | 21, 30, 35 | csb 3894 |
. . . . . . 7
class
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π) |
37 | 20, 36 | cop 4635 |
. . . . . 6
class
β¨(leβndx), β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β© |
38 | | csts 17096 |
. . . . . 6
class
sSet |
39 | 17, 37, 38 | co 7409 |
. . . . 5
class (π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©) |
40 | 6, 16, 39 | csb 3894 |
. . . 4
class
β¦(π§
/s (π§
~QG ((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©) |
41 | 4, 5, 40 | csb 3894 |
. . 3
class
β¦β€ring / π§β¦β¦(π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©) |
42 | 2, 3, 41 | cmpt 5232 |
. 2
class (π β β0
β¦ β¦β€ring / π§β¦β¦(π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©)) |
43 | 1, 42 | wceq 1542 |
1
wff
β€/nβ€ = (π β β0 β¦
β¦β€ring / π§β¦β¦(π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©)) |