Metamath Proof Explorer


Theorem pcopt

Description: Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

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

Proof

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