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 ⊢ φ → F ∈ II Cn J
pcoval.3 ⊢ φ → G ∈ II Cn J
pcoval2.4 ⊢ φ → F ⁡ 1 = G ⁡ 0
Assertion pcocn ⊢ φ → F * 𝑝 ⁡ J G ∈ II Cn J

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢ φ → F ∈ II Cn J
2 pcoval.3 ⊢ φ → G ∈ II Cn J
3 pcoval2.4 ⊢ φ → F ⁡ 1 = G ⁡ 0
4 1 2 pcoval ⊢ φ → F * 𝑝 ⁡ J G = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
5 iitopon ⊢ II ∈ TopOn ⁡ 0 1
6 5 a1i ⊢ φ → II ∈ TopOn ⁡ 0 1
7 6 cnmptid ⊢ φ → x ∈ 0 1 ⟼ x ∈ II Cn II
8 0elunit ⊢ 0 ∈ 0 1
9 8 a1i ⊢ φ → 0 ∈ 0 1
10 6 6 9 cnmptc ⊢ φ → x ∈ 0 1 ⟼ 0 ∈ II Cn II
11 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
12 eqid ⊢ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2 = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2
13 eqid ⊢ topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1 = topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1
14 dfii2 ⊢ II = topGen ⁡ ran ⁡ . ↾ 𝑡 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 ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → F ⁡ 1 = G ⁡ 0
27 simprl ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → y = 1 2
28 27 oveq2d ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → 2 ⁢ y = 2 ⁢ 1 2
29 2thalfe1 ⊢ 2 ⁢ 1 2 = 1
30 28 29 eqtrdi ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → 2 ⁢ y = 1
31 30 fveq2d ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → F ⁡ 2 ⁢ y = F ⁡ 1
32 30 oveq1d ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → 2 ⁢ y − 1 = 1 − 1
33 1m1e0 ⊢ 1 − 1 = 0
34 32 33 eqtrdi ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → 2 ⁢ y − 1 = 0
35 34 fveq2d ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → G ⁡ 2 ⁢ y − 1 = G ⁡ 0
36 26 31 35 3eqtr4d ⊢ φ ∧ y = 1 2 ∧ z ∈ 0 1 → F ⁡ 2 ⁢ y = G ⁡ 2 ⁢ y − 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 ⁡ . ↾ 𝑡 0 1 2 ∈ TopOn ⁡ 0 1 2
41 37 39 40 mp2an ⊢ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2 ∈ TopOn ⁡ 0 1 2
42 41 a1i ⊢ φ → topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2 ∈ TopOn ⁡ 0 1 2
43 42 6 cnmpt1st ⊢ φ → y ∈ 0 1 2 , z ∈ 0 1 ⟼ y ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2 × t II Cn topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2
44 12 iihalf1cn ⊢ x ∈ 0 1 2 ⟼ 2 ⁢ x ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2 Cn II
45 44 a1i ⊢ φ → x ∈ 0 1 2 ⟼ 2 ⁢ x ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2 Cn II
46 oveq2 ⊢ x = y → 2 ⁢ x = 2 ⁢ y
47 42 6 43 42 45 46 cnmpt21 ⊢ φ → y ∈ 0 1 2 , z ∈ 0 1 ⟼ 2 ⁢ y ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2 × t II Cn II
48 42 6 47 1 cnmpt21f ⊢ φ → y ∈ 0 1 2 , z ∈ 0 1 ⟼ F ⁡ 2 ⁢ y ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2 × t II Cn J
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 ⁡ . ↾ 𝑡 1 2 1 ∈ TopOn ⁡ 1 2 1
52 37 50 51 mp2an ⊢ topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1 ∈ TopOn ⁡ 1 2 1
53 52 a1i ⊢ φ → topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1 ∈ TopOn ⁡ 1 2 1
54 53 6 cnmpt1st ⊢ φ → y ∈ 1 2 1 , z ∈ 0 1 ⟼ y ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1 × t II Cn topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1
55 13 iihalf2cn ⊢ x ∈ 1 2 1 ⟼ 2 ⁢ x − 1 ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1 Cn II
56 55 a1i ⊢ φ → x ∈ 1 2 1 ⟼ 2 ⁢ x − 1 ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1 Cn II
57 46 oveq1d ⊢ x = y → 2 ⁢ x − 1 = 2 ⁢ y − 1
58 53 6 54 53 56 57 cnmpt21 ⊢ φ → y ∈ 1 2 1 , z ∈ 0 1 ⟼ 2 ⁢ y − 1 ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1 × t II Cn II
59 53 6 58 2 cnmpt21f ⊢ φ → y ∈ 1 2 1 , z ∈ 0 1 ⟼ G ⁡ 2 ⁢ y − 1 ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1 × t II Cn J
60 11 12 13 14 16 18 25 6 36 48 59 cnmpopc ⊢ φ → y ∈ 0 1 , z ∈ 0 1 ⟼ if y ≤ 1 2 F ⁡ 2 ⁢ y G ⁡ 2 ⁢ y − 1 ∈ II × t II Cn J
61 breq1 ⊢ y = x → y ≤ 1 2 ↔ x ≤ 1 2
62 oveq2 ⊢ y = x → 2 ⁢ y = 2 ⁢ x
63 62 fveq2d ⊢ y = x → F ⁡ 2 ⁢ y = F ⁡ 2 ⁢ x
64 62 oveq1d ⊢ y = x → 2 ⁢ y − 1 = 2 ⁢ x − 1
65 64 fveq2d ⊢ y = x → G ⁡ 2 ⁢ y − 1 = G ⁡ 2 ⁢ x − 1
66 61 63 65 ifbieq12d ⊢ y = x → if y ≤ 1 2 F ⁡ 2 ⁢ y G ⁡ 2 ⁢ y − 1 = if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
67 66 adantr ⊢ y = x ∧ z = 0 → if y ≤ 1 2 F ⁡ 2 ⁢ y G ⁡ 2 ⁢ y − 1 = if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
68 6 7 10 6 6 60 67 cnmpt12 ⊢ φ → x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 ∈ II Cn J
69 4 68 eqeltrd ⊢ φ → F * 𝑝 ⁡ J G ∈ II Cn J