Step | Hyp | Ref
| Expression |
1 | | homdmcoa.o |
. . 3
β’ Β· =
(compaβπΆ) |
2 | | eqid 2726 |
. . 3
β’
(ArrowβπΆ) =
(ArrowβπΆ) |
3 | | coaval.x |
. . 3
β’ β =
(compβπΆ) |
4 | 1, 2, 3 | coafval 18024 |
. 2
β’ Β· =
(π β
(ArrowβπΆ), π β {β β (ArrowβπΆ) β£
(codaββ) = (domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) |
5 | | homdmcoa.h |
. . . . 5
β’ π» =
(HomaβπΆ) |
6 | 2, 5 | homarw 18006 |
. . . 4
β’ (ππ»π) β (ArrowβπΆ) |
7 | | homdmcoa.g |
. . . 4
β’ (π β πΊ β (ππ»π)) |
8 | 6, 7 | sselid 3975 |
. . 3
β’ (π β πΊ β (ArrowβπΆ)) |
9 | | fveqeq2 6893 |
. . . 4
β’ (β = πΉ β ((codaββ) =
(domaβπ) β (codaβπΉ) =
(domaβπ))) |
10 | 2, 5 | homarw 18006 |
. . . . 5
β’ (ππ»π) β (ArrowβπΆ) |
11 | | homdmcoa.f |
. . . . . 6
β’ (π β πΉ β (ππ»π)) |
12 | 11 | adantr 480 |
. . . . 5
β’ ((π β§ π = πΊ) β πΉ β (ππ»π)) |
13 | 10, 12 | sselid 3975 |
. . . 4
β’ ((π β§ π = πΊ) β πΉ β (ArrowβπΆ)) |
14 | 5 | homacd 18001 |
. . . . . 6
β’ (πΉ β (ππ»π) β (codaβπΉ) = π) |
15 | 12, 14 | syl 17 |
. . . . 5
β’ ((π β§ π = πΊ) β (codaβπΉ) = π) |
16 | | simpr 484 |
. . . . . . 7
β’ ((π β§ π = πΊ) β π = πΊ) |
17 | 16 | fveq2d 6888 |
. . . . . 6
β’ ((π β§ π = πΊ) β (domaβπ) =
(domaβπΊ)) |
18 | 7 | adantr 480 |
. . . . . . 7
β’ ((π β§ π = πΊ) β πΊ β (ππ»π)) |
19 | 5 | homadm 18000 |
. . . . . . 7
β’ (πΊ β (ππ»π) β (domaβπΊ) = π) |
20 | 18, 19 | syl 17 |
. . . . . 6
β’ ((π β§ π = πΊ) β (domaβπΊ) = π) |
21 | 17, 20 | eqtrd 2766 |
. . . . 5
β’ ((π β§ π = πΊ) β (domaβπ) = π) |
22 | 15, 21 | eqtr4d 2769 |
. . . 4
β’ ((π β§ π = πΊ) β (codaβπΉ) =
(domaβπ)) |
23 | 9, 13, 22 | elrabd 3680 |
. . 3
β’ ((π β§ π = πΊ) β πΉ β {β β (ArrowβπΆ) β£
(codaββ) = (domaβπ)}) |
24 | | otex 5458 |
. . . 4
β’
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β© β V |
25 | 24 | a1i 11 |
. . 3
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β© β V) |
26 | | simprr 770 |
. . . . . 6
β’ ((π β§ (π = πΊ β§ π = πΉ)) β π = πΉ) |
27 | 26 | fveq2d 6888 |
. . . . 5
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
(domaβπ) = (domaβπΉ)) |
28 | 5 | homadm 18000 |
. . . . . . 7
β’ (πΉ β (ππ»π) β (domaβπΉ) = π) |
29 | 12, 28 | syl 17 |
. . . . . 6
β’ ((π β§ π = πΊ) β (domaβπΉ) = π) |
30 | 29 | adantrr 714 |
. . . . 5
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
(domaβπΉ) = π) |
31 | 27, 30 | eqtrd 2766 |
. . . 4
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
(domaβπ) = π) |
32 | 16 | fveq2d 6888 |
. . . . . 6
β’ ((π β§ π = πΊ) β (codaβπ) =
(codaβπΊ)) |
33 | 5 | homacd 18001 |
. . . . . . 7
β’ (πΊ β (ππ»π) β (codaβπΊ) = π) |
34 | 18, 33 | syl 17 |
. . . . . 6
β’ ((π β§ π = πΊ) β (codaβπΊ) = π) |
35 | 32, 34 | eqtrd 2766 |
. . . . 5
β’ ((π β§ π = πΊ) β (codaβπ) = π) |
36 | 35 | adantrr 714 |
. . . 4
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
(codaβπ) = π) |
37 | 21 | adantrr 714 |
. . . . . . 7
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
(domaβπ) = π) |
38 | 31, 37 | opeq12d 4876 |
. . . . . 6
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
β¨(domaβπ), (domaβπ)β© = β¨π, πβ©) |
39 | 38, 36 | oveq12d 7422 |
. . . . 5
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
(β¨(domaβπ), (domaβπ)β© β
(codaβπ)) = (β¨π, πβ© β π)) |
40 | | simprl 768 |
. . . . . 6
β’ ((π β§ (π = πΊ β§ π = πΉ)) β π = πΊ) |
41 | 40 | fveq2d 6888 |
. . . . 5
β’ ((π β§ (π = πΊ β§ π = πΉ)) β (2nd βπ) = (2nd βπΊ)) |
42 | 26 | fveq2d 6888 |
. . . . 5
β’ ((π β§ (π = πΊ β§ π = πΉ)) β (2nd βπ) = (2nd βπΉ)) |
43 | 39, 41, 42 | oveq123d 7425 |
. . . 4
β’ ((π β§ (π = πΊ β§ π = πΉ)) β ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ)) = ((2nd βπΊ)(β¨π, πβ© β π)(2nd βπΉ))) |
44 | 31, 36, 43 | oteq123d 4883 |
. . 3
β’ ((π β§ (π = πΊ β§ π = πΉ)) β
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β© = β¨π, π, ((2nd βπΊ)(β¨π, πβ© β π)(2nd βπΉ))β©) |
45 | 8, 23, 25, 44 | ovmpodv2 7561 |
. 2
β’ (π β ( Β· = (π β (ArrowβπΆ), π β {β β (ArrowβπΆ) β£
(codaββ) = (domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β© β
(codaβπ))(2nd βπ))β©) β (πΊ Β· πΉ) = β¨π, π, ((2nd βπΊ)(β¨π, πβ© β π)(2nd βπΉ))β©)) |
46 | 4, 45 | mpi 20 |
1
β’ (π β (πΊ Β· πΉ) = β¨π, π, ((2nd βπΊ)(β¨π, πβ© β π)(2nd βπΉ))β©) |