Metamath Proof Explorer

Theorem pcohtpylem

Description: Lemma for pcohtpy . (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses pcohtpy.4 
|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )
pcohtpy.5 
|- ( ph -> F ( ~=ph ` J ) H )
pcohtpy.6 
|- ( ph -> G ( ~=ph ` J ) K )
pcohtpylem.7 
|- P = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) )
pcohtpylem.8 
|- ( ph -> M e. ( F ( PHtpy ` J ) H ) )
pcohtpylem.9 
|- ( ph -> N e. ( G ( PHtpy ` J ) K ) )
Assertion pcohtpylem 
|- ( ph -> P e. ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) )

Proof

Step Hyp Ref Expression
1 pcohtpy.4 
 |-  ( ph -> ( F ` 1 ) = ( G ` 0 ) )
2 pcohtpy.5 
 |-  ( ph -> F ( ~=ph ` J ) H )
3 pcohtpy.6 
 |-  ( ph -> G ( ~=ph ` J ) K )
4 pcohtpylem.7 
 |-  P = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) )
5 pcohtpylem.8 
 |-  ( ph -> M e. ( F ( PHtpy ` J ) H ) )
6 pcohtpylem.9 
 |-  ( ph -> N e. ( G ( PHtpy ` J ) K ) )
7 isphtpc 
 |-  ( F ( ~=ph ` J ) H <-> ( F e. ( II Cn J ) /\ H e. ( II Cn J ) /\ ( F ( PHtpy ` J ) H ) =/= (/) ) )
