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 φ F II Cn J
isphtpy.3 φ G II Cn J
Assertion isphtpy φ H F PHtpy J G H F II Htpy J G s 0 1 0 H s = F 0 1 H s = F 1

Proof

Step Hyp Ref Expression
1 isphtpy.2 φ F II Cn J
2 isphtpy.3 φ G II Cn J
3 cntop2 F II Cn J J 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 f II Htpy j g | s 0 1 0 h s = f 0 1 h s = f 1 = h f II Htpy J g | s 0 1 0 h s = f 0 1 h s = f 1
8 4 4 7 mpoeq123dv j = J f II Cn j , g II Cn j h f II Htpy j g | s 0 1 0 h s = f 0 1 h s = f 1 = f II Cn J , g II Cn J h f II Htpy J g | s 0 1 0 h s = f 0 1 h s = f 1
9 df-phtpy PHtpy = j Top f II Cn j , g II Cn j h f II Htpy j g | s 0 1 0 h s = f 0 1 h s = f 1
10 ovex II Cn J V
11 10 10 mpoex f II Cn J , g II Cn J h f II Htpy J g | s 0 1 0 h s = f 0 1 h s = f 1 V
12 8 9 11 fvmpt J Top PHtpy J = f II Cn J , g II Cn J h f II Htpy J g | s 0 1 0 h s = f 0 1 h s = f 1
13 1 3 12 3syl φ PHtpy J = f II Cn J , g II Cn J h f II Htpy J g | s 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 s 0 1 0 h s = f 0 1 h s = f 1 s 0 1 0 h s = F 0 1 h s = F 1
22 14 21 rabeqbidv f = F g = G h f II Htpy J g | s 0 1 0 h s = f 0 1 h s = f 1 = h F II Htpy J G | s 0 1 0 h s = F 0 1 h s = F 1
23 22 adantl φ f = F g = G h f II Htpy J g | s 0 1 0 h s = f 0 1 h s = f 1 = h F II Htpy J G | s 0 1 0 h s = F 0 1 h s = F 1
24 ovex F II Htpy J G V
25 24 rabex h F II Htpy J G | s 0 1 0 h s = F 0 1 h s = F 1 V
26 25 a1i φ h F II Htpy J G | s 0 1 0 h s = F 0 1 h s = F 1 V
27 13 23 1 2 26 ovmpod φ F PHtpy J G = h F II Htpy J G | s 0 1 0 h s = F 0 1 h s = F 1
28 27 eleq2d φ H F PHtpy J G H h F II Htpy J G | s 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 s 0 1 0 h s = F 0 1 h s = F 1 s 0 1 0 H s = F 0 1 H s = F 1
35 34 elrab H h F II Htpy J G | s 0 1 0 h s = F 0 1 h s = F 1 H F II Htpy J G s 0 1 0 H s = F 0 1 H s = F 1
36 28 35 bitrdi φ H F PHtpy J G H F II Htpy J G s 0 1 0 H s = F 0 1 H s = F 1