Metamath Proof Explorer

Theorem coaval

Description: Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homdmcoa.o 
|- .x. = ( compA ` C )
homdmcoa.h 
|- H = ( HomA ` C )
homdmcoa.f 
|- ( ph -> F e. ( X H Y ) )
homdmcoa.g 
|- ( ph -> G e. ( Y H Z ) )
coaval.x 
|- .xb = ( comp ` C )
Assertion coaval 
|- ( ph -> ( G .x. F ) = <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. )

Proof

Step Hyp Ref Expression
1 homdmcoa.o 
 |-  .x. = ( compA ` C )
2 homdmcoa.h 
 |-  H = ( HomA ` C )
3 homdmcoa.f 
 |-  ( ph -> F e. ( X H Y ) )
4 homdmcoa.g 
 |-  ( ph -> G e. ( Y H Z ) )
5 coaval.x 
 |-  .xb = ( comp ` C )
6 eqid 
 |-  ( Arrow ` C ) = ( Arrow ` C )
7 1 6 5 coafval 
 |-  .x. = ( g e. ( Arrow ` C ) , f e. { h e. ( Arrow ` C ) | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. )
8 6 2 homarw 
 |-  ( Y H Z ) C_ ( Arrow ` C )
9 8 4 sseldi 
 |-  ( ph -> G e. ( Arrow ` C ) )
10 fveqeq2 
 |-  ( h = F -> ( ( codA ` h ) = ( domA ` g ) <-> ( codA ` F ) = ( domA ` g ) ) )
11 6 2 homarw 
 |-  ( X H Y ) C_ ( Arrow ` C )
12 3 adantr 
 |-  ( ( ph /\ g = G ) -> F e. ( X H Y ) )
13 11 12 sseldi 
 |-  ( ( ph /\ g = G ) -> F e. ( Arrow ` C ) )
14 2 homacd 
 |-  ( F e. ( X H Y ) -> ( codA ` F ) = Y )
15 12 14 syl 
 |-  ( ( ph /\ g = G ) -> ( codA ` F ) = Y )
16 simpr 
 |-  ( ( ph /\ g = G ) -> g = G )
17 16 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( domA ` g ) = ( domA ` G ) )
18 4 adantr 
 |-  ( ( ph /\ g = G ) -> G e. ( Y H Z ) )
19 2 homadm 
 |-  ( G e. ( Y H Z ) -> ( domA ` G ) = Y )
20 18 19 syl 
 |-  ( ( ph /\ g = G ) -> ( domA ` G ) = Y )
21 17 20 eqtrd 
 |-  ( ( ph /\ g = G ) -> ( domA ` g ) = Y )
22 15 21 eqtr4d 
 |-  ( ( ph /\ g = G ) -> ( codA ` F ) = ( domA ` g ) )
23 10 13 22 elrabd 
 |-  ( ( ph /\ g = G ) -> F e. { h e. ( Arrow ` C ) | ( codA ` h ) = ( domA ` g ) } )
24 otex 
 |-  <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. e. _V
25 24 a1i 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. e. _V )
26 simprr 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> f = F )
27 26 fveq2d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( domA ` f ) = ( domA ` F ) )
28 2 homadm 
 |-  ( F e. ( X H Y ) -> ( domA ` F ) = X )
29 12 28 syl 
 |-  ( ( ph /\ g = G ) -> ( domA ` F ) = X )
30 29 adantrr 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( domA ` F ) = X )
31 27 30 eqtrd 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( domA ` f ) = X )
32 16 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( codA ` g ) = ( codA ` G ) )
33 2 homacd 
 |-  ( G e. ( Y H Z ) -> ( codA ` G ) = Z )
34 18 33 syl 
 |-  ( ( ph /\ g = G ) -> ( codA ` G ) = Z )
35 32 34 eqtrd 
 |-  ( ( ph /\ g = G ) -> ( codA ` g ) = Z )
36 35 adantrr 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( codA ` g ) = Z )
37 21 adantrr 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( domA ` g ) = Y )
38 31 37 opeq12d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> <. ( domA ` f ) , ( domA ` g ) >. = <. X , Y >. )
39 38 36 oveq12d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) = ( <. X , Y >. .xb Z ) )
40 simprl 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> g = G )
41 40 fveq2d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( 2nd ` g ) = ( 2nd ` G ) )
42 26 fveq2d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( 2nd ` f ) = ( 2nd ` F ) )
43 39 41 42 oveq123d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) = ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) )
44 31 36 43 oteq123d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. = <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. )
45 9 23 25 44 ovmpodv2 
 |-  ( ph -> ( .x. = ( g e. ( Arrow ` C ) , f e. { h e. ( Arrow ` C ) | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) -> ( G .x. F ) = <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. ) )
46 7 45 mpi 
 |-  ( ph -> ( G .x. F ) = <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. )