Theorem 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	⊢ 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
	pcorev.2	⊢ 𝑃 = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 1 ) } )
	pcorevlem.3	⊢ 𝐻 = ( 𝑠 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 − ( ( 1 − 𝑡 ) · ( 2 · 𝑠 ) ) ) , ( 1 − ( ( 1 − 𝑡 ) · ( 1 − ( ( 2 · 𝑠 ) − 1 ) ) ) ) ) ) )
Assertion	pcorevlem	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐻 ∈ ( ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( PHtpy ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) )

Proof

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