Metamath Proof Explorer

Theorem isphtpy

Description: Membership in the class of path homotopies between two continuous functions. (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 ) )
Assertion isphtpy 
|- ( ph -> ( H e. ( F ( PHtpy ` J ) G ) <-> ( H e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isphtpy.2 
 |-  ( ph -> F e. ( II Cn J ) )
2 isphtpy.3 
 |-  ( ph -> G e. ( II Cn J ) )
3 cntop2 
 |-  ( F e. ( II Cn J ) -> J e. Top )
4 oveq2 
 |-  ( j = J -> ( II Cn j ) = ( II Cn J ) )
5 oveq2 
 |-  ( j = J -> ( II Htpy j ) = ( II Htpy J ) )
6 5 oveqd 
 |-  ( j = J -> ( f ( II Htpy j ) g ) = ( f ( II Htpy J ) g ) )
7 6 rabeqdv 
 |-  ( j = J -> { h e. ( f ( II Htpy j ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } = { h e. ( f ( II Htpy J ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } )
8 4 4 7 mpoeq123dv 
 |-  ( j = J -> ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> { h e. ( f ( II Htpy j ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> { h e. ( f ( II Htpy J ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )
9 df-phtpy 
 |-  PHtpy = ( j e. Top |-> ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> { h e. ( f ( II Htpy j ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )
10 ovex 
 |-  ( II Cn J ) e. _V
11 10 10 mpoex 
 |-  ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> { h e. ( f ( II Htpy J ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) e. _V
12 8 9 11 fvmpt 
 |-  ( J e. Top -> ( PHtpy ` J ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> { h e. ( f ( II Htpy J ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )
13 1 3 12 3syl 
 |-  ( ph -> ( PHtpy ` J ) = ( f e. ( II Cn J ) , g e. ( II Cn J ) |-> { h e. ( f ( II Htpy J ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )
14 oveq12 
 |-  ( ( f = F /\ g = G ) -> ( f ( II Htpy J ) g ) = ( F ( II Htpy J ) G ) )
15 simpl 
 |-  ( ( f = F /\ g = G ) -> f = F )
16 15 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` 0 ) = ( F ` 0 ) )
17 16 eqeq2d 
 |-  ( ( f = F /\ g = G ) -> ( ( 0 h s ) = ( f ` 0 ) <-> ( 0 h s ) = ( F ` 0 ) ) )
18 15 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` 1 ) = ( F ` 1 ) )
19 18 eqeq2d 
 |-  ( ( f = F /\ g = G ) -> ( ( 1 h s ) = ( f ` 1 ) <-> ( 1 h s ) = ( F ` 1 ) ) )
20 17 19 anbi12d 
 |-  ( ( f = F /\ g = G ) -> ( ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) <-> ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) ) )
21 20 ralbidv 
 |-  ( ( f = F /\ g = G ) -> ( A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) <-> A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) ) )
22 14 21 rabeqbidv 
 |-  ( ( f = F /\ g = G ) -> { h e. ( f ( II Htpy J ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } = { h e. ( F ( II Htpy J ) G ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) } )
23 22 adantl 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> { h e. ( f ( II Htpy J ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } = { h e. ( F ( II Htpy J ) G ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) } )
24 ovex 
 |-  ( F ( II Htpy J ) G ) e. _V
25 24 rabex 
 |-  { h e. ( F ( II Htpy J ) G ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) } e. _V
26 25 a1i 
 |-  ( ph -> { h e. ( F ( II Htpy J ) G ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) } e. _V )
27 13 23 1 2 26 ovmpod 
 |-  ( ph -> ( F ( PHtpy ` J ) G ) = { h e. ( F ( II Htpy J ) G ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) } )
28 27 eleq2d 
 |-  ( ph -> ( H e. ( F ( PHtpy ` J ) G ) <-> H e. { h e. ( F ( II Htpy J ) G ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) } ) )
29 oveq 
 |-  ( h = H -> ( 0 h s ) = ( 0 H s ) )
30 29 eqeq1d 
 |-  ( h = H -> ( ( 0 h s ) = ( F ` 0 ) <-> ( 0 H s ) = ( F ` 0 ) ) )
31 oveq 
 |-  ( h = H -> ( 1 h s ) = ( 1 H s ) )
32 31 eqeq1d 
 |-  ( h = H -> ( ( 1 h s ) = ( F ` 1 ) <-> ( 1 H s ) = ( F ` 1 ) ) )
33 30 32 anbi12d 
 |-  ( h = H -> ( ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) <-> ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) )
34 33 ralbidv 
 |-  ( h = H -> ( A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) <-> A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) )
35 34 elrab 
 |-  ( H e. { h e. ( F ( II Htpy J ) G ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) } <-> ( H e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) )
36 28 35 bitrdi 
 |-  ( ph -> ( H e. ( F ( PHtpy ` J ) G ) <-> ( H e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) ) )