pcopt2

Description: Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015)

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

Proof

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

Metamath Proof Explorer

Theorem pcopt2

Proof