Theorem phtpcco2

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

	Ref	Expression
Hypotheses	phtpcco2.f	⊢ ( 𝜑 → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 )
	phtpcco2.p	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	phtpcco2	⊢ ( 𝜑 → ( 𝑃 ∘ 𝐹 ) ( ≃ph ‘ 𝐾 ) ( 𝑃 ∘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		phtpcco2.f	⊢ ( 𝜑 → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 )
2		phtpcco2.p	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
3		isphtpc	⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )
4	1 3	sylib	⊢ ( 𝜑 → ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )
5	4	simp1d	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
6		cnco	⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝑃 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑃 ∘ 𝐹 ) ∈ ( II Cn 𝐾 ) )
7	5 2 6	syl2anc	⊢ ( 𝜑 → ( 𝑃 ∘ 𝐹 ) ∈ ( II Cn 𝐾 ) )
8	4	simp2d	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
9		cnco	⊢ ( ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝑃 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑃 ∘ 𝐺 ) ∈ ( II Cn 𝐾 ) )
10	8 2 9	syl2anc	⊢ ( 𝜑 → ( 𝑃 ∘ 𝐺 ) ∈ ( II Cn 𝐾 ) )
11	4	simp3d	⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ )
12		n0	⊢ ( ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
13	11 12	sylib	⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
14	5	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → 𝐹 ∈ ( II Cn 𝐽 ) )
15	8	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → 𝐺 ∈ ( II Cn 𝐽 ) )
16	2	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
18	14 15 16 17	phtpyco2	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → ( 𝑃 ∘ 𝑓 ) ∈ ( ( 𝑃 ∘ 𝐹 ) ( PHtpy ‘ 𝐾 ) ( 𝑃 ∘ 𝐺 ) ) )
19	18	ne0d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → ( ( 𝑃 ∘ 𝐹 ) ( PHtpy ‘ 𝐾 ) ( 𝑃 ∘ 𝐺 ) ) ≠ ∅ )
20	13 19	exlimddv	⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝐹 ) ( PHtpy ‘ 𝐾 ) ( 𝑃 ∘ 𝐺 ) ) ≠ ∅ )
21		isphtpc	⊢ ( ( 𝑃 ∘ 𝐹 ) ( ≃ph ‘ 𝐾 ) ( 𝑃 ∘ 𝐺 ) ↔ ( ( 𝑃 ∘ 𝐹 ) ∈ ( II Cn 𝐾 ) ∧ ( 𝑃 ∘ 𝐺 ) ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ( PHtpy ‘ 𝐾 ) ( 𝑃 ∘ 𝐺 ) ) ≠ ∅ ) )
22	7 10 20 21	syl3anbrc	⊢ ( 𝜑 → ( 𝑃 ∘ 𝐹 ) ( ≃ph ‘ 𝐾 ) ( 𝑃 ∘ 𝐺 ) )