# 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 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
phtpyco2.g ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
phtpyco2.p ${⊢}{\phi }\to {P}\in \left({J}\mathrm{Cn}{K}\right)$
phtpyco2.h ${⊢}{\phi }\to {H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)$
Assertion phtpyco2 ${⊢}{\phi }\to {P}\circ {H}\in \left(\left({P}\circ {F}\right)\mathrm{PHtpy}\left({K}\right)\left({P}\circ {G}\right)\right)$

### Proof

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