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 2thalfe1 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
49 47 48 eqtrdi 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( 2 x. x ) = 1 )
50 49 oveq1d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. x ) M y ) = ( 1 M y ) )
51 49 oveq1d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. x ) - 1 ) = ( 1 - 1 ) )
52 1m1e0 
 |-  ( 1 - 1 ) = 0
53 51 52 eqtrdi 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. x ) - 1 ) = 0 )
54 53 oveq1d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( ( 2 x. x ) - 1 ) N y ) = ( 0 N y ) )
55 45 50 54 3eqtr4d 
 |-  ( ( ph /\ ( x = ( 1 / 2 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( 2 x. x ) M y ) = ( ( ( 2 x. x ) - 1 ) N y ) )
56 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
57 0re 
 |-  0 e. RR
58 iccssre 
 |-  ( ( 0 e. RR /\ ( 1 / 2 ) e. RR ) -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
59 57 28 58 mp2an 
 |-  ( 0 [,] ( 1 / 2 ) ) C_ RR
60 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( 0 [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
61 56 59 60 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) )
62 61 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
63 62 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 ) ) ) ) )
64 23 iihalf1cn 
 |-  ( z e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. z ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
65 64 a1i 
 |-  ( ph -> ( z e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. z ) ) e. ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
66 oveq2 
 |-  ( z = x -> ( 2 x. z ) = ( 2 x. x ) )
67 62 37 63 62 65 66 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 ) )
68 62 37 cnmpt2nd 
 |-  ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) , y e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
69 9 14 phtpycn 
 |-  ( ph -> ( F ( PHtpy ` J ) H ) C_ ( ( II tX II ) Cn J ) )
70 69 5 sseldd 
 |-  ( ph -> M e. ( ( II tX II ) Cn J ) )
71 62 37 67 68 70 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 ) )
72 iccssre 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
73 28 30 72 mp2an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ RR
74 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( 1 / 2 ) [,] 1 ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
75 56 73 74 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) )
76 75 a1i 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
77 76 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 ) ) ) )
78 24 iihalf2cn 
 |-  ( z e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. z ) - 1 ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
79 78 a1i 
 |-  ( ph -> ( z e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. z ) - 1 ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
80 66 oveq1d 
 |-  ( z = x -> ( ( 2 x. z ) - 1 ) = ( ( 2 x. x ) - 1 ) )
81 76 37 77 76 79 80 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 ) )
82 76 37 cnmpt2nd 
 |-  ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) , y e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn II ) )
83 12 15 phtpycn 
 |-  ( ph -> ( G ( PHtpy ` J ) K ) C_ ( ( II tX II ) Cn J ) )
84 83 6 sseldd 
 |-  ( ph -> N e. ( ( II tX II ) Cn J ) )
85 76 37 81 82 84 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 ) )
86 22 23 24 25 26 27 35 37 55 71 85 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 ) )
87 4 86 eqeltrid 
 |-  ( ph -> P e. ( ( II tX II ) Cn J ) )
88 simpll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ph )
89 elii1 
 |-  ( s e. ( 0 [,] ( 1 / 2 ) ) <-> ( s e. ( 0 [,] 1 ) /\ s <_ ( 1 / 2 ) ) )
90 iihalf1 
 |-  ( s e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
91 89 90 sylbir 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s <_ ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
92 91 adantll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
93 9 14 phtpyhtpy 
 |-  ( ph -> ( F ( PHtpy ` J ) H ) C_ ( F ( II Htpy J ) H ) )
94 93 5 sseldd 
 |-  ( ph -> M e. ( F ( II Htpy J ) H ) )
95 37 9 14 94 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 ) ) ) )
96 88 92 95 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 ) ) ) )
97 96 simpld 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( ( 2 x. s ) M 0 ) = ( F ` ( 2 x. s ) ) )
98 simpll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ph )
99 elii2 
 |-  ( ( s e. ( 0 [,] 1 ) /\ -. s <_ ( 1 / 2 ) ) -> s e. ( ( 1 / 2 ) [,] 1 ) )
100 99 adantll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> s e. ( ( 1 / 2 ) [,] 1 ) )
101 iihalf2 
 |-  ( s e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) )
