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 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
pcoval.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
pcoval2.4 ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
Assertion pcocn ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ∈ ( II Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 pcoval.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
2 pcoval.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
3 pcoval2.4 ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
4 1 2 pcoval ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
5 iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
6 5 a1i ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
7 6 cnmptid ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( II Cn II ) )
8 0elunit 0 ∈ ( 0 [,] 1 )
9 8 a1i ( 𝜑 → 0 ∈ ( 0 [,] 1 ) )
10 6 6 9 cnmptc ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 0 ) ∈ ( 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 ∈ ℝ
16 15 a1i ( 𝜑 → 0 ∈ ℝ )
17 1re 1 ∈ ℝ
18 17 a1i ( 𝜑 → 1 ∈ ℝ )
19 halfre ( 1 / 2 ) ∈ ℝ
20 halfge0 0 ≤ ( 1 / 2 )
21 halflt1 ( 1 / 2 ) < 1
22 19 17 21 ltleii ( 1 / 2 ) ≤ 1
23 elicc01 ( ( 1 / 2 ) ∈ ( 0 [,] 1 ) ↔ ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 1 ) )
24 19 20 22 23 mpbir3an ( 1 / 2 ) ∈ ( 0 [,] 1 )
25 24 a1i ( 𝜑 → ( 1 / 2 ) ∈ ( 0 [,] 1 ) )
26 3 adantr ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
27 simprl ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → 𝑦 = ( 1 / 2 ) )
28 27 oveq2d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑦 ) = ( 2 · ( 1 / 2 ) ) )
29 2cn 2 ∈ ℂ
30 2ne0 2 ≠ 0
31 29 30 recidi ( 2 · ( 1 / 2 ) ) = 1
32 28 31 eqtrdi ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑦 ) = 1 )
33 32 fveq2d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( 2 · 𝑦 ) ) = ( 𝐹 ‘ 1 ) )
34 32 oveq1d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑦 ) − 1 ) = ( 1 − 1 ) )
35 1m1e0 ( 1 − 1 ) = 0
36 34 35 eqtrdi ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑦 ) − 1 ) = 0 )
37 36 fveq2d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) = ( 𝐺 ‘ 0 ) )
38 26 33 37 3eqtr4d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( 2 · 𝑦 ) ) = ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) )
39 retopon ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
40 iccssre ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
41 15 19 40 mp2an ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
42 resttopon ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
43 39 41 42 mp2an ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) )
44 43 a1i ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
45 44 6 cnmpt1st ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ) )
46 12 iihalf1cn ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
47 46 a1i ( 𝜑 → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
48 oveq2 ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
49 44 6 45 44 47 48 cnmpt21 ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 2 · 𝑦 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn II ) )
50 44 6 49 1 cnmpt21f ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 2 · 𝑦 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn 𝐽 ) )
51 iccssre ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
52 19 17 51 mp2an ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ
53 resttopon ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
54 39 52 53 mp2an ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) )
55 54 a1i ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
56 55 6 cnmpt1st ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ) )
57 13 iihalf2cn ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
58 57 a1i ( 𝜑 → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
59 48 oveq1d ( 𝑥 = 𝑦 → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
60 55 6 56 55 58 59 cnmpt21 ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn II ) )
61 55 6 60 2 cnmpt21f ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn 𝐽 ) )
62 11 12 13 14 16 18 25 6 38 50 61 cnmpopc ( 𝜑 → ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑦 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
63 breq1 ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 1 / 2 ) ↔ 𝑥 ≤ ( 1 / 2 ) ) )
64 oveq2 ( 𝑦 = 𝑥 → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) )
65 64 fveq2d ( 𝑦 = 𝑥 → ( 𝐹 ‘ ( 2 · 𝑦 ) ) = ( 𝐹 ‘ ( 2 · 𝑥 ) ) )
66 64 oveq1d ( 𝑦 = 𝑥 → ( ( 2 · 𝑦 ) − 1 ) = ( ( 2 · 𝑥 ) − 1 ) )
67 66 fveq2d ( 𝑦 = 𝑥 → ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) = ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
68 63 65 67 ifbieq12d ( 𝑦 = 𝑥 → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑦 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
69 68 adantr ( ( 𝑦 = 𝑥𝑧 = 0 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑦 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
70 6 7 10 6 6 62 69 cnmpt12 ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ∈ ( II Cn 𝐽 ) )
71 4 70 eqeltrd ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ∈ ( II Cn 𝐽 ) )