Step | Hyp | Ref
| Expression |
1 | | hofval.m |
. 2
β’ π =
(HomFβπΆ) |
2 | | df-hof 18099 |
. . 3
β’
HomF = (π β Cat β¦
β¨(Homf βπ), β¦(Baseβπ) / πβ¦(π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π))))β©) |
3 | | simpr 485 |
. . . . 5
β’ ((π β§ π = πΆ) β π = πΆ) |
4 | 3 | fveq2d 6843 |
. . . 4
β’ ((π β§ π = πΆ) β (Homf
βπ) =
(Homf βπΆ)) |
5 | | fvexd 6854 |
. . . . 5
β’ ((π β§ π = πΆ) β (Baseβπ) β V) |
6 | 3 | fveq2d 6843 |
. . . . . 6
β’ ((π β§ π = πΆ) β (Baseβπ) = (BaseβπΆ)) |
7 | | hofval.b |
. . . . . 6
β’ π΅ = (BaseβπΆ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . 5
β’ ((π β§ π = πΆ) β (Baseβπ) = π΅) |
9 | | simpr 485 |
. . . . . . 7
β’ (((π β§ π = πΆ) β§ π = π΅) β π = π΅) |
10 | 9 | sqxpeqd 5663 |
. . . . . 6
β’ (((π β§ π = πΆ) β§ π = π΅) β (π Γ π) = (π΅ Γ π΅)) |
11 | | simplr 767 |
. . . . . . . . . 10
β’ (((π β§ π = πΆ) β§ π = π΅) β π = πΆ) |
12 | 11 | fveq2d 6843 |
. . . . . . . . 9
β’ (((π β§ π = πΆ) β§ π = π΅) β (Hom βπ) = (Hom βπΆ)) |
13 | | hofval.h |
. . . . . . . . 9
β’ π» = (Hom βπΆ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . . 8
β’ (((π β§ π = πΆ) β§ π = π΅) β (Hom βπ) = π») |
15 | 14 | oveqd 7368 |
. . . . . . 7
β’ (((π β§ π = πΆ) β§ π = π΅) β ((1st βπ¦)(Hom βπ)(1st βπ₯)) = ((1st βπ¦)π»(1st βπ₯))) |
16 | 14 | oveqd 7368 |
. . . . . . 7
β’ (((π β§ π = πΆ) β§ π = π΅) β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) = ((2nd βπ₯)π»(2nd βπ¦))) |
17 | 14 | fveq1d 6841 |
. . . . . . . 8
β’ (((π β§ π = πΆ) β§ π = π΅) β ((Hom βπ)βπ₯) = (π»βπ₯)) |
18 | 11 | fveq2d 6843 |
. . . . . . . . . . 11
β’ (((π β§ π = πΆ) β§ π = π΅) β (compβπ) = (compβπΆ)) |
19 | | hofval.o |
. . . . . . . . . . 11
β’ Β· =
(compβπΆ) |
20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (((π β§ π = πΆ) β§ π = π΅) β (compβπ) = Β· ) |
21 | 20 | oveqd 7368 |
. . . . . . . . 9
β’ (((π β§ π = πΆ) β§ π = π΅) β (β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦)) = (β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))) |
22 | 20 | oveqd 7368 |
. . . . . . . . . 10
β’ (((π β§ π = πΆ) β§ π = π΅) β (π₯(compβπ)(2nd βπ¦)) = (π₯ Β· (2nd
βπ¦))) |
23 | 22 | oveqd 7368 |
. . . . . . . . 9
β’ (((π β§ π = πΆ) β§ π = π΅) β (π(π₯(compβπ)(2nd βπ¦))β) = (π(π₯ Β· (2nd
βπ¦))β)) |
24 | | eqidd 2738 |
. . . . . . . . 9
β’ (((π β§ π = πΆ) β§ π = π΅) β π = π) |
25 | 21, 23, 24 | oveq123d 7372 |
. . . . . . . 8
β’ (((π β§ π = πΆ) β§ π = π΅) β ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π) = ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π)) |
26 | 17, 25 | mpteq12dv 5194 |
. . . . . . 7
β’ (((π β§ π = πΆ) β§ π = π΅) β (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π)) = (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))) |
27 | 15, 16, 26 | mpoeq123dv 7426 |
. . . . . 6
β’ (((π β§ π = πΆ) β§ π = π΅) β (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π))) = (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π)))) |
28 | 10, 10, 27 | mpoeq123dv 7426 |
. . . . 5
β’ (((π β§ π = πΆ) β§ π = π΅) β (π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π)))) = (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))) |
29 | 5, 8, 28 | csbied2 3893 |
. . . 4
β’ ((π β§ π = πΆ) β β¦(Baseβπ) / πβ¦(π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π)))) = (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))) |
30 | 4, 29 | opeq12d 4836 |
. . 3
β’ ((π β§ π = πΆ) β β¨(Homf
βπ),
β¦(Baseβπ) / πβ¦(π₯ β (π Γ π), π¦ β (π Γ π) β¦ (π β ((1st βπ¦)(Hom βπ)(1st βπ₯)), π β ((2nd βπ₯)(Hom βπ)(2nd βπ¦)) β¦ (β β ((Hom βπ)βπ₯) β¦ ((π(π₯(compβπ)(2nd βπ¦))β)(β¨(1st βπ¦), (1st βπ₯)β©(compβπ)(2nd βπ¦))π))))β© = β¨(Homf
βπΆ), (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))β©) |
31 | | hofval.c |
. . 3
β’ (π β πΆ β Cat) |
32 | | opex 5419 |
. . . 4
β’
β¨(Homf βπΆ), (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))β© β V |
33 | 32 | a1i 11 |
. . 3
β’ (π β
β¨(Homf βπΆ), (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))β© β V) |
34 | 2, 30, 31, 33 | fvmptd2 6953 |
. 2
β’ (π β
(HomFβπΆ) = β¨(Homf
βπΆ), (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))β©) |
35 | 1, 34 | eqtrid 2789 |
1
β’ (π β π = β¨(Homf
βπΆ), (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))β©) |