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 = ( comf ` C )
comfffval2.b 
|- B = ( Base ` C )
comfffval2.h 
|- H = ( Homf ` C )
comfffval2.x 
|- .x. = ( comp ` C )
Assertion comfffval2 
|- 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 comfffval2.o 
 |-  O = ( comf ` C )
2 comfffval2.b 
 |-  B = ( Base ` C )
3 comfffval2.h 
 |-  H = ( Homf ` C )
4 comfffval2.x 
 |-  .x. = ( comp ` C )
5 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
6 1 2 5 4 comfffval 
 |-  O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) ( Hom ` C ) y ) , f e. ( ( Hom ` C ) ` x ) |-> ( g ( x .x. y ) f ) ) )
7 xp2nd 
 |-  ( x e. ( B X. B ) -> ( 2nd ` x ) e. B )
8 7 adantr 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( 2nd ` x ) e. B )
9 simpr 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> y e. B )
10 3 2 5 8 9 homfval 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( ( 2nd ` x ) H y ) = ( ( 2nd ` x ) ( Hom ` C ) y ) )
11 xp1st 
 |-  ( x e. ( B X. B ) -> ( 1st ` x ) e. B )
12 11 adantr 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( 1st ` x ) e. B )
13 3 2 5 12 8 homfval 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( ( 1st ` x ) H ( 2nd ` x ) ) = ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
14 df-ov 
 |-  ( ( 1st ` x ) H ( 2nd ` x ) ) = ( H ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
15 df-ov 
 |-  ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) = ( ( Hom ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
16 13 14 15 3eqtr3g 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( H ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) = ( ( Hom ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
17 1st2nd2 
 |-  ( x e. ( B X. B ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
18 17 adantr 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
19 18 fveq2d 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( H ` x ) = ( H ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
20 18 fveq2d 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( ( Hom ` C ) ` x ) = ( ( Hom ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
21 16 19 20 3eqtr4d 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( H ` x ) = ( ( Hom ` C ) ` x ) )
22 eqidd 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( g ( x .x. y ) f ) = ( g ( x .x. y ) f ) )
23 10 21 22 mpoeq123dv 
 |-  ( ( x e. ( B X. B ) /\ y e. B ) -> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) = ( g e. ( ( 2nd ` x ) ( Hom ` C ) y ) , f e. ( ( Hom ` C ) ` x ) |-> ( g ( x .x. y ) f ) ) )
24 23 mpoeq3ia 
 |-  ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) ) = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) ( Hom ` C ) y ) , f e. ( ( Hom ` C ) ` x ) |-> ( g ( x .x. y ) f ) ) )
25 6 24 eqtr4i 
 |-  O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) H y ) , f e. ( H ` x ) |-> ( g ( x .x. y ) f ) ) )