Step | Hyp | Ref
| Expression |
1 | | hofcllem.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
2 | | hofcllem.h |
. . . . 5
β’ π» = (Hom βπΆ) |
3 | | eqid 2733 |
. . . . 5
β’
(compβπΆ) =
(compβπΆ) |
4 | | hofcl.c |
. . . . . 6
β’ (π β πΆ β Cat) |
5 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β πΆ β Cat) |
6 | | hofcllem.s |
. . . . . 6
β’ (π β π β π΅) |
7 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β π β π΅) |
8 | | hofcllem.z |
. . . . . 6
β’ (π β π β π΅) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β π β π΅) |
10 | | hofcllem.x |
. . . . . 6
β’ (π β π β π΅) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β π β π΅) |
12 | | hofcllem.p |
. . . . . 6
β’ (π β π β (ππ»π)) |
13 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β π β (ππ»π)) |
14 | | hofcllem.m |
. . . . . 6
β’ (π β πΎ β (ππ»π)) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β πΎ β (ππ»π)) |
16 | | hofcllem.t |
. . . . . 6
β’ (π β π β π΅) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β π β π΅) |
18 | | hofcllem.y |
. . . . . . 7
β’ (π β π β π΅) |
19 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β π β π΅) |
20 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β π β (ππ»π)) |
21 | | hofcllem.w |
. . . . . . . 8
β’ (π β π β π΅) |
22 | | hofcllem.n |
. . . . . . . 8
β’ (π β πΏ β (ππ»π)) |
23 | | hofcllem.q |
. . . . . . . 8
β’ (π β π β (ππ»π)) |
24 | 1, 2, 3, 4, 18, 21, 16, 22, 23 | catcocl 17570 |
. . . . . . 7
β’ (π β (π(β¨π, πβ©(compβπΆ)π)πΏ) β (ππ»π)) |
25 | 24 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β (π(β¨π, πβ©(compβπΆ)π)πΏ) β (ππ»π)) |
26 | 1, 2, 3, 5, 11, 19, 17, 20, 25 | catcocl 17570 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β ((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π) β (ππ»π)) |
27 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 26 | catass 17571 |
. . . 4
β’ ((π β§ π β (ππ»π)) β ((((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ)(β¨π, πβ©(compβπΆ)π)π) = (((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)(πΎ(β¨π, πβ©(compβπΆ)π)π))) |
28 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (ππ»π)) β π β π΅) |
29 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (ππ»π)) β πΏ β (ππ»π)) |
30 | 23 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (ππ»π)) β π β (ππ»π)) |
31 | 1, 2, 3, 5, 11, 19, 28, 20, 29, 17, 30 | catass 17571 |
. . . . . . 7
β’ ((π β§ π β (ππ»π)) β ((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π) = (π(β¨π, πβ©(compβπΆ)π)(πΏ(β¨π, πβ©(compβπΆ)π)π))) |
32 | 31 | oveq1d 7373 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β (((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ) = ((π(β¨π, πβ©(compβπΆ)π)(πΏ(β¨π, πβ©(compβπΆ)π)π))(β¨π, πβ©(compβπΆ)π)πΎ)) |
33 | 1, 2, 3, 5, 11, 19, 28, 20, 29 | catcocl 17570 |
. . . . . . 7
β’ ((π β§ π β (ππ»π)) β (πΏ(β¨π, πβ©(compβπΆ)π)π) β (ππ»π)) |
34 | 1, 2, 3, 5, 9, 11,
28, 15, 33, 17, 30 | catass 17571 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β ((π(β¨π, πβ©(compβπΆ)π)(πΏ(β¨π, πβ©(compβπΆ)π)π))(β¨π, πβ©(compβπΆ)π)πΎ) = (π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))) |
35 | 32, 34 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β (((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ) = (π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))) |
36 | 35 | oveq1d 7373 |
. . . 4
β’ ((π β§ π β (ππ»π)) β ((((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ)(β¨π, πβ©(compβπΆ)π)π) = ((π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))(β¨π, πβ©(compβπΆ)π)π)) |
37 | 27, 36 | eqtr3d 2775 |
. . 3
β’ ((π β§ π β (ππ»π)) β (((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)(πΎ(β¨π, πβ©(compβπΆ)π)π)) = ((π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))(β¨π, πβ©(compβπΆ)π)π)) |
38 | 37 | mpteq2dva 5206 |
. 2
β’ (π β (π β (ππ»π) β¦ (((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)(πΎ(β¨π, πβ©(compβπΆ)π)π))) = (π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))(β¨π, πβ©(compβπΆ)π)π))) |
39 | | hofcl.m |
. . 3
β’ π =
(HomFβπΆ) |
40 | 1, 2, 3, 4, 6, 8, 10, 12, 14 | catcocl 17570 |
. . 3
β’ (π β (πΎ(β¨π, πβ©(compβπΆ)π)π) β (ππ»π)) |
41 | 39, 4, 1, 2, 10, 18, 6, 16, 3, 40, 24 | hof2val 18150 |
. 2
β’ (π β ((πΎ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(2nd βπ)β¨π, πβ©)(π(β¨π, πβ©(compβπΆ)π)πΏ)) = (π β (ππ»π) β¦ (((π(β¨π, πβ©(compβπΆ)π)πΏ)(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)(πΎ(β¨π, πβ©(compβπΆ)π)π)))) |
42 | 39, 4, 1, 2, 8, 21,
6, 16, 3, 12, 23 | hof2val 18150 |
. . . 4
β’ (π β (π(β¨π, πβ©(2nd βπ)β¨π, πβ©)π) = (π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π))) |
43 | 39, 4, 1, 2, 10, 18, 8, 21, 3, 14, 22 | hof2val 18150 |
. . . 4
β’ (π β (πΎ(β¨π, πβ©(2nd βπ)β¨π, πβ©)πΏ) = (π β (ππ»π) β¦ ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))) |
44 | 42, 43 | oveq12d 7376 |
. . 3
β’ (π β ((π(β¨π, πβ©(2nd βπ)β¨π, πβ©)π)(β¨(ππ»π), (ππ»π)β©(compβπ·)(ππ»π))(πΎ(β¨π, πβ©(2nd βπ)β¨π, πβ©)πΏ)) = ((π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π))(β¨(ππ»π), (ππ»π)β©(compβπ·)(ππ»π))(π β (ππ»π) β¦ ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ)))) |
45 | | hofcl.d |
. . . 4
β’ π· = (SetCatβπ) |
46 | | hofcl.u |
. . . 4
β’ (π β π β π) |
47 | | eqid 2733 |
. . . 4
β’
(compβπ·) =
(compβπ·) |
48 | | eqid 2733 |
. . . . . 6
β’
(Homf βπΆ) = (Homf βπΆ) |
49 | 48, 1, 2, 10, 18 | homfval 17577 |
. . . . 5
β’ (π β (π(Homf βπΆ)π) = (ππ»π)) |
50 | 48, 1 | homffn 17578 |
. . . . . . . 8
β’
(Homf βπΆ) Fn (π΅ Γ π΅) |
51 | 50 | a1i 11 |
. . . . . . 7
β’ (π β (Homf
βπΆ) Fn (π΅ Γ π΅)) |
52 | | hofcl.h |
. . . . . . 7
β’ (π β ran
(Homf βπΆ) β π) |
53 | | df-f 6501 |
. . . . . . 7
β’
((Homf βπΆ):(π΅ Γ π΅)βΆπ β ((Homf
βπΆ) Fn (π΅ Γ π΅) β§ ran (Homf
βπΆ) β π)) |
54 | 51, 52, 53 | sylanbrc 584 |
. . . . . 6
β’ (π β (Homf
βπΆ):(π΅ Γ π΅)βΆπ) |
55 | 54, 10, 18 | fovcdmd 7527 |
. . . . 5
β’ (π β (π(Homf βπΆ)π) β π) |
56 | 49, 55 | eqeltrrd 2835 |
. . . 4
β’ (π β (ππ»π) β π) |
57 | 48, 1, 2, 8, 21 | homfval 17577 |
. . . . 5
β’ (π β (π(Homf βπΆ)π) = (ππ»π)) |
58 | 54, 8, 21 | fovcdmd 7527 |
. . . . 5
β’ (π β (π(Homf βπΆ)π) β π) |
59 | 57, 58 | eqeltrrd 2835 |
. . . 4
β’ (π β (ππ»π) β π) |
60 | 48, 1, 2, 6, 16 | homfval 17577 |
. . . . 5
β’ (π β (π(Homf βπΆ)π) = (ππ»π)) |
61 | 54, 6, 16 | fovcdmd 7527 |
. . . . 5
β’ (π β (π(Homf βπΆ)π) β π) |
62 | 60, 61 | eqeltrrd 2835 |
. . . 4
β’ (π β (ππ»π) β π) |
63 | 1, 2, 3, 5, 9, 11,
28, 15, 33 | catcocl 17570 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ) β (ππ»π)) |
64 | 63 | fmpttd 7064 |
. . . 4
β’ (π β (π β (ππ»π) β¦ ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ)):(ππ»π)βΆ(ππ»π)) |
65 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β πΆ β Cat) |
66 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β π β π΅) |
67 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β π β π΅) |
68 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β π β π΅) |
69 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β π β (ππ»π)) |
70 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (ππ»π)) β π β π΅) |
71 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β (ππ»π)) β π β (ππ»π)) |
72 | 23 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (ππ»π)) β π β (ππ»π)) |
73 | 1, 2, 3, 65, 67, 70, 68, 71, 72 | catcocl 17570 |
. . . . . 6
β’ ((π β§ π β (ππ»π)) β (π(β¨π, πβ©(compβπΆ)π)π) β (ππ»π)) |
74 | 1, 2, 3, 65, 66, 67, 68, 69, 73 | catcocl 17570 |
. . . . 5
β’ ((π β§ π β (ππ»π)) β ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π) β (ππ»π)) |
75 | 74 | fmpttd 7064 |
. . . 4
β’ (π β (π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π)):(ππ»π)βΆ(ππ»π)) |
76 | 45, 46, 47, 56, 59, 62, 64, 75 | setcco 17974 |
. . 3
β’ (π β ((π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π))(β¨(ππ»π), (ππ»π)β©(compβπ·)(ππ»π))(π β (ππ»π) β¦ ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))) = ((π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π)) β (π β (ππ»π) β¦ ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ)))) |
77 | | eqidd 2734 |
. . . 4
β’ (π β (π β (ππ»π) β¦ ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ)) = (π β (ππ»π) β¦ ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))) |
78 | | eqidd 2734 |
. . . 4
β’ (π β (π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π)) = (π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π))) |
79 | | oveq2 7366 |
. . . . 5
β’ (π = ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ) β (π(β¨π, πβ©(compβπΆ)π)π) = (π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))) |
80 | 79 | oveq1d 7373 |
. . . 4
β’ (π = ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ) β ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π) = ((π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))(β¨π, πβ©(compβπΆ)π)π)) |
81 | 63, 77, 78, 80 | fmptco 7076 |
. . 3
β’ (π β ((π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)π)) β (π β (ππ»π) β¦ ((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))) = (π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))(β¨π, πβ©(compβπΆ)π)π))) |
82 | 44, 76, 81 | 3eqtrd 2777 |
. 2
β’ (π β ((π(β¨π, πβ©(2nd βπ)β¨π, πβ©)π)(β¨(ππ»π), (ππ»π)β©(compβπ·)(ππ»π))(πΎ(β¨π, πβ©(2nd βπ)β¨π, πβ©)πΏ)) = (π β (ππ»π) β¦ ((π(β¨π, πβ©(compβπΆ)π)((πΏ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(compβπΆ)π)πΎ))(β¨π, πβ©(compβπΆ)π)π))) |
83 | 38, 41, 82 | 3eqtr4d 2783 |
1
β’ (π β ((πΎ(β¨π, πβ©(compβπΆ)π)π)(β¨π, πβ©(2nd βπ)β¨π, πβ©)(π(β¨π, πβ©(compβπΆ)π)πΏ)) = ((π(β¨π, πβ©(2nd βπ)β¨π, πβ©)π)(β¨(ππ»π), (ππ»π)β©(compβπ·)(ππ»π))(πΎ(β¨π, πβ©(2nd βπ)β¨π, πβ©)πΏ))) |