Metamath Proof Explorer


Theorem coaval

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

Ref Expression
Hypotheses homdmcoa.o ·˙=compaC
homdmcoa.h H=HomaC
homdmcoa.f φFXHY
homdmcoa.g φGYHZ
coaval.x ˙=compC
Assertion coaval φG·˙F=XZ2ndGXY˙Z2ndF

Proof

Step Hyp Ref Expression
1 homdmcoa.o ·˙=compaC
2 homdmcoa.h H=HomaC
3 homdmcoa.f φFXHY
4 homdmcoa.g φGYHZ
5 coaval.x ˙=compC
6 eqid ArrowC=ArrowC
7 1 6 5 coafval ·˙=gArrowC,fhArrowC|codah=domagdomafcodag2ndgdomafdomag˙codag2ndf
8 6 2 homarw YHZArrowC
9 8 4 sselid φGArrowC
10 fveqeq2 h=Fcodah=domagcodaF=domag
11 6 2 homarw XHYArrowC
12 3 adantr φg=GFXHY
13 11 12 sselid φg=GFArrowC
14 2 homacd FXHYcodaF=Y
15 12 14 syl φg=GcodaF=Y
16 simpr φg=Gg=G
17 16 fveq2d φg=Gdomag=domaG
18 4 adantr φg=GGYHZ
19 2 homadm GYHZdomaG=Y
20 18 19 syl φg=GdomaG=Y
21 17 20 eqtrd φg=Gdomag=Y
22 15 21 eqtr4d φg=GcodaF=domag
23 10 13 22 elrabd φg=GFhArrowC|codah=domag
24 otex domafcodag2ndgdomafdomag˙codag2ndfV
25 24 a1i φg=Gf=Fdomafcodag2ndgdomafdomag˙codag2ndfV
26 simprr φg=Gf=Ff=F
27 26 fveq2d φg=Gf=Fdomaf=domaF
28 2 homadm FXHYdomaF=X
29 12 28 syl φg=GdomaF=X
30 29 adantrr φg=Gf=FdomaF=X
31 27 30 eqtrd φg=Gf=Fdomaf=X
32 16 fveq2d φg=Gcodag=codaG
33 2 homacd GYHZcodaG=Z
34 18 33 syl φg=GcodaG=Z
35 32 34 eqtrd φg=Gcodag=Z
36 35 adantrr φg=Gf=Fcodag=Z
37 21 adantrr φg=Gf=Fdomag=Y
38 31 37 opeq12d φg=Gf=Fdomafdomag=XY
39 38 36 oveq12d φg=Gf=Fdomafdomag˙codag=XY˙Z
40 simprl φg=Gf=Fg=G
41 40 fveq2d φg=Gf=F2ndg=2ndG
42 26 fveq2d φg=Gf=F2ndf=2ndF
43 39 41 42 oveq123d φg=Gf=F2ndgdomafdomag˙codag2ndf=2ndGXY˙Z2ndF
44 31 36 43 oteq123d φg=Gf=Fdomafcodag2ndgdomafdomag˙codag2ndf=XZ2ndGXY˙Z2ndF
45 9 23 25 44 ovmpodv2 φ·˙=gArrowC,fhArrowC|codah=domagdomafcodag2ndgdomafdomag˙codag2ndfG·˙F=XZ2ndGXY˙Z2ndF
46 7 45 mpi φG·˙F=XZ2ndGXY˙Z2ndF