Metamath Proof Explorer

Theorem pcocn

Description: The concatenation of two paths is a path. (Contributed by Jeff Madsen, 19-Jun-2010) (Proof shortened by Mario Carneiro, 7-Jun-2014)

Ref Expression
Hypotheses pcoval.2 
|- ( ph -> F e. ( II Cn J ) )
pcoval.3 
|- ( ph -> G e. ( II Cn J ) )
pcoval2.4 
|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )
Assertion pcocn 
|- ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )

Proof

Step Hyp Ref Expression
1 pcoval.2 
 |-  ( ph -> F e. ( II Cn J ) )
2 pcoval.3 
 |-  ( ph -> G e. ( II Cn J ) )
3 pcoval2.4 
 |-  ( ph -> ( F ` 1 ) = ( G ` 0 ) )
4 1 2 pcoval 
 |-  ( ph -> ( F ( *p ` J ) G ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) )
5 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
6 5 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
7 6 cnmptid 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn II ) )
8 0elunit 
 |-  0 e. ( 0 [,] 1 )
9 8 a1i 
 |-  ( ph -> 0 e. ( 0 [,] 1 ) )
10 6 6 9 cnmptc 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> 0 ) e. ( II Cn II ) )
11 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
12 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) )
13 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) )
14 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
15 0re 
 |-  0 e. RR
16 15 a1i 
 |-  ( ph -> 0 e. RR )
17 1re 
 |-  1 e. RR
18 17 a1i 
 |-  ( ph -> 1 e. RR )
19 halfre 
 |-  ( 1 / 2 ) e. RR
20 halfge0 
 |-  0 <_ ( 1 / 2 )
21 halflt1 
 |-  ( 1 / 2 ) < 1
22 19 17 21 ltleii 
 |-  ( 1 / 2 ) <_ 1
23 elicc01 
 |-  ( ( 1 / 2 ) e. ( 0 [,] 1 ) <-> ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ 1 ) )
24 19 20 22 23 mpbir3an 
 |-  ( 1 / 2 ) e. ( 0 [,] 1 )
25 24 a1i 
 |-  ( ph -> ( 1 / 2 ) e. ( 0 [,] 1 ) )
26 3 adantr 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( F ` 1 ) = ( G ` 0 ) )
27 simprl 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> y = ( 1 / 2 ) )
28 27 oveq2d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = ( 2 x. ( 1 / 2 ) ) )
29 2cn 
 |-  2 e. CC
30 2ne0 
 |-  2 =/= 0
31 29 30 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
32 28 31 eqtrdi 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = 1 )
33 32 fveq2d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( F ` ( 2 x. y ) ) = ( F ` 1 ) )
34 32 oveq1d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. y ) - 1 ) = ( 1 - 1 ) )
35 1m1e0 
 |-  ( 1 - 1 ) = 0
36 34 35 eqtrdi 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. y ) - 1 ) = 0 )
37 36 fveq2d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( G ` ( ( 2 x. y ) - 1 ) ) = ( G ` 0 ) )
38 26 33 37 3eqtr4d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( F ` ( 2 x. y ) ) = ( G ` ( ( 2 x. y ) - 1 ) ) )
39 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
40 iccssre 
 |-  ( ( 0 e. RR /\ ( 1 / 2 ) e. RR ) -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
41 15 19 40 mp2an 
 |-  ( 0 [,] ( 1 / 2 ) ) C_ RR
42 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( 0 [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
43 39 41 42 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) )
44 43 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
45 44 6 cnmpt1st 
 |-  ( ph -> ( y e. ( 0 [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) ) )
46 12 iihalf1cn 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
47 46 a1i 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
48 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
49 44 6 45 44 47 48 cnmpt21 
 |-  ( ph -> ( y e. ( 0 [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> ( 2 x. y ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
50 44 6 49 1 cnmpt21f 
 |-  ( ph -> ( y e. ( 0 [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> ( F ` ( 2 x. y ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn J ) )
51 iccssre 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
52 19 17 51 mp2an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ RR
53 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( 1 / 2 ) [,] 1 ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
54 39 52 53 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) )
55 54 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
56 55 6 cnmpt1st 
 |-  ( ph -> ( y e. ( ( 1 / 2 ) [,] 1 ) , z e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) ) )
57 13 iihalf2cn 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
58 57 a1i 
 |-  ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
59 48 oveq1d 
 |-  ( x = y -> ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) )
60 55 6 56 55 58 59 cnmpt21 
 |-  ( ph -> ( y e. ( ( 1 / 2 ) [,] 1 ) , z e. ( 0 [,] 1 ) |-> ( ( 2 x. y ) - 1 ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn II ) )
61 55 6 60 2 cnmpt21f 
 |-  ( ph -> ( y e. ( ( 1 / 2 ) [,] 1 ) , z e. ( 0 [,] 1 ) |-> ( G ` ( ( 2 x. y ) - 1 ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn J ) )
62 11 12 13 14 16 18 25 6 38 50 61 cnmpopc 
 |-  ( ph -> ( y e. ( 0 [,] 1 ) , z e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( F ` ( 2 x. y ) ) , ( G ` ( ( 2 x. y ) - 1 ) ) ) ) e. ( ( II tX II ) Cn J ) )
63 breq1 
 |-  ( y = x -> ( y <_ ( 1 / 2 ) <-> x <_ ( 1 / 2 ) ) )
64 oveq2 
 |-  ( y = x -> ( 2 x. y ) = ( 2 x. x ) )
65 64 fveq2d 
 |-  ( y = x -> ( F ` ( 2 x. y ) ) = ( F ` ( 2 x. x ) ) )
66 64 oveq1d 
 |-  ( y = x -> ( ( 2 x. y ) - 1 ) = ( ( 2 x. x ) - 1 ) )
67 66 fveq2d 
 |-  ( y = x -> ( G ` ( ( 2 x. y ) - 1 ) ) = ( G ` ( ( 2 x. x ) - 1 ) ) )
68 63 65 67 ifbieq12d 
 |-  ( y = x -> if ( y <_ ( 1 / 2 ) , ( F ` ( 2 x. y ) ) , ( G ` ( ( 2 x. y ) - 1 ) ) ) = if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) )
69 68 adantr 
 |-  ( ( y = x /\ z = 0 ) -> if ( y <_ ( 1 / 2 ) , ( F ` ( 2 x. y ) ) , ( G ` ( ( 2 x. y ) - 1 ) ) ) = if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) )
70 6 7 10 6 6 62 69 cnmpt12 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) e. ( II Cn J ) )
71 4 70 eqeltrd 
 |-  ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )