cvmliftpht

Description: If G and H are path-homotopic, then their lifts M and N are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015)

	Ref	Expression
Hypotheses	cvmliftpht.b	$⊢ B = ⋃ C$
	cvmliftpht.m	$⊢ M = (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P))$
	cvmliftpht.n	$⊢ N = (ι f \in (II Cn C) \| (F \circ f = H \land f (0) = P))$
	cvmliftpht.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftpht.p	$⊢ φ \to P \in B$
	cvmliftpht.e	$⊢ φ \to F (P) = G (0)$
	cvmliftpht.g	$⊢ φ \to G ≃_{ph} (J) H$
Assertion	cvmliftpht	$⊢ φ \to M ≃_{ph} (C) N$

Proof

Step	Hyp	Ref	Expression
1		cvmliftpht.b	$⊢ B = ⋃ C$
2		cvmliftpht.m	$⊢ M = (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P))$
3		cvmliftpht.n	$⊢ N = (ι f \in (II Cn C) \| (F \circ f = H \land f (0) = P))$
4		cvmliftpht.f	$⊢ φ \to F \in (C CovMap J)$
5		cvmliftpht.p	$⊢ φ \to P \in B$
6		cvmliftpht.e	$⊢ φ \to F (P) = G (0)$
7		cvmliftpht.g	$⊢ φ \to G ≃_{ph} (J) H$
8		isphtpc	$⊢ G ≃_{ph} (J) H \leftrightarrow (G \in (II Cn J) \land H \in (II Cn J) \land G PHtpy (J) H \neq \emptyset)$
9	7 8	sylib	$⊢ φ \to (G \in (II Cn J) \land H \in (II Cn J) \land G PHtpy (J) H \neq \emptyset)$
10	9	simp1d	$⊢ φ \to G \in (II Cn J)$
11	1 2 4 10 5 6	cvmliftiota	$⊢ φ \to (M \in (II Cn C) \land F \circ M = G \land M (0) = P)$
12	11	simp1d	$⊢ φ \to M \in (II Cn C)$
13	9	simp2d	$⊢ φ \to H \in (II Cn J)$
14		phtpc01	$⊢ G ≃_{ph} (J) H \to (G (0) = H (0) \land G (1) = H (1))$
15	7 14	syl	$⊢ φ \to (G (0) = H (0) \land G (1) = H (1))$
16	15	simpld	$⊢ φ \to G (0) = H (0)$
17	6 16	eqtrd	$⊢ φ \to F (P) = H (0)$
18	1 3 4 13 5 17	cvmliftiota	$⊢ φ \to (N \in (II Cn C) \land F \circ N = H \land N (0) = P)$
19	18	simp1d	$⊢ φ \to N \in (II Cn C)$
20	9	simp3d	$⊢ φ \to G PHtpy (J) H \neq \emptyset$
21		n0	$⊢ G PHtpy (J) H \neq \emptyset \leftrightarrow \exists g g \in (G PHtpy (J) H)$
22	20 21	sylib	$⊢ φ \to \exists g g \in (G PHtpy (J) H)$
23	4	adantr	$⊢ (φ \land g \in (G PHtpy (J) H)) \to F \in (C CovMap J)$
24	10 13	phtpycn	$⊢ φ \to G PHtpy (J) H \subseteq (II \times_{t} II) Cn J$
25	24	sselda	$⊢ (φ \land g \in (G PHtpy (J) H)) \to g \in ((II \times_{t} II) Cn J)$
26	5	adantr	$⊢ (φ \land g \in (G PHtpy (J) H)) \to P \in B$
27	6	adantr	$⊢ (φ \land g \in (G PHtpy (J) H)) \to F (P) = G (0)$
28		0elunit	$⊢ 0 \in [0, 1]$
29	10	adantr	$⊢ (φ \land g \in (G PHtpy (J) H)) \to G \in (II Cn J)$
30	13	adantr	$⊢ (φ \land g \in (G PHtpy (J) H)) \to H \in (II Cn J)$
31		simpr	$⊢ (φ \land g \in (G PHtpy (J) H)) \to g \in (G PHtpy (J) H)$
32	29 30 31	phtpyi	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land 0 \in [0, 1]) \to (0 g 0 = G (0) \land 1 g 0 = G (1))$
33	28 32	mpan2	$⊢ (φ \land g \in (G PHtpy (J) H)) \to (0 g 0 = G (0) \land 1 g 0 = G (1))$
34	33	simpld	$⊢ (φ \land g \in (G PHtpy (J) H)) \to 0 g 0 = G (0)$
35	27 34	eqtr4d	$⊢ (φ \land g \in (G PHtpy (J) H)) \to F (P) = 0 g 0$
36	1 23 25 26 35	cvmlift2	$⊢ (φ \land g \in (G PHtpy (J) H)) \to \exists! h \in ((II \times_{t} II) Cn C) (F \circ h = g \land 0 h 0 = P)$
37		reurex	$⊢ \exists! h \in ((II \times_{t} II) Cn C) (F \circ h = g \land 0 h 0 = P) \to \exists h \in ((II \times_{t} II) Cn C) (F \circ h = g \land 0 h 0 = P)$
38	36 37	syl	$⊢ (φ \land g \in (G PHtpy (J) H)) \to \exists h \in ((II \times_{t} II) Cn C) (F \circ h = g \land 0 h 0 = P)$
39	4	ad2antrr	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to F \in (C CovMap J)$
40	5	ad2antrr	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to P \in B$
41	6	ad2antrr	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to F (P) = G (0)$
42	10	ad2antrr	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to G \in (II Cn J)$
43	13	ad2antrr	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to H \in (II Cn J)$
44		simplr	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to g \in (G PHtpy (J) H)$
45		simprl	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to h \in ((II \times_{t} II) Cn C)$
46		simprrl	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to F \circ h = g$
47		simprrr	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to 0 h 0 = P$
48	1 2 3 39 40 41 42 43 44 45 46 47	cvmliftphtlem	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to h \in (M PHtpy (C) N)$
49	48	ne0d	$⊢ ((φ \land g \in (G PHtpy (J) H)) \land (h \in ((II \times_{t} II) Cn C) \land (F \circ h = g \land 0 h 0 = P))) \to M PHtpy (C) N \neq \emptyset$
50	38 49	rexlimddv	$⊢ (φ \land g \in (G PHtpy (J) H)) \to M PHtpy (C) N \neq \emptyset$
51	22 50	exlimddv	$⊢ φ \to M PHtpy (C) N \neq \emptyset$
52		isphtpc	$⊢ M ≃_{ph} (C) N \leftrightarrow (M \in (II Cn C) \land N \in (II Cn C) \land M PHtpy (C) N \neq \emptyset)$
53	12 19 51 52	syl3anbrc	$⊢ φ \to M ≃_{ph} (C) N$

Metamath Proof Explorer

Theorem cvmliftpht

Proof