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 𝐽 ) )