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	$⊢ φ \to F \in (II Cn J)$
	pcoval.3	$⊢ φ \to G \in (II Cn J)$
	pcoval2.4	$⊢ φ \to F (1) = G (0)$
Assertion	pcocn	$⊢ φ \to F *_{𝑝} (J) G \in (II Cn J)$

Proof

Step	Hyp	Ref	Expression
1		pcoval.2	$⊢ φ \to F \in (II Cn J)$
2		pcoval.3	$⊢ φ \to G \in (II Cn J)$
3		pcoval2.4	$⊢ φ \to F (1) = G (0)$
4	1 2	pcoval	$⊢ φ \to F *_{𝑝} (J) G = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, F (2 x), G (2 x - 1)))$
5		iitopon	$⊢ II \in TopOn ([0, 1])$
6	5	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
7	6	cnmptid	$⊢ φ \to (x \in [0, 1] ⟼ x) \in (II Cn II)$
8		0elunit	$⊢ 0 \in [0, 1]$
9	8	a1i	$⊢ φ \to 0 \in [0, 1]$
10	6 6 9	cnmptc	$⊢ φ \to (x \in [0, 1] ⟼ 0) \in (II Cn II)$
11		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
12		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]$
13		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] = topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]$
14		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
15		0re	$⊢ 0 \in ℝ$
16	15	a1i	$⊢ φ \to 0 \in ℝ$
17		1re	$⊢ 1 \in ℝ$
18	17	a1i	$⊢ φ \to 1 \in ℝ$
19		halfre	$⊢ \frac{1}{2} \in ℝ$
20		halfge0	$⊢ 0 \leq \frac{1}{2}$
21		halflt1	$⊢ \frac{1}{2} < 1$
22	19 17 21	ltleii	$⊢ \frac{1}{2} \leq 1$
23		elicc01	$⊢ \frac{1}{2} \in [0, 1] \leftrightarrow (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2} \land \frac{1}{2} \leq 1)$
24	19 20 22 23	mpbir3an	$⊢ \frac{1}{2} \in [0, 1]$
25	24	a1i	$⊢ φ \to \frac{1}{2} \in [0, 1]$
26	3	adantr	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to F (1) = G (0)$
27		simprl	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to y = \frac{1}{2}$
28	27	oveq2d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to 2 y = 2 (\frac{1}{2})$
29		2cn	$⊢ 2 \in ℂ$
30		2ne0	$⊢ 2 \neq 0$
31	29 30	recidi	$⊢ 2 (\frac{1}{2}) = 1$
32	28 31	eqtrdi	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to 2 y = 1$
33	32	fveq2d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to F (2 y) = F (1)$
34	32	oveq1d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to 2 y - 1 = 1 - 1$
35		1m1e0	$⊢ 1 - 1 = 0$
36	34 35	eqtrdi	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to 2 y - 1 = 0$
37	36	fveq2d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to G (2 y - 1) = G (0)$
38	26 33 37	3eqtr4d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to F (2 y) = G (2 y - 1)$
39		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
40		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
41	15 19 40	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
42		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
43	39 41 42	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
44	43	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
45	44 6	cnmpt1st	$⊢ φ \to (y \in [0, \frac{1}{2}], z \in [0, 1] ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]))$
46	12	iihalf1cn	$⊢ (x \in [0, \frac{1}{2}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
47	46	a1i	$⊢ φ \to (x \in [0, \frac{1}{2}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
48		oveq2	$⊢ x = y \to 2 x = 2 y$
49	44 6 45 44 47 48	cnmpt21	$⊢ φ \to (y \in [0, \frac{1}{2}], z \in [0, 1] ⟼ 2 y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
50	44 6 49 1	cnmpt21f	$⊢ φ \to (y \in [0, \frac{1}{2}], z \in [0, 1] ⟼ F (2 y)) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn J)$
51		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
52	19 17 51	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
53		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
54	39 52 53	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
55	54	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
56	55 6	cnmpt1st	$⊢ φ \to (y \in [\frac{1}{2}, 1], z \in [0, 1] ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]))$
57	13	iihalf2cn	$⊢ (x \in [\frac{1}{2}, 1] ⟼ 2 x - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
58	57	a1i	$⊢ φ \to (x \in [\frac{1}{2}, 1] ⟼ 2 x - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
59	48	oveq1d	$⊢ x = y \to 2 x - 1 = 2 y - 1$
60	55 6 56 55 58 59	cnmpt21	$⊢ φ \to (y \in [\frac{1}{2}, 1], z \in [0, 1] ⟼ 2 y - 1) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
61	55 6 60 2	cnmpt21f	$⊢ φ \to (y \in [\frac{1}{2}, 1], z \in [0, 1] ⟼ G (2 y - 1)) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn J)$
62	11 12 13 14 16 18 25 6 38 50 61	cnmpopc	$⊢ φ \to (y \in [0, 1], z \in [0, 1] ⟼ if (y \leq \frac{1}{2}, F (2 y), G (2 y - 1))) \in ((II \times_{t} II) Cn J)$
63		breq1	$⊢ y = x \to (y \leq \frac{1}{2} \leftrightarrow x \leq \frac{1}{2})$
64		oveq2	$⊢ y = x \to 2 y = 2 x$
65	64	fveq2d	$⊢ y = x \to F (2 y) = F (2 x)$
66	64	oveq1d	$⊢ y = x \to 2 y - 1 = 2 x - 1$
67	66	fveq2d	$⊢ y = x \to G (2 y - 1) = G (2 x - 1)$
68	63 65 67	ifbieq12d	$⊢ y = x \to if (y \leq \frac{1}{2}, F (2 y), G (2 y - 1)) = if (x \leq \frac{1}{2}, F (2 x), G (2 x - 1))$
69	68	adantr	$⊢ (y = x \land z = 0) \to if (y \leq \frac{1}{2}, F (2 y), G (2 y - 1)) = if (x \leq \frac{1}{2}, F (2 x), G (2 x - 1))$
70	6 7 10 6 6 62 69	cnmpt12	$⊢ φ \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, F (2 x), G (2 x - 1))) \in (II Cn J)$
71	4 70	eqeltrd	$⊢ φ \to F *_{𝑝} (J) G \in (II Cn J)$

Metamath Proof Explorer

Theorem pcocn

Proof