Metamath Proof Explorer


Theorem comfffval

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses comfffval.o O = comp 𝑓 C
comfffval.b B = Base C
comfffval.h H = Hom C
comfffval.x · ˙ = comp C
Assertion comfffval O = x B × B , y B g 2 nd x H y , f H x g x · ˙ y f

Proof

Step Hyp Ref Expression
1 comfffval.o O = comp 𝑓 C
2 comfffval.b B = Base C
3 comfffval.h H = Hom C
4 comfffval.x · ˙ = comp C
5 fveq2 c = C Base c = Base C
6 5 2 syl6eqr c = C Base c = B
7 6 sqxpeqd c = C Base c × Base c = B × B
8 fveq2 c = C Hom c = Hom C
9 8 3 syl6eqr c = C Hom c = H
10 9 oveqd c = C 2 nd x Hom c y = 2 nd x H y
11 9 fveq1d c = C Hom c x = H x
12 fveq2 c = C comp c = comp C
13 12 4 syl6eqr c = C comp c = · ˙
14 13 oveqd c = C x comp c y = x · ˙ y
15 14 oveqd c = C g x comp c y f = g x · ˙ y f
16 10 11 15 mpoeq123dv c = C g 2 nd x Hom c y , f Hom c x g x comp c y f = g 2 nd x H y , f H x g x · ˙ y f
17 7 6 16 mpoeq123dv c = C x Base c × Base c , y Base c g 2 nd x Hom c y , f Hom c x g x comp c y f = x B × B , y B g 2 nd x H y , f H x g x · ˙ y f
18 df-comf comp 𝑓 = c V x Base c × Base c , y Base c g 2 nd x Hom c y , f Hom c x g x comp c y f
19 2 fvexi B V
20 19 19 xpex B × B V
21 20 19 mpoex x B × B , y B g 2 nd x H y , f H x g x · ˙ y f V
22 17 18 21 fvmpt C V comp 𝑓 C = x B × B , y B g 2 nd x H y , f H x g x · ˙ y f
23 fvprc ¬ C V comp 𝑓 C =
24 fvprc ¬ C V Base C =
25 2 24 syl5eq ¬ C V B =
26 25 olcd ¬ C V B × B = B =
27 0mpo0 B × B = B = x B × B , y B g 2 nd x H y , f H x g x · ˙ y f =
28 26 27 syl ¬ C V x B × B , y B g 2 nd x H y , f H x g x · ˙ y f =
29 23 28 eqtr4d ¬ C V comp 𝑓 C = x B × B , y B g 2 nd x H y , f H x g x · ˙ y f
30 22 29 pm2.61i comp 𝑓 C = x B × B , y B g 2 nd x H y , f H x g x · ˙ y f
31 1 30 eqtri O = x B × B , y B g 2 nd x H y , f H x g x · ˙ y f