This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( comf ` C )
comfffval.b 
|- B = ( Base ` C )
comfffval.h 
|- H = ( Hom ` C )
comfffval.x 
|- .x. = ( comp ` C )
Assertion comfffval 
|- O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) )

Proof

Step Hyp Ref Expression
1 comfffval.o 
 |-  O = ( comf ` C )
2 comfffval.b 
 |-  B = ( Base ` C )
3 comfffval.h 
 |-  H = ( Hom ` C )
4 comfffval.x 
 |-  .x. = ( comp ` C )
5 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
6 5 2 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
7 6 sqxpeqd 
 |-  ( c = C -> ( ( Base ` c ) X. ( Base ` c ) ) = ( B X. B ) )
8 fveq2 
 |-  ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
9 8 3 eqtr4di 
 |-  ( c = C -> ( Hom ` c ) = H )
10 9 oveqd 
 |-  ( c = C -> ( ( 2nd ` x ) ( Hom ` c ) y ) = ( ( 2nd ` x ) H y ) )
11 9 fveq1d 
 |-  ( c = C -> ( ( Hom ` c ) ` x ) = ( H ` x ) )
12 fveq2 
 |-  ( c = C -> ( comp ` c ) = ( comp ` C ) )
13 12 4 eqtr4di 
 |-  ( c = C -> ( comp ` c ) = .x. )
14 13 oveqd 
 |-  ( c = C -> ( x ( comp ` c ) y ) = ( x .x. y ) )
15 14 oveqd 
 |-  ( c = C -> ( g ( x ( comp ` c ) y ) f ) = ( g ( x .x. y ) f ) )
16 10 11 15 mpoeq123dv 
 |-  ( c = C -> ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x ( comp ` c ) y ) f ) ) = ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) )
17 7 6 16 mpoeq123dv 
 |-  ( c = C -> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) , y e. ( Base ` c ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x ( comp ` c ) y ) f ) ) ) = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) ) )
18 df-comf 
 |-  comf = ( c e. _V |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) , y e. ( Base ` c ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x ( comp ` c ) y ) f ) ) ) )
19 2 fvexi 
 |-  B e. _V
20 19 19 xpex 
 |-  ( B X. B ) e. _V
21 20 19 mpoex 
 |-  ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) ) e. _V
22 17 18 21 fvmpt 
 |-  ( C e. _V -> ( comf ` C ) = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) ) )
23 fvprc 
 |-  ( -. C e. _V -> ( comf ` C ) = (/) )
24 fvprc 
 |-  ( -. C e. _V -> ( Base ` C ) = (/) )
25 2 24 eqtrid 
 |-  ( -. C e. _V -> B = (/) )
26 25 olcd 
 |-  ( -. C e. _V -> ( ( B X. B ) = (/) \/ B = (/) ) )
27 0mpo0 
 |-  ( ( ( B X. B ) = (/) \/ B = (/) ) -> ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) ) = (/) )
28 26 27 syl 
 |-  ( -. C e. _V -> ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) ) = (/) )
29 23 28 eqtr4d 
 |-  ( -. C e. _V -> ( comf ` C ) = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) ) )
30 22 29 pm2.61i 
 |-  ( comf ` C ) = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) )
31 1 30 eqtri 
 |-  O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) )