Metamath Proof Explorer

Theorem pcoass

Description: Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010) (Proof shortened by Mario Carneiro, 8-Jun-2014)

Ref Expression
Hypotheses pcoass.2 
|- ( ph -> F e. ( II Cn J ) )
pcoass.3 
|- ( ph -> G e. ( II Cn J ) )
pcoass.4 
|- ( ph -> H e. ( II Cn J ) )
pcoass.5 
|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )
pcoass.6 
|- ( ph -> ( G ` 1 ) = ( H ` 0 ) )
pcoass.7 
|- P = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) )
Assertion pcoass 
|- ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) ( ~=ph ` J ) ( F ( *p ` J ) ( G ( *p ` J ) H ) ) )

Proof

Step Hyp Ref Expression
1 pcoass.2 
 |-  ( ph -> F e. ( II Cn J ) )
2 pcoass.3 
 |-  ( ph -> G e. ( II Cn J ) )
3 pcoass.4 
 |-  ( ph -> H e. ( II Cn J ) )
4 pcoass.5 
 |-  ( ph -> ( F ` 1 ) = ( G ` 0 ) )
5 pcoass.6 
 |-  ( ph -> ( G ` 1 ) = ( H ` 0 ) )
6 pcoass.7 
 |-  P = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) )
7 iftrue 
 |-  ( x <_ ( 1 / 4 ) -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = ( 2 x. x ) )
8 7 fveq2d 
 |-  ( x <_ ( 1 / 4 ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) )
9 8 adantl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) )
10 2cn 
 |-  2 e. CC
11 elicc01 
 |-  ( x e. ( 0 [,] 1 ) <-> ( x e. RR /\ 0 <_ x /\ x <_ 1 ) )
12 11 simp1bi 
 |-  ( x e. ( 0 [,] 1 ) -> x e. RR )
13 12 adantr 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x e. RR )
14 13 recnd 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x e. CC )
15 mulcom 
 |-  ( ( 2 e. CC /\ x e. CC ) -> ( 2 x. x ) = ( x x. 2 ) )
16 10 14 15 sylancr 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> ( 2 x. x ) = ( x x. 2 ) )
17 11 simp2bi 
 |-  ( x e. ( 0 [,] 1 ) -> 0 <_ x )
18 17 adantr 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> 0 <_ x )
19 simpr 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x <_ ( 1 / 4 ) )
20 0re 
 |-  0 e. RR
21 4nn 
 |-  4 e. NN
22 nnrecre 
 |-  ( 4 e. NN -> ( 1 / 4 ) e. RR )
23 21 22 ax-mp 
 |-  ( 1 / 4 ) e. RR
24 20 23 elicc2i 
 |-  ( x e. ( 0 [,] ( 1 / 4 ) ) <-> ( x e. RR /\ 0 <_ x /\ x <_ ( 1 / 4 ) ) )
25 13 18 19 24 syl3anbrc 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x e. ( 0 [,] ( 1 / 4 ) ) )
26 2rp 
 |-  2 e. RR+
27 10 mul02i 
 |-  ( 0 x. 2 ) = 0
28 23 recni 
 |-  ( 1 / 4 ) e. CC
29 28 2timesi 
 |-  ( 2 x. ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
30 2ne0 
 |-  2 =/= 0
31 recdiv2 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 1 / 2 ) / 2 ) = ( 1 / ( 2 x. 2 ) ) )
32 10 30 10 30 31 mp4an 
 |-  ( ( 1 / 2 ) / 2 ) = ( 1 / ( 2 x. 2 ) )
33 2t2e4 
 |-  ( 2 x. 2 ) = 4
34 33 oveq2i 
 |-  ( 1 / ( 2 x. 2 ) ) = ( 1 / 4 )
35 32 34 eqtri 
 |-  ( ( 1 / 2 ) / 2 ) = ( 1 / 4 )
36 35 35 oveq12i 
 |-  ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
37 halfcn 
 |-  ( 1 / 2 ) e. CC
38 2halves 
 |-  ( ( 1 / 2 ) e. CC -> ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( 1 / 2 ) )
39 37 38 ax-mp 
 |-  ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( 1 / 2 )
40 36 39 eqtr3i 
 |-  ( ( 1 / 4 ) + ( 1 / 4 ) ) = ( 1 / 2 )
41 29 40 eqtri 
 |-  ( 2 x. ( 1 / 4 ) ) = ( 1 / 2 )
42 10 28 41 mulcomli 
 |-  ( ( 1 / 4 ) x. 2 ) = ( 1 / 2 )
43 20 23 26 27 42 iccdili 
 |-  ( x e. ( 0 [,] ( 1 / 4 ) ) -> ( x x. 2 ) e. ( 0 [,] ( 1 / 2 ) ) )
44 25 43 syl 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> ( x x. 2 ) e. ( 0 [,] ( 1 / 2 ) ) )
45 16 44 eqeltrd 
 |-  ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. ( 0 [,] ( 1 / 2 ) ) )
46 2 3 5 pcocn 
 |-  ( ph -> ( G ( *p ` J ) H ) e. ( II Cn J ) )
