pcohtpylem

	Ref	Expression
Hypotheses	pcohtpy.4	$⊢ φ \to F (1) = G (0)$
	pcohtpy.5	$⊢ φ \to F ≃_{ph} (J) H$
	pcohtpy.6	$⊢ φ \to G ≃_{ph} (J) K$
	pcohtpylem.7	$⊢ P = (x \in [0, 1], y \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y))$
	pcohtpylem.8	$⊢ φ \to M \in (F PHtpy (J) H)$
	pcohtpylem.9	$⊢ φ \to N \in (G PHtpy (J) K)$
Assertion	pcohtpylem	$⊢ φ \to P \in ((F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K))$

Proof

Step	Hyp	Ref	Expression
1		pcohtpy.4	$⊢ φ \to F (1) = G (0)$
2		pcohtpy.5	$⊢ φ \to F ≃_{ph} (J) H$
3		pcohtpy.6	$⊢ φ \to G ≃_{ph} (J) K$
4		pcohtpylem.7	$⊢ P = (x \in [0, 1], y \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y))$
5		pcohtpylem.8	$⊢ φ \to M \in (F PHtpy (J) H)$
6		pcohtpylem.9	$⊢ φ \to N \in (G PHtpy (J) K)$
7		isphtpc	$⊢ F ≃_{ph} (J) H \leftrightarrow (F \in (II Cn J) \land H \in (II Cn J) \land F PHtpy (J) H \neq \emptyset)$
8	2 7	sylib	$⊢ φ \to (F \in (II Cn J) \land H \in (II Cn J) \land F PHtpy (J) H \neq \emptyset)$
9	8	simp1d	$⊢ φ \to F \in (II Cn J)$
10		isphtpc	$⊢ G ≃_{ph} (J) K \leftrightarrow (G \in (II Cn J) \land K \in (II Cn J) \land G PHtpy (J) K \neq \emptyset)$
11	3 10	sylib	$⊢ φ \to (G \in (II Cn J) \land K \in (II Cn J) \land G PHtpy (J) K \neq \emptyset)$
12	11	simp1d	$⊢ φ \to G \in (II Cn J)$
13	9 12 1	pcocn	$⊢ φ \to F *_{𝑝} (J) G \in (II Cn J)$
14	8	simp2d	$⊢ φ \to H \in (II Cn J)$
15	11	simp2d	$⊢ φ \to K \in (II Cn J)$
16	9 14 5	phtpy01	$⊢ φ \to (F (0) = H (0) \land F (1) = H (1))$
17	16	simprd	$⊢ φ \to F (1) = H (1)$
18	12 15 6	phtpy01	$⊢ φ \to (G (0) = K (0) \land G (1) = K (1))$
19	18	simpld	$⊢ φ \to G (0) = K (0)$
20	1 17 19	3eqtr3d	$⊢ φ \to H (1) = K (0)$
21	14 15 20	pcocn	$⊢ φ \to H *_{𝑝} (J) K \in (II Cn J)$
22		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
23		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]$
24		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] = topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]$
25		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
26		0red	$⊢ φ \to 0 \in ℝ$
27		1red	$⊢ φ \to 1 \in ℝ$
28		halfre	$⊢ \frac{1}{2} \in ℝ$
29		halfge0	$⊢ 0 \leq \frac{1}{2}$
30		1re	$⊢ 1 \in ℝ$
31		halflt1	$⊢ \frac{1}{2} < 1$
32	28 30 31	ltleii	$⊢ \frac{1}{2} \leq 1$
33		elicc01	$⊢ \frac{1}{2} \in [0, 1] \leftrightarrow (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2} \land \frac{1}{2} \leq 1)$
34	28 29 32 33	mpbir3an	$⊢ \frac{1}{2} \in [0, 1]$
35	34	a1i	$⊢ φ \to \frac{1}{2} \in [0, 1]$
36		iitopon	$⊢ II \in TopOn ([0, 1])$
37	36	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
38	1	adantr	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to F (1) = G (0)$
39	9 14 5	phtpyi	$⊢ (φ \land y \in [0, 1]) \to (0 M y = F (0) \land 1 M y = F (1))$
40	39	simprd	$⊢ (φ \land y \in [0, 1]) \to 1 M y = F (1)$
41	40	adantrl	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 1 M y = F (1)$
42	12 15 6	phtpyi	$⊢ (φ \land y \in [0, 1]) \to (0 N y = G (0) \land 1 N y = G (1))$
43	42	simpld	$⊢ (φ \land y \in [0, 1]) \to 0 N y = G (0)$
44	43	adantrl	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 0 N y = G (0)$
45	38 41 44	3eqtr4d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 1 M y = 0 N y$
46		simprl	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to x = \frac{1}{2}$
47	46	oveq2d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x = 2 (\frac{1}{2})$
48		2cn	$⊢ 2 \in ℂ$
49		2ne0	$⊢ 2 \neq 0$
50	48 49	recidi	$⊢ 2 (\frac{1}{2}) = 1$
51	47 50	eqtrdi	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x = 1$
52	51	oveq1d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x M y = 1 M y$
53	51	oveq1d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x - 1 = 1 - 1$
54		1m1e0	$⊢ 1 - 1 = 0$
55	53 54	eqtrdi	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x - 1 = 0$
56	55	oveq1d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to (2 x - 1) N y = 0 N y$
57	45 52 56	3eqtr4d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x M y = (2 x - 1) N y$
58		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
59		0re	$⊢ 0 \in ℝ$
60		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
61	59 28 60	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
62		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
63	58 61 62	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
64	63	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
65	64 37	cnmpt1st	$⊢ φ \to (x \in [0, \frac{1}{2}], y \in [0, 1] ⟼ x) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]))$
66	23	iihalf1cn	$⊢ (z \in [0, \frac{1}{2}] ⟼ 2 z) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
67	66	a1i	$⊢ φ \to (z \in [0, \frac{1}{2}] ⟼ 2 z) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
68		oveq2	$⊢ z = x \to 2 z = 2 x$
69	64 37 65 64 67 68	cnmpt21	$⊢ φ \to (x \in [0, \frac{1}{2}], y \in [0, 1] ⟼ 2 x) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
70	64 37	cnmpt2nd	$⊢ φ \to (x \in [0, \frac{1}{2}], y \in [0, 1] ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
71	9 14	phtpycn	$⊢ φ \to F PHtpy (J) H \subseteq (II \times_{t} II) Cn J$
72	71 5	sseldd	$⊢ φ \to M \in ((II \times_{t} II) Cn J)$
73	64 37 69 70 72	cnmpt22f	$⊢ φ \to (x \in [0, \frac{1}{2}], y \in [0, 1] ⟼ 2 x M y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn J)$
74		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
75	28 30 74	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
76		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
77	58 75 76	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
78	77	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
79	78 37	cnmpt1st	$⊢ φ \to (x \in [\frac{1}{2}, 1], y \in [0, 1] ⟼ x) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]))$
80	24	iihalf2cn	$⊢ (z \in [\frac{1}{2}, 1] ⟼ 2 z - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
81	80	a1i	$⊢ φ \to (z \in [\frac{1}{2}, 1] ⟼ 2 z - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
82	68	oveq1d	$⊢ z = x \to 2 z - 1 = 2 x - 1$
83	78 37 79 78 81 82	cnmpt21	$⊢ φ \to (x \in [\frac{1}{2}, 1], y \in [0, 1] ⟼ 2 x - 1) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
84	78 37	cnmpt2nd	$⊢ φ \to (x \in [\frac{1}{2}, 1], y \in [0, 1] ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
85	12 15	phtpycn	$⊢ φ \to G PHtpy (J) K \subseteq (II \times_{t} II) Cn J$
86	85 6	sseldd	$⊢ φ \to N \in ((II \times_{t} II) Cn J)$
87	78 37 83 84 86	cnmpt22f	$⊢ φ \to (x \in [\frac{1}{2}, 1], y \in [0, 1] ⟼ (2 x - 1) N y) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn J)$
88	22 23 24 25 26 27 35 37 57 73 87	cnmpopc	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y)) \in ((II \times_{t} II) Cn J)$
89	4 88	eqeltrid	$⊢ φ \to P \in ((II \times_{t} II) Cn J)$
90		simpll	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to φ$
91		elii1	$⊢ s \in [0, \frac{1}{2}] \leftrightarrow (s \in [0, 1] \land s \leq \frac{1}{2})$
92		iihalf1	$⊢ s \in [0, \frac{1}{2}] \to 2 s \in [0, 1]$
93	91 92	sylbir	$⊢ (s \in [0, 1] \land s \leq \frac{1}{2}) \to 2 s \in [0, 1]$
94	93	adantll	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 2 s \in [0, 1]$
95	9 14	phtpyhtpy	$⊢ φ \to F PHtpy (J) H \subseteq F (II Htpy J) H$
96	95 5	sseldd	$⊢ φ \to M \in (F (II Htpy J) H)$
97	37 9 14 96	htpyi	$⊢ (φ \land 2 s \in [0, 1]) \to (2 s M 0 = F (2 s) \land 2 s M 1 = H (2 s))$
98	90 94 97	syl2anc	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to (2 s M 0 = F (2 s) \land 2 s M 1 = H (2 s))$
99	98	simpld	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 2 s M 0 = F (2 s)$
100		simpll	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to φ$
101		elii2	$⊢ (s \in [0, 1] \land \neg s \leq \frac{1}{2}) \to s \in [\frac{1}{2}, 1]$
102	101	adantll	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to s \in [\frac{1}{2}, 1]$
103		iihalf2	$⊢ s \in [\frac{1}{2}, 1] \to 2 s - 1 \in [0, 1]$
104	102 103	syl	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to 2 s - 1 \in [0, 1]$
105	12 15	phtpyhtpy	$⊢ φ \to G PHtpy (J) K \subseteq G (II Htpy J) K$
106	105 6	sseldd	$⊢ φ \to N \in (G (II Htpy J) K)$
107	37 12 15 106	htpyi	$⊢ (φ \land 2 s - 1 \in [0, 1]) \to ((2 s - 1) N 0 = G (2 s - 1) \land (2 s - 1) N 1 = K (2 s - 1))$
108	100 104 107	syl2anc	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to ((2 s - 1) N 0 = G (2 s - 1) \land (2 s - 1) N 1 = K (2 s - 1))$
109	108	simpld	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to (2 s - 1) N 0 = G (2 s - 1)$
110	99 109	ifeq12da	$⊢ (φ \land s \in [0, 1]) \to if (s \leq \frac{1}{2}, 2 s M 0, (2 s - 1) N 0) = if (s \leq \frac{1}{2}, F (2 s), G (2 s - 1))$
111		simpr	$⊢ (φ \land s \in [0, 1]) \to s \in [0, 1]$
112		0elunit	$⊢ 0 \in [0, 1]$
113		simpl	$⊢ (x = s \land y = 0) \to x = s$
114	113	breq1d	$⊢ (x = s \land y = 0) \to (x \leq \frac{1}{2} \leftrightarrow s \leq \frac{1}{2})$
115	113	oveq2d	$⊢ (x = s \land y = 0) \to 2 x = 2 s$
116		simpr	$⊢ (x = s \land y = 0) \to y = 0$
117	115 116	oveq12d	$⊢ (x = s \land y = 0) \to 2 x M y = 2 s M 0$
118	115	oveq1d	$⊢ (x = s \land y = 0) \to 2 x - 1 = 2 s - 1$
119	118 116	oveq12d	$⊢ (x = s \land y = 0) \to (2 x - 1) N y = (2 s - 1) N 0$
120	114 117 119	ifbieq12d	$⊢ (x = s \land y = 0) \to if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y) = if (s \leq \frac{1}{2}, 2 s M 0, (2 s - 1) N 0)$
121		ovex	$⊢ 2 s M 0 \in V$
122		ovex	$⊢ (2 s - 1) N 0 \in V$
123	121 122	ifex	$⊢ if (s \leq \frac{1}{2}, 2 s M 0, (2 s - 1) N 0) \in V$
124	120 4 123	ovmpoa	$⊢ (s \in [0, 1] \land 0 \in [0, 1]) \to s P 0 = if (s \leq \frac{1}{2}, 2 s M 0, (2 s - 1) N 0)$
125	111 112 124	sylancl	$⊢ (φ \land s \in [0, 1]) \to s P 0 = if (s \leq \frac{1}{2}, 2 s M 0, (2 s - 1) N 0)$
126	9 12	pcovalg	$⊢ (φ \land s \in [0, 1]) \to (F *_{𝑝} (J) G) (s) = if (s \leq \frac{1}{2}, F (2 s), G (2 s - 1))$
127	110 125 126	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to s P 0 = (F *_{𝑝} (J) G) (s)$
128	98	simprd	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 2 s M 1 = H (2 s)$
129	108	simprd	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to (2 s - 1) N 1 = K (2 s - 1)$
130	128 129	ifeq12da	$⊢ (φ \land s \in [0, 1]) \to if (s \leq \frac{1}{2}, 2 s M 1, (2 s - 1) N 1) = if (s \leq \frac{1}{2}, H (2 s), K (2 s - 1))$
131		1elunit	$⊢ 1 \in [0, 1]$
132		simpl	$⊢ (x = s \land y = 1) \to x = s$
133	132	breq1d	$⊢ (x = s \land y = 1) \to (x \leq \frac{1}{2} \leftrightarrow s \leq \frac{1}{2})$
134	132	oveq2d	$⊢ (x = s \land y = 1) \to 2 x = 2 s$
135		simpr	$⊢ (x = s \land y = 1) \to y = 1$
136	134 135	oveq12d	$⊢ (x = s \land y = 1) \to 2 x M y = 2 s M 1$
137	134	oveq1d	$⊢ (x = s \land y = 1) \to 2 x - 1 = 2 s - 1$
138	137 135	oveq12d	$⊢ (x = s \land y = 1) \to (2 x - 1) N y = (2 s - 1) N 1$
139	133 136 138	ifbieq12d	$⊢ (x = s \land y = 1) \to if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y) = if (s \leq \frac{1}{2}, 2 s M 1, (2 s - 1) N 1)$
140		ovex	$⊢ 2 s M 1 \in V$
141		ovex	$⊢ (2 s - 1) N 1 \in V$
142	140 141	ifex	$⊢ if (s \leq \frac{1}{2}, 2 s M 1, (2 s - 1) N 1) \in V$
143	139 4 142	ovmpoa	$⊢ (s \in [0, 1] \land 1 \in [0, 1]) \to s P 1 = if (s \leq \frac{1}{2}, 2 s M 1, (2 s - 1) N 1)$
144	111 131 143	sylancl	$⊢ (φ \land s \in [0, 1]) \to s P 1 = if (s \leq \frac{1}{2}, 2 s M 1, (2 s - 1) N 1)$
145	14 15	pcovalg	$⊢ (φ \land s \in [0, 1]) \to (H *_{𝑝} (J) K) (s) = if (s \leq \frac{1}{2}, H (2 s), K (2 s - 1))$
146	130 144 145	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to s P 1 = (H *_{𝑝} (J) K) (s)$
147	9 14 5	phtpyi	$⊢ (φ \land s \in [0, 1]) \to (0 M s = F (0) \land 1 M s = F (1))$
148	147	simpld	$⊢ (φ \land s \in [0, 1]) \to 0 M s = F (0)$
149		simpl	$⊢ (x = 0 \land y = s) \to x = 0$
150	149 29	eqbrtrdi	$⊢ (x = 0 \land y = s) \to x \leq \frac{1}{2}$
151	150	iftrued	$⊢ (x = 0 \land y = s) \to if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y) = 2 x M y$
152	149	oveq2d	$⊢ (x = 0 \land y = s) \to 2 x = 2 \cdot 0$
153		2t0e0	$⊢ 2 \cdot 0 = 0$
154	152 153	eqtrdi	$⊢ (x = 0 \land y = s) \to 2 x = 0$
155		simpr	$⊢ (x = 0 \land y = s) \to y = s$
156	154 155	oveq12d	$⊢ (x = 0 \land y = s) \to 2 x M y = 0 M s$
157	151 156	eqtrd	$⊢ (x = 0 \land y = s) \to if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y) = 0 M s$
158		ovex	$⊢ 0 M s \in V$
159	157 4 158	ovmpoa	$⊢ (0 \in [0, 1] \land s \in [0, 1]) \to 0 P s = 0 M s$
160	112 111 159	sylancr	$⊢ (φ \land s \in [0, 1]) \to 0 P s = 0 M s$
161	9 12	pco0	$⊢ φ \to (F *_{𝑝} (J) G) (0) = F (0)$
162	161	adantr	$⊢ (φ \land s \in [0, 1]) \to (F *_{𝑝} (J) G) (0) = F (0)$
163	148 160 162	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to 0 P s = (F *_{𝑝} (J) G) (0)$
164	12 15 6	phtpyi	$⊢ (φ \land s \in [0, 1]) \to (0 N s = G (0) \land 1 N s = G (1))$
165	164	simprd	$⊢ (φ \land s \in [0, 1]) \to 1 N s = G (1)$
166	28 30	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
167	31 166	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
168		simpl	$⊢ (x = 1 \land y = s) \to x = 1$
169	168	breq1d	$⊢ (x = 1 \land y = s) \to (x \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
170	167 169	mtbiri	$⊢ (x = 1 \land y = s) \to \neg x \leq \frac{1}{2}$
171	170	iffalsed	$⊢ (x = 1 \land y = s) \to if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y) = (2 x - 1) N y$
172	168	oveq2d	$⊢ (x = 1 \land y = s) \to 2 x = 2 \cdot 1$
173		2t1e2	$⊢ 2 \cdot 1 = 2$
174	172 173	eqtrdi	$⊢ (x = 1 \land y = s) \to 2 x = 2$
175	174	oveq1d	$⊢ (x = 1 \land y = s) \to 2 x - 1 = 2 - 1$
176		2m1e1	$⊢ 2 - 1 = 1$
177	175 176	eqtrdi	$⊢ (x = 1 \land y = s) \to 2 x - 1 = 1$
178		simpr	$⊢ (x = 1 \land y = s) \to y = s$
179	177 178	oveq12d	$⊢ (x = 1 \land y = s) \to (2 x - 1) N y = 1 N s$
180	171 179	eqtrd	$⊢ (x = 1 \land y = s) \to if (x \leq \frac{1}{2}, 2 x M y, (2 x - 1) N y) = 1 N s$
181		ovex	$⊢ 1 N s \in V$
182	180 4 181	ovmpoa	$⊢ (1 \in [0, 1] \land s \in [0, 1]) \to 1 P s = 1 N s$
183	131 111 182	sylancr	$⊢ (φ \land s \in [0, 1]) \to 1 P s = 1 N s$
184	9 12	pco1	$⊢ φ \to (F *_{𝑝} (J) G) (1) = G (1)$
185	184	adantr	$⊢ (φ \land s \in [0, 1]) \to (F *_{𝑝} (J) G) (1) = G (1)$
186	165 183 185	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to 1 P s = (F *_{𝑝} (J) G) (1)$
187	13 21 89 127 146 163 186	isphtpy2d	$⊢ φ \to P \in ((F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K))$

Metamath Proof Explorer

Theorem pcohtpylem

Proof