8 2 7 sylib 
 |-  ( ph -> ( F e. ( II Cn J ) /\ H e. ( II Cn J ) /\ ( F ( PHtpy ` J ) H ) =/= (/) ) )
9 8 simp1d 
 |-  ( ph -> F e. ( II Cn J ) )
10 isphtpc 
 |-  ( G ( ~=ph ` J ) K <-> ( G e. ( II Cn J ) /\ K e. ( II Cn J ) /\ ( G ( PHtpy ` J ) K ) =/= (/) ) )
11 3 10 sylib 
 |-  ( ph -> ( G e. ( II Cn J ) /\ K e. ( II Cn J ) /\ ( G ( PHtpy ` J ) K ) =/= (/) ) )
12 11 simp1d 
 |-  ( ph -> G e. ( II Cn J ) )
13 9 12 1 pcocn 
 |-  ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )
14 8 simp2d 
 |-  ( ph -> H e. ( II Cn J ) )
15 11 simp2d 
 |-  ( ph -> K e. ( II Cn J ) )
16 9 14 5 phtpy01 
 |-  ( ph -> ( ( F ` 0 ) = ( H ` 0 ) /\ ( F ` 1 ) = ( H ` 1 ) ) )
17 16 simprd 
 |-  ( ph -> ( F ` 1 ) = ( H ` 1 ) )
18 12 15 6 phtpy01 
 |-  ( ph -> ( ( G ` 0 ) = ( K ` 0 ) /\ ( G ` 1 ) = ( K ` 1 ) ) )
19 18 simpld 
 |-  ( ph -> ( G ` 0 ) = ( K ` 0 ) )
20 1 17 19 3eqtr3d 
 |-  ( ph -> ( H ` 1 ) = ( K ` 0 ) )
21 14 15 20 pcocn 
 |-  ( ph -> ( H ( *p ` J ) K ) e. ( II Cn J ) )
22 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
23 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) )
24 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) )
25 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
26 0red 
 |-  ( ph -> 0 e. RR )
27 1red 
 |-  ( ph -> 1 e. RR )
28 halfre 
 |-  ( 1 / 2 ) e. RR
29 halfge0 
 |-  0 <_ ( 1 / 2 )
30 1re 
 |-  1 e. RR
31 halflt1 
 |-  ( 1 / 2 ) < 1
32 28 30 31 ltleii 
 |-  ( 1 / 2 ) <_ 1
33 elicc01 
 |-  ( ( 1 / 2 ) e. ( 0 [,] 1 ) <-> ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ 1 ) )
34 28 29 32 33 mpbir3an 
 |-  ( 1 / 2 ) e. ( 0 [,] 1 )
35 34 a1i 
 |-  ( ph -> ( 1 / 2 ) e. ( 0 [,] 1 ) )
36 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
37 36 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
38 1 adantr 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( F ` 1 ) = ( G ` 0 ) )
39 9 14 5 phtpyi 
 |-  ( ( ph /\ y e. ( 0 [,] 1 ) ) -> ( ( 0 M y ) = ( F ` 0 ) /\ ( 1 M y ) = ( F ` 1 ) ) )
40 39 simprd 
 |-  ( ( ph /\ y e. ( 0 [,] 1 ) ) -> ( 1 M y ) = ( F ` 1 ) )
41 40 adantrl 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( 1 M y ) = ( F ` 1 ) )
42 12 15 6 phtpyi 
 |-  ( ( ph /\ y e. ( 0 [,] 1 ) ) -> ( ( 0 N y ) = ( G ` 0 ) /\ ( 1 N y ) = ( G ` 1 ) ) )
43 42 simpld 
 |-  ( ( ph /\ y e. ( 0 [,] 1 ) ) -> ( 0 N y ) = ( G ` 0 ) )
44 43 adantrl 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( 0 N y ) = ( G ` 0 ) )
45 38 41 44 3eqtr4d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( 1 M y ) = ( 0 N y ) )
46 simprl 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> x = ( 1 / 2 ) )
47 46 oveq2d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( 2 x. x ) = ( 2 x. ( 1 / 2 ) ) )
48 2cn 
 |-  2 e. CC
49 2ne0 
 |-  2 =/= 0
50 48 49 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
51 47 50 eqtrdi 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( 2 x. x ) = 1 )
52 51 oveq1d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. x ) M y ) = ( 1 M y ) )
53 51 oveq1d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. x ) - 1 ) = ( 1 - 1 ) )
54 1m1e0 
 |-  ( 1 - 1 ) = 0
55 53 54 eqtrdi 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. x ) - 1 ) = 0 )
56 55 oveq1d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( ( 2 x. x ) - 1 ) N y ) = ( 0 N y ) )
57 45 52 56 3eqtr4d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. x ) M y ) = ( ( ( 2 x. x ) - 1 ) N y ) )
58 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
59 0re 
 |-  0 e. RR
60 iccssre 
 |-  ( ( 0 e. RR /\ ( 1 / 2 ) e. RR ) -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
61 59 28 60 mp2an 
 |-  ( 0 [,] ( 1 / 2 ) ) C_ RR
62 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( 0 [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
63 58 61 62 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) )
64 63 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
65 64 37 cnmpt1st 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) , y e. ( 0 [,] 1 ) |-> x ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) ) )
66 23 iihalf1cn 
 |-  ( z e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. z ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
67 66 a1i 
 |-  ( ph -> ( z e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. z ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
68 oveq2 
 |-  ( z = x -> ( 2 x. z ) = ( 2 x. x ) )
69 64 37 65 64 67 68 cnmpt21 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) , y e. ( 0 [,] 1 ) |-> ( 2 x. x ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
70 64 37 cnmpt2nd 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) , y e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
71 9 14 phtpycn 
 |-  ( ph -> ( F ( PHtpy ` J ) H ) C_ ( ( II tX II ) Cn J ) )
72 71 5 sseldd 
 |-  ( ph -> M e. ( ( II tX II ) Cn J ) )
73 64 37 69 70 72 cnmpt22f 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) , y e. ( 0 [,] 1 ) |-> ( ( 2 x. x ) M y ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn J ) )
74 iccssre 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
75 28 30 74 mp2an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ RR
76 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( 1 / 2 ) [,] 1 ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
77 58 75 76 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) )
78 77 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
79 78 37 cnmpt1st 
 |-  ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) , y e. ( 0 [,] 1 ) |-> x ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) ) )
80 24 iihalf2cn 
 |-  ( z e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. z ) - 1 ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
81 80 a1i 
 |-  ( ph -> ( z e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. z ) - 1 ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
82 68 oveq1d 
 |-  ( z = x -> ( ( 2 x. z ) - 1 ) = ( ( 2 x. x ) - 1 ) )
83 78 37 79 78 81 82 cnmpt21 
 |-  ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn II ) )
84 78 37 cnmpt2nd 
 |-  ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) , y e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn II ) )