47 1 46 pcoval1 
 |-  ( ( ph /\ ( 2 x. x ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) = ( F ` ( 2 x. ( 2 x. x ) ) ) )
48 1 2 pcoval1 
 |-  ( ( ph /\ ( 2 x. x ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) = ( F ` ( 2 x. ( 2 x. x ) ) ) )
49 47 48 eqtr4d 
 |-  ( ( ph /\ ( 2 x. x ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
50 45 49 sylan2 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
51 50 anassrs 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
52 9 51 eqtrd 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
53 52 adantlr 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
54 simplll 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ph )
55 12 ad2antlr 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> x e. RR )
56 55 adantr 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x e. RR )
57 letric 
 |-  ( ( x e. RR /\ ( 1 / 4 ) e. RR ) -> ( x <_ ( 1 / 4 ) \/ ( 1 / 4 ) <_ x ) )
58 55 23 57 sylancl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( x <_ ( 1 / 4 ) \/ ( 1 / 4 ) <_ x ) )
59 58 orcanai 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 1 / 4 ) <_ x )
60 simplr 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x <_ ( 1 / 2 ) )
61 halfre 
 |-  ( 1 / 2 ) e. RR
62 23 61 elicc2i 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) <-> ( x e. RR /\ ( 1 / 4 ) <_ x /\ x <_ ( 1 / 2 ) ) )
63 56 59 60 62 syl3anbrc 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
64 62 simp1bi 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> x e. RR )
65 readdcl 
 |-  ( ( x e. RR /\ ( 1 / 4 ) e. RR ) -> ( x + ( 1 / 4 ) ) e. RR )
66 64 23 65 sylancl 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) e. RR )
67 23 a1i 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 4 ) e. RR )
68 62 simp2bi 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 4 ) <_ x )
69 67 64 67 68 leadd1dd 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( ( 1 / 4 ) + ( 1 / 4 ) ) <_ ( x + ( 1 / 4 ) ) )
70 40 69 eqbrtrrid 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 2 ) <_ ( x + ( 1 / 4 ) ) )
71 61 a1i 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 2 ) e. RR )
72 62 simp3bi 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> x <_ ( 1 / 2 ) )
73 2lt4 
 |-  2 < 4
74 2re 
 |-  2 e. RR
75 4re 
 |-  4 e. RR
76 2pos 
 |-  0 < 2
77 4pos 
 |-  0 < 4
78 74 75 76 77 ltrecii 
 |-  ( 2 < 4 <-> ( 1 / 4 ) < ( 1 / 2 ) )
79 73 78 mpbi 
 |-  ( 1 / 4 ) < ( 1 / 2 )
80 23 61 79 ltleii 
 |-  ( 1 / 4 ) <_ ( 1 / 2 )
81 80 a1i 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 4 ) <_ ( 1 / 2 ) )
82 64 67 71 71 72 81 le2addd 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) <_ ( ( 1 / 2 ) + ( 1 / 2 ) ) )
83 ax-1cn 
 |-  1 e. CC
