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 2thalfe1 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
30 28 29 eqtrdi 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = 1 )
31 30 fveq2d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( F ` ( 2 x. y ) ) = ( F ` 1 ) )
32 30 oveq1d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. y ) - 1 ) = ( 1 - 1 ) )
33 1m1e0 
 |-  ( 1 - 1 ) = 0
34 32 33 eqtrdi 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. y ) - 1 ) = 0 )
35 34 fveq2d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( G ` ( ( 2 x. y ) - 1 ) ) = ( G ` 0 ) )
36 26 31 35 3eqtr4d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( F ` ( 2 x. y ) ) = ( G ` ( ( 2 x. y ) - 1 ) ) )
37 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
38 iccssre 
 |-  ( ( 0 e. RR /\ ( 1 / 2 ) e. RR ) -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
39 15 19 38 mp2an 
 |-  ( 0 [,] ( 1 / 2 ) ) C_ RR
40 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( 0 [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
41 37 39 40 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) )
42 41 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
43 42 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 ) ) ) ) )
44 12 iihalf1cn 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
45 44 a1i 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
46 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
47 42 6 43 42 45 46 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 ) )
48 42 6 47 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 ) )
49 iccssre 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
50 19 17 49 mp2an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ RR
51 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( 1 / 2 ) [,] 1 ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
52 37 50 51 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) )
53 52 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
54 53 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 ) ) ) )
55 13 iihalf2cn 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
56 55 a1i 
 |-  ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
57 46 oveq1d 
 |-  ( x = y -> ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) )
58 53 6 54 53 56 57 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 ) )
59 53 6 58 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 ) )
60 11 12 13 14 16 18 25 6 36 48 59 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 ) )
61 breq1 
 |-  ( y = x -> ( y <_ ( 1 / 2 ) <-> x <_ ( 1 / 2 ) ) )
62 oveq2 
 |-  ( y = x -> ( 2 x. y ) = ( 2 x. x ) )
63 62 fveq2d 
 |-  ( y = x -> ( F ` ( 2 x. y ) ) = ( F ` ( 2 x. x ) ) )
64 62 oveq1d 
 |-  ( y = x -> ( ( 2 x. y ) - 1 ) = ( ( 2 x. x ) - 1 ) )
65 64 fveq2d 
 |-  ( y = x -> ( G ` ( ( 2 x. y ) - 1 ) ) = ( G ` ( ( 2 x. x ) - 1 ) ) )
66 61 63 65 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 ) ) ) )
67 66 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 ) ) ) )
68 6 7 10 6 6 60 67 cnmpt12 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( G ` ( ( 2 x. x ) - 1 ) ) ) ) e. ( II Cn J ) )
69 4 68 eqeltrd 
 |-  ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )