Metamath Proof Explorer

Theorem phtpycc

Description: Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 7-Jun-2014)

Ref Expression
Hypotheses phtpycc.1 ⊢ 𝑀 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐾 ( 2 · 𝑦 ) ) , ( 𝑥 𝐿 ( ( 2 · 𝑦 ) − 1 ) ) ) )
phtpycc.3 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
phtpycc.4 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
phtpycc.5 ⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐽 ) )
phtpycc.6 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
phtpycc.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
Assertion phtpycc ( 𝜑 → 𝑀 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) )

Proof

Step Hyp Ref Expression
1 phtpycc.1 ⊢ 𝑀 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐾 ( 2 · 𝑦 ) ) , ( 𝑥 𝐿 ( ( 2 · 𝑦 ) − 1 ) ) ) )
2 phtpycc.3 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
3 phtpycc.4 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
4 phtpycc.5 ⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐽 ) )
5 phtpycc.6 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
6 phtpycc.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
7 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
8 7 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
9 2 3 phtpyhtpy ⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ⊆ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
10 9 5 sseldd ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
11 3 4 phtpyhtpy ⊢ ( 𝜑 → ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ⊆ ( 𝐺 ( II Htpy 𝐽 ) 𝐻 ) )
12 11 6 sseldd ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐺 ( II Htpy 𝐽 ) 𝐻 ) )
13 1 8 2 3 4 10 12 htpycc ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐻 ) )
14 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑠 ∈ ( 0 [,] 1 ) )
16 simpr ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → 𝑦 = 𝑠 )
17 16 breq1d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( 𝑦 ≤ ( 1 / 2 ) ↔ 𝑠 ≤ ( 1 / 2 ) ) )
18 simpl ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → 𝑥 = 0 )
19 16 oveq2d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( 2 · 𝑦 ) = ( 2 · 𝑠 ) )
20 18 19 oveq12d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( 𝑥 𝐾 ( 2 · 𝑦 ) ) = ( 0 𝐾 ( 2 · 𝑠 ) ) )
21 19 oveq1d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( ( 2 · 𝑦 ) − 1 ) = ( ( 2 · 𝑠 ) − 1 ) )
22 18 21 oveq12d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( 𝑥 𝐿 ( ( 2 · 𝑦 ) − 1 ) ) = ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) )
23 17 20 22 ifbieq12d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐾 ( 2 · 𝑦 ) ) , ( 𝑥 𝐿 ( ( 2 · 𝑦 ) − 1 ) ) ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 0 𝐾 ( 2 · 𝑠 ) ) , ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) )
24 ovex ⊢ ( 0 𝐾 ( 2 · 𝑠 ) ) ∈ V
25 ovex ⊢ ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ∈ V
26 24 25 ifex ⊢ if ( 𝑠 ≤ ( 1 / 2 ) , ( 0 𝐾 ( 2 · 𝑠 ) ) , ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) ∈ V
27 23 1 26 ovmpoa ⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝑀 𝑠 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 0 𝐾 ( 2 · 𝑠 ) ) , ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) )
28 14 15 27 sylancr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝑀 𝑠 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 0 𝐾 ( 2 · 𝑠 ) ) , ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) )
29 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → 𝜑 )
30 elii1 ⊢ ( 𝑠 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≤ ( 1 / 2 ) ) )
31 iihalf1 ⊢ ( 𝑠 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑠 ) ∈ ( 0 [,] 1 ) )
32 30 31 sylbir ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( 2 · 𝑠 ) ∈ ( 0 [,] 1 ) )
33 32 adantll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( 2 · 𝑠 ) ∈ ( 0 [,] 1 ) )
34 2 3 5 phtpyi ⊢ ( ( 𝜑 ∧ ( 2 · 𝑠 ) ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐾 ( 2 · 𝑠 ) ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐾 ( 2 · 𝑠 ) ) = ( 𝐹 ‘ 1 ) ) )
35 29 33 34 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( ( 0 𝐾 ( 2 · 𝑠 ) ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐾 ( 2 · 𝑠 ) ) = ( 𝐹 ‘ 1 ) ) )
36 35 simpld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( 0 𝐾 ( 2 · 𝑠 ) ) = ( 𝐹 ‘ 0 ) )
37 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → 𝜑 )
38 elii2 ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → 𝑠 ∈ ( ( 1 / 2 ) [,] 1 ) )
39 iihalf2 ⊢ ( 𝑠 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑠 ) − 1 ) ∈ ( 0 [,] 1 ) )
40 38 39 syl ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( ( 2 · 𝑠 ) − 1 ) ∈ ( 0 [,] 1 ) )
41 40 adantll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( ( 2 · 𝑠 ) − 1 ) ∈ ( 0 [,] 1 ) )
42 3 4 6 phtpyi ⊢ ( ( 𝜑 ∧ ( ( 2 · 𝑠 ) − 1 ) ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) = ( 𝐺 ‘ 0 ) ∧ ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) = ( 𝐺 ‘ 1 ) ) )
43 37 41 42 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) = ( 𝐺 ‘ 0 ) ∧ ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) = ( 𝐺 ‘ 1 ) ) )
44 43 simpld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) = ( 𝐺 ‘ 0 ) )
45 2 3 5 phtpy01 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )
47 46 simpld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
48 44 47 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) = ( 𝐹 ‘ 0 ) )
49 36 48 ifeqda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → if ( 𝑠 ≤ ( 1 / 2 ) , ( 0 𝐾 ( 2 · 𝑠 ) ) , ( 0 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) = ( 𝐹 ‘ 0 ) )
50 28 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝑀 𝑠 ) = ( 𝐹 ‘ 0 ) )
51 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
52 simpr ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → 𝑦 = 𝑠 )
53 52 breq1d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 𝑦 ≤ ( 1 / 2 ) ↔ 𝑠 ≤ ( 1 / 2 ) ) )
54 simpl ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → 𝑥 = 1 )
55 52 oveq2d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 2 · 𝑦 ) = ( 2 · 𝑠 ) )
56 54 55 oveq12d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 𝑥 𝐾 ( 2 · 𝑦 ) ) = ( 1 𝐾 ( 2 · 𝑠 ) ) )
57 55 oveq1d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( ( 2 · 𝑦 ) − 1 ) = ( ( 2 · 𝑠 ) − 1 ) )
58 54 57 oveq12d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 𝑥 𝐿 ( ( 2 · 𝑦 ) − 1 ) ) = ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) )
59 53 56 58 ifbieq12d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐾 ( 2 · 𝑦 ) ) , ( 𝑥 𝐿 ( ( 2 · 𝑦 ) − 1 ) ) ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 𝐾 ( 2 · 𝑠 ) ) , ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) )
60 ovex ⊢ ( 1 𝐾 ( 2 · 𝑠 ) ) ∈ V
61 ovex ⊢ ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ∈ V
62 60 61 ifex ⊢ if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 𝐾 ( 2 · 𝑠 ) ) , ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) ∈ V
63 59 1 62 ovmpoa ⊢ ( ( 1 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝑀 𝑠 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 𝐾 ( 2 · 𝑠 ) ) , ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) )
64 51 15 63 sylancr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝑀 𝑠 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 𝐾 ( 2 · 𝑠 ) ) , ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) )
65 35 simprd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( 1 𝐾 ( 2 · 𝑠 ) ) = ( 𝐹 ‘ 1 ) )
66 43 simprd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) = ( 𝐺 ‘ 1 ) )
67 46 simprd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
68 66 67 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) = ( 𝐹 ‘ 1 ) )
69 65 68 ifeqda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → if ( 𝑠 ≤ ( 1 / 2 ) , ( 1 𝐾 ( 2 · 𝑠 ) ) , ( 1 𝐿 ( ( 2 · 𝑠 ) − 1 ) ) ) = ( 𝐹 ‘ 1 ) )
70 64 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝑀 𝑠 ) = ( 𝐹 ‘ 1 ) )
71 2 4 13 50 70 isphtpyd ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) )