Metamath Proof Explorer


Theorem comfffval2

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfffval2.o O=comp𝑓C
comfffval2.b B=BaseC
comfffval2.h H=Hom𝑓C
comfffval2.x ·˙=compC
Assertion comfffval2 O=xB×B,yBg2ndxHy,fHxgx·˙yf

Proof

Step Hyp Ref Expression
1 comfffval2.o O=comp𝑓C
2 comfffval2.b B=BaseC
3 comfffval2.h H=Hom𝑓C
4 comfffval2.x ·˙=compC
5 eqid HomC=HomC
6 1 2 5 4 comfffval O=xB×B,yBg2ndxHomCy,fHomCxgx·˙yf
7 xp2nd xB×B2ndxB
8 7 adantr xB×ByB2ndxB
9 simpr xB×ByByB
10 3 2 5 8 9 homfval xB×ByB2ndxHy=2ndxHomCy
11 xp1st xB×B1stxB
12 11 adantr xB×ByB1stxB
13 3 2 5 12 8 homfval xB×ByB1stxH2ndx=1stxHomC2ndx
14 df-ov 1stxH2ndx=H1stx2ndx
15 df-ov 1stxHomC2ndx=HomC1stx2ndx
16 13 14 15 3eqtr3g xB×ByBH1stx2ndx=HomC1stx2ndx
17 1st2nd2 xB×Bx=1stx2ndx
18 17 adantr xB×ByBx=1stx2ndx
19 18 fveq2d xB×ByBHx=H1stx2ndx
20 18 fveq2d xB×ByBHomCx=HomC1stx2ndx
21 16 19 20 3eqtr4d xB×ByBHx=HomCx
22 eqidd xB×ByBgx·˙yf=gx·˙yf
23 10 21 22 mpoeq123dv xB×ByBg2ndxHy,fHxgx·˙yf=g2ndxHomCy,fHomCxgx·˙yf
24 23 mpoeq3ia xB×B,yBg2ndxHy,fHxgx·˙yf=xB×B,yBg2ndxHomCy,fHomCxgx·˙yf
25 6 24 eqtr4i O=xB×B,yBg2ndxHy,fHxgx·˙yf