Metamath Proof Explorer

Theorem phtpycc

Description: Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 7-Jun-2014)

Ref Expression
Hypotheses phtpycc.1 
|- M = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( x K ( 2 x. y ) ) , ( x L ( ( 2 x. y ) - 1 ) ) ) )
phtpycc.3 
|- ( ph -> F e. ( II Cn J ) )
phtpycc.4 
|- ( ph -> G e. ( II Cn J ) )
phtpycc.5 
|- ( ph -> H e. ( II Cn J ) )
phtpycc.6 
|- ( ph -> K e. ( F ( PHtpy ` J ) G ) )
phtpycc.7 
|- ( ph -> L e. ( G ( PHtpy ` J ) H ) )
Assertion phtpycc 
|- ( ph -> M e. ( F ( PHtpy ` J ) H ) )

Proof

Step Hyp Ref Expression
1 phtpycc.1 
 |-  M = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( x K ( 2 x. y ) ) , ( x L ( ( 2 x. y ) - 1 ) ) ) )
2 phtpycc.3 
 |-  ( ph -> F e. ( II Cn J ) )
3 phtpycc.4 
 |-  ( ph -> G e. ( II Cn J ) )
4 phtpycc.5 
 |-  ( ph -> H e. ( II Cn J ) )
5 phtpycc.6 
 |-  ( ph -> K e. ( F ( PHtpy ` J ) G ) )
6 phtpycc.7 
 |-  ( ph -> L e. ( G ( PHtpy ` J ) H ) )
7 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
8 7 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
9 2 3 phtpyhtpy 
 |-  ( ph -> ( F ( PHtpy ` J ) G ) C_ ( F ( II Htpy J ) G ) )
10 9 5 sseldd 
 |-  ( ph -> K e. ( F ( II Htpy J ) G ) )
11 3 4 phtpyhtpy 
 |-  ( ph -> ( G ( PHtpy ` J ) H ) C_ ( G ( II Htpy J ) H ) )
12 11 6 sseldd 
 |-  ( ph -> L e. ( G ( II Htpy J ) H ) )
13 1 8 2 3 4 10 12 htpycc 
 |-  ( ph -> M e. ( F ( II Htpy J ) H ) )
14 0elunit 
 |-  0 e. ( 0 [,] 1 )
15 simpr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> s e. ( 0 [,] 1 ) )
16 simpr 
 |-  ( ( x = 0 /\ y = s ) -> y = s )
17 16 breq1d 
 |-  ( ( x = 0 /\ y = s ) -> ( y <_ ( 1 / 2 ) <-> s <_ ( 1 / 2 ) ) )
18 simpl 
 |-  ( ( x = 0 /\ y = s ) -> x = 0 )
19 16 oveq2d 
 |-  ( ( x = 0 /\ y = s ) -> ( 2 x. y ) = ( 2 x. s ) )
20 18 19 oveq12d 
 |-  ( ( x = 0 /\ y = s ) -> ( x K ( 2 x. y ) ) = ( 0 K ( 2 x. s ) ) )
21 19 oveq1d 
 |-  ( ( x = 0 /\ y = s ) -> ( ( 2 x. y ) - 1 ) = ( ( 2 x. s ) - 1 ) )
22 18 21 oveq12d 
 |-  ( ( x = 0 /\ y = s ) -> ( x L ( ( 2 x. y ) - 1 ) ) = ( 0 L ( ( 2 x. s ) - 1 ) ) )
23 17 20 22 ifbieq12d 
 |-  ( ( x = 0 /\ y = s ) -> if ( y <_ ( 1 / 2 ) , ( x K ( 2 x. y ) ) , ( x L ( ( 2 x. y ) - 1 ) ) ) = if ( s <_ ( 1 / 2 ) , ( 0 K ( 2 x. s ) ) , ( 0 L ( ( 2 x. s ) - 1 ) ) ) )
24 ovex 
 |-  ( 0 K ( 2 x. s ) ) e. _V
25 ovex 
 |-  ( 0 L ( ( 2 x. s ) - 1 ) ) e. _V
26 24 25 ifex 
 |-  if ( s <_ ( 1 / 2 ) , ( 0 K ( 2 x. s ) ) , ( 0 L ( ( 2 x. s ) - 1 ) ) ) e. _V
27 23 1 26 ovmpoa 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( 0 M s ) = if ( s <_ ( 1 / 2 ) , ( 0 K ( 2 x. s ) ) , ( 0 L ( ( 2 x. s ) - 1 ) ) ) )
28 14 15 27 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 M s ) = if ( s <_ ( 1 / 2 ) , ( 0 K ( 2 x. s ) ) , ( 0 L ( ( 2 x. s ) - 1 ) ) ) )
29 simpll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ph )
30 elii1 
 |-  ( s e. ( 0 [,] ( 1 / 2 ) ) <-> ( s e. ( 0 [,] 1 ) /\ s <_ ( 1 / 2 ) ) )
31 iihalf1 
 |-  ( s e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
32 30 31 sylbir 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s <_ ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
33 32 adantll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( 2 x. s ) e. ( 0 [,] 1 ) )
34 2 3 5 phtpyi 
 |-  ( ( ph /\ ( 2 x. s ) e. ( 0 [,] 1 ) ) -> ( ( 0 K ( 2 x. s ) ) = ( F ` 0 ) /\ ( 1 K ( 2 x. s ) ) = ( F ` 1 ) ) )
35 29 33 34 syl2anc 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( ( 0 K ( 2 x. s ) ) = ( F ` 0 ) /\ ( 1 K ( 2 x. s ) ) = ( F ` 1 ) ) )
36 35 simpld 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( 0 K ( 2 x. s ) ) = ( F ` 0 ) )
37 simpll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ph )
38 elii2 
 |-  ( ( s e. ( 0 [,] 1 ) /\ -. s <_ ( 1 / 2 ) ) -> s e. ( ( 1 / 2 ) [,] 1 ) )
39 iihalf2 
 |-  ( s e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) )
40 38 39 syl 
 |-  ( ( s e. ( 0 [,] 1 ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) )
41 40 adantll 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) )
42 3 4 6 phtpyi 
 |-  ( ( ph /\ ( ( 2 x. s ) - 1 ) e. ( 0 [,] 1 ) ) -> ( ( 0 L ( ( 2 x. s ) - 1 ) ) = ( G ` 0 ) /\ ( 1 L ( ( 2 x. s ) - 1 ) ) = ( G ` 1 ) ) )
43 37 41 42 syl2anc 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( 0 L ( ( 2 x. s ) - 1 ) ) = ( G ` 0 ) /\ ( 1 L ( ( 2 x. s ) - 1 ) ) = ( G ` 1 ) ) )
44 43 simpld 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( 0 L ( ( 2 x. s ) - 1 ) ) = ( G ` 0 ) )
45 2 3 5 phtpy01 
 |-  ( ph -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
46 45 ad2antrr 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
47 46 simpld 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( F ` 0 ) = ( G ` 0 ) )
48 44 47 eqtr4d 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( 0 L ( ( 2 x. s ) - 1 ) ) = ( F ` 0 ) )
49 36 48 ifeqda 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> if ( s <_ ( 1 / 2 ) , ( 0 K ( 2 x. s ) ) , ( 0 L ( ( 2 x. s ) - 1 ) ) ) = ( F ` 0 ) )
50 28 49 eqtrd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 M s ) = ( F ` 0 ) )
51 1elunit 
 |-  1 e. ( 0 [,] 1 )
52 simpr 
 |-  ( ( x = 1 /\ y = s ) -> y = s )
53 52 breq1d 
 |-  ( ( x = 1 /\ y = s ) -> ( y <_ ( 1 / 2 ) <-> s <_ ( 1 / 2 ) ) )
54 simpl 
 |-  ( ( x = 1 /\ y = s ) -> x = 1 )
55 52 oveq2d 
 |-  ( ( x = 1 /\ y = s ) -> ( 2 x. y ) = ( 2 x. s ) )
56 54 55 oveq12d 
 |-  ( ( x = 1 /\ y = s ) -> ( x K ( 2 x. y ) ) = ( 1 K ( 2 x. s ) ) )
57 55 oveq1d 
 |-  ( ( x = 1 /\ y = s ) -> ( ( 2 x. y ) - 1 ) = ( ( 2 x. s ) - 1 ) )
58 54 57 oveq12d 
 |-  ( ( x = 1 /\ y = s ) -> ( x L ( ( 2 x. y ) - 1 ) ) = ( 1 L ( ( 2 x. s ) - 1 ) ) )
59 53 56 58 ifbieq12d 
 |-  ( ( x = 1 /\ y = s ) -> if ( y <_ ( 1 / 2 ) , ( x K ( 2 x. y ) ) , ( x L ( ( 2 x. y ) - 1 ) ) ) = if ( s <_ ( 1 / 2 ) , ( 1 K ( 2 x. s ) ) , ( 1 L ( ( 2 x. s ) - 1 ) ) ) )
60 ovex 
 |-  ( 1 K ( 2 x. s ) ) e. _V
61 ovex 
 |-  ( 1 L ( ( 2 x. s ) - 1 ) ) e. _V
62 60 61 ifex 
 |-  if ( s <_ ( 1 / 2 ) , ( 1 K ( 2 x. s ) ) , ( 1 L ( ( 2 x. s ) - 1 ) ) ) e. _V
63 59 1 62 ovmpoa 
 |-  ( ( 1 e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( 1 M s ) = if ( s <_ ( 1 / 2 ) , ( 1 K ( 2 x. s ) ) , ( 1 L ( ( 2 x. s ) - 1 ) ) ) )
64 51 15 63 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 M s ) = if ( s <_ ( 1 / 2 ) , ( 1 K ( 2 x. s ) ) , ( 1 L ( ( 2 x. s ) - 1 ) ) ) )
65 35 simprd 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ s <_ ( 1 / 2 ) ) -> ( 1 K ( 2 x. s ) ) = ( F ` 1 ) )
66 43 simprd 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( 1 L ( ( 2 x. s ) - 1 ) ) = ( G ` 1 ) )
67 46 simprd 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( F ` 1 ) = ( G ` 1 ) )
68 66 67 eqtr4d 
 |-  ( ( ( ph /\ s e. ( 0 [,] 1 ) ) /\ -. s <_ ( 1 / 2 ) ) -> ( 1 L ( ( 2 x. s ) - 1 ) ) = ( F ` 1 ) )
69 65 68 ifeqda 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> if ( s <_ ( 1 / 2 ) , ( 1 K ( 2 x. s ) ) , ( 1 L ( ( 2 x. s ) - 1 ) ) ) = ( F ` 1 ) )
70 64 69 eqtrd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 M s ) = ( F ` 1 ) )
71 2 4 13 50 70 isphtpyd 
 |-  ( ph -> M e. ( F ( PHtpy ` J ) H ) )