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