Step | Hyp | Ref
| Expression |
1 | | funcsetcestrc.s |
. . . . . 6
β’ π = (SetCatβπ) |
2 | | funcsetcestrc.u |
. . . . . . 7
β’ (π β π β WUni) |
3 | 2 | adantr 479 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β π β WUni) |
4 | | eqid 2730 |
. . . . . 6
β’ (Hom
βπ) = (Hom
βπ) |
5 | | funcsetcestrc.c |
. . . . . . . . . . 11
β’ πΆ = (Baseβπ) |
6 | 1, 2 | setcbas 18034 |
. . . . . . . . . . 11
β’ (π β π = (Baseβπ)) |
7 | 5, 6 | eqtr4id 2789 |
. . . . . . . . . 10
β’ (π β πΆ = π) |
8 | 7 | eleq2d 2817 |
. . . . . . . . 9
β’ (π β (π β πΆ β π β π)) |
9 | 8 | biimpcd 248 |
. . . . . . . 8
β’ (π β πΆ β (π β π β π)) |
10 | 9 | 3ad2ant1 1131 |
. . . . . . 7
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β π β π)) |
11 | 10 | impcom 406 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β π β π) |
12 | 7 | eleq2d 2817 |
. . . . . . . . 9
β’ (π β (π β πΆ β π β π)) |
13 | 12 | biimpcd 248 |
. . . . . . . 8
β’ (π β πΆ β (π β π β π)) |
14 | 13 | 3ad2ant2 1132 |
. . . . . . 7
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β π β π)) |
15 | 14 | impcom 406 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β π β π) |
16 | 1, 3, 4, 11, 15 | setchom 18036 |
. . . . 5
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (π(Hom βπ)π) = (π βm π)) |
17 | 16 | eleq2d 2817 |
. . . 4
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (π» β (π(Hom βπ)π) β π» β (π βm π))) |
18 | 7 | eleq2d 2817 |
. . . . . . . . 9
β’ (π β (π β πΆ β π β π)) |
19 | 18 | biimpcd 248 |
. . . . . . . 8
β’ (π β πΆ β (π β π β π)) |
20 | 19 | 3ad2ant3 1133 |
. . . . . . 7
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β π β π)) |
21 | 20 | impcom 406 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β π β π) |
22 | 1, 3, 4, 15, 21 | setchom 18036 |
. . . . 5
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (π(Hom βπ)π) = (π βm π)) |
23 | 22 | eleq2d 2817 |
. . . 4
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΎ β (π(Hom βπ)π) β πΎ β (π βm π))) |
24 | 17, 23 | anbi12d 629 |
. . 3
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β ((π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π)) β (π» β (π βm π) β§ πΎ β (π βm π)))) |
25 | | elmapi 8847 |
. . . . . . . . 9
β’ (πΎ β (π βm π) β πΎ:πβΆπ) |
26 | | elmapi 8847 |
. . . . . . . . 9
β’ (π» β (π βm π) β π»:πβΆπ) |
27 | | fco 6742 |
. . . . . . . . 9
β’ ((πΎ:πβΆπ β§ π»:πβΆπ) β (πΎ β π»):πβΆπ) |
28 | 25, 26, 27 | syl2anr 595 |
. . . . . . . 8
β’ ((π» β (π βm π) β§ πΎ β (π βm π)) β (πΎ β π»):πβΆπ) |
29 | 28 | adantl 480 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΎ β π»):πβΆπ) |
30 | | elmapg 8837 |
. . . . . . . . . 10
β’ ((π β πΆ β§ π β πΆ) β ((πΎ β π») β (π βm π) β (πΎ β π»):πβΆπ)) |
31 | 30 | ancoms 457 |
. . . . . . . . 9
β’ ((π β πΆ β§ π β πΆ) β ((πΎ β π») β (π βm π) β (πΎ β π»):πβΆπ)) |
32 | 31 | 3adant2 1129 |
. . . . . . . 8
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β ((πΎ β π») β (π βm π) β (πΎ β π»):πβΆπ)) |
33 | 32 | ad2antlr 723 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((πΎ β π») β (π βm π) β (πΎ β π»):πβΆπ)) |
34 | 29, 33 | mpbird 256 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΎ β π») β (π βm π)) |
35 | | fvresi 7174 |
. . . . . 6
β’ ((πΎ β π») β (π βm π) β (( I βΎ (π βm π))β(πΎ β π»)) = (πΎ β π»)) |
36 | 34, 35 | syl 17 |
. . . . 5
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (( I βΎ (π βm π))β(πΎ β π»)) = (πΎ β π»)) |
37 | | funcsetcestrc.f |
. . . . . . . . 9
β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) |
38 | | funcsetcestrc.o |
. . . . . . . . 9
β’ (π β Ο β π) |
39 | | funcsetcestrc.g |
. . . . . . . . 9
β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) |
40 | 1, 5, 37, 2, 38, 39 | funcsetcestrclem5 18117 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ) = ( I βΎ (π βm π))) |
41 | 40 | 3adantr2 1168 |
. . . . . . 7
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (ππΊπ) = ( I βΎ (π βm π))) |
42 | 41 | adantr 479 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (ππΊπ) = ( I βΎ (π βm π))) |
43 | 3 | adantr 479 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π β WUni) |
44 | | eqid 2730 |
. . . . . . 7
β’
(compβπ) =
(compβπ) |
45 | 11 | adantr 479 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π β π) |
46 | 15 | adantr 479 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π β π) |
47 | 21 | adantr 479 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π β π) |
48 | 26 | ad2antrl 724 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π»:πβΆπ) |
49 | 25 | ad2antll 725 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β πΎ:πβΆπ) |
50 | 1, 43, 44, 45, 46, 47, 48, 49 | setcco 18039 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΎ(β¨π, πβ©(compβπ)π)π») = (πΎ β π»)) |
51 | 42, 50 | fveq12d 6899 |
. . . . 5
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (( I βΎ (π βm π))β(πΎ β π»))) |
52 | | funcsetcestrc.e |
. . . . . . 7
β’ πΈ = (ExtStrCatβπ) |
53 | | eqid 2730 |
. . . . . . 7
β’
(compβπΈ) =
(compβπΈ) |
54 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18113 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (πΉβπ) β π) |
55 | 54 | 3ad2antr1 1186 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) β π) |
56 | 55 | adantr 479 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΉβπ) β π) |
57 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18113 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (πΉβπ) β π) |
58 | 57 | 3ad2antr2 1187 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) β π) |
59 | 58 | adantr 479 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΉβπ) β π) |
60 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18113 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (πΉβπ) β π) |
61 | 60 | 3ad2antr3 1188 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) β π) |
62 | 61 | adantr 479 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΉβπ) β π) |
63 | | eqid 2730 |
. . . . . . 7
β’
(Baseβ(πΉβπ)) = (Baseβ(πΉβπ)) |
64 | | eqid 2730 |
. . . . . . 7
β’
(Baseβ(πΉβπ)) = (Baseβ(πΉβπ)) |
65 | | eqid 2730 |
. . . . . . 7
β’
(Baseβ(πΉβπ)) = (Baseβ(πΉβπ)) |
66 | | simpll 763 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π) |
67 | | 3simpa 1146 |
. . . . . . . . . . 11
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β πΆ β§ π β πΆ)) |
68 | 67 | ad2antlr 723 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (π β πΆ β§ π β πΆ)) |
69 | | simprl 767 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π» β (π βm π)) |
70 | 1, 5, 37, 2, 38, 39 | funcsetcestrclem6 18118 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ) β§ π» β (π βm π)) β ((ππΊπ)βπ») = π») |
71 | 66, 68, 69, 70 | syl3anc 1369 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)βπ») = π») |
72 | 1, 5, 37 | funcsetcestrclem1 18112 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
73 | 72 | 3ad2antr1 1186 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
74 | 73 | fveq2d 6896 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = (Baseβ{β¨(Baseβndx),
πβ©})) |
75 | | eqid 2730 |
. . . . . . . . . . . . . . 15
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
76 | 75 | 1strbas 17167 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx),
πβ©})) |
77 | 76 | eqcomd 2736 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (Baseβ{β¨(Baseβndx),
πβ©}) = π) |
78 | 77 | 3ad2ant1 1131 |
. . . . . . . . . . . 12
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
79 | 78 | adantl 480 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
80 | 74, 79 | eqtrd 2770 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = π) |
81 | 80 | adantr 479 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (Baseβ(πΉβπ)) = π) |
82 | 1, 5, 37 | funcsetcestrclem1 18112 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
83 | 82 | 3ad2antr2 1187 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
84 | 83 | fveq2d 6896 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = (Baseβ{β¨(Baseβndx),
πβ©})) |
85 | | eqid 2730 |
. . . . . . . . . . . . . . 15
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
86 | 85 | 1strbas 17167 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx),
πβ©})) |
87 | 86 | eqcomd 2736 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (Baseβ{β¨(Baseβndx),
πβ©}) = π) |
88 | 87 | 3ad2ant2 1132 |
. . . . . . . . . . . 12
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
89 | 88 | adantl 480 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
90 | 84, 89 | eqtrd 2770 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = π) |
91 | 90 | adantr 479 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (Baseβ(πΉβπ)) = π) |
92 | 71, 81, 91 | feq123d 6707 |
. . . . . . . 8
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπ»):(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ)) β π»:πβΆπ)) |
93 | 48, 92 | mpbird 256 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)βπ»):(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ))) |
94 | | 3simpc 1148 |
. . . . . . . . . . 11
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β πΆ β§ π β πΆ)) |
95 | 94 | ad2antlr 723 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (π β πΆ β§ π β πΆ)) |
96 | | simprr 769 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β πΎ β (π βm π)) |
97 | 1, 5, 37, 2, 38, 39 | funcsetcestrclem6 18118 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ) β§ πΎ β (π βm π)) β ((ππΊπ)βπΎ) = πΎ) |
98 | 66, 95, 96, 97 | syl3anc 1369 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)βπΎ) = πΎ) |
99 | 1, 5, 37 | funcsetcestrclem1 18112 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
100 | 99 | 3ad2antr3 1188 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
101 | 100 | fveq2d 6896 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = (Baseβ{β¨(Baseβndx),
πβ©})) |
102 | | eqid 2730 |
. . . . . . . . . . . . . . 15
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
103 | 102 | 1strbas 17167 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx),
πβ©})) |
104 | 103 | eqcomd 2736 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (Baseβ{β¨(Baseβndx),
πβ©}) = π) |
105 | 104 | 3ad2ant3 1133 |
. . . . . . . . . . . 12
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
106 | 105 | adantl 480 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
107 | 101, 106 | eqtrd 2770 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = π) |
108 | 107 | adantr 479 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (Baseβ(πΉβπ)) = π) |
109 | 98, 91, 108 | feq123d 6707 |
. . . . . . . 8
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπΎ):(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ)) β πΎ:πβΆπ)) |
110 | 49, 109 | mpbird 256 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)βπΎ):(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ))) |
111 | 52, 43, 53, 56, 59, 62, 63, 64, 65, 93, 110 | estrcco 18087 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»)) = (((ππΊπ)βπΎ) β ((ππΊπ)βπ»))) |
112 | 98, 71 | coeq12d 5865 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπΎ) β ((ππΊπ)βπ»)) = (πΎ β π»)) |
113 | 111, 112 | eqtrd 2770 |
. . . . 5
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»)) = (πΎ β π»)) |
114 | 36, 51, 113 | 3eqtr4d 2780 |
. . . 4
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»))) |
115 | 114 | ex 411 |
. . 3
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β ((π» β (π βm π) β§ πΎ β (π βm π)) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»)))) |
116 | 24, 115 | sylbid 239 |
. 2
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β ((π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π)) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»)))) |
117 | 116 | 3impia 1115 |
1
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ) β§ (π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»))) |