pcorevlem

Description: Lemma for pcorev . Prove continuity of the homotopy function. (Contributed by Jeff Madsen, 11-Jun-2010) (Proof shortened by Mario Carneiro, 8-Jun-2014)

	Ref	Expression
Hypotheses	pcorev.1	$⊢ G = (x \in [0, 1] ⟼ F (1 - x))$
	pcorev.2	$⊢ P = [0, 1] \times \{F (1)\}$
	pcorevlem.3	$⊢ H = (s \in [0, 1], t \in [0, 1] ⟼ F (if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1)))))$
Assertion	pcorevlem	$⊢ F \in (II Cn J) \to (H \in ((G _{𝑝} (J) F) PHtpy (J) P) \land (G _{𝑝} (J) F) ≃_{ph} (J) P)$

Proof

Step	Hyp	Ref	Expression
1		pcorev.1	$⊢ G = (x \in [0, 1] ⟼ F (1 - x))$
2		pcorev.2	$⊢ P = [0, 1] \times \{F (1)\}$
3		pcorevlem.3	$⊢ H = (s \in [0, 1], t \in [0, 1] ⟼ F (if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1)))))$
4		iitopon	$⊢ II \in TopOn ([0, 1])$
5	4	a1i	$⊢ F \in (II Cn J) \to II \in TopOn ([0, 1])$
6		iirevcn	$⊢ (x \in [0, 1] ⟼ 1 - x) \in (II Cn II)$
7	6	a1i	$⊢ F \in (II Cn J) \to (x \in [0, 1] ⟼ 1 - x) \in (II Cn II)$
8		id	$⊢ F \in (II Cn J) \to F \in (II Cn J)$
9	5 7 8	cnmpt11f	$⊢ F \in (II Cn J) \to (x \in [0, 1] ⟼ F (1 - x)) \in (II Cn J)$
10	1 9	eqeltrid	$⊢ F \in (II Cn J) \to G \in (II Cn J)$
11		1elunit	$⊢ 1 \in [0, 1]$
12		oveq2	$⊢ x = 1 \to 1 - x = 1 - 1$
13		1m1e0	$⊢ 1 - 1 = 0$
14	12 13	syl6eq	$⊢ x = 1 \to 1 - x = 0$
15	14	fveq2d	$⊢ x = 1 \to F (1 - x) = F (0)$
16		fvex	$⊢ F (0) \in V$
17	15 1 16	fvmpt	$⊢ 1 \in [0, 1] \to G (1) = F (0)$
18	11 17	mp1i	$⊢ F \in (II Cn J) \to G (1) = F (0)$
19	10 8 18	pcocn	$⊢ F \in (II Cn J) \to G *_{𝑝} (J) F \in (II Cn J)$
20		cntop2	$⊢ F \in (II Cn J) \to J \in Top$
21		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
22	20 21	sylib	$⊢ F \in (II Cn J) \to J \in TopOn (⋃ J)$
23		iiuni	$⊢ [0, 1] = ⋃ II$
24		eqid	$⊢ ⋃ J = ⋃ J$
25	23 24	cnf	$⊢ F \in (II Cn J) \to F : [0, 1] ⟶ ⋃ J$
26		ffvelrn	$⊢ (F : [0, 1] ⟶ ⋃ J \land 1 \in [0, 1]) \to F (1) \in ⋃ J$
27	25 11 26	sylancl	$⊢ F \in (II Cn J) \to F (1) \in ⋃ J$
28	2	pcoptcl	$⊢ (J \in TopOn (⋃ J) \land F (1) \in ⋃ J) \to (P \in (II Cn J) \land P (0) = F (1) \land P (1) = F (1))$
29	22 27 28	syl2anc	$⊢ F \in (II Cn J) \to (P \in (II Cn J) \land P (0) = F (1) \land P (1) = F (1))$
30	29	simp1d	$⊢ F \in (II Cn J) \to P \in (II Cn J)$
31		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
32		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]$
33		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] = topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]$
34		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
35		0red	$⊢ F \in (II Cn J) \to 0 \in ℝ$
36		1red	$⊢ F \in (II Cn J) \to 1 \in ℝ$
37		halfre	$⊢ \frac{1}{2} \in ℝ$
38		halfge0	$⊢ 0 \leq \frac{1}{2}$
39		1re	$⊢ 1 \in ℝ$
40		halflt1	$⊢ \frac{1}{2} < 1$
41	37 39 40	ltleii	$⊢ \frac{1}{2} \leq 1$
42		elicc01	$⊢ \frac{1}{2} \in [0, 1] \leftrightarrow (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2} \land \frac{1}{2} \leq 1)$
43	37 38 41 42	mpbir3an	$⊢ \frac{1}{2} \in [0, 1]$
44	43	a1i	$⊢ F \in (II Cn J) \to \frac{1}{2} \in [0, 1]$
45		simprl	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to s = \frac{1}{2}$
46	45	oveq2d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s = 2 (\frac{1}{2})$
47		2cn	$⊢ 2 \in ℂ$
48		2ne0	$⊢ 2 \neq 0$
49	47 48	recidi	$⊢ 2 (\frac{1}{2}) = 1$
50	46 49	syl6eq	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s = 1$
51	50	oveq1d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s - 1 = 1 - 1$
52	51 13	syl6eq	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s - 1 = 0$
53	52	oveq2d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 1 - (2 s - 1) = 1 - 0$
54		1m0e1	$⊢ 1 - 0 = 1$
55	53 54	syl6eq	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 1 - (2 s - 1) = 1$
56	50 55	eqtr4d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s = 1 - (2 s - 1)$
57	56	oveq2d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to (1 - t) 2 s = (1 - t) (1 - (2 s - 1))$
58	57	oveq2d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 1 - (1 - t) 2 s = 1 - (1 - t) (1 - (2 s - 1))$
59		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
60		0re	$⊢ 0 \in ℝ$
61		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
62	60 37 61	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
63		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
64	59 62 63	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
65	64	a1i	$⊢ F \in (II Cn J) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
66	65 5	cnmpt2nd	$⊢ F \in (II Cn J) \to (s \in [0, \frac{1}{2}], t \in [0, 1] ⟼ t) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
67		oveq2	$⊢ x = t \to 1 - x = 1 - t$
68	65 5 66 5 7 67	cnmpt21	$⊢ F \in (II Cn J) \to (s \in [0, \frac{1}{2}], t \in [0, 1] ⟼ 1 - t) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
69	65 5	cnmpt1st	$⊢ F \in (II Cn J) \to (s \in [0, \frac{1}{2}], t \in [0, 1] ⟼ s) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]))$
70	32	iihalf1cn	$⊢ (x \in [0, \frac{1}{2}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
71	70	a1i	$⊢ F \in (II Cn J) \to (x \in [0, \frac{1}{2}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
72		oveq2	$⊢ x = s \to 2 x = 2 s$
73	65 5 69 65 71 72	cnmpt21	$⊢ F \in (II Cn J) \to (s \in [0, \frac{1}{2}], t \in [0, 1] ⟼ 2 s) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
74		iimulcn	$⊢ (x \in [0, 1], y \in [0, 1] ⟼ x y) \in ((II \times_{t} II) Cn II)$
75	74	a1i	$⊢ F \in (II Cn J) \to (x \in [0, 1], y \in [0, 1] ⟼ x y) \in ((II \times_{t} II) Cn II)$
76		oveq12	$⊢ (x = 1 - t \land y = 2 s) \to x y = (1 - t) 2 s$
77	65 5 68 73 5 5 75 76	cnmpt22	$⊢ F \in (II Cn J) \to (s \in [0, \frac{1}{2}], t \in [0, 1] ⟼ (1 - t) 2 s) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
78		oveq2	$⊢ x = (1 - t) 2 s \to 1 - x = 1 - (1 - t) 2 s$
79	65 5 77 5 7 78	cnmpt21	$⊢ F \in (II Cn J) \to (s \in [0, \frac{1}{2}], t \in [0, 1] ⟼ 1 - (1 - t) 2 s) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
80		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
81	37 39 80	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
82		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
83	59 81 82	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
84	83	a1i	$⊢ F \in (II Cn J) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
85	84 5	cnmpt2nd	$⊢ F \in (II Cn J) \to (s \in [\frac{1}{2}, 1], t \in [0, 1] ⟼ t) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
86	84 5 85 5 7 67	cnmpt21	$⊢ F \in (II Cn J) \to (s \in [\frac{1}{2}, 1], t \in [0, 1] ⟼ 1 - t) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
87	84 5	cnmpt1st	$⊢ F \in (II Cn J) \to (s \in [\frac{1}{2}, 1], t \in [0, 1] ⟼ s) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]))$
88	33	iihalf2cn	$⊢ (x \in [\frac{1}{2}, 1] ⟼ 2 x - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
89	88	a1i	$⊢ F \in (II Cn J) \to (x \in [\frac{1}{2}, 1] ⟼ 2 x - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
90	72	oveq1d	$⊢ x = s \to 2 x - 1 = 2 s - 1$
91	84 5 87 84 89 90	cnmpt21	$⊢ F \in (II Cn J) \to (s \in [\frac{1}{2}, 1], t \in [0, 1] ⟼ 2 s - 1) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
92		oveq2	$⊢ x = 2 s - 1 \to 1 - x = 1 - (2 s - 1)$
93	84 5 91 5 7 92	cnmpt21	$⊢ F \in (II Cn J) \to (s \in [\frac{1}{2}, 1], t \in [0, 1] ⟼ 1 - (2 s - 1)) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
94		oveq12	$⊢ (x = 1 - t \land y = 1 - (2 s - 1)) \to x y = (1 - t) (1 - (2 s - 1))$
95	84 5 86 93 5 5 75 94	cnmpt22	$⊢ F \in (II Cn J) \to (s \in [\frac{1}{2}, 1], t \in [0, 1] ⟼ (1 - t) (1 - (2 s - 1))) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
96		oveq2	$⊢ x = (1 - t) (1 - (2 s - 1)) \to 1 - x = 1 - (1 - t) (1 - (2 s - 1))$
97	84 5 95 5 7 96	cnmpt21	$⊢ F \in (II Cn J) \to (s \in [\frac{1}{2}, 1], t \in [0, 1] ⟼ 1 - (1 - t) (1 - (2 s - 1))) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
98	31 32 33 34 35 36 44 5 58 79 97	cnmpopc	$⊢ F \in (II Cn J) \to (s \in [0, 1], t \in [0, 1] ⟼ if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1)))) \in ((II \times_{t} II) Cn II)$
99	5 5 98 8	cnmpt21f	$⊢ F \in (II Cn J) \to (s \in [0, 1], t \in [0, 1] ⟼ F (if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1))))) \in ((II \times_{t} II) Cn J)$
100	3 99	eqeltrid	$⊢ F \in (II Cn J) \to H \in ((II \times_{t} II) Cn J)$
101		simpr	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to y \in [0, 1]$
102		0elunit	$⊢ 0 \in [0, 1]$
103		simpl	$⊢ (s = y \land t = 0) \to s = y$
104	103	breq1d	$⊢ (s = y \land t = 0) \to (s \leq \frac{1}{2} \leftrightarrow y \leq \frac{1}{2})$
105		simpr	$⊢ (s = y \land t = 0) \to t = 0$
106	105	oveq2d	$⊢ (s = y \land t = 0) \to 1 - t = 1 - 0$
107	106 54	syl6eq	$⊢ (s = y \land t = 0) \to 1 - t = 1$
108	103	oveq2d	$⊢ (s = y \land t = 0) \to 2 s = 2 y$
109	107 108	oveq12d	$⊢ (s = y \land t = 0) \to (1 - t) 2 s = 1 2 y$
110	109	oveq2d	$⊢ (s = y \land t = 0) \to 1 - (1 - t) 2 s = 1 - 1 2 y$
111	108	oveq1d	$⊢ (s = y \land t = 0) \to 2 s - 1 = 2 y - 1$
112	111	oveq2d	$⊢ (s = y \land t = 0) \to 1 - (2 s - 1) = 1 - (2 y - 1)$
113	107 112	oveq12d	$⊢ (s = y \land t = 0) \to (1 - t) (1 - (2 s - 1)) = 1 (1 - (2 y - 1))$
114	113	oveq2d	$⊢ (s = y \land t = 0) \to 1 - (1 - t) (1 - (2 s - 1)) = 1 - 1 (1 - (2 y - 1))$
115	104 110 114	ifbieq12d	$⊢ (s = y \land t = 0) \to if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1))) = if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1)))$
116	115	fveq2d	$⊢ (s = y \land t = 0) \to F (if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1)))) = F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1))))$
117		fvex	$⊢ F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1)))) \in V$
118	116 3 117	ovmpoa	$⊢ (y \in [0, 1] \land 0 \in [0, 1]) \to y H 0 = F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1))))$
119	101 102 118	sylancl	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to y H 0 = F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1))))$
120		iftrue	$⊢ y \leq \frac{1}{2} \to if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1))) = 1 - 1 2 y$
121	120	adantl	$⊢ ((F \in (II Cn J) \land y \in [0, 1]) \land y \leq \frac{1}{2}) \to if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1))) = 1 - 1 2 y$
122	121	fveq2d	$⊢ ((F \in (II Cn J) \land y \in [0, 1]) \land y \leq \frac{1}{2}) \to F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1)))) = F (1 - 1 2 y)$
123		elii1	$⊢ y \in [0, \frac{1}{2}] \leftrightarrow (y \in [0, 1] \land y \leq \frac{1}{2})$
124	10 8	pcoval1	$⊢ (F \in (II Cn J) \land y \in [0, \frac{1}{2}]) \to (G *_{𝑝} (J) F) (y) = G (2 y)$
125		iihalf1	$⊢ y \in [0, \frac{1}{2}] \to 2 y \in [0, 1]$
126	125	adantl	$⊢ (F \in (II Cn J) \land y \in [0, \frac{1}{2}]) \to 2 y \in [0, 1]$
127		oveq2	$⊢ x = 2 y \to 1 - x = 1 - 2 y$
128	127	fveq2d	$⊢ x = 2 y \to F (1 - x) = F (1 - 2 y)$
129		fvex	$⊢ F (1 - 2 y) \in V$
130	128 1 129	fvmpt	$⊢ 2 y \in [0, 1] \to G (2 y) = F (1 - 2 y)$
131		unitssre	$⊢ [0, 1] \subseteq ℝ$
132	131	sseli	$⊢ 2 y \in [0, 1] \to 2 y \in ℝ$
133	132	recnd	$⊢ 2 y \in [0, 1] \to 2 y \in ℂ$
134	133	mulid2d	$⊢ 2 y \in [0, 1] \to 1 2 y = 2 y$
135	134	oveq2d	$⊢ 2 y \in [0, 1] \to 1 - 1 2 y = 1 - 2 y$
136	135	fveq2d	$⊢ 2 y \in [0, 1] \to F (1 - 1 2 y) = F (1 - 2 y)$
137	130 136	eqtr4d	$⊢ 2 y \in [0, 1] \to G (2 y) = F (1 - 1 2 y)$
138	126 137	syl	$⊢ (F \in (II Cn J) \land y \in [0, \frac{1}{2}]) \to G (2 y) = F (1 - 1 2 y)$
139	124 138	eqtrd	$⊢ (F \in (II Cn J) \land y \in [0, \frac{1}{2}]) \to (G *_{𝑝} (J) F) (y) = F (1 - 1 2 y)$
140	123 139	sylan2br	$⊢ (F \in (II Cn J) \land (y \in [0, 1] \land y \leq \frac{1}{2})) \to (G *_{𝑝} (J) F) (y) = F (1 - 1 2 y)$
141	140	anassrs	$⊢ ((F \in (II Cn J) \land y \in [0, 1]) \land y \leq \frac{1}{2}) \to (G *_{𝑝} (J) F) (y) = F (1 - 1 2 y)$
142	122 141	eqtr4d	$⊢ ((F \in (II Cn J) \land y \in [0, 1]) \land y \leq \frac{1}{2}) \to F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1)))) = (G *_{𝑝} (J) F) (y)$
143		iffalse	$⊢ \neg y \leq \frac{1}{2} \to if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1))) = 1 - 1 (1 - (2 y - 1))$
144	143	adantl	$⊢ ((F \in (II Cn J) \land y \in [0, 1]) \land \neg y \leq \frac{1}{2}) \to if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1))) = 1 - 1 (1 - (2 y - 1))$
145	144	fveq2d	$⊢ ((F \in (II Cn J) \land y \in [0, 1]) \land \neg y \leq \frac{1}{2}) \to F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1)))) = F (1 - 1 (1 - (2 y - 1)))$
146		elii2	$⊢ (y \in [0, 1] \land \neg y \leq \frac{1}{2}) \to y \in [\frac{1}{2}, 1]$
147	10 8 18	pcoval2	$⊢ (F \in (II Cn J) \land y \in [\frac{1}{2}, 1]) \to (G *_{𝑝} (J) F) (y) = F (2 y - 1)$
148		iihalf2	$⊢ y \in [\frac{1}{2}, 1] \to 2 y - 1 \in [0, 1]$
149	148	adantl	$⊢ (F \in (II Cn J) \land y \in [\frac{1}{2}, 1]) \to 2 y - 1 \in [0, 1]$
150		ax-1cn	$⊢ 1 \in ℂ$
151	131	sseli	$⊢ 2 y - 1 \in [0, 1] \to 2 y - 1 \in ℝ$
152	151	recnd	$⊢ 2 y - 1 \in [0, 1] \to 2 y - 1 \in ℂ$
153		subcl	$⊢ (1 \in ℂ \land 2 y - 1 \in ℂ) \to 1 - (2 y - 1) \in ℂ$
154	150 152 153	sylancr	$⊢ 2 y - 1 \in [0, 1] \to 1 - (2 y - 1) \in ℂ$
155	154	mulid2d	$⊢ 2 y - 1 \in [0, 1] \to 1 (1 - (2 y - 1)) = 1 - (2 y - 1)$
156	155	oveq2d	$⊢ 2 y - 1 \in [0, 1] \to 1 - 1 (1 - (2 y - 1)) = 1 - (1 - (2 y - 1))$
157		nncan	$⊢ (1 \in ℂ \land 2 y - 1 \in ℂ) \to 1 - (1 - (2 y - 1)) = 2 y - 1$
158	150 152 157	sylancr	$⊢ 2 y - 1 \in [0, 1] \to 1 - (1 - (2 y - 1)) = 2 y - 1$
159	156 158	eqtr2d	$⊢ 2 y - 1 \in [0, 1] \to 2 y - 1 = 1 - 1 (1 - (2 y - 1))$
160	149 159	syl	$⊢ (F \in (II Cn J) \land y \in [\frac{1}{2}, 1]) \to 2 y - 1 = 1 - 1 (1 - (2 y - 1))$
161	160	fveq2d	$⊢ (F \in (II Cn J) \land y \in [\frac{1}{2}, 1]) \to F (2 y - 1) = F (1 - 1 (1 - (2 y - 1)))$
162	147 161	eqtrd	$⊢ (F \in (II Cn J) \land y \in [\frac{1}{2}, 1]) \to (G *_{𝑝} (J) F) (y) = F (1 - 1 (1 - (2 y - 1)))$
163	146 162	sylan2	$⊢ (F \in (II Cn J) \land (y \in [0, 1] \land \neg y \leq \frac{1}{2})) \to (G *_{𝑝} (J) F) (y) = F (1 - 1 (1 - (2 y - 1)))$
164	163	anassrs	$⊢ ((F \in (II Cn J) \land y \in [0, 1]) \land \neg y \leq \frac{1}{2}) \to (G *_{𝑝} (J) F) (y) = F (1 - 1 (1 - (2 y - 1)))$
165	145 164	eqtr4d	$⊢ ((F \in (II Cn J) \land y \in [0, 1]) \land \neg y \leq \frac{1}{2}) \to F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1)))) = (G *_{𝑝} (J) F) (y)$
166	142 165	pm2.61dan	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1)))) = (G *_{𝑝} (J) F) (y)$
167	119 166	eqtrd	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to y H 0 = (G *_{𝑝} (J) F) (y)$
168	131	sseli	$⊢ y \in [0, 1] \to y \in ℝ$
169	168	recnd	$⊢ y \in [0, 1] \to y \in ℂ$
170		mulcl	$⊢ (2 \in ℂ \land y \in ℂ) \to 2 y \in ℂ$
171	47 169 170	sylancr	$⊢ y \in [0, 1] \to 2 y \in ℂ$
172	171	adantl	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 2 y \in ℂ$
173	172	mul02d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 0 \cdot 2 y = 0$
174	173	oveq2d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - 0 \cdot 2 y = 1 - 0$
175	174 54	syl6eq	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - 0 \cdot 2 y = 1$
176		subcl	$⊢ (2 y \in ℂ \land 1 \in ℂ) \to 2 y - 1 \in ℂ$
177	172 150 176	sylancl	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 2 y - 1 \in ℂ$
178	150 177 153	sylancr	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - (2 y - 1) \in ℂ$
179	178	mul02d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 0 \cdot (1 - (2 y - 1)) = 0$
180	179	oveq2d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - 0 \cdot (1 - (2 y - 1)) = 1 - 0$
181	180 54	syl6eq	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - 0 \cdot (1 - (2 y - 1)) = 1$
182	175 181	ifeq12d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1))) = if (y \leq \frac{1}{2}, 1, 1)$
183		ifid	$⊢ if (y \leq \frac{1}{2}, 1, 1) = 1$
184	182 183	syl6eq	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1))) = 1$
185	184	fveq2d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to F (if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1)))) = F (1)$
186		simpl	$⊢ (s = y \land t = 1) \to s = y$
187	186	breq1d	$⊢ (s = y \land t = 1) \to (s \leq \frac{1}{2} \leftrightarrow y \leq \frac{1}{2})$
188		simpr	$⊢ (s = y \land t = 1) \to t = 1$
189	188	oveq2d	$⊢ (s = y \land t = 1) \to 1 - t = 1 - 1$
190	189 13	syl6eq	$⊢ (s = y \land t = 1) \to 1 - t = 0$
191	186	oveq2d	$⊢ (s = y \land t = 1) \to 2 s = 2 y$
192	190 191	oveq12d	$⊢ (s = y \land t = 1) \to (1 - t) 2 s = 0 \cdot 2 y$
193	192	oveq2d	$⊢ (s = y \land t = 1) \to 1 - (1 - t) 2 s = 1 - 0 \cdot 2 y$
194	191	oveq1d	$⊢ (s = y \land t = 1) \to 2 s - 1 = 2 y - 1$
195	194	oveq2d	$⊢ (s = y \land t = 1) \to 1 - (2 s - 1) = 1 - (2 y - 1)$
196	190 195	oveq12d	$⊢ (s = y \land t = 1) \to (1 - t) (1 - (2 s - 1)) = 0 \cdot (1 - (2 y - 1))$
197	196	oveq2d	$⊢ (s = y \land t = 1) \to 1 - (1 - t) (1 - (2 s - 1)) = 1 - 0 \cdot (1 - (2 y - 1))$
198	187 193 197	ifbieq12d	$⊢ (s = y \land t = 1) \to if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1))) = if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1)))$
199	198	fveq2d	$⊢ (s = y \land t = 1) \to F (if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1)))) = F (if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1))))$
200		fvex	$⊢ F (if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1)))) \in V$
201	199 3 200	ovmpoa	$⊢ (y \in [0, 1] \land 1 \in [0, 1]) \to y H 1 = F (if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1))))$
202	101 11 201	sylancl	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to y H 1 = F (if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1))))$
203	2	fveq1i	$⊢ P (y) = ([0, 1] \times \{F (1)\}) (y)$
204		fvex	$⊢ F (1) \in V$
205	204	fvconst2	$⊢ y \in [0, 1] \to ([0, 1] \times \{F (1)\}) (y) = F (1)$
206	205	adantl	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to ([0, 1] \times \{F (1)\}) (y) = F (1)$
207	203 206	syl5eq	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to P (y) = F (1)$
208	185 202 207	3eqtr4d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to y H 1 = P (y)$
209		simpl	$⊢ (s = 0 \land t = y) \to s = 0$
210	209 38	eqbrtrdi	$⊢ (s = 0 \land t = y) \to s \leq \frac{1}{2}$
211	210	iftrued	$⊢ (s = 0 \land t = y) \to if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1))) = 1 - (1 - t) 2 s$
212		simpr	$⊢ (s = 0 \land t = y) \to t = y$
213	212	oveq2d	$⊢ (s = 0 \land t = y) \to 1 - t = 1 - y$
214	209	oveq2d	$⊢ (s = 0 \land t = y) \to 2 s = 2 \cdot 0$
215		2t0e0	$⊢ 2 \cdot 0 = 0$
216	214 215	syl6eq	$⊢ (s = 0 \land t = y) \to 2 s = 0$
217	213 216	oveq12d	$⊢ (s = 0 \land t = y) \to (1 - t) 2 s = (1 - y) \cdot 0$
218	217	oveq2d	$⊢ (s = 0 \land t = y) \to 1 - (1 - t) 2 s = 1 - (1 - y) \cdot 0$
219	211 218	eqtrd	$⊢ (s = 0 \land t = y) \to if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1))) = 1 - (1 - y) \cdot 0$
220	219	fveq2d	$⊢ (s = 0 \land t = y) \to F (if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1)))) = F (1 - (1 - y) \cdot 0)$
221		fvex	$⊢ F (1 - (1 - y) \cdot 0) \in V$
222	220 3 221	ovmpoa	$⊢ (0 \in [0, 1] \land y \in [0, 1]) \to 0 H y = F (1 - (1 - y) \cdot 0)$
223	102 222	mpan	$⊢ y \in [0, 1] \to 0 H y = F (1 - (1 - y) \cdot 0)$
224		subcl	$⊢ (1 \in ℂ \land y \in ℂ) \to 1 - y \in ℂ$
225	150 169 224	sylancr	$⊢ y \in [0, 1] \to 1 - y \in ℂ$
226	225	mul01d	$⊢ y \in [0, 1] \to (1 - y) \cdot 0 = 0$
227	226	oveq2d	$⊢ y \in [0, 1] \to 1 - (1 - y) \cdot 0 = 1 - 0$
228	227 54	syl6eq	$⊢ y \in [0, 1] \to 1 - (1 - y) \cdot 0 = 1$
229	228	fveq2d	$⊢ y \in [0, 1] \to F (1 - (1 - y) \cdot 0) = F (1)$
230	223 229	eqtrd	$⊢ y \in [0, 1] \to 0 H y = F (1)$
231	10 8	pco0	$⊢ F \in (II Cn J) \to (G *_{𝑝} (J) F) (0) = G (0)$
232		oveq2	$⊢ x = 0 \to 1 - x = 1 - 0$
233	232 54	syl6eq	$⊢ x = 0 \to 1 - x = 1$
234	233	fveq2d	$⊢ x = 0 \to F (1 - x) = F (1)$
235	234 1 204	fvmpt	$⊢ 0 \in [0, 1] \to G (0) = F (1)$
236	102 235	ax-mp	$⊢ G (0) = F (1)$
237	231 236	syl6req	$⊢ F \in (II Cn J) \to F (1) = (G *_{𝑝} (J) F) (0)$
238	230 237	sylan9eqr	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 0 H y = (G *_{𝑝} (J) F) (0)$
239	37 39	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
240	40 239	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
241		simpl	$⊢ (s = 1 \land t = y) \to s = 1$
242	241	breq1d	$⊢ (s = 1 \land t = y) \to (s \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
243	240 242	mtbiri	$⊢ (s = 1 \land t = y) \to \neg s \leq \frac{1}{2}$
244	243	iffalsed	$⊢ (s = 1 \land t = y) \to if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1))) = 1 - (1 - t) (1 - (2 s - 1))$
245		simpr	$⊢ (s = 1 \land t = y) \to t = y$
246	245	oveq2d	$⊢ (s = 1 \land t = y) \to 1 - t = 1 - y$
247	241	oveq2d	$⊢ (s = 1 \land t = y) \to 2 s = 2 \cdot 1$
248		2t1e2	$⊢ 2 \cdot 1 = 2$
249	247 248	syl6eq	$⊢ (s = 1 \land t = y) \to 2 s = 2$
250	249	oveq1d	$⊢ (s = 1 \land t = y) \to 2 s - 1 = 2 - 1$
251		2m1e1	$⊢ 2 - 1 = 1$
252	250 251	syl6eq	$⊢ (s = 1 \land t = y) \to 2 s - 1 = 1$
253	252	oveq2d	$⊢ (s = 1 \land t = y) \to 1 - (2 s - 1) = 1 - 1$
254	253 13	syl6eq	$⊢ (s = 1 \land t = y) \to 1 - (2 s - 1) = 0$
255	246 254	oveq12d	$⊢ (s = 1 \land t = y) \to (1 - t) (1 - (2 s - 1)) = (1 - y) \cdot 0$
256	255	oveq2d	$⊢ (s = 1 \land t = y) \to 1 - (1 - t) (1 - (2 s - 1)) = 1 - (1 - y) \cdot 0$
257	244 256	eqtrd	$⊢ (s = 1 \land t = y) \to if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1))) = 1 - (1 - y) \cdot 0$
258	257	fveq2d	$⊢ (s = 1 \land t = y) \to F (if (s \leq \frac{1}{2}, 1 - (1 - t) 2 s, 1 - (1 - t) (1 - (2 s - 1)))) = F (1 - (1 - y) \cdot 0)$
259	258 3 221	ovmpoa	$⊢ (1 \in [0, 1] \land y \in [0, 1]) \to 1 H y = F (1 - (1 - y) \cdot 0)$
260	11 259	mpan	$⊢ y \in [0, 1] \to 1 H y = F (1 - (1 - y) \cdot 0)$
261	260 229	eqtrd	$⊢ y \in [0, 1] \to 1 H y = F (1)$
262	10 8	pco1	$⊢ F \in (II Cn J) \to (G *_{𝑝} (J) F) (1) = F (1)$
263	262	eqcomd	$⊢ F \in (II Cn J) \to F (1) = (G *_{𝑝} (J) F) (1)$
264	261 263	sylan9eqr	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 H y = (G *_{𝑝} (J) F) (1)$
265	19 30 100 167 208 238 264	isphtpy2d	$⊢ F \in (II Cn J) \to H \in ((G *_{𝑝} (J) F) PHtpy (J) P)$
266	265	ne0d	$⊢ F \in (II Cn J) \to (G *_{𝑝} (J) F) PHtpy (J) P \neq \emptyset$
267		isphtpc	$⊢ (G _{𝑝} (J) F) ≃_{ph} (J) P \leftrightarrow (G _{𝑝} (J) F \in (II Cn J) \land P \in (II Cn J) \land (G *_{𝑝} (J) F) PHtpy (J) P \neq \emptyset)$
268	19 30 266 267	syl3anbrc	$⊢ F \in (II Cn J) \to (G *_{𝑝} (J) F) ≃_{ph} (J) P$
269	265 268	jca	$⊢ F \in (II Cn J) \to (H \in ((G _{𝑝} (J) F) PHtpy (J) P) \land (G _{𝑝} (J) F) ≃_{ph} (J) P)$

Metamath Proof Explorer

Theorem pcorevlem

Proof