85 12 15 phtpycn 
 |-  ( ph -> ( G ( PHtpy ` J ) K ) C_ ( ( II tX II ) Cn J ) )
86 85 6 sseldd 
 |-  ( ph -> N e. ( ( II tX II ) Cn J ) )
87 78 37 83 84 86 cnmpt22f 
 |-  ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 2 x. x ) - 1 ) N y ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn J ) )
88 22 23 24 25 26 27 35 37 57 73 87 cnmpopc 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) ) e. ( ( II tX II ) Cn J ) )
89 4 88 eqeltrid 
 |-  ( ph -> P e. ( ( II tX II ) Cn J ) )
90 simpll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ph )
91 elii1 
 |-  ( s e. ( 0 [,] ( 1 / 2 ) ) <-> ( s e. ( 0 [,] 1 ) /\ s <_ ( 1 / 2 ) ) )
92 iihalf1 
 |-  ( s e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
93 91 92 sylbir 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s <_ ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
94 93 adantll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
95 9 14 phtpyhtpy 
 |-  ( ph -> ( F ( PHtpy ` J ) H ) C_ ( F ( II Htpy J ) H ) )
96 95 5 sseldd 
 |-  ( ph -> M e. ( F ( II Htpy J ) H ) )
97 37 9 14 96 htpyi 
 |-  ( ( ph /\ ( 2 x. s ) e. ( 0 [,] 1 ) ) -> ( ( ( 2 x. s ) M 0 ) = ( F ` ( 2 x. s ) ) /\ ( ( 2 x. s ) M 1 ) = ( H ` ( 2 x. s ) ) ) )
98 90 94 97 syl2anc 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( ( ( 2 x. s ) M 0 ) = ( F ` ( 2 x. s ) ) /\ ( ( 2 x. s ) M 1 ) = ( H ` ( 2 x. s ) ) ) )
99 98 simpld 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( ( 2 x. s ) M 0 ) = ( F ` ( 2 x. s ) ) )
100 simpll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ph )
101 elii2 
 |-  ( ( s e. ( 0 [,] 1 ) /\ -. s <_ ( 1 / 2 ) ) -> s e. ( ( 1 / 2 ) [,] 1 ) )
102 101 adantll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> s e. ( ( 1 / 2 ) [,] 1 ) )
103 iihalf2 
 |-  ( s e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) )
104 102 103 syl 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) )
105 12 15 phtpyhtpy 
 |-  ( ph -> ( G ( PHtpy ` J ) K ) C_ ( G ( II Htpy J ) K ) )
106 105 6 sseldd 
 |-  ( ph -> N e. ( G ( II Htpy J ) K ) )
107 37 12 15 106 htpyi 
 |-  ( ( ph /\ ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) ) -> ( ( ( ( 2 x. s ) - 1 ) N 0 ) = ( G ` ( ( 2 x. s ) - 1 ) ) /\ ( ( ( 2 x. s ) - 1 ) N 1 ) = ( K ` ( ( 2 x. s ) - 1 ) ) ) )
