Step | Hyp | Ref
| Expression |
1 | | funcsetcestrc.s |
. . . . . 6
β’ π = (SetCatβπ) |
2 | | funcsetcestrc.u |
. . . . . . 7
β’ (π β π β WUni) |
3 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β π β WUni) |
4 | | eqid 2737 |
. . . . . 6
β’ (Hom
βπ) = (Hom
βπ) |
5 | | funcsetcestrc.c |
. . . . . . . . . . 11
β’ πΆ = (Baseβπ) |
6 | 1, 2 | setcbas 17971 |
. . . . . . . . . . 11
β’ (π β π = (Baseβπ)) |
7 | 5, 6 | eqtr4id 2796 |
. . . . . . . . . 10
β’ (π β πΆ = π) |
8 | 7 | eleq2d 2824 |
. . . . . . . . 9
β’ (π β (π β πΆ β π β π)) |
9 | 8 | biimpcd 249 |
. . . . . . . 8
β’ (π β πΆ β (π β π β π)) |
10 | 9 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β π β π)) |
11 | 10 | impcom 409 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β π β π) |
12 | 7 | eleq2d 2824 |
. . . . . . . . 9
β’ (π β (π β πΆ β π β π)) |
13 | 12 | biimpcd 249 |
. . . . . . . 8
β’ (π β πΆ β (π β π β π)) |
14 | 13 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β π β π)) |
15 | 14 | impcom 409 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β π β π) |
16 | 1, 3, 4, 11, 15 | setchom 17973 |
. . . . 5
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (π(Hom βπ)π) = (π βm π)) |
17 | 16 | eleq2d 2824 |
. . . 4
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (π» β (π(Hom βπ)π) β π» β (π βm π))) |
18 | 7 | eleq2d 2824 |
. . . . . . . . 9
β’ (π β (π β πΆ β π β π)) |
19 | 18 | biimpcd 249 |
. . . . . . . 8
β’ (π β πΆ β (π β π β π)) |
20 | 19 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β π β π)) |
21 | 20 | impcom 409 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β π β π) |
22 | 1, 3, 4, 15, 21 | setchom 17973 |
. . . . 5
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (π(Hom βπ)π) = (π βm π)) |
23 | 22 | eleq2d 2824 |
. . . 4
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΎ β (π(Hom βπ)π) β πΎ β (π βm π))) |
24 | 17, 23 | anbi12d 632 |
. . 3
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β ((π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π)) β (π» β (π βm π) β§ πΎ β (π βm π)))) |
25 | | elmapi 8794 |
. . . . . . . . 9
β’ (πΎ β (π βm π) β πΎ:πβΆπ) |
26 | | elmapi 8794 |
. . . . . . . . 9
β’ (π» β (π βm π) β π»:πβΆπ) |
27 | | fco 6697 |
. . . . . . . . 9
β’ ((πΎ:πβΆπ β§ π»:πβΆπ) β (πΎ β π»):πβΆπ) |
28 | 25, 26, 27 | syl2anr 598 |
. . . . . . . 8
β’ ((π» β (π βm π) β§ πΎ β (π βm π)) β (πΎ β π»):πβΆπ) |
29 | 28 | adantl 483 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΎ β π»):πβΆπ) |
30 | | elmapg 8785 |
. . . . . . . . . 10
β’ ((π β πΆ β§ π β πΆ) β ((πΎ β π») β (π βm π) β (πΎ β π»):πβΆπ)) |
31 | 30 | ancoms 460 |
. . . . . . . . 9
β’ ((π β πΆ β§ π β πΆ) β ((πΎ β π») β (π βm π) β (πΎ β π»):πβΆπ)) |
32 | 31 | 3adant2 1132 |
. . . . . . . 8
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β ((πΎ β π») β (π βm π) β (πΎ β π»):πβΆπ)) |
33 | 32 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((πΎ β π») β (π βm π) β (πΎ β π»):πβΆπ)) |
34 | 29, 33 | mpbird 257 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΎ β π») β (π βm π)) |
35 | | fvresi 7124 |
. . . . . 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 18054 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ) = ( I βΎ (π βm π))) |
41 | 40 | 3adantr2 1171 |
. . . . . . 7
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (ππΊπ) = ( I βΎ (π βm π))) |
42 | 41 | adantr 482 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (ππΊπ) = ( I βΎ (π βm π))) |
43 | 3 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π β WUni) |
44 | | eqid 2737 |
. . . . . . 7
β’
(compβπ) =
(compβπ) |
45 | 11 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π β π) |
46 | 15 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π β π) |
47 | 21 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π β π) |
48 | 26 | ad2antrl 727 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π»:πβΆπ) |
49 | 25 | ad2antll 728 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β πΎ:πβΆπ) |
50 | 1, 43, 44, 45, 46, 47, 48, 49 | setcco 17976 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΎ(β¨π, πβ©(compβπ)π)π») = (πΎ β π»)) |
51 | 42, 50 | fveq12d 6854 |
. . . . 5
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (( I βΎ (π βm π))β(πΎ β π»))) |
52 | | funcsetcestrc.e |
. . . . . . 7
β’ πΈ = (ExtStrCatβπ) |
53 | | eqid 2737 |
. . . . . . 7
β’
(compβπΈ) =
(compβπΈ) |
54 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18050 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (πΉβπ) β π) |
55 | 54 | 3ad2antr1 1189 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) β π) |
56 | 55 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΉβπ) β π) |
57 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18050 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (πΉβπ) β π) |
58 | 57 | 3ad2antr2 1190 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) β π) |
59 | 58 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΉβπ) β π) |
60 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18050 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (πΉβπ) β π) |
61 | 60 | 3ad2antr3 1191 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) β π) |
62 | 61 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (πΉβπ) β π) |
63 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(πΉβπ)) = (Baseβ(πΉβπ)) |
64 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(πΉβπ)) = (Baseβ(πΉβπ)) |
65 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(πΉβπ)) = (Baseβ(πΉβπ)) |
66 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π) |
67 | | 3simpa 1149 |
. . . . . . . . . . 11
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β πΆ β§ π β πΆ)) |
68 | 67 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (π β πΆ β§ π β πΆ)) |
69 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β π» β (π βm π)) |
70 | 1, 5, 37, 2, 38, 39 | funcsetcestrclem6 18055 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ) β§ π» β (π βm π)) β ((ππΊπ)βπ») = π») |
71 | 66, 68, 69, 70 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)βπ») = π») |
72 | 1, 5, 37 | funcsetcestrclem1 18049 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
73 | 72 | 3ad2antr1 1189 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
74 | 73 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = (Baseβ{β¨(Baseβndx),
πβ©})) |
75 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
76 | 75 | 1strbas 17107 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx),
πβ©})) |
77 | 76 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (Baseβ{β¨(Baseβndx),
πβ©}) = π) |
78 | 77 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
79 | 78 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
80 | 74, 79 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = π) |
81 | 80 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (Baseβ(πΉβπ)) = π) |
82 | 1, 5, 37 | funcsetcestrclem1 18049 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
83 | 82 | 3ad2antr2 1190 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
84 | 83 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = (Baseβ{β¨(Baseβndx),
πβ©})) |
85 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
86 | 85 | 1strbas 17107 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx),
πβ©})) |
87 | 86 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (Baseβ{β¨(Baseβndx),
πβ©}) = π) |
88 | 87 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
89 | 88 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
90 | 84, 89 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = π) |
91 | 90 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (Baseβ(πΉβπ)) = π) |
92 | 71, 81, 91 | feq123d 6662 |
. . . . . . . 8
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπ»):(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ)) β π»:πβΆπ)) |
93 | 48, 92 | mpbird 257 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)βπ»):(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ))) |
94 | | 3simpc 1151 |
. . . . . . . . . . 11
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β (π β πΆ β§ π β πΆ)) |
95 | 94 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (π β πΆ β§ π β πΆ)) |
96 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β πΎ β (π βm π)) |
97 | 1, 5, 37, 2, 38, 39 | funcsetcestrclem6 18055 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ) β§ πΎ β (π βm π)) β ((ππΊπ)βπΎ) = πΎ) |
98 | 66, 95, 96, 97 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)βπΎ) = πΎ) |
99 | 1, 5, 37 | funcsetcestrclem1 18049 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
100 | 99 | 3ad2antr3 1191 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
101 | 100 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = (Baseβ{β¨(Baseβndx),
πβ©})) |
102 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
103 | 102 | 1strbas 17107 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx),
πβ©})) |
104 | 103 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (Baseβ{β¨(Baseβndx),
πβ©}) = π) |
105 | 104 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
β’ ((π β πΆ β§ π β πΆ β§ π β πΆ) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
106 | 105 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β
(Baseβ{β¨(Baseβndx), πβ©}) = π) |
107 | 101, 106 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = π) |
108 | 107 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (Baseβ(πΉβπ)) = π) |
109 | 98, 91, 108 | feq123d 6662 |
. . . . . . . 8
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπΎ):(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ)) β πΎ:πβΆπ)) |
110 | 49, 109 | mpbird 257 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)βπΎ):(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ))) |
111 | 52, 43, 53, 56, 59, 62, 63, 64, 65, 93, 110 | estrcco 18024 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»)) = (((ππΊπ)βπΎ) β ((ππΊπ)βπ»))) |
112 | 98, 71 | coeq12d 5825 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπΎ) β ((ππΊπ)βπ»)) = (πΎ β π»)) |
113 | 111, 112 | eqtrd 2777 |
. . . . 5
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»)) = (πΎ β π»)) |
114 | 36, 51, 113 | 3eqtr4d 2787 |
. . . 4
β’ (((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β§ (π» β (π βm π) β§ πΎ β (π βm π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»))) |
115 | 114 | ex 414 |
. . 3
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β ((π» β (π βm π) β§ πΎ β (π βm π)) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»)))) |
116 | 24, 115 | sylbid 239 |
. 2
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ)) β ((π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π)) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»)))) |
117 | 116 | 3impia 1118 |
1
β’ ((π β§ (π β πΆ β§ π β πΆ β§ π β πΆ) β§ (π» β (π(Hom βπ)π) β§ πΎ β (π(Hom βπ)π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ)π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπΈ)(πΉβπ))((ππΊπ)βπ»))) |