Metamath Proof Explorer

Theorem pcopt2

Description: Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypothesis pcopt.1 
|- P = ( ( 0 [,] 1 ) X. { Y } )
Assertion pcopt2 
|- ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F ( *p ` J ) P ) ( ~=ph ` J ) F )

Proof

Step Hyp Ref Expression
1 pcopt.1 
 |-  P = ( ( 0 [,] 1 ) X. { Y } )
2 1 fveq1i 
 |-  ( P ` ( ( 2 x. x ) - 1 ) ) = ( ( ( 0 [,] 1 ) X. { Y } ) ` ( ( 2 x. x ) - 1 ) )
3 simpr 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F ` 1 ) = Y )
4 iiuni 
 |-  ( 0 [,] 1 ) = U. II
5 eqid 
 |-  U. J = U. J
6 4 5 cnf 
 |-  ( F e. ( II Cn J ) -> F : ( 0 [,] 1 ) --> U. J )
7 6 adantr 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> F : ( 0 [,] 1 ) --> U. J )
8 1elunit 
 |-  1 e. ( 0 [,] 1 )
9 ffvelrn 
 |-  ( ( F : ( 0 [,] 1 ) --> U. J /\ 1 e. ( 0 [,] 1 ) ) -> ( F ` 1 ) e. U. J )
10 7 8 9 sylancl 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F ` 1 ) e. U. J )
11 3 10 eqeltrrd 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> Y e. U. J )
12 elii2 
 |-  ( ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) -> x e. ( ( 1 / 2 ) [,] 1 ) )
13 iihalf2 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. x ) - 1 ) e. ( 0 [,] 1 ) )
14 12 13 syl 
 |-  ( ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( 2 x. x ) - 1 ) e. ( 0 [,] 1 ) )
15 fvconst2g 
 |-  ( ( Y e. U. J /\ ( ( 2 x. x ) - 1 ) e. ( 0 [,] 1 ) ) -> ( ( ( 0 [,] 1 ) X. { Y } ) ` ( ( 2 x. x ) - 1 ) ) = Y )
16 11 14 15 syl2an 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) ) -> ( ( ( 0 [,] 1 ) X. { Y } ) ` ( ( 2 x. x ) - 1 ) ) = Y )
17 2 16 eqtrid 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) ) -> ( P ` ( ( 2 x. x ) - 1 ) ) = Y )
18 simplr 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) ) -> ( F ` 1 ) = Y )
19 17 18 eqtr4d 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) ) -> ( P ` ( ( 2 x. x ) - 1 ) ) = ( F ` 1 ) )
20 19 anassrs 
 |-  ( ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> ( P ` ( ( 2 x. x ) - 1 ) ) = ( F ` 1 ) )
21 20 ifeq2da 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ x e. ( 0 [,] 1 ) ) -> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( P ` ( ( 2 x. x ) - 1 ) ) ) = if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( F ` 1 ) ) )
22 21 mpteq2dva 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( P ` ( ( 2 x. x ) - 1 ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( F ` 1 ) ) ) )
23 simpl 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> F e. ( II Cn J ) )
24 cntop2 
 |-  ( F e. ( II Cn J ) -> J e. Top )
25 24 adantr 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> J e. Top )
26 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
27 25 26 sylib 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> J e. ( TopOn ` U. J ) )
28 1 pcoptcl 
 |-  ( ( J e. ( TopOn ` U. J ) /\ Y e. U. J ) -> ( P e. ( II Cn J ) /\ ( P ` 0 ) = Y /\ ( P ` 1 ) = Y ) )
29 27 11 28 syl2anc 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( P e. ( II Cn J ) /\ ( P ` 0 ) = Y /\ ( P ` 1 ) = Y ) )
30 29 simp1d 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> P e. ( II Cn J ) )
31 23 30 pcoval 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F ( *p ` J ) P ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( P ` ( ( 2 x. x ) - 1 ) ) ) ) )
32 iftrue 
 |-  ( x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) = ( 2 x. x ) )
33 32 adantl 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 2 ) ) -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) = ( 2 x. x ) )
34 elii1 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) <-> ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 2 ) ) )
35 iihalf1 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. x ) e. ( 0 [,] 1 ) )
36 34 35 sylbir 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 2 ) ) -> ( 2 x. x ) e. ( 0 [,] 1 ) )
37 33 36 eqeltrd 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 2 ) ) -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) e. ( 0 [,] 1 ) )
38 37 ex 
 |-  ( x e. ( 0 [,] 1 ) -> ( x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) e. ( 0 [,] 1 ) ) )
39 iffalse 
 |-  ( -. x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) = 1 )
40 39 8 eqeltrdi 
 |-  ( -. x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) e. ( 0 [,] 1 ) )
41 38 40 pm2.61d1 
 |-  ( x e. ( 0 [,] 1 ) -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) e. ( 0 [,] 1 ) )
42 41 adantl 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ x e. ( 0 [,] 1 ) ) -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) e. ( 0 [,] 1 ) )
43 eqidd 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) )
44 7 feqmptd 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> F = ( y e. ( 0 [,] 1 ) |-> ( F ` y ) ) )
45 fveq2 
 |-  ( y = if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) -> ( F ` y ) = ( F ` if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) )
46 fvif 
 |-  ( F ` if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) = if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( F ` 1 ) )
47 45 46 eqtrdi 
 |-  ( y = if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) -> ( F ` y ) = if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( F ` 1 ) ) )