84 2halves 
 |-  ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
85 83 84 ax-mp 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
86 82 85 breqtrdi 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) <_ 1 )
87 1re 
 |-  1 e. RR
88 61 87 elicc2i 
 |-  ( ( x + ( 1 / 4 ) ) e. ( ( 1 / 2 ) [,] 1 ) <-> ( ( x + ( 1 / 4 ) ) e. RR /\ ( 1 / 2 ) <_ ( x + ( 1 / 4 ) ) /\ ( x + ( 1 / 4 ) ) <_ 1 ) )
89 66 70 86 88 syl3anbrc 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) e. ( ( 1 / 2 ) [,] 1 ) )
90 63 89 syl 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( x + ( 1 / 4 ) ) e. ( ( 1 / 2 ) [,] 1 ) )
91 2 3 pco0 
 |-  ( ph -> ( ( G ( *p ` J ) H ) ` 0 ) = ( G ` 0 ) )
92 4 91 eqtr4d 
 |-  ( ph -> ( F ` 1 ) = ( ( G ( *p ` J ) H ) ` 0 ) )
93 1 46 92 pcoval2 
 |-  ( ( ph /\ ( x + ( 1 / 4 ) ) e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) ) )
94 54 90 93 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) ) )
95 85 oveq2i 
 |-  ( ( 2 x. ( x + ( 1 / 4 ) ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 )
96 2cnd 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> 2 e. CC )
97 56 recnd 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x e. CC )
98 28 a1i 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 1 / 4 ) e. CC )
99 96 97 98 adddid 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. ( x + ( 1 / 4 ) ) ) = ( ( 2 x. x ) + ( 2 x. ( 1 / 4 ) ) ) )
100 41 oveq2i 
 |-  ( ( 2 x. x ) + ( 2 x. ( 1 / 4 ) ) ) = ( ( 2 x. x ) + ( 1 / 2 ) )
101 99 100 eqtrdi 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. ( x + ( 1 / 4 ) ) ) = ( ( 2 x. x ) + ( 1 / 2 ) ) )
102 101 oveq1d 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( 2 x. ( x + ( 1 / 4 ) ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( ( 2 x. x ) + ( 1 / 2 ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
103 95 102 syl5eqr 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) = ( ( ( 2 x. x ) + ( 1 / 2 ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
104 remulcl 
 |-  ( ( 2 e. RR /\ x e. RR ) -> ( 2 x. x ) e. RR )
105 74 56 104 sylancr 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. RR )
106 105 recnd 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. CC )
107 37 a1i 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 1 / 2 ) e. CC )
108 106 107 107 pnpcan2d 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( ( 2 x. x ) + ( 1 / 2 ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 2 x. x ) - ( 1 / 2 ) ) )
109 103 108 eqtrd 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) = ( ( 2 x. x ) - ( 1 / 2 ) ) )
110 109 fveq2d 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. x ) - ( 1 / 2 ) ) ) )
111 10 97 15 sylancr 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) = ( x x. 2 ) )
112 83 10 30 divcan1i 
 |-  ( ( 1 / 2 ) x. 2 ) = 1
113 23 61 26 42 112 iccdili 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x x. 2 ) e. ( ( 1 / 2 ) [,] 1 ) )
114 63 113 syl 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( x x. 2 ) e. ( ( 1 / 2 ) [,] 1 ) )
115 111 114 eqeltrd 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. ( ( 1 / 2 ) [,] 1 ) )
116 37 subidi 
 |-  ( ( 1 / 2 ) - ( 1 / 2 ) ) = 0
117 1mhlfehlf 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
118 61 87 61 116 117 iccshftli 
 |-  ( ( 2 x. x ) e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. x ) - ( 1 / 2 ) ) e. ( 0 [,] ( 1 / 2 ) ) )
