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	eqtrdi	$⊢ 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		ffvelcdm	$⊢ (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		2thalfe1	$⊢ 2 (\frac{1}{2}) = 1$
48	46 47	eqtrdi	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s = 1$
49	48	oveq1d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s - 1 = 1 - 1$
50	49 13	eqtrdi	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s - 1 = 0$
51	50	oveq2d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 1 - (2 s - 1) = 1 - 0$
52		1m0e1	$⊢ 1 - 0 = 1$
53	51 52	eqtrdi	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 1 - (2 s - 1) = 1$
54	48 53	eqtr4d	$⊢ (F \in (II Cn J) \land (s = \frac{1}{2} \land t \in [0, 1])) \to 2 s = 1 - (2 s - 1)$
55	54	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))$
56	55	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))$
57		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
58		0re	$⊢ 0 \in ℝ$
59		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
60	58 37 59	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
61		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
62	57 60 61	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
63	62	a1i	$⊢ F \in (II Cn J) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
64	63 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)$
65		oveq2	$⊢ x = t \to 1 - x = 1 - t$
66	63 5 64 5 7 65	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)$
67	63 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}]))$
68	32	iihalf1cn	$⊢ (x \in [0, \frac{1}{2}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
69	68	a1i	$⊢ F \in (II Cn J) \to (x \in [0, \frac{1}{2}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
70		oveq2	$⊢ x = s \to 2 x = 2 s$
71	63 5 67 63 69 70	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)$
72		iimulcn	$⊢ (x \in [0, 1], y \in [0, 1] ⟼ x y) \in ((II \times_{t} II) Cn II)$
73	72	a1i	$⊢ F \in (II Cn J) \to (x \in [0, 1], y \in [0, 1] ⟼ x y) \in ((II \times_{t} II) Cn II)$
74		oveq12	$⊢ (x = 1 - t \land y = 2 s) \to x y = (1 - t) 2 s$
75	63 5 66 71 5 5 73 74	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)$
76		oveq2	$⊢ x = (1 - t) 2 s \to 1 - x = 1 - (1 - t) 2 s$
77	63 5 75 5 7 76	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)$
78		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
79	37 39 78	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
80		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
81	57 79 80	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
82	81	a1i	$⊢ F \in (II Cn J) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
83	82 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)$
84	82 5 83 5 7 65	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)$
85	82 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]))$
86	33	iihalf2cn	$⊢ (x \in [\frac{1}{2}, 1] ⟼ 2 x - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
87	86	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)$
88	70	oveq1d	$⊢ x = s \to 2 x - 1 = 2 s - 1$
89	82 5 85 82 87 88	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)$
90		oveq2	$⊢ x = 2 s - 1 \to 1 - x = 1 - (2 s - 1)$
91	82 5 89 5 7 90	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)$
92		oveq12	$⊢ (x = 1 - t \land y = 1 - (2 s - 1)) \to x y = (1 - t) (1 - (2 s - 1))$
93	82 5 84 91 5 5 73 92	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)$
94		oveq2	$⊢ x = (1 - t) (1 - (2 s - 1)) \to 1 - x = 1 - (1 - t) (1 - (2 s - 1))$
95	82 5 93 5 7 94	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)$
96	31 32 33 34 35 36 44 5 56 77 95	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)$
97	5 5 96 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)$
98	3 97	eqeltrid	$⊢ F \in (II Cn J) \to H \in ((II \times_{t} II) Cn J)$
99		simpr	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to y \in [0, 1]$
100		0elunit	$⊢ 0 \in [0, 1]$
101		simpl	$⊢ (s = y \land t = 0) \to s = y$
102	101	breq1d	$⊢ (s = y \land t = 0) \to (s \leq \frac{1}{2} \leftrightarrow y \leq \frac{1}{2})$
103		simpr	$⊢ (s = y \land t = 0) \to t = 0$
104	103	oveq2d	$⊢ (s = y \land t = 0) \to 1 - t = 1 - 0$
105	104 52	eqtrdi	$⊢ (s = y \land t = 0) \to 1 - t = 1$
106	101	oveq2d	$⊢ (s = y \land t = 0) \to 2 s = 2 y$
107	105 106	oveq12d	$⊢ (s = y \land t = 0) \to (1 - t) 2 s = 1 2 y$
108	107	oveq2d	$⊢ (s = y \land t = 0) \to 1 - (1 - t) 2 s = 1 - 1 2 y$
109	106	oveq1d	$⊢ (s = y \land t = 0) \to 2 s - 1 = 2 y - 1$
110	109	oveq2d	$⊢ (s = y \land t = 0) \to 1 - (2 s - 1) = 1 - (2 y - 1)$
111	105 110	oveq12d	$⊢ (s = y \land t = 0) \to (1 - t) (1 - (2 s - 1)) = 1 (1 - (2 y - 1))$
112	111	oveq2d	$⊢ (s = y \land t = 0) \to 1 - (1 - t) (1 - (2 s - 1)) = 1 - 1 (1 - (2 y - 1))$
113	102 108 112	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)))$
114	113	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))))$
115		fvex	$⊢ F (if (y \leq \frac{1}{2}, 1 - 1 2 y, 1 - 1 (1 - (2 y - 1)))) \in V$
116	114 3 115	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))))$
117	99 100 116	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))))$
118		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$
119	118	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$
120	119	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)$
121		elii1	$⊢ y \in [0, \frac{1}{2}] \leftrightarrow (y \in [0, 1] \land y \leq \frac{1}{2})$
122	10 8	pcoval1	$⊢ (F \in (II Cn J) \land y \in [0, \frac{1}{2}]) \to (G *_{𝑝} (J) F) (y) = G (2 y)$
123		iihalf1	$⊢ y \in [0, \frac{1}{2}] \to 2 y \in [0, 1]$
124	123	adantl	$⊢ (F \in (II Cn J) \land y \in [0, \frac{1}{2}]) \to 2 y \in [0, 1]$
125		oveq2	$⊢ x = 2 y \to 1 - x = 1 - 2 y$
126	125	fveq2d	$⊢ x = 2 y \to F (1 - x) = F (1 - 2 y)$
127		fvex	$⊢ F (1 - 2 y) \in V$
128	126 1 127	fvmpt	$⊢ 2 y \in [0, 1] \to G (2 y) = F (1 - 2 y)$
129		unitssre	$⊢ [0, 1] \subseteq ℝ$
130	129	sseli	$⊢ 2 y \in [0, 1] \to 2 y \in ℝ$
131	130	recnd	$⊢ 2 y \in [0, 1] \to 2 y \in ℂ$
132	131	mullidd	$⊢ 2 y \in [0, 1] \to 1 2 y = 2 y$
133	132	oveq2d	$⊢ 2 y \in [0, 1] \to 1 - 1 2 y = 1 - 2 y$
134	133	fveq2d	$⊢ 2 y \in [0, 1] \to F (1 - 1 2 y) = F (1 - 2 y)$
135	128 134	eqtr4d	$⊢ 2 y \in [0, 1] \to G (2 y) = F (1 - 1 2 y)$
136	124 135	syl	$⊢ (F \in (II Cn J) \land y \in [0, \frac{1}{2}]) \to G (2 y) = F (1 - 1 2 y)$
137	122 136	eqtrd	$⊢ (F \in (II Cn J) \land y \in [0, \frac{1}{2}]) \to (G *_{𝑝} (J) F) (y) = F (1 - 1 2 y)$
138	121 137	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)$
139	138	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)$
140	120 139	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)$
141		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))$
142	141	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))$
143	142	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)))$
144		elii2	$⊢ (y \in [0, 1] \land \neg y \leq \frac{1}{2}) \to y \in [\frac{1}{2}, 1]$
145	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)$
146		iihalf2	$⊢ y \in [\frac{1}{2}, 1] \to 2 y - 1 \in [0, 1]$
147	146	adantl	$⊢ (F \in (II Cn J) \land y \in [\frac{1}{2}, 1]) \to 2 y - 1 \in [0, 1]$
148		ax-1cn	$⊢ 1 \in ℂ$
149	129	sseli	$⊢ 2 y - 1 \in [0, 1] \to 2 y - 1 \in ℝ$
150	149	recnd	$⊢ 2 y - 1 \in [0, 1] \to 2 y - 1 \in ℂ$
151		subcl	$⊢ (1 \in ℂ \land 2 y - 1 \in ℂ) \to 1 - (2 y - 1) \in ℂ$
152	148 150 151	sylancr	$⊢ 2 y - 1 \in [0, 1] \to 1 - (2 y - 1) \in ℂ$
153	152	mullidd	$⊢ 2 y - 1 \in [0, 1] \to 1 (1 - (2 y - 1)) = 1 - (2 y - 1)$
154	153	oveq2d	$⊢ 2 y - 1 \in [0, 1] \to 1 - 1 (1 - (2 y - 1)) = 1 - (1 - (2 y - 1))$
155		nncan	$⊢ (1 \in ℂ \land 2 y - 1 \in ℂ) \to 1 - (1 - (2 y - 1)) = 2 y - 1$
156	148 150 155	sylancr	$⊢ 2 y - 1 \in [0, 1] \to 1 - (1 - (2 y - 1)) = 2 y - 1$
157	154 156	eqtr2d	$⊢ 2 y - 1 \in [0, 1] \to 2 y - 1 = 1 - 1 (1 - (2 y - 1))$
158	147 157	syl	$⊢ (F \in (II Cn J) \land y \in [\frac{1}{2}, 1]) \to 2 y - 1 = 1 - 1 (1 - (2 y - 1))$
159	158	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)))$
160	145 159	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)))$
161	144 160	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)))$
162	161	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)))$
163	143 162	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)$
164	140 163	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)$
165	117 164	eqtrd	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to y H 0 = (G *_{𝑝} (J) F) (y)$
166		2cn	$⊢ 2 \in ℂ$
167	129	sseli	$⊢ y \in [0, 1] \to y \in ℝ$
168	167	recnd	$⊢ y \in [0, 1] \to y \in ℂ$
169		mulcl	$⊢ (2 \in ℂ \land y \in ℂ) \to 2 y \in ℂ$
170	166 168 169	sylancr	$⊢ y \in [0, 1] \to 2 y \in ℂ$
171	170	adantl	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 2 y \in ℂ$
172	171	mul02d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 0 \cdot 2 y = 0$
173	172	oveq2d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - 0 \cdot 2 y = 1 - 0$
174	173 52	eqtrdi	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - 0 \cdot 2 y = 1$
175		subcl	$⊢ (2 y \in ℂ \land 1 \in ℂ) \to 2 y - 1 \in ℂ$
176	171 148 175	sylancl	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 2 y - 1 \in ℂ$
177	148 176 151	sylancr	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - (2 y - 1) \in ℂ$
178	177	mul02d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 0 \cdot (1 - (2 y - 1)) = 0$
179	178	oveq2d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - 0 \cdot (1 - (2 y - 1)) = 1 - 0$
180	179 52	eqtrdi	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 - 0 \cdot (1 - (2 y - 1)) = 1$
181	174 180	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)$
182		ifid	$⊢ if (y \leq \frac{1}{2}, 1, 1) = 1$
183	181 182	eqtrdi	$⊢ (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$
184	183	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)$
185		simpl	$⊢ (s = y \land t = 1) \to s = y$
186	185	breq1d	$⊢ (s = y \land t = 1) \to (s \leq \frac{1}{2} \leftrightarrow y \leq \frac{1}{2})$
187		simpr	$⊢ (s = y \land t = 1) \to t = 1$
188	187	oveq2d	$⊢ (s = y \land t = 1) \to 1 - t = 1 - 1$
189	188 13	eqtrdi	$⊢ (s = y \land t = 1) \to 1 - t = 0$
190	185	oveq2d	$⊢ (s = y \land t = 1) \to 2 s = 2 y$
191	189 190	oveq12d	$⊢ (s = y \land t = 1) \to (1 - t) 2 s = 0 \cdot 2 y$
192	191	oveq2d	$⊢ (s = y \land t = 1) \to 1 - (1 - t) 2 s = 1 - 0 \cdot 2 y$
193	190	oveq1d	$⊢ (s = y \land t = 1) \to 2 s - 1 = 2 y - 1$
194	193	oveq2d	$⊢ (s = y \land t = 1) \to 1 - (2 s - 1) = 1 - (2 y - 1)$
195	189 194	oveq12d	$⊢ (s = y \land t = 1) \to (1 - t) (1 - (2 s - 1)) = 0 \cdot (1 - (2 y - 1))$
196	195	oveq2d	$⊢ (s = y \land t = 1) \to 1 - (1 - t) (1 - (2 s - 1)) = 1 - 0 \cdot (1 - (2 y - 1))$
197	186 192 196	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)))$
198	197	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))))$
199		fvex	$⊢ F (if (y \leq \frac{1}{2}, 1 - 0 \cdot 2 y, 1 - 0 \cdot (1 - (2 y - 1)))) \in V$
200	198 3 199	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))))$
201	99 11 200	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))))$
202	2	fveq1i	$⊢ P (y) = ([0, 1] \times \{F (1)\}) (y)$
203		fvex	$⊢ F (1) \in V$
204	203	fvconst2	$⊢ y \in [0, 1] \to ([0, 1] \times \{F (1)\}) (y) = F (1)$
205	204	adantl	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to ([0, 1] \times \{F (1)\}) (y) = F (1)$
206	202 205	eqtrid	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to P (y) = F (1)$
207	184 201 206	3eqtr4d	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to y H 1 = P (y)$
208		simpl	$⊢ (s = 0 \land t = y) \to s = 0$
209	208 38	eqbrtrdi	$⊢ (s = 0 \land t = y) \to s \leq \frac{1}{2}$
210	209	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$
211		simpr	$⊢ (s = 0 \land t = y) \to t = y$
212	211	oveq2d	$⊢ (s = 0 \land t = y) \to 1 - t = 1 - y$
213	208	oveq2d	$⊢ (s = 0 \land t = y) \to 2 s = 2 \cdot 0$
214		2t0e0	$⊢ 2 \cdot 0 = 0$
215	213 214	eqtrdi	$⊢ (s = 0 \land t = y) \to 2 s = 0$
216	212 215	oveq12d	$⊢ (s = 0 \land t = y) \to (1 - t) 2 s = (1 - y) \cdot 0$
217	216	oveq2d	$⊢ (s = 0 \land t = y) \to 1 - (1 - t) 2 s = 1 - (1 - y) \cdot 0$
218	210 217	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$
219	218	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)$
220		fvex	$⊢ F (1 - (1 - y) \cdot 0) \in V$
221	219 3 220	ovmpoa	$⊢ (0 \in [0, 1] \land y \in [0, 1]) \to 0 H y = F (1 - (1 - y) \cdot 0)$
222	100 221	mpan	$⊢ y \in [0, 1] \to 0 H y = F (1 - (1 - y) \cdot 0)$
223		subcl	$⊢ (1 \in ℂ \land y \in ℂ) \to 1 - y \in ℂ$
224	148 168 223	sylancr	$⊢ y \in [0, 1] \to 1 - y \in ℂ$
225	224	mul01d	$⊢ y \in [0, 1] \to (1 - y) \cdot 0 = 0$
226	225	oveq2d	$⊢ y \in [0, 1] \to 1 - (1 - y) \cdot 0 = 1 - 0$
227	226 52	eqtrdi	$⊢ y \in [0, 1] \to 1 - (1 - y) \cdot 0 = 1$
228	227	fveq2d	$⊢ y \in [0, 1] \to F (1 - (1 - y) \cdot 0) = F (1)$
229	222 228	eqtrd	$⊢ y \in [0, 1] \to 0 H y = F (1)$
230	10 8	pco0	$⊢ F \in (II Cn J) \to (G *_{𝑝} (J) F) (0) = G (0)$
231		oveq2	$⊢ x = 0 \to 1 - x = 1 - 0$
232	231 52	eqtrdi	$⊢ x = 0 \to 1 - x = 1$
233	232	fveq2d	$⊢ x = 0 \to F (1 - x) = F (1)$
234	233 1 203	fvmpt	$⊢ 0 \in [0, 1] \to G (0) = F (1)$
235	100 234	ax-mp	$⊢ G (0) = F (1)$
236	230 235	eqtr2di	$⊢ F \in (II Cn J) \to F (1) = (G *_{𝑝} (J) F) (0)$
237	229 236	sylan9eqr	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 0 H y = (G *_{𝑝} (J) F) (0)$
238	37 39	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
239	40 238	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
240		simpl	$⊢ (s = 1 \land t = y) \to s = 1$
241	240	breq1d	$⊢ (s = 1 \land t = y) \to (s \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
242	239 241	mtbiri	$⊢ (s = 1 \land t = y) \to \neg s \leq \frac{1}{2}$
243	242	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))$
244		simpr	$⊢ (s = 1 \land t = y) \to t = y$
245	244	oveq2d	$⊢ (s = 1 \land t = y) \to 1 - t = 1 - y$
246	240	oveq2d	$⊢ (s = 1 \land t = y) \to 2 s = 2 \cdot 1$
247		2t1e2	$⊢ 2 \cdot 1 = 2$
248	246 247	eqtrdi	$⊢ (s = 1 \land t = y) \to 2 s = 2$
249	248	oveq1d	$⊢ (s = 1 \land t = y) \to 2 s - 1 = 2 - 1$
250		2m1e1	$⊢ 2 - 1 = 1$
251	249 250	eqtrdi	$⊢ (s = 1 \land t = y) \to 2 s - 1 = 1$
252	251	oveq2d	$⊢ (s = 1 \land t = y) \to 1 - (2 s - 1) = 1 - 1$
253	252 13	eqtrdi	$⊢ (s = 1 \land t = y) \to 1 - (2 s - 1) = 0$
254	245 253	oveq12d	$⊢ (s = 1 \land t = y) \to (1 - t) (1 - (2 s - 1)) = (1 - y) \cdot 0$
255	254	oveq2d	$⊢ (s = 1 \land t = y) \to 1 - (1 - t) (1 - (2 s - 1)) = 1 - (1 - y) \cdot 0$
256	243 255	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$
257	256	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)$
258	257 3 220	ovmpoa	$⊢ (1 \in [0, 1] \land y \in [0, 1]) \to 1 H y = F (1 - (1 - y) \cdot 0)$
259	11 258	mpan	$⊢ y \in [0, 1] \to 1 H y = F (1 - (1 - y) \cdot 0)$
260	259 228	eqtrd	$⊢ y \in [0, 1] \to 1 H y = F (1)$
261	10 8	pco1	$⊢ F \in (II Cn J) \to (G *_{𝑝} (J) F) (1) = F (1)$
262	261	eqcomd	$⊢ F \in (II Cn J) \to F (1) = (G *_{𝑝} (J) F) (1)$
263	260 262	sylan9eqr	$⊢ (F \in (II Cn J) \land y \in [0, 1]) \to 1 H y = (G *_{𝑝} (J) F) (1)$
264	19 30 98 165 207 237 263	isphtpy2d	$⊢ F \in (II Cn J) \to H \in ((G *_{𝑝} (J) F) PHtpy (J) P)$
265	264	ne0d	$⊢ F \in (II Cn J) \to (G *_{𝑝} (J) F) PHtpy (J) P \neq \emptyset$
266		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)$
267	19 30 265 266	syl3anbrc	$⊢ F \in (II Cn J) \to (G *_{𝑝} (J) F) ≃_{ph} (J) P$
268	264 267	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