108 100 104 107 syl2anc 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( ( ( 2 x. s ) - 1 ) N 0 ) = ( G ` ( ( 2 x. s ) - 1 ) ) /\ ( ( ( 2 x. s ) - 1 ) N 1 ) = ( K ` ( ( 2 x. s ) - 1 ) ) ) )
109 108 simpld 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( ( 2 x. s ) - 1 ) N 0 ) = ( G ` ( ( 2 x. s ) - 1 ) ) )
110 99 109 ifeq12da 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 0 ) , ( ( ( 2 x. s ) - 1 ) N 0 ) ) = if ( s <_ ( 1 / 2 ) , ( F ` ( 2 x. s ) ) , ( G ` ( ( 2 x. s ) - 1 ) ) ) )
111 simpr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> s e. ( 0 [,] 1 ) )
112 0elunit 
 |-  0 e. ( 0 [,] 1 )
113 simpl 
 |-  ( ( x = s /\ y = 0 ) -> x = s )
114 113 breq1d 
 |-  ( ( x = s /\ y = 0 ) -> ( x <_ ( 1 / 2 ) <-> s <_ ( 1 / 2 ) ) )
115 113 oveq2d 
 |-  ( ( x = s /\ y = 0 ) -> ( 2 x. x ) = ( 2 x. s ) )
116 simpr 
 |-  ( ( x = s /\ y = 0 ) -> y = 0 )
117 115 116 oveq12d 
 |-  ( ( x = s /\ y = 0 ) -> ( ( 2 x. x ) M y ) = ( ( 2 x. s ) M 0 ) )
118 115 oveq1d 
 |-  ( ( x = s /\ y = 0 ) -> ( ( 2 x. x ) - 1 ) = ( ( 2 x. s ) - 1 ) )
119 118 116 oveq12d 
 |-  ( ( x = s /\ y = 0 ) -> ( ( ( 2 x. x ) - 1 ) N y ) = ( ( ( 2 x. s ) - 1 ) N 0 ) )
120 114 117 119 ifbieq12d 
 |-  ( ( x = s /\ y = 0 ) -> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) = if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 0 ) , ( ( ( 2 x. s ) - 1 ) N 0 ) ) )
121 ovex 
 |-  ( ( 2 x. s ) M 0 ) e. _V
122 ovex 
 |-  ( ( ( 2 x. s ) - 1 ) N 0 ) e. _V
123 121 122 ifex 
 |-  if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 0 ) , ( ( ( 2 x. s ) - 1 ) N 0 ) ) e. _V
124 120 4 123 ovmpoa 
 |-  ( ( s e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) -> ( s P 0 ) = if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 0 ) , ( ( ( 2 x. s ) - 1 ) N 0 ) ) )
125 111 112 124 sylancl 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s P 0 ) = if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 0 ) , ( ( ( 2 x. s ) - 1 ) N 0 ) ) )
126 9 12 pcovalg 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` s ) = if ( s <_ ( 1 / 2 ) , ( F ` ( 2 x. s ) ) , ( G ` ( ( 2 x. s ) - 1 ) ) ) )
127 110 125 126 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s P 0 ) = ( ( F ( *p ` J ) G ) ` s ) )
128 98 simprd 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( ( 2 x. s ) M 1 ) = ( H ` ( 2 x. s ) ) )
129 108 simprd 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( ( 2 x. s ) - 1 ) N 1 ) = ( K ` ( ( 2 x. s ) - 1 ) ) )
130 128 129 ifeq12da 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 1 ) , ( ( ( 2 x. s ) - 1 ) N 1 ) ) = if ( s <_ ( 1 / 2 ) , ( H ` ( 2 x. s ) ) , ( K ` ( ( 2 x. s ) - 1 ) ) ) )
131 1elunit 
 |-  1 e. ( 0 [,] 1 )
132 simpl 
 |-  ( ( x = s /\ y = 1 ) -> x = s )
133 132 breq1d 
 |-  ( ( x = s /\ y = 1 ) -> ( x <_ ( 1 / 2 ) <-> s <_ ( 1 / 2 ) ) )
134 132 oveq2d 
 |-  ( ( x = s /\ y = 1 ) -> ( 2 x. x ) = ( 2 x. s ) )
135 simpr 
 |-  ( ( x = s /\ y = 1 ) -> y = 1 )
136 134 135 oveq12d 
 |-  ( ( x = s /\ y = 1 ) -> ( ( 2 x. x ) M y ) = ( ( 2 x. s ) M 1 ) )
137 134 oveq1d 
 |-  ( ( x = s /\ y = 1 ) -> ( ( 2 x. x ) - 1 ) = ( ( 2 x. s ) - 1 ) )
138 137 135 oveq12d 
 |-  ( ( x = s /\ y = 1 ) -> ( ( ( 2 x. x ) - 1 ) N y ) = ( ( ( 2 x. s ) - 1 ) N 1 ) )
139 133 136 138 ifbieq12d 
 |-  ( ( x = s /\ y = 1 ) -> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) = if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 1 ) , ( ( ( 2 x. s ) - 1 ) N 1 ) ) )
140 ovex 
 |-  ( ( 2 x. s ) M 1 ) e. _V
141 ovex 
 |-  ( ( ( 2 x. s ) - 1 ) N 1 ) e. _V
142 140 141 ifex 
 |-  if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 1 ) , ( ( ( 2 x. s ) - 1 ) N 1 ) ) e. _V
143 139 4 142 ovmpoa 
 |-  ( ( s e. ( 0 [,] 1 ) /\ 1 e. ( 0 [,] 1 ) ) -> ( s P 1 ) = if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 1 ) , ( ( ( 2 x. s ) - 1 ) N 1 ) ) )