119 115 118 syl 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( 2 x. x ) - ( 1 / 2 ) ) e. ( 0 [,] ( 1 / 2 ) ) )
120 2 3 pcoval1 
 |-  ( ( ph /\ ( ( 2 x. x ) - ( 1 / 2 ) ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( G ` ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) ) )
121 54 119 120 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( G ` ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) ) )
122 96 106 107 subdid 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( ( 2 x. ( 2 x. x ) ) - ( 2 x. ( 1 / 2 ) ) ) )
123 10 30 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
124 123 oveq2i 
 |-  ( ( 2 x. ( 2 x. x ) ) - ( 2 x. ( 1 / 2 ) ) ) = ( ( 2 x. ( 2 x. x ) ) - 1 )
125 122 124 eqtrdi 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( ( 2 x. ( 2 x. x ) ) - 1 ) )
126 125 fveq2d 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( G ` ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
127 121 126 eqtrd 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
128 94 110 127 3eqtrd 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
129 iffalse 
 |-  ( -. x <_ ( 1 / 4 ) -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = ( x + ( 1 / 4 ) ) )
130 129 fveq2d 
 |-  ( -. x <_ ( 1 / 4 ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) )
131 130 adantl 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) )
132 1 2 4 pcoval2 
 |-  ( ( ph /\ ( 2 x. x ) e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
133 54 115 132 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
134 128 131 133 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
135 53 134 pm2.61dan 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
136 iftrue 
 |-  ( x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) )
137 136 fveq2d 
 |-  ( x <_ ( 1 / 2 ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) )
138 137 adantl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) )
139 iftrue 
 |-  ( x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
140 139 adantl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
141 135 138 140 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) )
142 elii2 
 |-  ( ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) -> x e. ( ( 1 / 2 ) [,] 1 ) )
143 halfge0 
 |-  0 <_ ( 1 / 2 )
144 halflt1 
 |-  ( 1 / 2 ) < 1
145 61 87 144 ltleii 
 |-  ( 1 / 2 ) <_ 1
146 elicc01 
 |-  ( ( 1 / 2 ) e. ( 0 [,] 1 ) <-> ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ 1 ) )
147 61 143 145 146 mpbir3an 
 |-  ( 1 / 2 ) e. ( 0 [,] 1 )
148 1elunit 
 |-  1 e. ( 0 [,] 1 )
149 iccss2 
 |-  ( ( ( 1 / 2 ) e. ( 0 [,] 1 ) /\ 1 e. ( 0 [,] 1 ) ) -> ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 ) )
150 147 148 149 mp2an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 )
151 150 sseli 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. ( 0 [,] 1 ) )
152 10 30 div0i 
 |-  ( 0 / 2 ) = 0
153 eqid 
 |-  ( 1 / 2 ) = ( 1 / 2 )
154 20 87 26 152 153 icccntri 
 |-  ( x e. ( 0 [,] 1 ) -> ( x / 2 ) e. ( 0 [,] ( 1 / 2 ) ) )
155 37 addid2i 
 |-  ( 0 + ( 1 / 2 ) ) = ( 1 / 2 )
156 20 61 61 155 85 iccshftri 
 |-  ( ( x / 2 ) e. ( 0 [,] ( 1 / 2 ) ) -> ( ( x / 2 ) + ( 1 / 2 ) ) e. ( ( 1 / 2 ) [,] 1 ) )
157 151 154 156 3syl 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( x / 2 ) + ( 1 / 2 ) ) e. ( ( 1 / 2 ) [,] 1 ) )
158 1 46 92 pcoval2 
 |-  ( ( ph /\ ( ( x / 2 ) + ( 1 / 2 ) ) e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) ) )
159 157 158 sylan2 
 |-  ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) ) )
160 61 87 elicc2i 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) <-> ( x e. RR /\ ( 1 / 2 ) <_ x /\ x <_ 1 ) )
161 160 simp1bi 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. RR )
162 161 recnd 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. CC )
163 1cnd 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> 1 e. CC )
164 2cnd 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> 2 e. CC )
165 30 a1i 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> 2 =/= 0 )
166 162 163 164 165 divdird 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( x + 1 ) / 2 ) = ( ( x / 2 ) + ( 1 / 2 ) ) )
167 166 oveq2d 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x + 1 ) / 2 ) ) = ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) )
168 peano2cn 
 |-  ( x e. CC -> ( x + 1 ) e. CC )
169 162 168 syl 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( x + 1 ) e. CC )
170 169 164 165 divcan2d 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x + 1 ) / 2 ) ) = ( x + 1 ) )
171 167 170 eqtr3d 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( x + 1 ) )
172 162 163 171 mvrraddd 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) = x )
173 172 fveq2d 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) ) = ( ( G ( *p ` J ) H ) ` x ) )
174 173 adantl 
 |-  ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) ) = ( ( G ( *p ` J ) H ) ` x ) )
175 2 3 5 pcoval2 
 |-  ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( G ( *p ` J ) H ) ` x ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
176 159 174 175 3eqtrd 
 |-  ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
177 142 176 sylan2 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
178 177 anassrs 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
179 iffalse 
 |-  ( -. x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( ( x / 2 ) + ( 1 / 2 ) ) )
180 179 fveq2d 
 |-  ( -. x <_ ( 1 / 2 ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) )
181 180 adantl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) )
182 iffalse 
 |-  ( -. x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
183 182 adantl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
184 178 181 183 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) )
185 141 184 pm2.61dan 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) )
186 185 mpteq2dva 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) ) )
187 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
188 187 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
189 188 cnmptid 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn II ) )
190 0elunit 
 |-  0 e. ( 0 [,] 1 )
191 190 a1i 
 |-  ( ph -> 0 e. ( 0 [,] 1 ) )
192 188 188 191 cnmptc 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> 0 ) e. ( II Cn II ) )
193 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
194 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) )
195 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) )
196 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
197 0red 
 |-  ( ph -> 0 e. RR )
198 1red 
 |-  ( ph -> 1 e. RR )
199 147 a1i 
 |-  ( ph -> ( 1 / 2 ) e. ( 0 [,] 1 ) )
200 simprl 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> y = ( 1 / 2 ) )
201 200 oveq1d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 2 ) + ( 1 / 4 ) ) )
202 37 28 addcomi 
 |-  ( ( 1 / 2 ) + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) )
203 201 202 eqtrdi 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) ) )
204 23 61 ltnlei 
 |-  ( ( 1 / 4 ) < ( 1 / 2 ) <-> -. ( 1 / 2 ) <_ ( 1 / 4 ) )
205 79 204 mpbi 
 |-  -. ( 1 / 2 ) <_ ( 1 / 4 )
206 200 breq1d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y <_ ( 1 / 4 ) <-> ( 1 / 2 ) <_ ( 1 / 4 ) ) )
207 205 206 mtbiri 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> -. y <_ ( 1 / 4 ) )
208 207 iffalsed 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) = ( y + ( 1 / 4 ) ) )
209 200 oveq1d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y / 2 ) = ( ( 1 / 2 ) / 2 ) )
210 209 35 eqtrdi 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y / 2 ) = ( 1 / 4 ) )
211 210 oveq1d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( ( y / 2 ) + ( 1 / 2 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) ) )
212 203 208 211 3eqtr4d 
 |-  ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) = ( ( y / 2 ) + ( 1 / 2 ) ) )
213 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) )
214 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) = ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
215 61 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
216 75 77 recgt0ii 
 |-  0 < ( 1 / 4 )
217 20 23 216 ltleii 
 |-  0 <_ ( 1 / 4 )
218 20 61 elicc2i 
 |-  ( ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) ) <-> ( ( 1 / 4 ) e. RR /\ 0 <_ ( 1 / 4 ) /\ ( 1 / 4 ) <_ ( 1 / 2 ) ) )
219 23 217 80 218 mpbir3an 
 |-  ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) )
220 219 a1i 
 |-  ( ph -> ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) ) )
221 simprl 
 |-  ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> y = ( 1 / 4 ) )
222 221 oveq2d 
 |-  ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = ( 2 x. ( 1 / 4 ) ) )
223 221 oveq1d 
 |-  ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) ) )
224 29 222 223 3eqtr4a 
 |-  ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = ( y + ( 1 / 4 ) ) )
225 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
226 0xr 
 |-  0 e. RR*
227 61 rexri 
 |-  ( 1 / 2 ) e. RR*
228 lbicc2 
 |-  ( ( 0 e. RR* /\ ( 1 / 2 ) e. RR* /\ 0 <_ ( 1 / 2 ) ) -> 0 e. ( 0 [,] ( 1 / 2 ) ) )
229 226 227 143 228 mp3an 
 |-  0 e. ( 0 [,] ( 1 / 2 ) )
230 iccss2 
 |-  ( ( 0 e. ( 0 [,] ( 1 / 2 ) ) /\ ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( 0 [,] ( 1 / 4 ) ) C_ ( 0 [,] ( 1 / 2 ) ) )
231 229 219 230 mp2an 
 |-  ( 0 [,] ( 1 / 4 ) ) C_ ( 0 [,] ( 1 / 2 ) )
232 iccssre 
 |-  ( ( 0 e. RR /\ ( 1 / 2 ) e. RR ) -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
233 20 61 232 mp2an 
 |-  ( 0 [,] ( 1 / 2 ) ) C_ RR
234 231 233 sstri 
 |-  ( 0 [,] ( 1 / 4 ) ) C_ RR
235 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( 0 [,] ( 1 / 4 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 4 ) ) ) )
236 225 234 235 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 4 ) ) )
237 236 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 4 ) ) ) )
238 237 188 cnmpt1st 
 |-  ( ph -> ( y e. ( 0 [,] ( 1 / 4 ) ) , z e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) tX II ) Cn ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) ) )
239 retop 
 |-  ( topGen ` ran (,) ) e. Top
