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 |
|
ffvelrn |
|- ( ( 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
|
mulid2d |
|- ( ( 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
|
mulid2d |
|- ( ( ( 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 ) ) |