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 ‘ 𝐽 ) 𝐻 ) )