Theorem pcohtpy

Description: Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	pcohtpy.4	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
	pcohtpy.5	⊢ ( 𝜑 → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐻 )
	pcohtpy.6	⊢ ( 𝜑 → 𝐺 ( ≃ph ‘ 𝐽 ) 𝐾 )
Assertion	pcohtpy	⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		pcohtpy.4	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
2		pcohtpy.5	⊢ ( 𝜑 → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐻 )
3		pcohtpy.6	⊢ ( 𝜑 → 𝐺 ( ≃ph ‘ 𝐽 ) 𝐾 )
4		isphtpc	⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐻 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ ) )
5	2 4	sylib	⊢ ( 𝜑 → ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ ) )
6	5	simp1d	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
7		isphtpc	⊢ ( 𝐺 ( ≃ph ‘ 𝐽 ) 𝐾 ↔ ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝐾 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ≠ ∅ ) )
8	3 7	sylib	⊢ ( 𝜑 → ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝐾 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ≠ ∅ ) )
9	8	simp1d	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
10	6 9 1	pcocn	⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ∈ ( II Cn 𝐽 ) )
11	5	simp2d	⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐽 ) )
12	8	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ( II Cn 𝐽 ) )
13		phtpc01	⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐻 → ( ( 𝐹 ‘ 0 ) = ( 𝐻 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐻 ‘ 1 ) ) )
14	2 13	syl	⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) = ( 𝐻 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐻 ‘ 1 ) ) )
15	14	simprd	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐻 ‘ 1 ) )
16		phtpc01	⊢ ( 𝐺 ( ≃ph ‘ 𝐽 ) 𝐾 → ( ( 𝐺 ‘ 0 ) = ( 𝐾 ‘ 0 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐾 ‘ 1 ) ) )
17	3 16	syl	⊢ ( 𝜑 → ( ( 𝐺 ‘ 0 ) = ( 𝐾 ‘ 0 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐾 ‘ 1 ) ) )
18	17	simpld	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ( 𝐾 ‘ 0 ) )
19	1 15 18	3eqtr3d	⊢ ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝐾 ‘ 0 ) )
20	11 12 19	pcocn	⊢ ( 𝜑 → ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ∈ ( II Cn 𝐽 ) )
21	5	simp3d	⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ )
22		n0	⊢ ( ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ ↔ ∃ 𝑚 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
23	21 22	sylib	⊢ ( 𝜑 → ∃ 𝑚 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
24	8	simp3d	⊢ ( 𝜑 → ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ≠ ∅ )
25		n0	⊢ ( ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ≠ ∅ ↔ ∃ 𝑛 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) )
26	24 25	sylib	⊢ ( 𝜑 → ∃ 𝑛 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) )
27		exdistrv	⊢ ( ∃ 𝑚 ∃ 𝑛 ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) ↔ ( ∃ 𝑚 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ ∃ 𝑛 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) )
28	23 26 27	sylanbrc	⊢ ( 𝜑 → ∃ 𝑚 ∃ 𝑛 ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) )
29	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) ) → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
30	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) ) → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐻 )
31	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) ) → 𝐺 ( ≃ph ‘ 𝐽 ) 𝐾 )
32		eqid	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑚 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑛 𝑦 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑚 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑛 𝑦 ) ) )
33		simprl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) ) → 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
34		simprr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) ) → 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) )
35	29 30 31 32 33 34	pcohtpylem	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑚 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑛 𝑦 ) ) ) ∈ ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( PHtpy ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ) )
36	35	ne0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( PHtpy ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ) ≠ ∅ )
37	36	ex	⊢ ( 𝜑 → ( ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( PHtpy ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ) ≠ ∅ ) )
38	37	exlimdvv	⊢ ( 𝜑 → ( ∃ 𝑚 ∃ 𝑛 ( 𝑚 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ∧ 𝑛 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( PHtpy ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ) ≠ ∅ ) )
39	28 38	mpd	⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( PHtpy ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ) ≠ ∅ )
40		isphtpc	⊢ ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ↔ ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ∈ ( II Cn 𝐽 ) ∧ ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( PHtpy ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ) ≠ ∅ ) )
41	10 20 39 40	syl3anbrc	⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) )