144 111 131 143 sylancl 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s P 1 ) = if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 1 ) , ( ( ( 2 x. s ) - 1 ) N 1 ) ) )
145 14 15 pcovalg 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( H ( *p ` J ) K ) ` s ) = if ( s <_ ( 1 / 2 ) , ( H ` ( 2 x. s ) ) , ( K ` ( ( 2 x. s ) - 1 ) ) ) )
146 130 144 145 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s P 1 ) = ( ( H ( *p ` J ) K ) ` s ) )
147 9 14 5 phtpyi 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 0 M s ) = ( F ` 0 ) /\ ( 1 M s ) = ( F ` 1 ) ) )
148 147 simpld 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 M s ) = ( F ` 0 ) )
149 simpl 
 |-  ( ( x = 0 /\ y = s ) -> x = 0 )
150 149 29 eqbrtrdi 
 |-  ( ( x = 0 /\ y = s ) -> x <_ ( 1 / 2 ) )
151 150 iftrued 
 |-  ( ( x = 0 /\ y = s ) -> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) = ( ( 2 x. x ) M y ) )
152 149 oveq2d 
 |-  ( ( x = 0 /\ y = s ) -> ( 2 x. x ) = ( 2 x. 0 ) )
153 2t0e0 
 |-  ( 2 x. 0 ) = 0
154 152 153 eqtrdi 
 |-  ( ( x = 0 /\ y = s ) -> ( 2 x. x ) = 0 )
155 simpr 
 |-  ( ( x = 0 /\ y = s ) -> y = s )
156 154 155 oveq12d 
 |-  ( ( x = 0 /\ y = s ) -> ( ( 2 x. x ) M y ) = ( 0 M s ) )
157 151 156 eqtrd 
 |-  ( ( x = 0 /\ y = s ) -> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) = ( 0 M s ) )
158 ovex 
 |-  ( 0 M s ) e. _V
159 157 4 158 ovmpoa 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( 0 P s ) = ( 0 M s ) )
160 112 111 159 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 P s ) = ( 0 M s ) )
161 9 12 pco0 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` 0 ) )
162 161 adantr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` 0 ) )
163 148 160 162 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 P s ) = ( ( F ( *p ` J ) G ) ` 0 ) )
164 12 15 6 phtpyi 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 0 N s ) = ( G ` 0 ) /\ ( 1 N s ) = ( G ` 1 ) ) )
165 164 simprd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 N s ) = ( G ` 1 ) )
166 28 30 ltnlei 
 |-  ( ( 1 / 2 ) < 1 <-> -. 1 <_ ( 1 / 2 ) )
167 31 166 mpbi 
 |-  -. 1 <_ ( 1 / 2 )
168 simpl 
 |-  ( ( x = 1 /\ y = s ) -> x = 1 )
169 168 breq1d 
 |-  ( ( x = 1 /\ y = s ) -> ( x <_ ( 1 / 2 ) <-> 1 <_ ( 1 / 2 ) ) )
170 167 169 mtbiri 
 |-  ( ( x = 1 /\ y = s ) -> -. x <_ ( 1 / 2 ) )
171 170 iffalsed 
 |-  ( ( x = 1 /\ y = s ) -> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) = ( ( ( 2 x. x ) - 1 ) N y ) )
172 168 oveq2d 
 |-  ( ( x = 1 /\ y = s ) -> ( 2 x. x ) = ( 2 x. 1 ) )
173 2t1e2 
 |-  ( 2 x. 1 ) = 2
174 172 173 eqtrdi 
 |-  ( ( x = 1 /\ y = s ) -> ( 2 x. x ) = 2 )
175 174 oveq1d 
 |-  ( ( x = 1 /\ y = s ) -> ( ( 2 x. x ) - 1 ) = ( 2 - 1 ) )
176 2m1e1 
 |-  ( 2 - 1 ) = 1
177 175 176 eqtrdi 
 |-  ( ( x = 1 /\ y = s ) -> ( ( 2 x. x ) - 1 ) = 1 )
178 simpr 
 |-  ( ( x = 1 /\ y = s ) -> y = s )
179 177 178 oveq12d 
 |-  ( ( x = 1 /\ y = s ) -> ( ( ( 2 x. x ) - 1 ) N y ) = ( 1 N s ) )
180 171 179 eqtrd 
 |-  ( ( x = 1 /\ y = s ) -> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) = ( 1 N s ) )
181 ovex 
 |-  ( 1 N s ) e. _V
182 180 4 181 ovmpoa 
 |-  ( ( 1 e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( 1 P s ) = ( 1 N s ) )
183 131 111 182 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 P s ) = ( 1 N s ) )
184 9 12 pco1 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ` 1 ) = ( G ` 1 ) )
185 184 adantr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` 1 ) = ( G ` 1 ) )
186 165 183 185 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 P s ) = ( ( F ( *p ` J ) G ) ` 1 ) )
187 13 21 89 127 146 163 186 isphtpy2d 
 |-  ( ph -> P e. ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) )