Metamath Proof Explorer

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