Step | Hyp | Ref
| Expression |
1 | | ismon.s |
. 2
β’ π = (MonoβπΆ) |
2 | | ismon.c |
. . 3
β’ (π β πΆ β Cat) |
3 | | fvexd 6854 |
. . . . 5
β’ (π = πΆ β (Baseβπ) β V) |
4 | | fveq2 6839 |
. . . . . 6
β’ (π = πΆ β (Baseβπ) = (BaseβπΆ)) |
5 | | ismon.b |
. . . . . 6
β’ π΅ = (BaseβπΆ) |
6 | 4, 5 | eqtr4di 2795 |
. . . . 5
β’ (π = πΆ β (Baseβπ) = π΅) |
7 | | fvexd 6854 |
. . . . . 6
β’ ((π = πΆ β§ π = π΅) β (Hom βπ) β V) |
8 | | simpl 483 |
. . . . . . . 8
β’ ((π = πΆ β§ π = π΅) β π = πΆ) |
9 | 8 | fveq2d 6843 |
. . . . . . 7
β’ ((π = πΆ β§ π = π΅) β (Hom βπ) = (Hom βπΆ)) |
10 | | ismon.h |
. . . . . . 7
β’ π» = (Hom βπΆ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . 6
β’ ((π = πΆ β§ π = π΅) β (Hom βπ) = π») |
12 | | simplr 767 |
. . . . . . 7
β’ (((π = πΆ β§ π = π΅) β§ β = π») β π = π΅) |
13 | | simpr 485 |
. . . . . . . . 9
β’ (((π = πΆ β§ π = π΅) β§ β = π») β β = π») |
14 | 13 | oveqd 7368 |
. . . . . . . 8
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (π₯βπ¦) = (π₯π»π¦)) |
15 | 13 | oveqd 7368 |
. . . . . . . . . . . 12
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (π§βπ₯) = (π§π»π₯)) |
16 | | simpll 765 |
. . . . . . . . . . . . . . . 16
β’ (((π = πΆ β§ π = π΅) β§ β = π») β π = πΆ) |
17 | 16 | fveq2d 6843 |
. . . . . . . . . . . . . . 15
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (compβπ) = (compβπΆ)) |
18 | | ismon.o |
. . . . . . . . . . . . . . 15
β’ Β· =
(compβπΆ) |
19 | 17, 18 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (compβπ) = Β· ) |
20 | 19 | oveqd 7368 |
. . . . . . . . . . . . 13
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (β¨π§, π₯β©(compβπ)π¦) = (β¨π§, π₯β© Β· π¦)) |
21 | 20 | oveqd 7368 |
. . . . . . . . . . . 12
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (π(β¨π§, π₯β©(compβπ)π¦)π) = (π(β¨π§, π₯β© Β· π¦)π)) |
22 | 15, 21 | mpteq12dv 5194 |
. . . . . . . . . . 11
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π)) = (π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))) |
23 | 22 | cnveqd 5829 |
. . . . . . . . . 10
β’ (((π = πΆ β§ π = π΅) β§ β = π») β β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π)) = β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))) |
24 | 23 | funeqd 6520 |
. . . . . . . . 9
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (Fun β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π)) β Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π)))) |
25 | 12, 24 | raleqbidv 3317 |
. . . . . . . 8
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (βπ§ β π Fun β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π)) β βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π)))) |
26 | 14, 25 | rabeqbidv 3422 |
. . . . . . 7
β’ (((π = πΆ β§ π = π΅) β§ β = π») β {π β (π₯βπ¦) β£ βπ§ β π Fun β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π))} = {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))}) |
27 | 12, 12, 26 | mpoeq123dv 7426 |
. . . . . 6
β’ (((π = πΆ β§ π = π΅) β§ β = π») β (π₯ β π, π¦ β π β¦ {π β (π₯βπ¦) β£ βπ§ β π Fun β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π))}) = (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))})) |
28 | 7, 11, 27 | csbied2 3893 |
. . . . 5
β’ ((π = πΆ β§ π = π΅) β β¦(Hom βπ) / ββ¦(π₯ β π, π¦ β π β¦ {π β (π₯βπ¦) β£ βπ§ β π Fun β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π))}) = (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))})) |
29 | 3, 6, 28 | csbied2 3893 |
. . . 4
β’ (π = πΆ β β¦(Baseβπ) / πβ¦β¦(Hom
βπ) / ββ¦(π₯ β π, π¦ β π β¦ {π β (π₯βπ¦) β£ βπ§ β π Fun β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π))}) = (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))})) |
30 | | df-mon 17573 |
. . . 4
β’ Mono =
(π β Cat β¦
β¦(Baseβπ) / πβ¦β¦(Hom
βπ) / ββ¦(π₯ β π, π¦ β π β¦ {π β (π₯βπ¦) β£ βπ§ β π Fun β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π))})) |
31 | 5 | fvexi 6853 |
. . . . 5
β’ π΅ β V |
32 | 31, 31 | mpoex 8004 |
. . . 4
β’ (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))}) β V |
33 | 29, 30, 32 | fvmpt 6945 |
. . 3
β’ (πΆ β Cat β
(MonoβπΆ) = (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))})) |
34 | 2, 33 | syl 17 |
. 2
β’ (π β (MonoβπΆ) = (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))})) |
35 | 1, 34 | eqtrid 2789 |
1
β’ (π β π = (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))})) |