pcoass

Description: Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010) (Proof shortened by Mario Carneiro, 8-Jun-2014)

	Ref	Expression
Hypotheses	pcoass.2	$⊢ φ \to F \in (II Cn J)$
	pcoass.3	$⊢ φ \to G \in (II Cn J)$
	pcoass.4	$⊢ φ \to H \in (II Cn J)$
	pcoass.5	$⊢ φ \to F (1) = G (0)$
	pcoass.6	$⊢ φ \to G (1) = H (0)$
	pcoass.7	$⊢ P = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})))$
Assertion	pcoass	$⊢ φ \to ((F _{𝑝} (J) G) _{𝑝} (J) H) ≃_{ph} (J) (F _{𝑝} (J) (G _{𝑝} (J) H))$

Proof

Step	Hyp	Ref	Expression
1		pcoass.2	$⊢ φ \to F \in (II Cn J)$
2		pcoass.3	$⊢ φ \to G \in (II Cn J)$
3		pcoass.4	$⊢ φ \to H \in (II Cn J)$
4		pcoass.5	$⊢ φ \to F (1) = G (0)$
5		pcoass.6	$⊢ φ \to G (1) = H (0)$
6		pcoass.7	$⊢ P = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})))$
7		iftrue	$⊢ x \leq \frac{1}{4} \to if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})) = 2 x$
8	7	fveq2d	$⊢ x \leq \frac{1}{4} \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))) = (F _{𝑝} (J) (G _{𝑝} (J) H)) (2 x)$
9	8	adantl	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{4}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))) = (F _{𝑝} (J) (G _{𝑝} (J) H)) (2 x)$
10		2cn	$⊢ 2 \in ℂ$
11		elicc01	$⊢ x \in [0, 1] \leftrightarrow (x \in ℝ \land 0 \leq x \land x \leq 1)$
12	11	simp1bi	$⊢ x \in [0, 1] \to x \in ℝ$
13	12	adantr	$⊢ (x \in [0, 1] \land x \leq \frac{1}{4}) \to x \in ℝ$
14	13	recnd	$⊢ (x \in [0, 1] \land x \leq \frac{1}{4}) \to x \in ℂ$
15		mulcom	$⊢ (2 \in ℂ \land x \in ℂ) \to 2 x = x \cdot 2$
16	10 14 15	sylancr	$⊢ (x \in [0, 1] \land x \leq \frac{1}{4}) \to 2 x = x \cdot 2$
17	11	simp2bi	$⊢ x \in [0, 1] \to 0 \leq x$
18	17	adantr	$⊢ (x \in [0, 1] \land x \leq \frac{1}{4}) \to 0 \leq x$
19		simpr	$⊢ (x \in [0, 1] \land x \leq \frac{1}{4}) \to x \leq \frac{1}{4}$
20		0re	$⊢ 0 \in ℝ$
21		4nn	$⊢ 4 \in ℕ$
22		nnrecre	$⊢ 4 \in ℕ \to \frac{1}{4} \in ℝ$
23	21 22	ax-mp	$⊢ \frac{1}{4} \in ℝ$
24	20 23	elicc2i	$⊢ x \in [0, \frac{1}{4}] \leftrightarrow (x \in ℝ \land 0 \leq x \land x \leq \frac{1}{4})$
25	13 18 19 24	syl3anbrc	$⊢ (x \in [0, 1] \land x \leq \frac{1}{4}) \to x \in [0, \frac{1}{4}]$
26		2rp	$⊢ 2 \in ℝ^{+}$
27	10	mul02i	$⊢ 0 \cdot 2 = 0$
28	23	recni	$⊢ \frac{1}{4} \in ℂ$
29	28	2timesi	$⊢ 2 (\frac{1}{4}) = (\frac{1}{4}) + (\frac{1}{4})$
30		2ne0	$⊢ 2 \neq 0$
31		recdiv2	$⊢ ((2 \in ℂ \land 2 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{1}{2}}{2} = \frac{1}{2 \cdot 2}$
32	10 30 10 30 31	mp4an	$⊢ \frac{\frac{1}{2}}{2} = \frac{1}{2 \cdot 2}$
33		2t2e4	$⊢ 2 \cdot 2 = 4$
34	33	oveq2i	$⊢ \frac{1}{2 \cdot 2} = \frac{1}{4}$
35	32 34	eqtri	$⊢ \frac{\frac{1}{2}}{2} = \frac{1}{4}$
36	35 35	oveq12i	$⊢ (\frac{\frac{1}{2}}{2}) + (\frac{\frac{1}{2}}{2}) = (\frac{1}{4}) + (\frac{1}{4})$
37		halfcn	$⊢ \frac{1}{2} \in ℂ$
38		2halves	$⊢ \frac{1}{2} \in ℂ \to (\frac{\frac{1}{2}}{2}) + (\frac{\frac{1}{2}}{2}) = \frac{1}{2}$
39	37 38	ax-mp	$⊢ (\frac{\frac{1}{2}}{2}) + (\frac{\frac{1}{2}}{2}) = \frac{1}{2}$
40	36 39	eqtr3i	$⊢ (\frac{1}{4}) + (\frac{1}{4}) = \frac{1}{2}$
41	29 40	eqtri	$⊢ 2 (\frac{1}{4}) = \frac{1}{2}$
42	10 28 41	mulcomli	$⊢ (\frac{1}{4}) \cdot 2 = \frac{1}{2}$
43	20 23 26 27 42	iccdili	$⊢ x \in [0, \frac{1}{4}] \to x \cdot 2 \in [0, \frac{1}{2}]$
44	25 43	syl	$⊢ (x \in [0, 1] \land x \leq \frac{1}{4}) \to x \cdot 2 \in [0, \frac{1}{2}]$
45	16 44	eqeltrd	$⊢ (x \in [0, 1] \land x \leq \frac{1}{4}) \to 2 x \in [0, \frac{1}{2}]$
46	2 3 5	pcocn	$⊢ φ \to G *_{𝑝} (J) H \in (II Cn J)$
47	1 46	pcoval1	$⊢ (φ \land 2 x \in [0, \frac{1}{2}]) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (2 x) = F (2 2 x)$
48	1 2	pcoval1	$⊢ (φ \land 2 x \in [0, \frac{1}{2}]) \to (F *_{𝑝} (J) G) (2 x) = F (2 2 x)$
49	47 48	eqtr4d	$⊢ (φ \land 2 x \in [0, \frac{1}{2}]) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (2 x) = (F *_{𝑝} (J) G) (2 x)$
50	45 49	sylan2	$⊢ (φ \land (x \in [0, 1] \land x \leq \frac{1}{4})) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (2 x) = (F *_{𝑝} (J) G) (2 x)$
51	50	anassrs	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{4}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (2 x) = (F *_{𝑝} (J) G) (2 x)$
52	9 51	eqtrd	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{4}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))) = (F *_{𝑝} (J) G) (2 x)$
53	52	adantlr	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land x \leq \frac{1}{4}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))) = (F *_{𝑝} (J) G) (2 x)$
54		simplll	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to φ$
55	12	ad2antlr	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \to x \in ℝ$
56	55	adantr	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to x \in ℝ$
57		letric	$⊢ (x \in ℝ \land \frac{1}{4} \in ℝ) \to (x \leq \frac{1}{4} \lor \frac{1}{4} \leq x)$
58	55 23 57	sylancl	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \to (x \leq \frac{1}{4} \lor \frac{1}{4} \leq x)$
59	58	orcanai	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to \frac{1}{4} \leq x$
60		simplr	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to x \leq \frac{1}{2}$
61		halfre	$⊢ \frac{1}{2} \in ℝ$
62	23 61	elicc2i	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \leftrightarrow (x \in ℝ \land \frac{1}{4} \leq x \land x \leq \frac{1}{2})$
63	56 59 60 62	syl3anbrc	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to x \in [\frac{1}{4}, \frac{1}{2}]$
64	62	simp1bi	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to x \in ℝ$
65		readdcl	$⊢ (x \in ℝ \land \frac{1}{4} \in ℝ) \to x + (\frac{1}{4}) \in ℝ$
66	64 23 65	sylancl	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to x + (\frac{1}{4}) \in ℝ$
67	23	a1i	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to \frac{1}{4} \in ℝ$
68	62	simp2bi	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to \frac{1}{4} \leq x$
69	67 64 67 68	leadd1dd	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to (\frac{1}{4}) + (\frac{1}{4}) \leq x + (\frac{1}{4})$
70	40 69	eqbrtrrid	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to \frac{1}{2} \leq x + (\frac{1}{4})$
71	61	a1i	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to \frac{1}{2} \in ℝ$
72	62	simp3bi	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to x \leq \frac{1}{2}$
73		2lt4	$⊢ 2 < 4$
74		2re	$⊢ 2 \in ℝ$
75		4re	$⊢ 4 \in ℝ$
76		2pos	$⊢ 0 < 2$
77		4pos	$⊢ 0 < 4$
78	74 75 76 77	ltrecii	$⊢ 2 < 4 \leftrightarrow \frac{1}{4} < \frac{1}{2}$
79	73 78	mpbi	$⊢ \frac{1}{4} < \frac{1}{2}$
80	23 61 79	ltleii	$⊢ \frac{1}{4} \leq \frac{1}{2}$
81	80	a1i	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to \frac{1}{4} \leq \frac{1}{2}$
82	64 67 71 71 72 81	le2addd	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to x + (\frac{1}{4}) \leq (\frac{1}{2}) + (\frac{1}{2})$
83		ax-1cn	$⊢ 1 \in ℂ$
84		2halves	$⊢ 1 \in ℂ \to (\frac{1}{2}) + (\frac{1}{2}) = 1$
85	83 84	ax-mp	$⊢ (\frac{1}{2}) + (\frac{1}{2}) = 1$
86	82 85	breqtrdi	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to x + (\frac{1}{4}) \leq 1$
87		1re	$⊢ 1 \in ℝ$
88	61 87	elicc2i	$⊢ x + (\frac{1}{4}) \in [\frac{1}{2}, 1] \leftrightarrow (x + (\frac{1}{4}) \in ℝ \land \frac{1}{2} \leq x + (\frac{1}{4}) \land x + (\frac{1}{4}) \leq 1)$
89	66 70 86 88	syl3anbrc	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to x + (\frac{1}{4}) \in [\frac{1}{2}, 1]$
90	63 89	syl	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to x + (\frac{1}{4}) \in [\frac{1}{2}, 1]$
91	2 3	pco0	$⊢ φ \to (G *_{𝑝} (J) H) (0) = G (0)$
92	4 91	eqtr4d	$⊢ φ \to F (1) = (G *_{𝑝} (J) H) (0)$
93	1 46 92	pcoval2	$⊢ (φ \land x + (\frac{1}{4}) \in [\frac{1}{2}, 1]) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (x + (\frac{1}{4})) = (G *_{𝑝} (J) H) (2 (x + (\frac{1}{4})) - 1)$
94	54 90 93	syl2anc	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (x + (\frac{1}{4})) = (G *_{𝑝} (J) H) (2 (x + (\frac{1}{4})) - 1)$
95	85	oveq2i	$⊢ 2 (x + (\frac{1}{4})) - ((\frac{1}{2}) + (\frac{1}{2})) = 2 (x + (\frac{1}{4})) - 1$
96		2cnd	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 \in ℂ$
97	56	recnd	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to x \in ℂ$
98	28	a1i	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to \frac{1}{4} \in ℂ$
99	96 97 98	adddid	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 (x + (\frac{1}{4})) = 2 x + 2 (\frac{1}{4})$
100	41	oveq2i	$⊢ 2 x + 2 (\frac{1}{4}) = 2 x + (\frac{1}{2})$
101	99 100	eqtrdi	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 (x + (\frac{1}{4})) = 2 x + (\frac{1}{2})$
102	101	oveq1d	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 (x + (\frac{1}{4})) - ((\frac{1}{2}) + (\frac{1}{2})) = 2 x + (\frac{1}{2}) - ((\frac{1}{2}) + (\frac{1}{2}))$
103	95 102	eqtr3id	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 (x + (\frac{1}{4})) - 1 = 2 x + (\frac{1}{2}) - ((\frac{1}{2}) + (\frac{1}{2}))$
104		remulcl	$⊢ (2 \in ℝ \land x \in ℝ) \to 2 x \in ℝ$
105	74 56 104	sylancr	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 x \in ℝ$
106	105	recnd	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 x \in ℂ$
107	37	a1i	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to \frac{1}{2} \in ℂ$
108	106 107 107	pnpcan2d	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 x + (\frac{1}{2}) - ((\frac{1}{2}) + (\frac{1}{2})) = 2 x - (\frac{1}{2})$
109	103 108	eqtrd	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 (x + (\frac{1}{4})) - 1 = 2 x - (\frac{1}{2})$
110	109	fveq2d	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to (G _{𝑝} (J) H) (2 (x + (\frac{1}{4})) - 1) = (G _{𝑝} (J) H) (2 x - (\frac{1}{2}))$
111	10 97 15	sylancr	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 x = x \cdot 2$
112	83 10 30	divcan1i	$⊢ (\frac{1}{2}) \cdot 2 = 1$
113	23 61 26 42 112	iccdili	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to x \cdot 2 \in [\frac{1}{2}, 1]$
114	63 113	syl	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to x \cdot 2 \in [\frac{1}{2}, 1]$
115	111 114	eqeltrd	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 x \in [\frac{1}{2}, 1]$
116	37	subidi	$⊢ (\frac{1}{2}) - (\frac{1}{2}) = 0$
117		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
118	61 87 61 116 117	iccshftli	$⊢ 2 x \in [\frac{1}{2}, 1] \to 2 x - (\frac{1}{2}) \in [0, \frac{1}{2}]$
119	115 118	syl	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 x - (\frac{1}{2}) \in [0, \frac{1}{2}]$
120	2 3	pcoval1	$⊢ (φ \land 2 x - (\frac{1}{2}) \in [0, \frac{1}{2}]) \to (G *_{𝑝} (J) H) (2 x - (\frac{1}{2})) = G (2 (2 x - (\frac{1}{2})))$
121	54 119 120	syl2anc	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to (G *_{𝑝} (J) H) (2 x - (\frac{1}{2})) = G (2 (2 x - (\frac{1}{2})))$
122	96 106 107	subdid	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 (2 x - (\frac{1}{2})) = 2 2 x - 2 (\frac{1}{2})$
123	10 30	recidi	$⊢ 2 (\frac{1}{2}) = 1$
124	123	oveq2i	$⊢ 2 2 x - 2 (\frac{1}{2}) = 2 2 x - 1$
125	122 124	eqtrdi	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to 2 (2 x - (\frac{1}{2})) = 2 2 x - 1$
126	125	fveq2d	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to G (2 (2 x - (\frac{1}{2}))) = G (2 2 x - 1)$
127	121 126	eqtrd	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to (G *_{𝑝} (J) H) (2 x - (\frac{1}{2})) = G (2 2 x - 1)$
128	94 110 127	3eqtrd	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (x + (\frac{1}{4})) = G (2 2 x - 1)$
129		iffalse	$⊢ \neg x \leq \frac{1}{4} \to if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})) = x + (\frac{1}{4})$
130	129	fveq2d	$⊢ \neg x \leq \frac{1}{4} \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))) = (F _{𝑝} (J) (G _{𝑝} (J) H)) (x + (\frac{1}{4}))$
131	130	adantl	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))) = (F _{𝑝} (J) (G _{𝑝} (J) H)) (x + (\frac{1}{4}))$
132	1 2 4	pcoval2	$⊢ (φ \land 2 x \in [\frac{1}{2}, 1]) \to (F *_{𝑝} (J) G) (2 x) = G (2 2 x - 1)$
133	54 115 132	syl2anc	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to (F *_{𝑝} (J) G) (2 x) = G (2 2 x - 1)$
134	128 131 133	3eqtr4d	$⊢ (((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \land \neg x \leq \frac{1}{4}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))) = (F *_{𝑝} (J) G) (2 x)$
135	53 134	pm2.61dan	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))) = (F *_{𝑝} (J) G) (2 x)$
136		iftrue	$⊢ x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))$
137	136	fveq2d	$⊢ x \leq \frac{1}{2} \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) = (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})))$
138	137	adantl	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) = (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})))$
139		iftrue	$⊢ x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, (F _{𝑝} (J) G) (2 x), H (2 x - 1)) = (F _{𝑝} (J) G) (2 x)$
140	139	adantl	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \to if (x \leq \frac{1}{2}, (F _{𝑝} (J) G) (2 x), H (2 x - 1)) = (F _{𝑝} (J) G) (2 x)$
141	135 138 140	3eqtr4d	$⊢ ((φ \land x \in [0, 1]) \land x \leq \frac{1}{2}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) = if (x \leq \frac{1}{2}, (F *_{𝑝} (J) G) (2 x), H (2 x - 1))$
142		elii2	$⊢ (x \in [0, 1] \land \neg x \leq \frac{1}{2}) \to x \in [\frac{1}{2}, 1]$
143		halfge0	$⊢ 0 \leq \frac{1}{2}$
144		halflt1	$⊢ \frac{1}{2} < 1$
145	61 87 144	ltleii	$⊢ \frac{1}{2} \leq 1$
146		elicc01	$⊢ \frac{1}{2} \in [0, 1] \leftrightarrow (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2} \land \frac{1}{2} \leq 1)$
147	61 143 145 146	mpbir3an	$⊢ \frac{1}{2} \in [0, 1]$
148		1elunit	$⊢ 1 \in [0, 1]$
149		iccss2	$⊢ (\frac{1}{2} \in [0, 1] \land 1 \in [0, 1]) \to [\frac{1}{2}, 1] \subseteq [0, 1]$
150	147 148 149	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq [0, 1]$
151	150	sseli	$⊢ x \in [\frac{1}{2}, 1] \to x \in [0, 1]$
152	10 30	div0i	$⊢ \frac{0}{2} = 0$
153		eqid	$⊢ \frac{1}{2} = \frac{1}{2}$
154	20 87 26 152 153	icccntri	$⊢ x \in [0, 1] \to \frac{x}{2} \in [0, \frac{1}{2}]$
155	37	addlidi	$⊢ 0 + (\frac{1}{2}) = \frac{1}{2}$
156	20 61 61 155 85	iccshftri	$⊢ \frac{x}{2} \in [0, \frac{1}{2}] \to (\frac{x}{2}) + (\frac{1}{2}) \in [\frac{1}{2}, 1]$
157	151 154 156	3syl	$⊢ x \in [\frac{1}{2}, 1] \to (\frac{x}{2}) + (\frac{1}{2}) \in [\frac{1}{2}, 1]$
158	1 46 92	pcoval2	$⊢ (φ \land (\frac{x}{2}) + (\frac{1}{2}) \in [\frac{1}{2}, 1]) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) ((\frac{x}{2}) + (\frac{1}{2})) = (G *_{𝑝} (J) H) (2 ((\frac{x}{2}) + (\frac{1}{2})) - 1)$
159	157 158	sylan2	$⊢ (φ \land x \in [\frac{1}{2}, 1]) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) ((\frac{x}{2}) + (\frac{1}{2})) = (G *_{𝑝} (J) H) (2 ((\frac{x}{2}) + (\frac{1}{2})) - 1)$
160	61 87	elicc2i	$⊢ x \in [\frac{1}{2}, 1] \leftrightarrow (x \in ℝ \land \frac{1}{2} \leq x \land x \leq 1)$
161	160	simp1bi	$⊢ x \in [\frac{1}{2}, 1] \to x \in ℝ$
162	161	recnd	$⊢ x \in [\frac{1}{2}, 1] \to x \in ℂ$
163		1cnd	$⊢ x \in [\frac{1}{2}, 1] \to 1 \in ℂ$
164		2cnd	$⊢ x \in [\frac{1}{2}, 1] \to 2 \in ℂ$
165	30	a1i	$⊢ x \in [\frac{1}{2}, 1] \to 2 \neq 0$
166	162 163 164 165	divdird	$⊢ x \in [\frac{1}{2}, 1] \to \frac{x + 1}{2} = (\frac{x}{2}) + (\frac{1}{2})$
167	166	oveq2d	$⊢ x \in [\frac{1}{2}, 1] \to 2 (\frac{x + 1}{2}) = 2 ((\frac{x}{2}) + (\frac{1}{2}))$
168		peano2cn	$⊢ x \in ℂ \to x + 1 \in ℂ$
169	162 168	syl	$⊢ x \in [\frac{1}{2}, 1] \to x + 1 \in ℂ$
170	169 164 165	divcan2d	$⊢ x \in [\frac{1}{2}, 1] \to 2 (\frac{x + 1}{2}) = x + 1$
171	167 170	eqtr3d	$⊢ x \in [\frac{1}{2}, 1] \to 2 ((\frac{x}{2}) + (\frac{1}{2})) = x + 1$
172	162 163 171	mvrraddd	$⊢ x \in [\frac{1}{2}, 1] \to 2 ((\frac{x}{2}) + (\frac{1}{2})) - 1 = x$
173	172	fveq2d	$⊢ x \in [\frac{1}{2}, 1] \to (G _{𝑝} (J) H) (2 ((\frac{x}{2}) + (\frac{1}{2})) - 1) = (G _{𝑝} (J) H) (x)$
174	173	adantl	$⊢ (φ \land x \in [\frac{1}{2}, 1]) \to (G _{𝑝} (J) H) (2 ((\frac{x}{2}) + (\frac{1}{2})) - 1) = (G _{𝑝} (J) H) (x)$
175	2 3 5	pcoval2	$⊢ (φ \land x \in [\frac{1}{2}, 1]) \to (G *_{𝑝} (J) H) (x) = H (2 x - 1)$
176	159 174 175	3eqtrd	$⊢ (φ \land x \in [\frac{1}{2}, 1]) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) ((\frac{x}{2}) + (\frac{1}{2})) = H (2 x - 1)$
177	142 176	sylan2	$⊢ (φ \land (x \in [0, 1] \land \neg x \leq \frac{1}{2})) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) ((\frac{x}{2}) + (\frac{1}{2})) = H (2 x - 1)$
178	177	anassrs	$⊢ ((φ \land x \in [0, 1]) \land \neg x \leq \frac{1}{2}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) ((\frac{x}{2}) + (\frac{1}{2})) = H (2 x - 1)$
179		iffalse	$⊢ \neg x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = (\frac{x}{2}) + (\frac{1}{2})$
180	179	fveq2d	$⊢ \neg x \leq \frac{1}{2} \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) = (F _{𝑝} (J) (G _{𝑝} (J) H)) ((\frac{x}{2}) + (\frac{1}{2}))$
181	180	adantl	$⊢ ((φ \land x \in [0, 1]) \land \neg x \leq \frac{1}{2}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) = (F _{𝑝} (J) (G _{𝑝} (J) H)) ((\frac{x}{2}) + (\frac{1}{2}))$
182		iffalse	$⊢ \neg x \leq \frac{1}{2} \to if (x \leq \frac{1}{2}, (F *_{𝑝} (J) G) (2 x), H (2 x - 1)) = H (2 x - 1)$
183	182	adantl	$⊢ ((φ \land x \in [0, 1]) \land \neg x \leq \frac{1}{2}) \to if (x \leq \frac{1}{2}, (F *_{𝑝} (J) G) (2 x), H (2 x - 1)) = H (2 x - 1)$
184	178 181 183	3eqtr4d	$⊢ ((φ \land x \in [0, 1]) \land \neg x \leq \frac{1}{2}) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) = if (x \leq \frac{1}{2}, (F *_{𝑝} (J) G) (2 x), H (2 x - 1))$
185	141 184	pm2.61dan	$⊢ (φ \land x \in [0, 1]) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) = if (x \leq \frac{1}{2}, (F *_{𝑝} (J) G) (2 x), H (2 x - 1))$
186	185	mpteq2dva	$⊢ φ \to (x \in [0, 1] ⟼ (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})))) = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, (F *_{𝑝} (J) G) (2 x), H (2 x - 1)))$
187		iitopon	$⊢ II \in TopOn ([0, 1])$
188	187	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
189	188	cnmptid	$⊢ φ \to (x \in [0, 1] ⟼ x) \in (II Cn II)$
190		0elunit	$⊢ 0 \in [0, 1]$
191	190	a1i	$⊢ φ \to 0 \in [0, 1]$
192	188 188 191	cnmptc	$⊢ φ \to (x \in [0, 1] ⟼ 0) \in (II Cn II)$
193		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
194		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]$
195		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] = topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]$
196		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
197		0red	$⊢ φ \to 0 \in ℝ$
198		1red	$⊢ φ \to 1 \in ℝ$
199	147	a1i	$⊢ φ \to \frac{1}{2} \in [0, 1]$
200		simprl	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to y = \frac{1}{2}$
201	200	oveq1d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to y + (\frac{1}{4}) = (\frac{1}{2}) + (\frac{1}{4})$
202	37 28	addcomi	$⊢ (\frac{1}{2}) + (\frac{1}{4}) = (\frac{1}{4}) + (\frac{1}{2})$
203	201 202	eqtrdi	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to y + (\frac{1}{4}) = (\frac{1}{4}) + (\frac{1}{2})$
204	23 61	ltnlei	$⊢ \frac{1}{4} < \frac{1}{2} \leftrightarrow \neg \frac{1}{2} \leq \frac{1}{4}$
205	79 204	mpbi	$⊢ \neg \frac{1}{2} \leq \frac{1}{4}$
206	200	breq1d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to (y \leq \frac{1}{4} \leftrightarrow \frac{1}{2} \leq \frac{1}{4})$
207	205 206	mtbiri	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to \neg y \leq \frac{1}{4}$
208	207	iffalsed	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})) = y + (\frac{1}{4})$
209	200	oveq1d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to \frac{y}{2} = \frac{\frac{1}{2}}{2}$
210	209 35	eqtrdi	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to \frac{y}{2} = \frac{1}{4}$
211	210	oveq1d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to (\frac{y}{2}) + (\frac{1}{2}) = (\frac{1}{4}) + (\frac{1}{2})$
212	203 208 211	3eqtr4d	$⊢ (φ \land (y = \frac{1}{2} \land z \in [0, 1])) \to if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})) = (\frac{y}{2}) + (\frac{1}{2})$
213		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}]$
214		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}] = topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}]$
215	61	a1i	$⊢ φ \to \frac{1}{2} \in ℝ$
216	75 77	recgt0ii	$⊢ 0 < \frac{1}{4}$
217	20 23 216	ltleii	$⊢ 0 \leq \frac{1}{4}$
218	20 61	elicc2i	$⊢ \frac{1}{4} \in [0, \frac{1}{2}] \leftrightarrow (\frac{1}{4} \in ℝ \land 0 \leq \frac{1}{4} \land \frac{1}{4} \leq \frac{1}{2})$
219	23 217 80 218	mpbir3an	$⊢ \frac{1}{4} \in [0, \frac{1}{2}]$
220	219	a1i	$⊢ φ \to \frac{1}{4} \in [0, \frac{1}{2}]$
221		simprl	$⊢ (φ \land (y = \frac{1}{4} \land z \in [0, 1])) \to y = \frac{1}{4}$
222	221	oveq2d	$⊢ (φ \land (y = \frac{1}{4} \land z \in [0, 1])) \to 2 y = 2 (\frac{1}{4})$
223	221	oveq1d	$⊢ (φ \land (y = \frac{1}{4} \land z \in [0, 1])) \to y + (\frac{1}{4}) = (\frac{1}{4}) + (\frac{1}{4})$
224	29 222 223	3eqtr4a	$⊢ (φ \land (y = \frac{1}{4} \land z \in [0, 1])) \to 2 y = y + (\frac{1}{4})$
225		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
226		0xr	$⊢ 0 \in ℝ^{*}$
227	61	rexri	$⊢ \frac{1}{2} \in ℝ^{*}$
228		lbicc2	$⊢ (0 \in ℝ^{} \land \frac{1}{2} \in ℝ^{} \land 0 \leq \frac{1}{2}) \to 0 \in [0, \frac{1}{2}]$
229	226 227 143 228	mp3an	$⊢ 0 \in [0, \frac{1}{2}]$
230		iccss2	$⊢ (0 \in [0, \frac{1}{2}] \land \frac{1}{4} \in [0, \frac{1}{2}]) \to [0, \frac{1}{4}] \subseteq [0, \frac{1}{2}]$
231	229 219 230	mp2an	$⊢ [0, \frac{1}{4}] \subseteq [0, \frac{1}{2}]$
232		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
233	20 61 232	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
234	231 233	sstri	$⊢ [0, \frac{1}{4}] \subseteq ℝ$
235		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{4}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}] \in TopOn ([0, \frac{1}{4}])$
236	225 234 235	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}] \in TopOn ([0, \frac{1}{4}])$
237	236	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}] \in TopOn ([0, \frac{1}{4}])$
238	237 188	cnmpt1st	$⊢ φ \to (y \in [0, \frac{1}{4}], z \in [0, 1] ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}]))$
239		retop	$⊢ topGen (ran (.)) \in Top$
240		ovex	$⊢ [0, \frac{1}{2}] \in V$
241		restabs	$⊢ (topGen (ran (.)) \in Top \land [0, \frac{1}{4}] \subseteq [0, \frac{1}{2}] \land [0, \frac{1}{2}] \in V) \to (topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) ↾_{𝑡} [0, \frac{1}{4}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}]$
242	239 231 240 241	mp3an	$⊢ (topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) ↾_{𝑡} [0, \frac{1}{4}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}]$
243	242	eqcomi	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}] = (topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) ↾_{𝑡} [0, \frac{1}{4}]$
244		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
245	225 233 244	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
246	245	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
247	231	a1i	$⊢ φ \to [0, \frac{1}{4}] \subseteq [0, \frac{1}{2}]$
248	194	iihalf1cn	$⊢ (x \in [0, \frac{1}{2}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
249	248	a1i	$⊢ φ \to (x \in [0, \frac{1}{2}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
250	243 246 247 249	cnmpt1res	$⊢ φ \to (x \in [0, \frac{1}{4}] ⟼ 2 x) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}]) Cn II)$
251		oveq2	$⊢ x = y \to 2 x = 2 y$
252	237 188 238 237 250 251	cnmpt21	$⊢ φ \to (y \in [0, \frac{1}{4}], z \in [0, 1] ⟼ 2 y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{4}]) \times_{t} II) Cn II)$
253		iccssre	$⊢ (\frac{1}{4} \in ℝ \land \frac{1}{2} \in ℝ) \to [\frac{1}{4}, \frac{1}{2}] \subseteq ℝ$
254	23 61 253	mp2an	$⊢ [\frac{1}{4}, \frac{1}{2}] \subseteq ℝ$
255		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{4}, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}] \in TopOn ([\frac{1}{4}, \frac{1}{2}])$
256	225 254 255	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}] \in TopOn ([\frac{1}{4}, \frac{1}{2}])$
257	256	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}] \in TopOn ([\frac{1}{4}, \frac{1}{2}])$
258	257 188	cnmpt1st	$⊢ φ \to (y \in [\frac{1}{4}, \frac{1}{2}], z \in [0, 1] ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}]))$
259		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
260	254	a1i	$⊢ φ \to [\frac{1}{4}, \frac{1}{2}] \subseteq ℝ$
261		unitssre	$⊢ [0, 1] \subseteq ℝ$
262	261	a1i	$⊢ φ \to [0, 1] \subseteq ℝ$
263	150 89	sselid	$⊢ x \in [\frac{1}{4}, \frac{1}{2}] \to x + (\frac{1}{4}) \in [0, 1]$
264	263	adantl	$⊢ (φ \land x \in [\frac{1}{4}, \frac{1}{2}]) \to x + (\frac{1}{4}) \in [0, 1]$
265	259	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
266	265	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
267	266	cnmptid	$⊢ φ \to (x \in ℂ ⟼ x) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
268	23	a1i	$⊢ φ \to \frac{1}{4} \in ℝ$
269	268	recnd	$⊢ φ \to \frac{1}{4} \in ℂ$
270	266 266 269	cnmptc	$⊢ φ \to (x \in ℂ ⟼ \frac{1}{4}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
271	259	addcn	$⊢ + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
272	271	a1i	$⊢ φ \to + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
273	266 267 270 272	cnmpt12f	$⊢ φ \to (x \in ℂ ⟼ x + (\frac{1}{4})) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
274	259 214 196 260 262 264 273	cnmptre	$⊢ φ \to (x \in [\frac{1}{4}, \frac{1}{2}] ⟼ x + (\frac{1}{4})) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}]) Cn II)$
275		oveq1	$⊢ x = y \to x + (\frac{1}{4}) = y + (\frac{1}{4})$
276	257 188 258 257 274 275	cnmpt21	$⊢ φ \to (y \in [\frac{1}{4}, \frac{1}{2}], z \in [0, 1] ⟼ y + (\frac{1}{4})) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{4}, \frac{1}{2}]) \times_{t} II) Cn II)$
277	193 213 214 194 197 215 220 188 224 252 276	cnmpopc	$⊢ φ \to (y \in [0, \frac{1}{2}], z \in [0, 1] ⟼ if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4}))) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} II) Cn II)$
278		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
279	61 87 278	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
280		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
281	225 279 280	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
282	281	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
283	282 188	cnmpt1st	$⊢ φ \to (y \in [\frac{1}{2}, 1], z \in [0, 1] ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn (topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]))$
284	279	a1i	$⊢ φ \to [\frac{1}{2}, 1] \subseteq ℝ$
285	150 157	sselid	$⊢ x \in [\frac{1}{2}, 1] \to (\frac{x}{2}) + (\frac{1}{2}) \in [0, 1]$
286	285	adantl	$⊢ (φ \land x \in [\frac{1}{2}, 1]) \to (\frac{x}{2}) + (\frac{1}{2}) \in [0, 1]$
287	259	divccn	$⊢ (2 \in ℂ \land 2 \neq 0) \to (x \in ℂ ⟼ \frac{x}{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
288	10 30 287	mp2an	$⊢ (x \in ℂ ⟼ \frac{x}{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
289	288	a1i	$⊢ φ \to (x \in ℂ ⟼ \frac{x}{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
290	37	a1i	$⊢ φ \to \frac{1}{2} \in ℂ$
291	266 266 290	cnmptc	$⊢ φ \to (x \in ℂ ⟼ \frac{1}{2}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
292	266 289 291 272	cnmpt12f	$⊢ φ \to (x \in ℂ ⟼ (\frac{x}{2}) + (\frac{1}{2})) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
293	259 195 196 284 262 286 292	cnmptre	$⊢ φ \to (x \in [\frac{1}{2}, 1] ⟼ (\frac{x}{2}) + (\frac{1}{2})) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
294		oveq1	$⊢ x = y \to \frac{x}{2} = \frac{y}{2}$
295	294	oveq1d	$⊢ x = y \to (\frac{x}{2}) + (\frac{1}{2}) = (\frac{y}{2}) + (\frac{1}{2})$
296	282 188 283 282 293 295	cnmpt21	$⊢ φ \to (y \in [\frac{1}{2}, 1], z \in [0, 1] ⟼ (\frac{y}{2}) + (\frac{1}{2})) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} II) Cn II)$
297	193 194 195 196 197 198 199 188 212 277 296	cnmpopc	$⊢ φ \to (y \in [0, 1], z \in [0, 1] ⟼ if (y \leq \frac{1}{2}, if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})), (\frac{y}{2}) + (\frac{1}{2}))) \in ((II \times_{t} II) Cn II)$
298		breq1	$⊢ x = y \to (x \leq \frac{1}{2} \leftrightarrow y \leq \frac{1}{2})$
299		breq1	$⊢ x = y \to (x \leq \frac{1}{4} \leftrightarrow y \leq \frac{1}{4})$
300	299 251 275	ifbieq12d	$⊢ x = y \to if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})) = if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4}))$
301	298 300 295	ifbieq12d	$⊢ x = y \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = if (y \leq \frac{1}{2}, if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})), (\frac{y}{2}) + (\frac{1}{2}))$
302	301	equcoms	$⊢ y = x \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = if (y \leq \frac{1}{2}, if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})), (\frac{y}{2}) + (\frac{1}{2}))$
303	302	adantr	$⊢ (y = x \land z = 0) \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = if (y \leq \frac{1}{2}, if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})), (\frac{y}{2}) + (\frac{1}{2}))$
304	303	eqcomd	$⊢ (y = x \land z = 0) \to if (y \leq \frac{1}{2}, if (y \leq \frac{1}{4}, 2 y, y + (\frac{1}{4})), (\frac{y}{2}) + (\frac{1}{2})) = if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))$
305	188 189 192 188 188 297 304	cnmpt12	$⊢ φ \to (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))) \in (II Cn II)$
306	6 305	eqeltrid	$⊢ φ \to P \in (II Cn II)$
307		iiuni	$⊢ [0, 1] = ⋃ II$
308	307 307	cnf	$⊢ P \in (II Cn II) \to P : [0, 1] ⟶ [0, 1]$
309	306 308	syl	$⊢ φ \to P : [0, 1] ⟶ [0, 1]$
310	6	fmpt	$⊢ \forall x \in [0, 1] if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) \in [0, 1] \leftrightarrow P : [0, 1] ⟶ [0, 1]$
311	309 310	sylibr	$⊢ φ \to \forall x \in [0, 1] if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) \in [0, 1]$
312	6	a1i	$⊢ φ \to P = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})))$
313	1 46 92	pcocn	$⊢ φ \to F _{𝑝} (J) (G _{𝑝} (J) H) \in (II Cn J)$
314		eqid	$⊢ ⋃ J = ⋃ J$
315	307 314	cnf	$⊢ F _{𝑝} (J) (G _{𝑝} (J) H) \in (II Cn J) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) : [0, 1] ⟶ ⋃ J$
316	313 315	syl	$⊢ φ \to (F _{𝑝} (J) (G _{𝑝} (J) H)) : [0, 1] ⟶ ⋃ J$
317	316	feqmptd	$⊢ φ \to F _{𝑝} (J) (G _{𝑝} (J) H) = (y \in [0, 1] ⟼ (F _{𝑝} (J) (G _{𝑝} (J) H)) (y))$
318		fveq2	$⊢ y = if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) \to (F _{𝑝} (J) (G _{𝑝} (J) H)) (y) = (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})))$
319	311 312 317 318	fmptcof	$⊢ φ \to (F _{𝑝} (J) (G _{𝑝} (J) H)) \circ P = (x \in [0, 1] ⟼ (F _{𝑝} (J) (G _{𝑝} (J) H)) (if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2}))))$
320	1 2 4	pcocn	$⊢ φ \to F *_{𝑝} (J) G \in (II Cn J)$
321	320 3	pcoval	$⊢ φ \to (F _{𝑝} (J) G) _{𝑝} (J) H = (x \in [0, 1] ⟼ if (x \leq \frac{1}{2}, (F *_{𝑝} (J) G) (2 x), H (2 x - 1)))$
322	186 319 321	3eqtr4rd	$⊢ φ \to (F _{𝑝} (J) G) _{𝑝} (J) H = (F _{𝑝} (J) (G _{𝑝} (J) H)) \circ P$
323		id	$⊢ x = 0 \to x = 0$
324	323 143	eqbrtrdi	$⊢ x = 0 \to x \leq \frac{1}{2}$
325	324	iftrued	$⊢ x = 0 \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4}))$
326	323 217	eqbrtrdi	$⊢ x = 0 \to x \leq \frac{1}{4}$
327	326	iftrued	$⊢ x = 0 \to if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})) = 2 x$
328		oveq2	$⊢ x = 0 \to 2 x = 2 \cdot 0$
329		2t0e0	$⊢ 2 \cdot 0 = 0$
330	328 329	eqtrdi	$⊢ x = 0 \to 2 x = 0$
331	325 327 330	3eqtrd	$⊢ x = 0 \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = 0$
332		c0ex	$⊢ 0 \in V$
333	331 6 332	fvmpt	$⊢ 0 \in [0, 1] \to P (0) = 0$
334	191 333	syl	$⊢ φ \to P (0) = 0$
335	148	a1i	$⊢ φ \to 1 \in [0, 1]$
336	61 87	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
337	144 336	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
338		breq1	$⊢ x = 1 \to (x \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
339	337 338	mtbiri	$⊢ x = 1 \to \neg x \leq \frac{1}{2}$
340	339	iffalsed	$⊢ x = 1 \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = (\frac{x}{2}) + (\frac{1}{2})$
341		oveq1	$⊢ x = 1 \to \frac{x}{2} = \frac{1}{2}$
342	341	oveq1d	$⊢ x = 1 \to (\frac{x}{2}) + (\frac{1}{2}) = (\frac{1}{2}) + (\frac{1}{2})$
343	342 85	eqtrdi	$⊢ x = 1 \to (\frac{x}{2}) + (\frac{1}{2}) = 1$
344	340 343	eqtrd	$⊢ x = 1 \to if (x \leq \frac{1}{2}, if (x \leq \frac{1}{4}, 2 x, x + (\frac{1}{4})), (\frac{x}{2}) + (\frac{1}{2})) = 1$
345		1ex	$⊢ 1 \in V$
346	344 6 345	fvmpt	$⊢ 1 \in [0, 1] \to P (1) = 1$
347	335 346	syl	$⊢ φ \to P (1) = 1$
348	313 306 334 347	reparpht	$⊢ φ \to ((F _{𝑝} (J) (G _{𝑝} (J) H)) \circ P) ≃_{ph} (J) (F _{𝑝} (J) (G _{𝑝} (J) H))$
349	322 348	eqbrtrd	$⊢ φ \to ((F _{𝑝} (J) G) _{𝑝} (J) H) ≃_{ph} (J) (F _{𝑝} (J) (G _{𝑝} (J) H))$

Metamath Proof Explorer

Theorem pcoass

Proof