102 100 101 syl 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) )
103 12 15 phtpyhtpy 
 |-  ( ph -> ( G ( PHtpy ` J ) K ) C_ ( G ( II Htpy J ) K ) )
104 103 6 sseldd 
 |-  ( ph -> N e. ( G ( II Htpy J ) K ) )
105 37 12 15 104 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 ) ) ) )
106 98 102 105 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 ) ) ) )
107 106 simpld 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( ( 2 x. s ) - 1 ) N 0 ) = ( G ` ( ( 2 x. s ) - 1 ) ) )
108 97 107 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 ) ) ) )
109 simpr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> s e. ( 0 [,] 1 ) )
110 0elunit 
 |-  0 e. ( 0 [,] 1 )
111 simpl 
 |-  ( ( x = s /\ y = 0 ) -> x = s )
112 111 breq1d 
 |-  ( ( x = s /\ y = 0 ) -> ( x <_ ( 1 / 2 ) <-> s <_ ( 1 / 2 ) ) )
113 111 oveq2d 
 |-  ( ( x = s /\ y = 0 ) -> ( 2 x. x ) = ( 2 x. s ) )
114 simpr 
 |-  ( ( x = s /\ y = 0 ) -> y = 0 )
115 113 114 oveq12d 
 |-  ( ( x = s /\ y = 0 ) -> ( ( 2 x. x ) M y ) = ( ( 2 x. s ) M 0 ) )
116 113 oveq1d 
 |-  ( ( x = s /\ y = 0 ) -> ( ( 2 x. x ) - 1 ) = ( ( 2 x. s ) - 1 ) )
117 116 114 oveq12d 
 |-  ( ( x = s /\ y = 0 ) -> ( ( ( 2 x. x ) - 1 ) N y ) = ( ( ( 2 x. s ) - 1 ) N 0 ) )
118 112 115 117 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 ) ) )
119 ovex 
 |-  ( ( 2 x. s ) M 0 ) e. _V
120 ovex 
 |-  ( ( ( 2 x. s ) - 1 ) N 0 ) e. _V
121 119 120 ifex 
 |-  if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 0 ) , ( ( ( 2 x. s ) - 1 ) N 0 ) ) e. _V
122 118 4 121 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 ) ) )
123 109 110 122 sylancl 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s P 0 ) = if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 0 ) , ( ( ( 2 x. s ) - 1 ) N 0 ) ) )
124 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 ) ) ) )
125 108 123 124 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s P 0 ) = ( ( F ( *p ` J ) G ) ` s ) )
126 96 simprd 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( ( 2 x. s ) M 1 ) = ( H ` ( 2 x. s ) ) )
127 106 simprd 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( ( 2 x. s ) - 1 ) N 1 ) = ( K ` ( ( 2 x. s ) - 1 ) ) )
128 126 127 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 ) ) ) )
129 1elunit 
 |-  1 e. ( 0 [,] 1 )
130 simpl 
 |-  ( ( x = s /\ y = 1 ) -> x = s )
131 130 breq1d 
 |-  ( ( x = s /\ y = 1 ) -> ( x <_ ( 1 / 2 ) <-> s <_ ( 1 / 2 ) ) )
132 130 oveq2d 
 |-  ( ( x = s /\ y = 1 ) -> ( 2 x. x ) = ( 2 x. s ) )
133 simpr 
 |-  ( ( x = s /\ y = 1 ) -> y = 1 )
134 132 133 oveq12d 
 |-  ( ( x = s /\ y = 1 ) -> ( ( 2 x. x ) M y ) = ( ( 2 x. s ) M 1 ) )
135 132 oveq1d 
 |-  ( ( x = s /\ y = 1 ) -> ( ( 2 x. x ) - 1 ) = ( ( 2 x. s ) - 1 ) )
136 135 133 oveq12d 
 |-  ( ( x = s /\ y = 1 ) -> ( ( ( 2 x. x ) - 1 ) N y ) = ( ( ( 2 x. s ) - 1 ) N 1 ) )
137 131 134 136 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 ) ) )
138 ovex 
 |-  ( ( 2 x. s ) M 1 ) e. _V
139 ovex 
 |-  ( ( ( 2 x. s ) - 1 ) N 1 ) e. _V
140 138 139 ifex 
 |-  if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 1 ) , ( ( ( 2 x. s ) - 1 ) N 1 ) ) e. _V