48 42 43 44 47 fmptco 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F o. ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( F ` ( 2 x. x ) ) , ( F ` 1 ) ) ) )
49 22 31 48 3eqtr4d 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F ( *p ` J ) P ) = ( F o. ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) ) )
50 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
51 50 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
52 51 cnmptid 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn II ) )
53 0elunit 
 |-  0 e. ( 0 [,] 1 )
54 53 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> 0 e. ( 0 [,] 1 ) )
55 51 51 54 cnmptc 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( x e. ( 0 [,] 1 ) |-> 0 ) e. ( II Cn II ) )
56 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
57 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) )
58 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) )
59 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
60 0re 
 |-  0 e. RR
61 60 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> 0 e. RR )
62 1re 
 |-  1 e. RR
63 62 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> 1 e. RR )
64 halfre 
 |-  ( 1 / 2 ) e. RR
65 halfge0 
 |-  0 <_ ( 1 / 2 )
66 halflt1 
 |-  ( 1 / 2 ) < 1
67 64 62 66 ltleii 
 |-  ( 1 / 2 ) <_ 1
68 elicc01 
 |-  ( ( 1 / 2 ) e. ( 0 [,] 1 ) <-> ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ 1 ) )
69 64 65 67 68 mpbir3an 
 |-  ( 1 / 2 ) e. ( 0 [,] 1 )
70 69 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( 1 / 2 ) e. ( 0 [,] 1 ) )
71 simprl 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> y = ( 1 / 2 ) )
72 71 oveq2d 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = ( 2 x. ( 1 / 2 ) ) )
73 2cn 
 |-  2 e. CC
74 2ne0 
 |-  2 =/= 0
75 73 74 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
76 72 75 eqtrdi 
 |-  ( ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = 1 )
77 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
78 iccssre 
 |-  ( ( 0 e. RR /\ ( 1 / 2 ) e. RR ) -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
79 60 64 78 mp2an 
 |-  ( 0 [,] ( 1 / 2 ) ) C_ RR
80 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( 0 [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
81 77 79 80 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) )
82 81 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
83 82 51 cnmpt1st 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( y e. ( 0 [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) ) )
84 57 iihalf1cn 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
85 84 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
86 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
87 82 51 83 82 85 86 cnmpt21 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( y e. ( 0 [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> ( 2 x. y ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
88 iccssre 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
89 64 62 88 mp2an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ RR
90 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( 1 / 2 ) [,] 1 ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
91 77 89 90 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) )
92 91 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
93 8 a1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> 1 e. ( 0 [,] 1 ) )
94 92 51 51 93 cnmpt2c 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( y e. ( ( 1 / 2 ) [,] 1 ) , z e. ( 0 [,] 1 ) |-> 1 ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn II ) )
95 56 57 58 59 61 63 70 51 76 87 94 cnmpopc 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( y e. ( 0 [,] 1 ) , z e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( 2 x. y ) , 1 ) ) e. ( ( II tX II ) Cn II ) )
96 breq1 
 |-  ( y = x -> ( y <_ ( 1 / 2 ) <-> x <_ ( 1 / 2 ) ) )
97 oveq2 
 |-  ( y = x -> ( 2 x. y ) = ( 2 x. x ) )
98 96 97 ifbieq1d 
 |-  ( y = x -> if ( y <_ ( 1 / 2 ) , ( 2 x. y ) , 1 ) = if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) )
99 98 adantr 
 |-  ( ( y = x /\ z = 0 ) -> if ( y <_ ( 1 / 2 ) , ( 2 x. y ) , 1 ) = if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) )
100 51 52 55 51 51 95 99 cnmpt12 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) e. ( II Cn II ) )
101 id 
 |-  ( x = 0 -> x = 0 )
102 101 65 eqbrtrdi 
 |-  ( x = 0 -> x <_ ( 1 / 2 ) )
103 102 32 syl 
 |-  ( x = 0 -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) = ( 2 x. x ) )
104 oveq2 
 |-  ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) )
105 2t0e0 
 |-  ( 2 x. 0 ) = 0
106 104 105 eqtrdi 
 |-  ( x = 0 -> ( 2 x. x ) = 0 )
107 103 106 eqtrd 
 |-  ( x = 0 -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) = 0 )
108 eqid 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) )
109 c0ex 
 |-  0 e. _V
110 107 108 109 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) ` 0 ) = 0 )
111 53 110 mp1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) ` 0 ) = 0 )
112 64 62 ltnlei 
 |-  ( ( 1 / 2 ) < 1 <-> -. 1 <_ ( 1 / 2 ) )
113 66 112 mpbi 
 |-  -. 1 <_ ( 1 / 2 )
114 breq1 
 |-  ( x = 1 -> ( x <_ ( 1 / 2 ) <-> 1 <_ ( 1 / 2 ) ) )
115 113 114 mtbiri 
 |-  ( x = 1 -> -. x <_ ( 1 / 2 ) )
116 115 39 syl 
 |-  ( x = 1 -> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) = 1 )
117 1ex 
 |-  1 e. _V
118 116 108 117 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) ` 1 ) = 1 )
119 8 118 mp1i 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) ` 1 ) = 1 )
120 23 100 111 119 reparpht 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F o. ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( 2 x. x ) , 1 ) ) ) ( ~=ph ` J ) F )
121 49 120 eqbrtrd 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = Y ) -> ( F ( *p ` J ) P ) ( ~=ph ` J ) F )