240 ovex 
 |-  ( 0 [,] ( 1 / 2 ) ) e. _V
241 restabs 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( 0 [,] ( 1 / 4 ) ) C_ ( 0 [,] ( 1 / 2 ) ) /\ ( 0 [,] ( 1 / 2 ) ) e. _V ) -> ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) |`t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) )
242 239 231 240 241 mp3an 
 |-  ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) |`t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) )
243 242 eqcomi 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) = ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) |`t ( 0 [,] ( 1 / 4 ) ) )
244 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( 0 [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
245 225 233 244 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) )
246 245 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
247 231 a1i 
 |-  ( ph -> ( 0 [,] ( 1 / 4 ) ) C_ ( 0 [,] ( 1 / 2 ) ) )
248 194 iihalf1cn 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
249 248 a1i 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
250 243 246 247 249 cnmpt1res 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 4 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) Cn II ) )
251 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
252 237 188 238 237 250 251 cnmpt21 
 |-  ( ph -> ( y e. ( 0 [,] ( 1 / 4 ) ) , z e. ( 0 [,] 1 ) |-> ( 2 x. y ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 4 ) ) ) tX II ) Cn II ) )
253 iccssre 
 |-  ( ( ( 1 / 4 ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR )
254 23 61 253 mp2an 
 |-  ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR
255 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) )
256 225 254 255 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
257 256 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) )
258 257 188 cnmpt1st 
 |-  ( ph -> ( y e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) tX II ) Cn ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) ) )
259 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
260 254 a1i 
 |-  ( ph -> ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR )
261 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
262 261 a1i 
 |-  ( ph -> ( 0 [,] 1 ) C_ RR )
263 150 89 sseldi 
 |-  ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) e. ( 0 [,] 1 ) )
264 263 adantl 
 |-  ( ( ph /\ x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) -> ( x + ( 1 / 4 ) ) e. ( 0 [,] 1 ) )
265 259 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
266 265 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
267 266 cnmptid 
 |-  ( ph -> ( x e. CC |-> x ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
268 23 a1i 
 |-  ( ph -> ( 1 / 4 ) e. RR )
269 268 recnd 
 |-  ( ph -> ( 1 / 4 ) e. CC )
270 266 266 269 cnmptc 
 |-  ( ph -> ( x e. CC |-> ( 1 / 4 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
271 259 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
272 271 a1i 
 |-  ( ph -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
273 266 267 270 272 cnmpt12f 
 |-  ( ph -> ( x e. CC |-> ( x + ( 1 / 4 ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
274 259 214 196 260 262 264 273 cnmptre 
 |-  ( ph -> ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) |-> ( x + ( 1 / 4 ) ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) Cn II ) )
275 oveq1 
 |-  ( x = y -> ( x + ( 1 / 4 ) ) = ( y + ( 1 / 4 ) ) )
276 257 188 258 257 274 275 cnmpt21 
 |-  ( ph -> ( y e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> ( y + ( 1 / 4 ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
277 193 213 214 194 197 215 220 188 224 252 276 cnmpopc 
 |-  ( ph -> ( y e. ( 0 [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
278 iccssre 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
279 61 87 278 mp2an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ RR
280 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( 1 / 2 ) [,] 1 ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
281 225 279 280 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) )
282 281 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
283 282 188 cnmpt1st 
 |-  ( ph -> ( 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 ) ) ) )
284 279 a1i 
 |-  ( ph -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
285 150 157 sseldi 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( x / 2 ) + ( 1 / 2 ) ) e. ( 0 [,] 1 ) )
286 285 adantl 
 |-  ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( x / 2 ) + ( 1 / 2 ) ) e. ( 0 [,] 1 ) )
287 259 divccn 
 |-  ( ( 2 e. CC /\ 2 =/= 0 ) -> ( x e. CC |-> ( x / 2 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
288 10 30 287 mp2an 
 |-  ( x e. CC |-> ( x / 2 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
289 288 a1i 
 |-  ( ph -> ( x e. CC |-> ( x / 2 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
290 37 a1i 
 |-  ( ph -> ( 1 / 2 ) e. CC )
291 266 266 290 cnmptc 
 |-  ( ph -> ( x e. CC |-> ( 1 / 2 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
292 266 289 291 272 cnmpt12f 
 |-  ( ph -> ( x e. CC |-> ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
293 259 195 196 284 262 286 292 cnmptre 
 |-  ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
294 oveq1 
 |-  ( x = y -> ( x / 2 ) = ( y / 2 ) )
295 294 oveq1d 
 |-  ( x = y -> ( ( x / 2 ) + ( 1 / 2 ) ) = ( ( y / 2 ) + ( 1 / 2 ) ) )
296 282 188 283 282 293 295 cnmpt21 
 |-  ( ph -> ( y e. ( ( 1 / 2 ) [,] 1 ) , z e. ( 0 [,] 1 ) |-> ( ( y / 2 ) + ( 1 / 2 ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn II ) )
297 193 194 195 196 197 198 199 188 212 277 296 cnmpopc 
 |-  ( ph -> ( y e. ( 0 [,] 1 ) , z e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) ) e. ( ( II tX II ) Cn II ) )
298 breq1 
 |-  ( x = y -> ( x <_ ( 1 / 2 ) <-> y <_ ( 1 / 2 ) ) )
299 breq1 
 |-  ( x = y -> ( x <_ ( 1 / 4 ) <-> y <_ ( 1 / 4 ) ) )
300 299 251 275 ifbieq12d 
 |-  ( x = y -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) )
301 298 300 295 ifbieq12d 
 |-  ( x = y -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) )
302 301 equcoms 
 |-  ( y = x -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) )
303 302 adantr 
 |-  ( ( y = x /\ z = 0 ) -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) )
304 303 eqcomd 
 |-  ( ( y = x /\ z = 0 ) -> if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) = if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) )
305 188 189 192 188 188 297 304 cnmpt12 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) e. ( II Cn II ) )
306 6 305 eqeltrid 
 |-  ( ph -> P e. ( II Cn II ) )
307 iiuni 
 |-  ( 0 [,] 1 ) = U. II
308 307 307 cnf 
 |-  ( P e. ( II Cn II ) -> P : ( 0 [,] 1 ) --> ( 0 [,] 1 ) )
309 306 308 syl 
 |-  ( ph -> P : ( 0 [,] 1 ) --> ( 0 [,] 1 ) )
310 6 fmpt 
 |-  ( A. x e. ( 0 [,] 1 ) if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( 0 [,] 1 ) <-> P : ( 0 [,] 1 ) --> ( 0 [,] 1 ) )
311 309 310 sylibr 
 |-  ( ph -> A. x e. ( 0 [,] 1 ) if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( 0 [,] 1 ) )
312 6 a1i 
 |-  ( ph -> P = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) )
313 1 46 92 pcocn 
 |-  ( ph -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) e. ( II Cn J ) )
314 eqid 
 |-  U. J = U. J
315 307 314 cnf 
 |-  ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) e. ( II Cn J ) -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) : ( 0 [,] 1 ) --> U. J )
316 313 315 syl 
 |-  ( ph -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) : ( 0 [,] 1 ) --> U. J )
317 316 feqmptd 
 |-  ( ph -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) = ( y e. ( 0 [,] 1 ) |-> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` y ) ) )
