Metamath Proof Explorer

Theorem pcofval

Description: The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 7-Jun-2014) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Assertion pcofval 
|- ( *p ` J ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = J -> ( II Cn j ) = ( II Cn J ) )
2 eqidd 
 |-  ( j = J -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) )
3 1 1 2 mpoeq123dv 
 |-  ( j = J -> ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) )
4 df-pco 
 |-  *p = ( j e. Top |-> ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) )
5 ovex 
 |-  ( II Cn J ) e. _V
6 5 5 mpoex 
 |-  ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) e. _V
7 3 4 6 fvmpt 
 |-  ( J e. Top -> ( *p ` J ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) )
8 4 fvmptndm 
 |-  ( -. J e. Top -> ( *p ` J ) = (/) )
9 cntop2 
 |-  ( f e. ( II Cn J ) -> J e. Top )
10 9 con3i 
 |-  ( -. J e. Top -> -. f e. ( II Cn J ) )
11 10 eq0rdv 
 |-  ( -. J e. Top -> ( II Cn J ) = (/) )
12 11 olcd 
 |-  ( -. J e. Top -> ( ( II Cn J ) = (/) \/ ( II Cn J ) = (/) ) )
13 0mpo0 
 |-  ( ( ( II Cn J ) = (/) \/ ( II Cn J ) = (/) ) -> ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) = (/) )
14 12 13 syl 
 |-  ( -. J e. Top -> ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) = (/) )
15 8 14 eqtr4d 
 |-  ( -. J e. Top -> ( *p ` J ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) )
16 7 15 pm2.61i 
 |-  ( *p ` J ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) )