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	$⊢ φ \to J \in TopOn (X)$
	ishtpy.3	$⊢ φ \to F \in (J Cn K)$
	ishtpy.4	$⊢ φ \to G \in (J Cn K)$
	htpycom.6	$⊢ M = (x \in X, y \in [0, 1] ⟼ x H (1 - y))$
	htpycom.7	$⊢ φ \to H \in (F (J Htpy K) G)$
Assertion	htpycom	$⊢ φ \to M \in (G (J Htpy K) F)$

Proof

Step	Hyp	Ref	Expression
1		ishtpy.1	$⊢ φ \to J \in TopOn (X)$
2		ishtpy.3	$⊢ φ \to F \in (J Cn K)$
3		ishtpy.4	$⊢ φ \to G \in (J Cn K)$
4		htpycom.6	$⊢ M = (x \in X, y \in [0, 1] ⟼ x H (1 - y))$
5		htpycom.7	$⊢ φ \to H \in (F (J Htpy K) G)$
6		iitopon	$⊢ II \in TopOn ([0, 1])$
7	6	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
8	1 7	cnmpt1st	$⊢ φ \to (x \in X, y \in [0, 1] ⟼ x) \in ((J \times_{t} II) Cn J)$
9	1 7	cnmpt2nd	$⊢ φ \to (x \in X, y \in [0, 1] ⟼ y) \in ((J \times_{t} II) Cn II)$
10		iirevcn	$⊢ (z \in [0, 1] ⟼ 1 - z) \in (II Cn II)$
11	10	a1i	$⊢ φ \to (z \in [0, 1] ⟼ 1 - z) \in (II Cn II)$
12		oveq2	$⊢ z = y \to 1 - z = 1 - y$
13	1 7 9 7 11 12	cnmpt21	$⊢ φ \to (x \in X, y \in [0, 1] ⟼ 1 - y) \in ((J \times_{t} II) Cn II)$
14	1 2 3	htpycn	$⊢ φ \to F (J Htpy K) G \subseteq (J \times_{t} II) Cn K$
15	14 5	sseldd	$⊢ φ \to H \in ((J \times_{t} II) Cn K)$
16	1 7 8 13 15	cnmpt22f	$⊢ φ \to (x \in X, y \in [0, 1] ⟼ x H (1 - y)) \in ((J \times_{t} II) Cn K)$
17	4 16	eqeltrid	$⊢ φ \to M \in ((J \times_{t} II) Cn K)$
18		simpr	$⊢ (φ \land t \in X) \to t \in X$
19		0elunit	$⊢ 0 \in [0, 1]$
20		oveq1	$⊢ x = t \to x H (1 - y) = t H (1 - y)$
21		oveq2	$⊢ y = 0 \to 1 - y = 1 - 0$
22		1m0e1	$⊢ 1 - 0 = 1$
23	21 22	eqtrdi	$⊢ y = 0 \to 1 - y = 1$
24	23	oveq2d	$⊢ y = 0 \to t H (1 - y) = t H 1$
25		ovex	$⊢ t H 1 \in V$
26	20 24 4 25	ovmpo	$⊢ (t \in X \land 0 \in [0, 1]) \to t M 0 = t H 1$
27	18 19 26	sylancl	$⊢ (φ \land t \in X) \to t M 0 = t H 1$
28	1 2 3 5	htpyi	$⊢ (φ \land t \in X) \to (t H 0 = F (t) \land t H 1 = G (t))$
29	28	simprd	$⊢ (φ \land t \in X) \to t H 1 = G (t)$
30	27 29	eqtrd	$⊢ (φ \land t \in X) \to t M 0 = G (t)$
31		1elunit	$⊢ 1 \in [0, 1]$
32		oveq2	$⊢ y = 1 \to 1 - y = 1 - 1$
33		1m1e0	$⊢ 1 - 1 = 0$
34	32 33	eqtrdi	$⊢ y = 1 \to 1 - y = 0$
35	34	oveq2d	$⊢ y = 1 \to t H (1 - y) = t H 0$
36		ovex	$⊢ t H 0 \in V$
37	20 35 4 36	ovmpo	$⊢ (t \in X \land 1 \in [0, 1]) \to t M 1 = t H 0$
38	18 31 37	sylancl	$⊢ (φ \land t \in X) \to t M 1 = t H 0$
39	28	simpld	$⊢ (φ \land t \in X) \to t H 0 = F (t)$
40	38 39	eqtrd	$⊢ (φ \land t \in X) \to t M 1 = F (t)$
41	1 3 2 17 30 40	ishtpyd	$⊢ φ \to M \in (G (J Htpy K) F)$

Metamath Proof Explorer

Theorem htpycom

Proof