Metamath Proof Explorer


Theorem phtpyco2

Description: Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses phtpyco2.f φ F II Cn J
phtpyco2.g φ G II Cn J
phtpyco2.p φ P J Cn K
phtpyco2.h φ H F PHtpy J G
Assertion phtpyco2 φ P H P F PHtpy K P G

Proof

Step Hyp Ref Expression
1 phtpyco2.f φ F II Cn J
2 phtpyco2.g φ G II Cn J
3 phtpyco2.p φ P J Cn K
4 phtpyco2.h φ H F PHtpy J G
5 cnco F II Cn J P J Cn K P F II Cn K
6 1 3 5 syl2anc φ P F II Cn K
7 cnco G II Cn J P J Cn K P G II Cn K
8 2 3 7 syl2anc φ P G II Cn K
9 1 2 phtpyhtpy φ F PHtpy J G F II Htpy J G
10 9 4 sseldd φ H F II Htpy J G
11 1 2 3 10 htpyco2 φ P H P F II Htpy K P G
12 1 2 4 phtpyi φ s 0 1 0 H s = F 0 1 H s = F 1
13 12 simpld φ s 0 1 0 H s = F 0
14 13 fveq2d φ s 0 1 P 0 H s = P F 0
15 iitopon II TopOn 0 1
16 txtopon II TopOn 0 1 II TopOn 0 1 II × t II TopOn 0 1 × 0 1
17 15 15 16 mp2an II × t II TopOn 0 1 × 0 1
18 cntop2 F II Cn J J Top
19 1 18 syl φ J Top
20 toptopon2 J Top J TopOn J
21 19 20 sylib φ J TopOn J
22 1 2 phtpycn φ F PHtpy J G II × t II Cn J
23 22 4 sseldd φ H II × t II Cn J
24 cnf2 II × t II TopOn 0 1 × 0 1 J TopOn J H II × t II Cn J H : 0 1 × 0 1 J
25 17 21 23 24 mp3an2i φ H : 0 1 × 0 1 J
26 0elunit 0 0 1
27 simpr φ s 0 1 s 0 1
28 opelxpi 0 0 1 s 0 1 0 s 0 1 × 0 1
29 26 27 28 sylancr φ s 0 1 0 s 0 1 × 0 1
30 fvco3 H : 0 1 × 0 1 J 0 s 0 1 × 0 1 P H 0 s = P H 0 s
31 25 29 30 syl2an2r φ s 0 1 P H 0 s = P H 0 s
32 df-ov 0 P H s = P H 0 s
33 df-ov 0 H s = H 0 s
34 33 fveq2i P 0 H s = P H 0 s
35 31 32 34 3eqtr4g φ s 0 1 0 P H s = P 0 H s
36 iiuni 0 1 = II
37 eqid J = J
38 36 37 cnf F II Cn J F : 0 1 J
39 1 38 syl φ F : 0 1 J
40 39 adantr φ s 0 1 F : 0 1 J
41 fvco3 F : 0 1 J 0 0 1 P F 0 = P F 0
42 40 26 41 sylancl φ s 0 1 P F 0 = P F 0
43 14 35 42 3eqtr4d φ s 0 1 0 P H s = P F 0
44 12 simprd φ s 0 1 1 H s = F 1
45 44 fveq2d φ s 0 1 P 1 H s = P F 1
46 1elunit 1 0 1
47 opelxpi 1 0 1 s 0 1 1 s 0 1 × 0 1
48 46 27 47 sylancr φ s 0 1 1 s 0 1 × 0 1
49 fvco3 H : 0 1 × 0 1 J 1 s 0 1 × 0 1 P H 1 s = P H 1 s
50 25 48 49 syl2an2r φ s 0 1 P H 1 s = P H 1 s
51 df-ov 1 P H s = P H 1 s
52 df-ov 1 H s = H 1 s
53 52 fveq2i P 1 H s = P H 1 s
54 50 51 53 3eqtr4g φ s 0 1 1 P H s = P 1 H s
55 fvco3 F : 0 1 J 1 0 1 P F 1 = P F 1
56 40 46 55 sylancl φ s 0 1 P F 1 = P F 1
57 45 54 56 3eqtr4d φ s 0 1 1 P H s = P F 1
58 6 8 11 43 57 isphtpyd φ P H P F PHtpy K P G