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		ffvelcdm	$⊢ (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	eqtrid	$⊢ ((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		2thalfe1	$⊢ 2 (\frac{1}{2}) = 1$
78	76 77	eqtrdi	$⊢ ((F \in (II Cn J) \land F (0) = Y) \land (y = \frac{1}{2} \land z \in [0, 1])) \to 2 y = 1$
79	78	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$
80		1m1e0	$⊢ 1 - 1 = 0$
81	79 80	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$
82		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
83		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
84	64 68 83	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
85		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
86	82 84 85	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
87	86	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
88	87 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)$
89		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
90	68 66 89	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
91		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
92	82 90 91	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
93	92	a1i	$⊢ (F \in (II Cn J) \land F (0) = Y) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
94	93 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]))$
95	62	iihalf2cn	$⊢ (x \in [\frac{1}{2}, 1] ⟼ 2 x - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
96	95	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)$
97		oveq2	$⊢ x = y \to 2 x = 2 y$
98	97	oveq1d	$⊢ x = y \to 2 x - 1 = 2 y - 1$
99	93 56 94 93 96 98	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)$
100	60 61 62 63 65 67 74 56 81 88 99	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)$
101		breq1	$⊢ y = x \to (y \leq \frac{1}{2} \leftrightarrow x \leq \frac{1}{2})$
102		oveq2	$⊢ y = x \to 2 y = 2 x$
103	102	oveq1d	$⊢ y = x \to 2 y - 1 = 2 x - 1$
104	101 103	ifbieq2d	$⊢ y = x \to if (y \leq \frac{1}{2}, 0, 2 y - 1) = if (x \leq \frac{1}{2}, 0, 2 x - 1)$
105	104	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)$
106	56 57 59 56 56 100 105	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)$
107		id	$⊢ x = 0 \to x = 0$
108	107 69	eqbrtrdi	$⊢ x = 0 \to x \leq \frac{1}{2}$
109	108 43	syl	$⊢ x = 0 \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 0$
110		c0ex	$⊢ 0 \in V$
111	109 47 110	fvmpt	$⊢ 0 \in [0, 1] \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) (0) = 0$
112	8 111	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$
113		1elunit	$⊢ 1 \in [0, 1]$
114	68 66	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
115	70 114	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
116		breq1	$⊢ x = 1 \to (x \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
117	115 116	mtbiri	$⊢ x = 1 \to \neg x \leq \frac{1}{2}$
118	117 36	syl	$⊢ x = 1 \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 2 x - 1$
119		oveq2	$⊢ x = 1 \to 2 x = 2 \cdot 1$
120		2t1e2	$⊢ 2 \cdot 1 = 2$
121	119 120	eqtrdi	$⊢ x = 1 \to 2 x = 2$
122	121	oveq1d	$⊢ x = 1 \to 2 x - 1 = 2 - 1$
123		2m1e1	$⊢ 2 - 1 = 1$
124	122 123	eqtrdi	$⊢ x = 1 \to 2 x - 1 = 1$
125	118 124	eqtrd	$⊢ x = 1 \to if (x \leq \frac{1}{2}, 0, 2 x - 1) = 1$
126		1ex	$⊢ 1 \in V$
127	125 47 126	fvmpt	$⊢ 1 \in [0, 1] \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 0, 2 x - 1)) (1) = 1$
128	113 127	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$
129	34 106 112 128	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$
130	54 129	eqbrtrd	$⊢ (F \in (II Cn J) \land F (0) = Y) \to (P *_{𝑝} (J) F) ≃_{ph} (J) F$

Metamath Proof Explorer

Theorem pcopt

Proof