pcopt

Description: Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

		Ref	Expression
	Hypothesis	pcopt.1	$⊢ P = [0, 1] \times \{Y\}$
	Assertion	pcopt	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (P *_{𝑝} (J) F) ≃_{ph} (J) F$

Proof

Step	Hyp	Ref	Expression
1		pcopt.1	$⊢ P = [0, 1] \times \{Y\}$
2	1	fveq1i	$⊢ P (2 x) = ([0, 1] \times \{Y\}) (2 x)$
3		simpr	$⊢ (F \in (II Cn J) \land F (0) = Y) \to F (0) = Y$
4		iiuni	$⊢ [0, 1] = ⋃ II$
5		eqid	$⊢ ⋃ J = ⋃ J$
6	4 5	cnf	$⊢ F \in (II Cn J) \to F : [0, 1] ⟶ ⋃ J$
7	6	adantr	$⊢ (F \in (II Cn J) \land F (0) = Y) \to F : [0, 1] ⟶ ⋃ J$
8		0elunit	$⊢ 0 \in [0, 1]$
9		ffvelrn	$⊢ (F : [0, 1] ⟶ ⋃ J \land 0 \in [0, 1]) \to F (0) \in ⋃ J$
10	7 8 9	sylancl	$⊢ (F \in (II Cn J) \land F (0) = Y) \to F (0) \in ⋃ J$
11	3 10	eqeltrrd	$⊢ (F \in (II Cn J) \land F (0) = Y) \to Y \in ⋃ J$
12		elii1	$⊢ x \in [0, \frac{1}{2}] \leftrightarrow (x \in [0, 1] \land x \leq \frac{1}{2})$
13		iihalf1	$⊢ x \in [0, \frac{1}{2}] \to 2 x \in [0, 1]$
14	12 13	sylbir	$⊢ (x \in [0, 1] \land x \leq \frac{1}{2}) \to 2 x \in [0, 1]$
15		fvconst2g	$⊢ (Y \in ⋃ J \land 2 x \in [0, 1]) \to ([0, 1] \times \{Y\}) (2 x) = Y$
16	11 14 15	syl2an	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (x \in [0, 1] \land x \leq \frac{1}{2})) \to ([0, 1] \times \{Y\}) (2 x) = Y$
17	2 16	syl5eq	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (x \in [0, 1] \land x \leq \frac{1}{2})) \to P (2 x) = Y$
18		simplr	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (x \in [0, 1] \land x \leq \frac{1}{2})) \to F (0) = Y$
19	17 18	eqtr4d	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (x \in [0, 1] \land x \leq \frac{1}{2})) \to P (2 x) = F (0)$
20	19	ifeq1d	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (x \in [0, 1] \land x \leq \frac{1}{2})) \to if (x \leq \frac{1}{2}, P (2 x), F (2 x - 1)) = if (x \leq \frac{1}{2}, F (0), F (2 x - 1))$
21	20	expr	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land x \in [0, 1]) \to (x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, P (2 x), F (2 x - 1)) = if (x \leq \frac{1}{2}, F (0), F (2 x - 1)))$
22		iffalse	$⊢ \neg x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, P (2 x), F (2 x - 1)) = F (2 x - 1)$
23		iffalse	$⊢ \neg x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, F (0), F (2 x - 1)) = F (2 x - 1)$
24	22 23	eqtr4d	$⊢ \neg x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, P (2 x), F (2 x - 1)) = if (x \leq \frac{1}{2}, F (0), F (2 x - 1))$
25	21 24	pm2.61d1	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land x \in [0, 1]) \to if (x \leq \frac{1}{2}, P (2 x), F (2 x - 1)) = if (x \leq \frac{1}{2}, F (0), F (2 x - 1))$
26	25	mpteq2dva	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, P (2 x), F (2 x - 1))) = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, F (0), F (2 x - 1)))$
27		cntop2	$⊢ F \in (II Cn J) \to J \in Top$
28	27	adantr	$⊢ (F \in (II Cn J) \land F (0) = Y) \to J \in Top$
29		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
30	28 29	sylib	$⊢ (F \in (II Cn J) \land F (0) = Y) \to J \in TopOn (⋃ J)$
31	1	pcoptcl	$⊢ (J \in TopOn (⋃ J) \land Y \in ⋃ J) \to (P \in (II Cn J) \land P (0) = Y \land P (1) = Y)$
32	30 11 31	syl2anc	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (P \in (II Cn J) \land P (0) = Y \land P (1) = Y)$
33	32	simp1d	$⊢ (F \in (II Cn J) \land F (0) = Y) \to P \in (II Cn J)$
34		simpl	$⊢ (F \in (II Cn J) \land F (0) = Y) \to F \in (II Cn J)$
35	33 34	pcoval	$⊢ (F \in (II Cn J) \land F (0) = Y) \to P *_{𝑝} (J) F = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, P (2 x), F (2 x - 1)))$
36		iffalse	$⊢ \neg x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 2 x - 1$
37	36	adantl	$⊢ (x \in [0, 1] \land \neg x \leq \frac{1}{2}) \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 2 x - 1$
38		elii2	$⊢ (x \in [0, 1] \land \neg x \leq \frac{1}{2}) \to x \in [\frac{1}{2}, 1]$
39		iihalf2	$⊢ x \in [\frac{1}{2}, 1] \to 2 x - 1 \in [0, 1]$
40	38 39	syl	$⊢ (x \in [0, 1] \land \neg x \leq \frac{1}{2}) \to 2 x - 1 \in [0, 1]$
41	37 40	eqeltrd	$⊢ (x \in [0, 1] \land \neg x \leq \frac{1}{2}) \to if (x \leq \frac{1}{2}, 0, 2 x - 1) \in [0, 1]$
42	41	ex	$⊢ x \in [0, 1] \to (\neg x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, 0, 2 x - 1) \in [0, 1])$
43		iftrue	$⊢ x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 0$
44	43 8	eqeltrdi	$⊢ x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, 0, 2 x - 1) \in [0, 1]$
45	42 44	pm2.61d2	$⊢ x \in [0, 1] \to if (x \leq \frac{1}{2}, 0, 2 x - 1) \in [0, 1]$
46	45	adantl	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land x \in [0, 1]) \to if (x \leq \frac{1}{2}, 0, 2 x - 1) \in [0, 1]$
47		eqid	$⊢ (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1))$
48	47	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1))$
49	7	feqmptd	$⊢ (F \in (II Cn J) \land F (0) = Y) \to F = (y \in [0, 1] ⟼ F (y))$
50		fveq2	$⊢ y = if (x \leq \frac{1}{2}, 0, 2 x - 1) \to F (y) = F (if (x \leq \frac{1}{2}, 0, 2 x - 1))$
51		fvif	$⊢ F (if (x \leq \frac{1}{2}, 0, 2 x - 1)) = if (x \leq \frac{1}{2}, F (0), F (2 x - 1))$
52	50 51	eqtrdi	$⊢ y = if (x \leq \frac{1}{2}, 0, 2 x - 1) \to F (y) = if (x \leq \frac{1}{2}, F (0), F (2 x - 1))$
53	46 48 49 52	fmptco	$⊢ (F \in (II Cn J) \land F (0) = Y) \to F \circ (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, F (0), F (2 x - 1)))$
54	26 35 53	3eqtr4d	$⊢ (F \in (II Cn J) \land F (0) = Y) \to P *_{𝑝} (J) F = F \circ (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1))$
55		iitopon	$⊢ II \in TopOn ([0, 1])$
56	55	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to II \in TopOn ([0, 1])$
57	56	cnmptid	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (x \in [0, 1] ⟼ x) \in (II Cn II)$
58	8	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to 0 \in [0, 1]$
59	56 56 58	cnmptc	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (x \in [0, 1] ⟼ 0) \in (II Cn II)$
60		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
61		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]$
62		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] = topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]$
63		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
64		0re	$⊢ 0 \in ℝ$
65	64	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to 0 \in ℝ$
66		1re	$⊢ 1 \in ℝ$
67	66	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to 1 \in ℝ$
68		halfre	$⊢ \frac{1}{2} \in ℝ$
69		halfge0	$⊢ 0 \leq \frac{1}{2}$
70		halflt1	$⊢ \frac{1}{2} < 1$
71	68 66 70	ltleii	$⊢ \frac{1}{2} \leq 1$
72		elicc01	$⊢ \frac{1}{2} \in [0, 1] \leftrightarrow (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2} \land \frac{1}{2} \leq 1)$
73	68 69 71 72	mpbir3an	$⊢ \frac{1}{2} \in [0, 1]$
74	73	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to \frac{1}{2} \in [0, 1]$
75		simprl	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (y = \frac{1}{2} \land z \in [0, 1])) \to y = \frac{1}{2}$
76	75	oveq2d	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (y = \frac{1}{2} \land z \in [0, 1])) \to 2 y = 2 (\frac{1}{2})$
77		2cn	$⊢ 2 \in ℂ$
78		2ne0	$⊢ 2 \neq 0$
79	77 78	recidi	$⊢ 2 (\frac{1}{2}) = 1$
80	76 79	eqtrdi	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (y = \frac{1}{2} \land z \in [0, 1])) \to 2 y = 1$
81	80	oveq1d	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (y = \frac{1}{2} \land z \in [0, 1])) \to 2 y - 1 = 1 - 1$
82		1m1e0	$⊢ 1 - 1 = 0$
83	81 82	eqtr2di	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (y = \frac{1}{2} \land z \in [0, 1])) \to 0 = 2 y - 1$
84		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
85		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
86	64 68 85	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
87		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
88	84 86 87	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
89	88	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
90	89 56 56 58	cnmpt2c	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (y \in [0, \frac{1}{2}], z \in [0, 1] ⟼ 0) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
91		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
92	68 66 91	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
93		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
94	84 92 93	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
95	94	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
96	95 56	cnmpt1st	$⊢ (F \in (II Cn J) \land F (0) = Y) \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]))$
97	62	iihalf2cn	$⊢ (x \in [\frac{1}{2}, 1] ⟼ 2 x - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
98	97	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (x \in [\frac{1}{2}, 1] ⟼ 2 x - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
99		oveq2	$⊢ x = y \to 2 x = 2 y$
100	99	oveq1d	$⊢ x = y \to 2 x - 1 = 2 y - 1$
101	95 56 96 95 98 100	cnmpt21	$⊢ (F \in (II Cn J) \land F (0) = Y) \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)$
102	60 61 62 63 65 67 74 56 83 90 101	cnmpopc	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (y \in [0, 1], z \in [0, 1] ⟼ if (y \leq \frac{1}{2}, 0, 2 y - 1)) \in ((II \times_{t} II) Cn II)$
103		breq1	$⊢ y = x \to (y \leq \frac{1}{2} \leftrightarrow x \leq \frac{1}{2})$
104		oveq2	$⊢ y = x \to 2 y = 2 x$
105	104	oveq1d	$⊢ y = x \to 2 y - 1 = 2 x - 1$
106	103 105	ifbieq2d	$⊢ y = x \to if (y \leq \frac{1}{2}, 0, 2 y - 1) = if (x \leq \frac{1}{2}, 0, 2 x - 1)$
107	106	adantr	$⊢ (y = x \land z = 0) \to if (y \leq \frac{1}{2}, 0, 2 y - 1) = if (x \leq \frac{1}{2}, 0, 2 x - 1)$
108	56 57 59 56 56 102 107	cnmpt12	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) \in (II Cn II)$
109		id	$⊢ x = 0 \to x = 0$
110	109 69	eqbrtrdi	$⊢ x = 0 \to x \leq \frac{1}{2}$
111	110 43	syl	$⊢ x = 0 \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 0$
112		c0ex	$⊢ 0 \in V$
113	111 47 112	fvmpt	$⊢ 0 \in [0, 1] \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) (0) = 0$
114	8 113	mp1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) (0) = 0$
115		1elunit	$⊢ 1 \in [0, 1]$
116	68 66	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
117	70 116	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
118		breq1	$⊢ x = 1 \to (x \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
119	117 118	mtbiri	$⊢ x = 1 \to \neg x \leq \frac{1}{2}$
120	119 36	syl	$⊢ x = 1 \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 2 x - 1$
121		oveq2	$⊢ x = 1 \to 2 x = 2 \cdot 1$
122		2t1e2	$⊢ 2 \cdot 1 = 2$
123	121 122	eqtrdi	$⊢ x = 1 \to 2 x = 2$
124	123	oveq1d	$⊢ x = 1 \to 2 x - 1 = 2 - 1$
125		2m1e1	$⊢ 2 - 1 = 1$
126	124 125	eqtrdi	$⊢ x = 1 \to 2 x - 1 = 1$
127	120 126	eqtrd	$⊢ x = 1 \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 1$
128		1ex	$⊢ 1 \in V$
129	127 47 128	fvmpt	$⊢ 1 \in [0, 1] \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) (1) = 1$
130	115 129	mp1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) (1) = 1$
131	34 108 114 130	reparpht	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (F \circ (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1))) ≃_{ph} (J) F$
132	54 131	eqbrtrd	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (P *_{𝑝} (J) F) ≃_{ph} (J) F$

Metamath Proof Explorer

Theorem pcopt

Proof