Metamath Proof Explorer

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 ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) )