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 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 ‘ 𝐽 ) 𝑃 ) )