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 
|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
pcorev.2 
|- P = ( ( 0 [,] 1 ) X. { ( F ` 1 ) } )
pcorevlem.3 
|- H = ( s e. ( 0 [,] 1 ) , t e. ( 0 [,] 1 ) |-> ( F ` if ( s <_ ( 1 / 2 ) , ( 1 - ( ( 1 - t ) x. ( 2 x. s ) ) ) , ( 1 - ( ( 1 - t ) x. ( 1 - ( ( 2 x. s ) - 1 ) ) ) ) ) ) )
Assertion pcorevlem 
|- ( F e. ( II Cn J ) -> ( H e. ( ( G ( *p ` J ) F ) ( PHtpy ` J ) P ) /\ ( G ( *p ` J ) F ) ( ~=ph ` J ) P ) )

Proof

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