Description: Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | homdmcoa.o | |
|
homdmcoa.h | |
||
homdmcoa.f | |
||
homdmcoa.g | |
||
coaval.x | |
||
Assertion | coaval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | homdmcoa.o | |
|
2 | homdmcoa.h | |
|
3 | homdmcoa.f | |
|
4 | homdmcoa.g | |
|
5 | coaval.x | |
|
6 | eqid | |
|
7 | 1 6 5 | coafval | |
8 | 6 2 | homarw | |
9 | 8 4 | sselid | |
10 | fveqeq2 | |
|
11 | 6 2 | homarw | |
12 | 3 | adantr | |
13 | 11 12 | sselid | |
14 | 2 | homacd | |
15 | 12 14 | syl | |
16 | simpr | |
|
17 | 16 | fveq2d | |
18 | 4 | adantr | |
19 | 2 | homadm | |
20 | 18 19 | syl | |
21 | 17 20 | eqtrd | |
22 | 15 21 | eqtr4d | |
23 | 10 13 22 | elrabd | |
24 | otex | |
|
25 | 24 | a1i | |
26 | simprr | |
|
27 | 26 | fveq2d | |
28 | 2 | homadm | |
29 | 12 28 | syl | |
30 | 29 | adantrr | |
31 | 27 30 | eqtrd | |
32 | 16 | fveq2d | |
33 | 2 | homacd | |
34 | 18 33 | syl | |
35 | 32 34 | eqtrd | |
36 | 35 | adantrr | |
37 | 21 | adantrr | |
38 | 31 37 | opeq12d | |
39 | 38 36 | oveq12d | |
40 | simprl | |
|
41 | 40 | fveq2d | |
42 | 26 | fveq2d | |
43 | 39 41 42 | oveq123d | |
44 | 31 36 43 | oteq123d | |
45 | 9 23 25 44 | ovmpodv2 | |
46 | 7 45 | mpi | |