Step | Hyp | Ref
| Expression |
1 | | hofval.m |
. . . 4
β’ π =
(HomFβπΆ) |
2 | | hofval.c |
. . . 4
β’ (π β πΆ β Cat) |
3 | | hof1.b |
. . . 4
β’ π΅ = (BaseβπΆ) |
4 | | hof1.h |
. . . 4
β’ π» = (Hom βπΆ) |
5 | | hof2.o |
. . . 4
β’ Β· =
(compβπΆ) |
6 | 1, 2, 3, 4, 5 | hofval 18101 |
. . 3
β’ (π β π = β¨(Homf
βπΆ), (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))β©) |
7 | | fvex 6852 |
. . . 4
β’
(Homf βπΆ) β V |
8 | 3 | fvexi 6853 |
. . . . . 6
β’ π΅ β V |
9 | 8, 8 | xpex 7679 |
. . . . 5
β’ (π΅ Γ π΅) β V |
10 | 9, 9 | mpoex 8004 |
. . . 4
β’ (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π)))) β V |
11 | 7, 10 | op2ndd 7924 |
. . 3
β’ (π = β¨(Homf
βπΆ), (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))β© β (2nd
βπ) = (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))) |
12 | 6, 11 | syl 17 |
. 2
β’ (π β (2nd
βπ) = (π₯ β (π΅ Γ π΅), π¦ β (π΅ Γ π΅) β¦ (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))))) |
13 | | simprr 771 |
. . . . . 6
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β π¦ = β¨π, πβ©) |
14 | 13 | fveq2d 6843 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (1st βπ¦) = (1st
ββ¨π, πβ©)) |
15 | | hof2.z |
. . . . . . 7
β’ (π β π β π΅) |
16 | | hof2.w |
. . . . . . 7
β’ (π β π β π΅) |
17 | | op1stg 7925 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (1st ββ¨π, πβ©) = π) |
18 | 15, 16, 17 | syl2anc 584 |
. . . . . 6
β’ (π β (1st
ββ¨π, πβ©) = π) |
19 | 18 | adantr 481 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (1st
ββ¨π, πβ©) = π) |
20 | 14, 19 | eqtrd 2777 |
. . . 4
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (1st βπ¦) = π) |
21 | | simprl 769 |
. . . . . 6
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β π₯ = β¨π, πβ©) |
22 | 21 | fveq2d 6843 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (1st βπ₯) = (1st
ββ¨π, πβ©)) |
23 | | hof1.x |
. . . . . . 7
β’ (π β π β π΅) |
24 | | hof1.y |
. . . . . . 7
β’ (π β π β π΅) |
25 | | op1stg 7925 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (1st ββ¨π, πβ©) = π) |
26 | 23, 24, 25 | syl2anc 584 |
. . . . . 6
β’ (π β (1st
ββ¨π, πβ©) = π) |
27 | 26 | adantr 481 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (1st
ββ¨π, πβ©) = π) |
28 | 22, 27 | eqtrd 2777 |
. . . 4
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (1st βπ₯) = π) |
29 | 20, 28 | oveq12d 7369 |
. . 3
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β ((1st
βπ¦)π»(1st βπ₯)) = (ππ»π)) |
30 | 21 | fveq2d 6843 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (2nd βπ₯) = (2nd
ββ¨π, πβ©)) |
31 | | op2ndg 7926 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (2nd ββ¨π, πβ©) = π) |
32 | 23, 24, 31 | syl2anc 584 |
. . . . . 6
β’ (π β (2nd
ββ¨π, πβ©) = π) |
33 | 32 | adantr 481 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (2nd
ββ¨π, πβ©) = π) |
34 | 30, 33 | eqtrd 2777 |
. . . 4
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (2nd βπ₯) = π) |
35 | 13 | fveq2d 6843 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (2nd βπ¦) = (2nd
ββ¨π, πβ©)) |
36 | | op2ndg 7926 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (2nd ββ¨π, πβ©) = π) |
37 | 15, 16, 36 | syl2anc 584 |
. . . . . 6
β’ (π β (2nd
ββ¨π, πβ©) = π) |
38 | 37 | adantr 481 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (2nd
ββ¨π, πβ©) = π) |
39 | 35, 38 | eqtrd 2777 |
. . . 4
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (2nd βπ¦) = π) |
40 | 34, 39 | oveq12d 7369 |
. . 3
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β ((2nd
βπ₯)π»(2nd βπ¦)) = (ππ»π)) |
41 | 21 | fveq2d 6843 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (π»βπ₯) = (π»ββ¨π, πβ©)) |
42 | | df-ov 7354 |
. . . . 5
β’ (ππ»π) = (π»ββ¨π, πβ©) |
43 | 41, 42 | eqtr4di 2795 |
. . . 4
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (π»βπ₯) = (ππ»π)) |
44 | 20, 28 | opeq12d 4836 |
. . . . . 6
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β β¨(1st
βπ¦), (1st
βπ₯)β© =
β¨π, πβ©) |
45 | 44, 39 | oveq12d 7369 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))
= (β¨π, πβ© Β· π)) |
46 | 21, 39 | oveq12d 7369 |
. . . . . 6
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (π₯ Β· (2nd
βπ¦)) = (β¨π, πβ© Β· π)) |
47 | 46 | oveqd 7368 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (π(π₯ Β· (2nd
βπ¦))β) = (π(β¨π, πβ© Β· π)β)) |
48 | | eqidd 2738 |
. . . . 5
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β π = π) |
49 | 45, 47, 48 | oveq123d 7372 |
. . . 4
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π) = ((π(β¨π, πβ© Β· π)β)(β¨π, πβ© Β· π)π)) |
50 | 43, 49 | mpteq12dv 5194 |
. . 3
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π)) = (β β (ππ»π) β¦ ((π(β¨π, πβ© Β· π)β)(β¨π, πβ© Β· π)π))) |
51 | 29, 40, 50 | mpoeq123dv 7426 |
. 2
β’ ((π β§ (π₯ = β¨π, πβ© β§ π¦ = β¨π, πβ©)) β (π β ((1st βπ¦)π»(1st βπ₯)), π β ((2nd βπ₯)π»(2nd βπ¦)) β¦ (β β (π»βπ₯) β¦ ((π(π₯ Β· (2nd
βπ¦))β)(β¨(1st
βπ¦), (1st
βπ₯)β© Β·
(2nd βπ¦))π))) = (π β (ππ»π), π β (ππ»π) β¦ (β β (ππ»π) β¦ ((π(β¨π, πβ© Β· π)β)(β¨π, πβ© Β· π)π)))) |
52 | 23, 24 | opelxpd 5669 |
. 2
β’ (π β β¨π, πβ© β (π΅ Γ π΅)) |
53 | 15, 16 | opelxpd 5669 |
. 2
β’ (π β β¨π, πβ© β (π΅ Γ π΅)) |
54 | | ovex 7384 |
. . . 4
β’ (ππ»π) β V |
55 | | ovex 7384 |
. . . 4
β’ (ππ»π) β V |
56 | 54, 55 | mpoex 8004 |
. . 3
β’ (π β (ππ»π), π β (ππ»π) β¦ (β β (ππ»π) β¦ ((π(β¨π, πβ© Β· π)β)(β¨π, πβ© Β· π)π))) β V |
57 | 56 | a1i 11 |
. 2
β’ (π β (π β (ππ»π), π β (ππ»π) β¦ (β β (ππ»π) β¦ ((π(β¨π, πβ© Β· π)β)(β¨π, πβ© Β· π)π))) β V) |
58 | 12, 51, 52, 53, 57 | ovmpod 7501 |
1
β’ (π β (β¨π, πβ©(2nd βπ)β¨π, πβ©) = (π β (ππ»π), π β (ππ»π) β¦ (β β (ππ»π) β¦ ((π(β¨π, πβ© Β· π)β)(β¨π, πβ© Β· π)π)))) |