Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. 2
β’ (π β (BaseβπΆ) = (BaseβπΆ)) |
2 | | eqidd 2734 |
. 2
β’ (π β (Hom βπΆ) = (Hom βπΆ)) |
3 | | eqidd 2734 |
. 2
β’ (π β (compβπΆ) = (compβπΆ)) |
4 | | mndtccat.c |
. . 3
β’ (π β πΆ = (MndToCatβπ)) |
5 | | fvexd 6858 |
. . 3
β’ (π β (MndToCatβπ) β V) |
6 | 4, 5 | eqeltrd 2834 |
. 2
β’ (π β πΆ β V) |
7 | | biid 261 |
. 2
β’ (((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€))) β ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) |
8 | | mndtccat.m |
. . . . 5
β’ (π β π β Mnd) |
9 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
10 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
11 | 9, 10 | mndidcl 18576 |
. . . . 5
β’ (π β Mnd β
(0gβπ)
β (Baseβπ)) |
12 | 8, 11 | syl 17 |
. . . 4
β’ (π β (0gβπ) β (Baseβπ)) |
13 | 12 | adantr 482 |
. . 3
β’ ((π β§ π¦ β (BaseβπΆ)) β (0gβπ) β (Baseβπ)) |
14 | 4 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β (BaseβπΆ)) β πΆ = (MndToCatβπ)) |
15 | 8 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β (BaseβπΆ)) β π β Mnd) |
16 | | eqidd 2734 |
. . . 4
β’ ((π β§ π¦ β (BaseβπΆ)) β (BaseβπΆ) = (BaseβπΆ)) |
17 | | simpr 486 |
. . . 4
β’ ((π β§ π¦ β (BaseβπΆ)) β π¦ β (BaseβπΆ)) |
18 | | eqidd 2734 |
. . . 4
β’ ((π β§ π¦ β (BaseβπΆ)) β (Hom βπΆ) = (Hom βπΆ)) |
19 | 14, 15, 16, 17, 17, 18 | mndtchom 47196 |
. . 3
β’ ((π β§ π¦ β (BaseβπΆ)) β (π¦(Hom βπΆ)π¦) = (Baseβπ)) |
20 | 13, 19 | eleqtrrd 2837 |
. 2
β’ ((π β§ π¦ β (BaseβπΆ)) β (0gβπ) β (π¦(Hom βπΆ)π¦)) |
21 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β πΆ = (MndToCatβπ)) |
22 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π β Mnd) |
23 | | eqidd 2734 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (BaseβπΆ) = (BaseβπΆ)) |
24 | | simpr1l 1231 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π₯ β (BaseβπΆ)) |
25 | | simpr1r 1232 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π¦ β (BaseβπΆ)) |
26 | | eqidd 2734 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (compβπΆ) = (compβπΆ)) |
27 | 21, 22, 23, 24, 25, 25, 26 | mndtcco 47197 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (β¨π₯, π¦β©(compβπΆ)π¦) = (+gβπ)) |
28 | 27 | oveqd 7375 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β ((0gβπ)(β¨π₯, π¦β©(compβπΆ)π¦)π) = ((0gβπ)(+gβπ)π)) |
29 | | simpr31 1264 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π β (π₯(Hom βπΆ)π¦)) |
30 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (Hom βπΆ) = (Hom βπΆ)) |
31 | 21, 22, 23, 24, 25, 30 | mndtchom 47196 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π₯(Hom βπΆ)π¦) = (Baseβπ)) |
32 | 29, 31 | eleqtrd 2836 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π β (Baseβπ)) |
33 | | eqid 2733 |
. . . . 5
β’
(+gβπ) = (+gβπ) |
34 | 9, 33, 10 | mndlid 18581 |
. . . 4
β’ ((π β Mnd β§ π β (Baseβπ)) β
((0gβπ)(+gβπ)π) = π) |
35 | 22, 32, 34 | syl2anc 585 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β ((0gβπ)(+gβπ)π) = π) |
36 | 28, 35 | eqtrd 2773 |
. 2
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β ((0gβπ)(β¨π₯, π¦β©(compβπΆ)π¦)π) = π) |
37 | | simpr2l 1233 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π§ β (BaseβπΆ)) |
38 | 21, 22, 23, 25, 25, 37, 26 | mndtcco 47197 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (β¨π¦, π¦β©(compβπΆ)π§) = (+gβπ)) |
39 | 38 | oveqd 7375 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π(β¨π¦, π¦β©(compβπΆ)π§)(0gβπ)) = (π(+gβπ)(0gβπ))) |
40 | | simpr32 1265 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π β (π¦(Hom βπΆ)π§)) |
41 | 21, 22, 23, 25, 37, 30 | mndtchom 47196 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π¦(Hom βπΆ)π§) = (Baseβπ)) |
42 | 40, 41 | eleqtrd 2836 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π β (Baseβπ)) |
43 | 9, 33, 10 | mndrid 18582 |
. . . 4
β’ ((π β Mnd β§ π β (Baseβπ)) β (π(+gβπ)(0gβπ)) = π) |
44 | 22, 42, 43 | syl2anc 585 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π(+gβπ)(0gβπ)) = π) |
45 | 39, 44 | eqtrd 2773 |
. 2
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π(β¨π¦, π¦β©(compβπΆ)π§)(0gβπ)) = π) |
46 | 9, 33 | mndcl 18569 |
. . . 4
β’ ((π β Mnd β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π(+gβπ)π) β (Baseβπ)) |
47 | 22, 42, 32, 46 | syl3anc 1372 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π(+gβπ)π) β (Baseβπ)) |
48 | 21, 22, 23, 24, 25, 37, 26 | mndtcco 47197 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (β¨π₯, π¦β©(compβπΆ)π§) = (+gβπ)) |
49 | 48 | oveqd 7375 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) = (π(+gβπ)π)) |
50 | 21, 22, 23, 24, 37, 30 | mndtchom 47196 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π₯(Hom βπΆ)π§) = (Baseβπ)) |
51 | 47, 49, 50 | 3eltr4d 2849 |
. 2
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(Hom βπΆ)π§)) |
52 | | simpr33 1266 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π β (π§(Hom βπΆ)π€)) |
53 | | simpr2r 1234 |
. . . . . 6
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π€ β (BaseβπΆ)) |
54 | 21, 22, 23, 37, 53, 30 | mndtchom 47196 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π§(Hom βπΆ)π€) = (Baseβπ)) |
55 | 52, 54 | eleqtrd 2836 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π β (Baseβπ)) |
56 | 9, 33 | mndass 18570 |
. . . 4
β’ ((π β Mnd β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π(+gβπ)π)(+gβπ)π) = (π(+gβπ)(π(+gβπ)π))) |
57 | 22, 55, 42, 32, 56 | syl13anc 1373 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β ((π(+gβπ)π)(+gβπ)π) = (π(+gβπ)(π(+gβπ)π))) |
58 | 21, 22, 23, 24, 25, 53, 26 | mndtcco 47197 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (β¨π₯, π¦β©(compβπΆ)π€) = (+gβπ)) |
59 | 21, 22, 23, 25, 37, 53, 26 | mndtcco 47197 |
. . . . 5
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (β¨π¦, π§β©(compβπΆ)π€) = (+gβπ)) |
60 | 59 | oveqd 7375 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π(β¨π¦, π§β©(compβπΆ)π€)π) = (π(+gβπ)π)) |
61 | | eqidd 2734 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π = π) |
62 | 58, 60, 61 | oveq123d 7379 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β ((π(β¨π¦, π§β©(compβπΆ)π€)π)(β¨π₯, π¦β©(compβπΆ)π€)π) = ((π(+gβπ)π)(+gβπ)π)) |
63 | 21, 22, 23, 24, 37, 53, 26 | mndtcco 47197 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (β¨π₯, π§β©(compβπΆ)π€) = (+gβπ)) |
64 | | eqidd 2734 |
. . . 4
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β π = π) |
65 | 63, 64, 49 | oveq123d 7379 |
. . 3
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β (π(β¨π₯, π§β©(compβπΆ)π€)(π(β¨π₯, π¦β©(compβπΆ)π§)π)) = (π(+gβπ)(π(+gβπ)π))) |
66 | 57, 62, 65 | 3eqtr4d 2783 |
. 2
β’ ((π β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§) β§ π β (π§(Hom βπΆ)π€)))) β ((π(β¨π¦, π§β©(compβπΆ)π€)π)(β¨π₯, π¦β©(compβπΆ)π€)π) = (π(β¨π₯, π§β©(compβπΆ)π€)(π(β¨π₯, π¦β©(compβπΆ)π§)π))) |
67 | 1, 2, 3, 6, 7, 20,
36, 45, 51, 66 | iscatd2 17566 |
1
β’ (π β (πΆ β Cat β§ (IdβπΆ) = (π¦ β (BaseβπΆ) β¦ (0gβπ)))) |