318 fveq2 
 |-  ( y = if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` y ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) )
319 311 312 317 318 fmptcof 
 |-  ( ph -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) o. P ) = ( x e. ( 0 [,] 1 ) |-> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) ) )
320 1 2 4 pcocn 
 |-  ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )
321 320 3 pcoval 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) ) )
322 186 319 321 3eqtr4rd 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) o. P ) )
323 id 
 |-  ( x = 0 -> x = 0 )
324 323 143 eqbrtrdi 
 |-  ( x = 0 -> x <_ ( 1 / 2 ) )
325 324 iftrued 
 |-  ( x = 0 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) )
326 323 217 eqbrtrdi 
 |-  ( x = 0 -> x <_ ( 1 / 4 ) )
327 326 iftrued 
 |-  ( x = 0 -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = ( 2 x. x ) )
328 oveq2 
 |-  ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) )
329 2t0e0 
 |-  ( 2 x. 0 ) = 0
330 328 329 eqtrdi 
 |-  ( x = 0 -> ( 2 x. x ) = 0 )
331 325 327 330 3eqtrd 
 |-  ( x = 0 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = 0 )
332 c0ex 
 |-  0 e. _V
333 331 6 332 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( P ` 0 ) = 0 )
334 191 333 syl 
 |-  ( ph -> ( P ` 0 ) = 0 )
335 148 a1i 
 |-  ( ph -> 1 e. ( 0 [,] 1 ) )
336 61 87 ltnlei 
 |-  ( ( 1 / 2 ) < 1 <-> -. 1 <_ ( 1 / 2 ) )
337 144 336 mpbi 
 |-  -. 1 <_ ( 1 / 2 )
338 breq1 
 |-  ( x = 1 -> ( x <_ ( 1 / 2 ) <-> 1 <_ ( 1 / 2 ) ) )
339 337 338 mtbiri 
 |-  ( x = 1 -> -. x <_ ( 1 / 2 ) )
340 339 iffalsed 
 |-  ( x = 1 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( ( x / 2 ) + ( 1 / 2 ) ) )
341 oveq1 
 |-  ( x = 1 -> ( x / 2 ) = ( 1 / 2 ) )
342 341 oveq1d 
 |-  ( x = 1 -> ( ( x / 2 ) + ( 1 / 2 ) ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) )
343 342 85 eqtrdi 
 |-  ( x = 1 -> ( ( x / 2 ) + ( 1 / 2 ) ) = 1 )
344 340 343 eqtrd 
 |-  ( x = 1 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = 1 )
345 1ex 
 |-  1 e. _V
346 344 6 345 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( P ` 1 ) = 1 )
347 335 346 syl 
 |-  ( ph -> ( P ` 1 ) = 1 )
348 313 306 334 347 reparpht 
 |-  ( ph -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) o. P ) ( ~=ph ` J ) ( F ( *p ` J ) ( G ( *p ` J ) H ) ) )
349 322 348 eqbrtrd 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) ( ~=ph ` J ) ( F ( *p ` J ) ( G ( *p ` J ) H ) ) )