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 2thalfe1 ⊢ ( 2 · ( 1 / 2 ) ) = 1
30 28 29 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑦 ) = 1 )
31 30 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( 2 · 𝑦 ) ) = ( 𝐹 ‘ 1 ) )
32 30 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑦 ) − 1 ) = ( 1 − 1 ) )
33 1m1e0 ⊢ ( 1 − 1 ) = 0
34 32 33 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑦 ) − 1 ) = 0 )
35 34 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) = ( 𝐺 ‘ 0 ) )
36 26 31 35 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( 2 · 𝑦 ) ) = ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) )
37 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
38 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
39 15 19 38 mp2an ⊢ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
40 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
41 37 39 40 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) )
42 41 a1i ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
43 42 6 cnmpt1st ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ) )
44 12 iihalf1cn ⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
45 44 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
46 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
47 42 6 43 42 45 46 cnmpt21 ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 2 · 𝑦 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn II ) )
48 42 6 47 1 cnmpt21f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 2 · 𝑦 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn 𝐽 ) )
49 iccssre ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
50 19 17 49 mp2an ⊢ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ
51 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
52 37 50 51 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) )
53 52 a1i ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
54 53 6 cnmpt1st ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ) )
55 13 iihalf2cn ⊢ ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
56 55 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
57 46 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
58 53 6 54 53 56 57 cnmpt21 ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn II ) )
59 53 6 58 2 cnmpt21f ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn 𝐽 ) )
60 11 12 13 14 16 18 25 6 36 48 59 cnmpopc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑦 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
61 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 1 / 2 ) ↔ 𝑥 ≤ ( 1 / 2 ) ) )
62 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 2 · 𝑦 ) = ( 2 · 𝑥 ) )
63 62 fveq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ ( 2 · 𝑦 ) ) = ( 𝐹 ‘ ( 2 · 𝑥 ) ) )
64 62 oveq1d ⊢ ( 𝑦 = 𝑥 → ( ( 2 · 𝑦 ) − 1 ) = ( ( 2 · 𝑥 ) − 1 ) )
65 64 fveq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) = ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
66 61 63 65 ifbieq12d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑦 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
67 66 adantr ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑧 = 0 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑦 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑦 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
68 6 7 10 6 6 60 67 cnmpt12 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ∈ ( II Cn 𝐽 ) )
69 4 68 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ∈ ( II Cn 𝐽 ) )