MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pco Unicode version

Definition df-pco 18497
Description: Define the concatenation of two paths in a topological space 
J. For simplicity of definition, we define it on all paths, not just those whose endpoints line up. Definition of [Hatcher] p. 26. Hatcher denotes path concatenation with a square dot; other authors, such as Munkres, use a star. (Contributed by Jeff Madsen, 15-Jun-2010.)
Assertion
Ref Expression
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 ) ) ) ) ) )
Distinct variable group:    f, g, j, x

Detailed syntax breakdown of Definition df-pco
StepHypRef Expression
1 cpco 18492 . 2  class  *p
2 vj . . 3  set  j
3 ctop 16625 . . 3  class  Top
4 vf . . . 4  set  f
5 vg . . . 4  set  g
6 cii 18373 . . . . 5  class  II
72cv 1627 . . . . 5  class  j
8 ccn 16948 . . . . 5  class  Cn
96, 7, 8co 5819 . . . 4  class  ( II 
Cn  j )
10 vx . . . . 5  set  x
11 cc0 8732 . . . . . 6  class  0
12 c1 8733 . . . . . 6  class  1
13 cicc 10653 . . . . . 6  class  [,]
1411, 12, 13co 5819 . . . . 5  class  ( 0 [,] 1 )
1510cv 1627 . . . . . . 7  class  x
16 c2 9790 . . . . . . . 8  class  2
17 cdiv 9418 . . . . . . . 8  class  /
1812, 16, 17co 5819 . . . . . . 7  class  ( 1  /  2 )
19 cle 8863 . . . . . . 7  class  <_
2015, 18, 19wbr 4024 . . . . . 6  wff  x  <_ 
( 1  /  2
)
21 cmul 8737 . . . . . . . 8  class  x.
2216, 15, 21co 5819 . . . . . . 7  class  ( 2  x.  x )
234cv 1627 . . . . . . 7  class  f
2422, 23cfv 5221 . . . . . 6  class  ( f `
 ( 2  x.  x ) )
25 cmin 9032 . . . . . . . 8  class  -
2622, 12, 25co 5819 . . . . . . 7  class  ( ( 2  x.  x )  -  1 )
275cv 1627 . . . . . . 7  class  g
2826, 27cfv 5221 . . . . . 6  class  ( g `
 ( ( 2  x.  x )  - 
1 ) )
2920, 24, 28cif 3566 . . . . 5  class  if ( x  <_  ( 1  /  2 ) ,  ( f `  (
2  x.  x ) ) ,  ( g `
 ( ( 2  x.  x )  - 
1 ) ) )
3010, 14, 29cmpt 4078 . . . 4  class  ( x  e.  ( 0 [,] 1 )  |->  if ( x  <_  ( 1  /  2 ) ,  ( f `  (
2  x.  x ) ) ,  ( g `
 ( ( 2  x.  x )  - 
1 ) ) ) )
314, 5, 9, 9, 30cmpt2 5821 . . 3  class  ( 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 ) ) ) ) )
322, 3, 31cmpt 4078 . 2  class  ( 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 ) ) ) ) ) )
331, 32wceq 1628 1  wff  *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 ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  pcofval  18502
  Copyright terms: Public domain W3C validator