Theorem htpycom

Description: Given a homotopy from F to G , produce a homotopy from G to F . (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	ishtpy.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	ishtpy.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
	ishtpy.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
	htpycom.6	⊢ 𝑀 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 ( 1 − 𝑦 ) ) )
	htpycom.7	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
Assertion	htpycom	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ishtpy.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		ishtpy.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3		ishtpy.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
4		htpycom.6	⊢ 𝑀 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 ( 1 − 𝑦 ) ) )
5		htpycom.7	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
6		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
7	6	a1i	⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
8	1 7	cnmpt1st	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t II ) Cn 𝐽 ) )
9	1 7	cnmpt2nd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×t II ) Cn II ) )
10		iirevcn	⊢ ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑧 ) ) ∈ ( II Cn II )
11	10	a1i	⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑧 ) ) ∈ ( II Cn II ) )
12		oveq2	⊢ ( 𝑧 = 𝑦 → ( 1 − 𝑧 ) = ( 1 − 𝑦 ) )
13	1 7 9 7 11 12	cnmpt21	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑦 ) ) ∈ ( ( 𝐽 ×t II ) Cn II ) )
14	1 2 3	htpycn	⊢ ( 𝜑 → ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
15	14 5	sseldd	⊢ ( 𝜑 → 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
16	1 7 8 13 15	cnmpt22f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 ( 1 − 𝑦 ) ) ) ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
17	4 16	eqeltrid	⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑋 ) → 𝑡 ∈ 𝑋 )
19		0elunit	⊢ 0 ∈ ( 0 [,] 1 )
20		oveq1	⊢ ( 𝑥 = 𝑡 → ( 𝑥 𝐻 ( 1 − 𝑦 ) ) = ( 𝑡 𝐻 ( 1 − 𝑦 ) ) )
21		oveq2	⊢ ( 𝑦 = 0 → ( 1 − 𝑦 ) = ( 1 − 0 ) )
22		1m0e1	⊢ ( 1 − 0 ) = 1
23	21 22	eqtrdi	⊢ ( 𝑦 = 0 → ( 1 − 𝑦 ) = 1 )
24	23	oveq2d	⊢ ( 𝑦 = 0 → ( 𝑡 𝐻 ( 1 − 𝑦 ) ) = ( 𝑡 𝐻 1 ) )
25		ovex	⊢ ( 𝑡 𝐻 1 ) ∈ V
26	20 24 4 25	ovmpo	⊢ ( ( 𝑡 ∈ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑡 𝑀 0 ) = ( 𝑡 𝐻 1 ) )
27	18 19 26	sylancl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑋 ) → ( 𝑡 𝑀 0 ) = ( 𝑡 𝐻 1 ) )
28	1 2 3 5	htpyi	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑋 ) → ( ( 𝑡 𝐻 0 ) = ( 𝐹 ‘ 𝑡 ) ∧ ( 𝑡 𝐻 1 ) = ( 𝐺 ‘ 𝑡 ) ) )
29	28	simprd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑋 ) → ( 𝑡 𝐻 1 ) = ( 𝐺 ‘ 𝑡 ) )
30	27 29	eqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑋 ) → ( 𝑡 𝑀 0 ) = ( 𝐺 ‘ 𝑡 ) )
31		1elunit	⊢ 1 ∈ ( 0 [,] 1 )
32		oveq2	⊢ ( 𝑦 = 1 → ( 1 − 𝑦 ) = ( 1 − 1 ) )
33		1m1e0	⊢ ( 1 − 1 ) = 0
34	32 33	eqtrdi	⊢ ( 𝑦 = 1 → ( 1 − 𝑦 ) = 0 )
35	34	oveq2d	⊢ ( 𝑦 = 1 → ( 𝑡 𝐻 ( 1 − 𝑦 ) ) = ( 𝑡 𝐻 0 ) )
36		ovex	⊢ ( 𝑡 𝐻 0 ) ∈ V
37	20 35 4 36	ovmpo	⊢ ( ( 𝑡 ∈ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑡 𝑀 1 ) = ( 𝑡 𝐻 0 ) )
38	18 31 37	sylancl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑋 ) → ( 𝑡 𝑀 1 ) = ( 𝑡 𝐻 0 ) )
39	28	simpld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑋 ) → ( 𝑡 𝐻 0 ) = ( 𝐹 ‘ 𝑡 ) )
40	38 39	eqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑋 ) → ( 𝑡 𝑀 1 ) = ( 𝐹 ‘ 𝑡 ) )
41	1 3 2 17 30 40	ishtpyd	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐹 ) )