Metamath Proof Explorer

Theorem phtpycom

Description: Given a homotopy from F to G , produce a homotopy from G to F . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses isphtpy.2 
|- ( ph -> F e. ( II Cn J ) )
isphtpy.3 
|- ( ph -> G e. ( II Cn J ) )
phtpycom.6 
|- K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) )
phtpycom.7 
|- ( ph -> H e. ( F ( PHtpy ` J ) G ) )
Assertion phtpycom 
|- ( ph -> K e. ( G ( PHtpy ` J ) F ) )

Proof

Step Hyp Ref Expression
1 isphtpy.2 
 |-  ( ph -> F e. ( II Cn J ) )
2 isphtpy.3 
 |-  ( ph -> G e. ( II Cn J ) )
3 phtpycom.6 
 |-  K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) )
4 phtpycom.7 
 |-  ( ph -> H e. ( F ( PHtpy ` J ) G ) )
5 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
6 5 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
7 1 2 phtpyhtpy 
 |-  ( ph -> ( F ( PHtpy ` J ) G ) C_ ( F ( II Htpy J ) G ) )
8 7 4 sseldd 
 |-  ( ph -> H e. ( F ( II Htpy J ) G ) )
9 6 1 2 3 8 htpycom 
 |-  ( ph -> K e. ( G ( II Htpy J ) F ) )
10 0elunit 
 |-  0 e. ( 0 [,] 1 )
11 simpr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> t e. ( 0 [,] 1 ) )
12 oveq1 
 |-  ( x = 0 -> ( x H ( 1 - y ) ) = ( 0 H ( 1 - y ) ) )
13 oveq2 
 |-  ( y = t -> ( 1 - y ) = ( 1 - t ) )
14 13 oveq2d 
 |-  ( y = t -> ( 0 H ( 1 - y ) ) = ( 0 H ( 1 - t ) ) )
15 ovex 
 |-  ( 0 H ( 1 - t ) ) e. _V
16 12 14 3 15 ovmpo 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ t e. ( 0 [,] 1 ) ) -> ( 0 K t ) = ( 0 H ( 1 - t ) ) )
17 10 11 16 sylancr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( 0 K t ) = ( 0 H ( 1 - t ) ) )
18 iirev 
 |-  ( t e. ( 0 [,] 1 ) -> ( 1 - t ) e. ( 0 [,] 1 ) )
19 1 2 4 phtpyi 
 |-  ( ( ph /\ ( 1 - t ) e. ( 0 [,] 1 ) ) -> ( ( 0 H ( 1 - t ) ) = ( F ` 0 ) /\ ( 1 H ( 1 - t ) ) = ( F ` 1 ) ) )
20 18 19 sylan2 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( 0 H ( 1 - t ) ) = ( F ` 0 ) /\ ( 1 H ( 1 - t ) ) = ( F ` 1 ) ) )
21 20 simpld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( 0 H ( 1 - t ) ) = ( F ` 0 ) )
22 1 2 4 phtpy01 
 |-  ( ph -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
23 22 adantr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
24 23 simpld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( F ` 0 ) = ( G ` 0 ) )
25 17 21 24 3eqtrd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( 0 K t ) = ( G ` 0 ) )
26 1elunit 
 |-  1 e. ( 0 [,] 1 )
27 oveq1 
 |-  ( x = 1 -> ( x H ( 1 - y ) ) = ( 1 H ( 1 - y ) ) )
28 13 oveq2d 
 |-  ( y = t -> ( 1 H ( 1 - y ) ) = ( 1 H ( 1 - t ) ) )
29 ovex 
 |-  ( 1 H ( 1 - t ) ) e. _V
30 27 28 3 29 ovmpo 
 |-  ( ( 1 e. ( 0 [,] 1 ) /\ t e. ( 0 [,] 1 ) ) -> ( 1 K t ) = ( 1 H ( 1 - t ) ) )
31 26 11 30 sylancr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( 1 K t ) = ( 1 H ( 1 - t ) ) )
32 20 simprd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( 1 H ( 1 - t ) ) = ( F ` 1 ) )
33 23 simprd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( F ` 1 ) = ( G ` 1 ) )
34 31 32 33 3eqtrd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( 1 K t ) = ( G ` 1 ) )
35 2 1 9 25 34 isphtpyd 
 |-  ( ph -> K e. ( G ( PHtpy ` J ) F ) )