141 137 4 140 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 ) ) )
142 109 129 141 sylancl 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s P 1 ) = if ( s <_ ( 1 / 2 ) , ( ( 2 x. s ) M 1 ) , ( ( ( 2 x. s ) - 1 ) N 1 ) ) )
143 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 ) ) ) )
144 128 142 143 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s P 1 ) = ( ( H ( *p ` J ) K ) ` s ) )
145 9 14 5 phtpyi 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 0 M s ) = ( F ` 0 ) /\ ( 1 M s ) = ( F ` 1 ) ) )
146 145 simpld 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 M s ) = ( F ` 0 ) )
147 simpl 
 |-  ( ( x = 0 /\ y = s ) -> x = 0 )
148 147 29 eqbrtrdi 
 |-  ( ( x = 0 /\ y = s ) -> x <_ ( 1 / 2 ) )
149 148 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 ) )
150 147 oveq2d 
 |-  ( ( x = 0 /\ y = s ) -> ( 2 x. x ) = ( 2 x. 0 ) )
151 2t0e0 
 |-  ( 2 x. 0 ) = 0
152 150 151 eqtrdi 
 |-  ( ( x = 0 /\ y = s ) -> ( 2 x. x ) = 0 )
153 simpr 
 |-  ( ( x = 0 /\ y = s ) -> y = s )
154 152 153 oveq12d 
 |-  ( ( x = 0 /\ y = s ) -> ( ( 2 x. x ) M y ) = ( 0 M s ) )
155 149 154 eqtrd 
 |-  ( ( x = 0 /\ y = s ) -> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) = ( 0 M s ) )
156 ovex 
 |-  ( 0 M s ) e. _V
157 155 4 156 ovmpoa 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( 0 P s ) = ( 0 M s ) )
158 110 109 157 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 P s ) = ( 0 M s ) )
159 9 12 pco0 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` 0 ) )
160 159 adantr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` 0 ) = ( F ` 0 ) )
161 146 158 160 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 P s ) = ( ( F ( *p ` J ) G ) ` 0 ) )
162 12 15 6 phtpyi 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 0 N s ) = ( G ` 0 ) /\ ( 1 N s ) = ( G ` 1 ) ) )
163 162 simprd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 N s ) = ( G ` 1 ) )
164 28 30 ltnlei 
 |-  ( ( 1 / 2 ) < 1 <-> -. 1 <_ ( 1 / 2 ) )
165 31 164 mpbi 
 |-  -. 1 <_ ( 1 / 2 )
166 simpl 
 |-  ( ( x = 1 /\ y = s ) -> x = 1 )
167 166 breq1d 
 |-  ( ( x = 1 /\ y = s ) -> ( x <_ ( 1 / 2 ) <-> 1 <_ ( 1 / 2 ) ) )
168 165 167 mtbiri 
 |-  ( ( x = 1 /\ y = s ) -> -. x <_ ( 1 / 2 ) )
169 168 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 ) )
170 166 oveq2d 
 |-  ( ( x = 1 /\ y = s ) -> ( 2 x. x ) = ( 2 x. 1 ) )
171 2t1e2 
 |-  ( 2 x. 1 ) = 2
172 170 171 eqtrdi 
 |-  ( ( x = 1 /\ y = s ) -> ( 2 x. x ) = 2 )
173 172 oveq1d 
 |-  ( ( x = 1 /\ y = s ) -> ( ( 2 x. x ) - 1 ) = ( 2 - 1 ) )
174 2m1e1 
 |-  ( 2 - 1 ) = 1
175 173 174 eqtrdi 
 |-  ( ( x = 1 /\ y = s ) -> ( ( 2 x. x ) - 1 ) = 1 )
176 simpr 
 |-  ( ( x = 1 /\ y = s ) -> y = s )
177 175 176 oveq12d 
 |-  ( ( x = 1 /\ y = s ) -> ( ( ( 2 x. x ) - 1 ) N y ) = ( 1 N s ) )
178 169 177 eqtrd 
 |-  ( ( x = 1 /\ y = s ) -> if ( x <_ ( 1 / 2 ) , ( ( 2 x. x ) M y ) , ( ( ( 2 x. x ) - 1 ) N y ) ) = ( 1 N s ) )
179 ovex 
 |-  ( 1 N s ) e. _V
180 178 4 179 ovmpoa 
 |-  ( ( 1 e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( 1 P s ) = ( 1 N s ) )
181 129 109 180 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 P s ) = ( 1 N s ) )
182 9 12 pco1 
 |-  ( ph -> ( ( F ( *p ` J ) G ) ` 1 ) = ( G ` 1 ) )
183 182 adantr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` 1 ) = ( G ` 1 ) )
184 163 181 183 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 P s ) = ( ( F ( *p ` J ) G ) ` 1 ) )
185 13 21 87 125 144 161 184 isphtpy2d 
 |-  ( ph -> P e. ( ( F ( *p ` J ) G ) ( PHtpy ` J ) ( H ( *p ` J ) K ) ) )