Metamath Proof Explorer

Theorem phtpcco2

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

Ref Expression
Hypotheses phtpcco2.f 
|- ( ph -> F ( ~=ph ` J ) G )
phtpcco2.p 
|- ( ph -> P e. ( J Cn K ) )
Assertion phtpcco2 
|- ( ph -> ( P o. F ) ( ~=ph ` K ) ( P o. G ) )

Proof

Step Hyp Ref Expression
1 phtpcco2.f 
 |-  ( ph -> F ( ~=ph ` J ) G )
2 phtpcco2.p 
 |-  ( ph -> P e. ( J Cn K ) )
3 isphtpc 
 |-  ( F ( ~=ph ` J ) G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )
4 1 3 sylib 
 |-  ( ph -> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )
5 4 simp1d 
 |-  ( ph -> F e. ( II Cn J ) )
6 cnco 
 |-  ( ( F e. ( II Cn J ) /\ P e. ( J Cn K ) ) -> ( P o. F ) e. ( II Cn K ) )
7 5 2 6 syl2anc 
 |-  ( ph -> ( P o. F ) e. ( II Cn K ) )
8 4 simp2d 
 |-  ( ph -> G e. ( II Cn J ) )
9 cnco 
 |-  ( ( G e. ( II Cn J ) /\ P e. ( J Cn K ) ) -> ( P o. G ) e. ( II Cn K ) )
10 8 2 9 syl2anc 
 |-  ( ph -> ( P o. G ) e. ( II Cn K ) )
11 4 simp3d 
 |-  ( ph -> ( F ( PHtpy ` J ) G ) =/= (/) )
12 n0 
 |-  ( ( F ( PHtpy ` J ) G ) =/= (/) <-> E. f f e. ( F ( PHtpy ` J ) G ) )
13 11 12 sylib 
 |-  ( ph -> E. f f e. ( F ( PHtpy ` J ) G ) )
14 5 adantr 
 |-  ( ( ph /\ f e. ( F ( PHtpy ` J ) G ) ) -> F e. ( II Cn J ) )
15 8 adantr 
 |-  ( ( ph /\ f e. ( F ( PHtpy ` J ) G ) ) -> G e. ( II Cn J ) )
16 2 adantr 
 |-  ( ( ph /\ f e. ( F ( PHtpy ` J ) G ) ) -> P e. ( J Cn K ) )
17 simpr 
 |-  ( ( ph /\ f e. ( F ( PHtpy ` J ) G ) ) -> f e. ( F ( PHtpy ` J ) G ) )
18 14 15 16 17 phtpyco2 
 |-  ( ( ph /\ f e. ( F ( PHtpy ` J ) G ) ) -> ( P o. f ) e. ( ( P o. F ) ( PHtpy ` K ) ( P o. G ) ) )
19 18 ne0d 
 |-  ( ( ph /\ f e. ( F ( PHtpy ` J ) G ) ) -> ( ( P o. F ) ( PHtpy ` K ) ( P o. G ) ) =/= (/) )
20 13 19 exlimddv 
 |-  ( ph -> ( ( P o. F ) ( PHtpy ` K ) ( P o. G ) ) =/= (/) )
21 isphtpc 
 |-  ( ( P o. F ) ( ~=ph ` K ) ( P o. G ) <-> ( ( P o. F ) e. ( II Cn K ) /\ ( P o. G ) e. ( II Cn K ) /\ ( ( P o. F ) ( PHtpy ` K ) ( P o. G ) ) =/= (/) ) )
22 7 10 20 21 syl3anbrc 
 |-  ( ph -> ( P o. F ) ( ~=ph ` K ) ( P o. G ) )