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		2thalfe1	$⊢ 2 (\frac{1}{2}) = 1$
49	47 48	eqtrdi	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x = 1$
50	49	oveq1d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x M y = 1 M y$
51	49	oveq1d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x - 1 = 1 - 1$
52		1m1e0	$⊢ 1 - 1 = 0$
53	51 52	eqtrdi	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x - 1 = 0$
54	53	oveq1d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to (2 x - 1) N y = 0 N y$
55	45 50 54	3eqtr4d	$⊢ (φ \land (x = \frac{1}{2} \land y \in [0, 1])) \to 2 x M y = (2 x - 1) N y$
56		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
57		0re	$⊢ 0 \in ℝ$
58		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
59	57 28 58	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
60		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
61	56 59 60	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
62	61	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
63	62 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}]))$
64	23	iihalf1cn	$⊢ (z \in [0, \frac{1}{2}] ⟼ 2 z) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
65	64	a1i	$⊢ φ \to (z \in [0, \frac{1}{2}] ⟼ 2 z) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
66		oveq2	$⊢ z = x \to 2 z = 2 x$
67	62 37 63 62 65 66	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)$
68	62 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)$
69	9 14	phtpycn	$⊢ φ \to F PHtpy (J) H \subseteq (II \times_{t} II) Cn J$
70	69 5	sseldd	$⊢ φ \to M \in ((II \times_{t} II) Cn J)$
71	62 37 67 68 70	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)$
72		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
73	28 30 72	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
74		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
75	56 73 74	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
76	75	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
77	76 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]))$
78	24	iihalf2cn	$⊢ (z \in [\frac{1}{2}, 1] ⟼ 2 z - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
79	78	a1i	$⊢ φ \to (z \in [\frac{1}{2}, 1] ⟼ 2 z - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
80	66	oveq1d	$⊢ z = x \to 2 z - 1 = 2 x - 1$
81	76 37 77 76 79 80	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)$
82	76 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)$
83	12 15	phtpycn	$⊢ φ \to G PHtpy (J) K \subseteq (II \times_{t} II) Cn J$
84	83 6	sseldd	$⊢ φ \to N \in ((II \times_{t} II) Cn J)$
85	76 37 81 82 84	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)$
86	22 23 24 25 26 27 35 37 55 71 85	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)$
87	4 86	eqeltrid	$⊢ φ \to P \in ((II \times_{t} II) Cn J)$
88		simpll	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to φ$
89		elii1	$⊢ s \in [0, \frac{1}{2}] \leftrightarrow (s \in [0, 1] \land s \leq \frac{1}{2})$
90		iihalf1	$⊢ s \in [0, \frac{1}{2}] \to 2 s \in [0, 1]$
91	89 90	sylbir	$⊢ (s \in [0, 1] \land s \leq \frac{1}{2}) \to 2 s \in [0, 1]$
92	91	adantll	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 2 s \in [0, 1]$
93	9 14	phtpyhtpy	$⊢ φ \to F PHtpy (J) H \subseteq F (II Htpy J) H$
94	93 5	sseldd	$⊢ φ \to M \in (F (II Htpy J) H)$
95	37 9 14 94	htpyi	$⊢ (φ \land 2 s \in [0, 1]) \to (2 s M 0 = F (2 s) \land 2 s M 1 = H (2 s))$
96	88 92 95	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))$
97	96	simpld	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 2 s M 0 = F (2 s)$
98		simpll	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to φ$
99		elii2	$⊢ (s \in [0, 1] \land \neg s \leq \frac{1}{2}) \to s \in [\frac{1}{2}, 1]$
100	99	adantll	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to s \in [\frac{1}{2}, 1]$
101		iihalf2	$⊢ s \in [\frac{1}{2}, 1] \to 2 s - 1 \in [0, 1]$
102	100 101	syl	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to 2 s - 1 \in [0, 1]$
103	12 15	phtpyhtpy	$⊢ φ \to G PHtpy (J) K \subseteq G (II Htpy J) K$
104	103 6	sseldd	$⊢ φ \to N \in (G (II Htpy J) K)$
105	37 12 15 104	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))$
106	98 102 105	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))$
107	106	simpld	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to (2 s - 1) N 0 = G (2 s - 1)$
108	97 107	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))$
109		simpr	$⊢ (φ \land s \in [0, 1]) \to s \in [0, 1]$
110		0elunit	$⊢ 0 \in [0, 1]$
111		simpl	$⊢ (x = s \land y = 0) \to x = s$
112	111	breq1d	$⊢ (x = s \land y = 0) \to (x \leq \frac{1}{2} \leftrightarrow s \leq \frac{1}{2})$
113	111	oveq2d	$⊢ (x = s \land y = 0) \to 2 x = 2 s$
114		simpr	$⊢ (x = s \land y = 0) \to y = 0$
115	113 114	oveq12d	$⊢ (x = s \land y = 0) \to 2 x M y = 2 s M 0$
116	113	oveq1d	$⊢ (x = s \land y = 0) \to 2 x - 1 = 2 s - 1$
117	116 114	oveq12d	$⊢ (x = s \land y = 0) \to (2 x - 1) N y = (2 s - 1) N 0$
118	112 115 117	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)$
119		ovex	$⊢ 2 s M 0 \in V$
120		ovex	$⊢ (2 s - 1) N 0 \in V$
121	119 120	ifex	$⊢ if (s \leq \frac{1}{2}, 2 s M 0, (2 s - 1) N 0) \in V$
122	118 4 121	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)$
123	109 110 122	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)$
124	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))$
125	108 123 124	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to s P 0 = (F *_{𝑝} (J) G) (s)$
126	96	simprd	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 2 s M 1 = H (2 s)$
127	106	simprd	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to (2 s - 1) N 1 = K (2 s - 1)$
128	126 127	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))$
129		1elunit	$⊢ 1 \in [0, 1]$
130		simpl	$⊢ (x = s \land y = 1) \to x = s$
131	130	breq1d	$⊢ (x = s \land y = 1) \to (x \leq \frac{1}{2} \leftrightarrow s \leq \frac{1}{2})$
132	130	oveq2d	$⊢ (x = s \land y = 1) \to 2 x = 2 s$
133		simpr	$⊢ (x = s \land y = 1) \to y = 1$
134	132 133	oveq12d	$⊢ (x = s \land y = 1) \to 2 x M y = 2 s M 1$
135	132	oveq1d	$⊢ (x = s \land y = 1) \to 2 x - 1 = 2 s - 1$
136	135 133	oveq12d	$⊢ (x = s \land y = 1) \to (2 x - 1) N y = (2 s - 1) N 1$
137	131 134 136	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)$
138		ovex	$⊢ 2 s M 1 \in V$
139		ovex	$⊢ (2 s - 1) N 1 \in V$
140	138 139	ifex	$⊢ if (s \leq \frac{1}{2}, 2 s M 1, (2 s - 1) N 1) \in V$
141	137 4 140	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)$
142	109 129 141	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)$
143	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))$
144	128 142 143	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to s P 1 = (H *_{𝑝} (J) K) (s)$
145	9 14 5	phtpyi	$⊢ (φ \land s \in [0, 1]) \to (0 M s = F (0) \land 1 M s = F (1))$
146	145	simpld	$⊢ (φ \land s \in [0, 1]) \to 0 M s = F (0)$
147		simpl	$⊢ (x = 0 \land y = s) \to x = 0$
148	147 29	eqbrtrdi	$⊢ (x = 0 \land y = s) \to x \leq \frac{1}{2}$
149	148	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$
150	147	oveq2d	$⊢ (x = 0 \land y = s) \to 2 x = 2 \cdot 0$
151		2t0e0	$⊢ 2 \cdot 0 = 0$
152	150 151	eqtrdi	$⊢ (x = 0 \land y = s) \to 2 x = 0$
153		simpr	$⊢ (x = 0 \land y = s) \to y = s$
154	152 153	oveq12d	$⊢ (x = 0 \land y = s) \to 2 x M y = 0 M s$
155	149 154	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$
156		ovex	$⊢ 0 M s \in V$
157	155 4 156	ovmpoa	$⊢ (0 \in [0, 1] \land s \in [0, 1]) \to 0 P s = 0 M s$
158	110 109 157	sylancr	$⊢ (φ \land s \in [0, 1]) \to 0 P s = 0 M s$
159	9 12	pco0	$⊢ φ \to (F *_{𝑝} (J) G) (0) = F (0)$
160	159	adantr	$⊢ (φ \land s \in [0, 1]) \to (F *_{𝑝} (J) G) (0) = F (0)$
161	146 158 160	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to 0 P s = (F *_{𝑝} (J) G) (0)$
162	12 15 6	phtpyi	$⊢ (φ \land s \in [0, 1]) \to (0 N s = G (0) \land 1 N s = G (1))$
163	162	simprd	$⊢ (φ \land s \in [0, 1]) \to 1 N s = G (1)$
164	28 30	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
165	31 164	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
166		simpl	$⊢ (x = 1 \land y = s) \to x = 1$
167	166	breq1d	$⊢ (x = 1 \land y = s) \to (x \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
168	165 167	mtbiri	$⊢ (x = 1 \land y = s) \to \neg x \leq \frac{1}{2}$
169	168	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$
170	166	oveq2d	$⊢ (x = 1 \land y = s) \to 2 x = 2 \cdot 1$
171		2t1e2	$⊢ 2 \cdot 1 = 2$
172	170 171	eqtrdi	$⊢ (x = 1 \land y = s) \to 2 x = 2$
173	172	oveq1d	$⊢ (x = 1 \land y = s) \to 2 x - 1 = 2 - 1$
174		2m1e1	$⊢ 2 - 1 = 1$
175	173 174	eqtrdi	$⊢ (x = 1 \land y = s) \to 2 x - 1 = 1$
176		simpr	$⊢ (x = 1 \land y = s) \to y = s$
177	175 176	oveq12d	$⊢ (x = 1 \land y = s) \to (2 x - 1) N y = 1 N s$
178	169 177	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$
179		ovex	$⊢ 1 N s \in V$
180	178 4 179	ovmpoa	$⊢ (1 \in [0, 1] \land s \in [0, 1]) \to 1 P s = 1 N s$
181	129 109 180	sylancr	$⊢ (φ \land s \in [0, 1]) \to 1 P s = 1 N s$
182	9 12	pco1	$⊢ φ \to (F *_{𝑝} (J) G) (1) = G (1)$
183	182	adantr	$⊢ (φ \land s \in [0, 1]) \to (F *_{𝑝} (J) G) (1) = G (1)$
184	163 181 183	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to 1 P s = (F *_{𝑝} (J) G) (1)$
185	13 21 87 125 144 161 184	isphtpy2d	$⊢ φ \to P \in ((F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K))$

Metamath Proof Explorer

Theorem pcohtpylem

Proof