cvmlift3lem1

	Ref	Expression
Hypotheses	cvmlift3.b	$⊢ B = ⋃ C$
	cvmlift3.y	$⊢ Y = ⋃ K$
	cvmlift3.f	$⊢ φ \to F \in (C CovMap J)$
	cvmlift3.k	$⊢ φ \to K \in SConn$
	cvmlift3.l	$⊢ φ \to K \in N-LocallyPConn$
	cvmlift3.o	$⊢ φ \to O \in Y$
	cvmlift3.g	$⊢ φ \to G \in (K Cn J)$
	cvmlift3.p	$⊢ φ \to P \in B$
	cvmlift3.e	$⊢ φ \to F (P) = G (O)$
	cvmlift3lem1.1	$⊢ φ \to M \in (II Cn K)$
	cvmlift3lem1.2	$⊢ φ \to M (0) = O$
	cvmlift3lem1.3	$⊢ φ \to N \in (II Cn K)$
	cvmlift3lem1.4	$⊢ φ \to N (0) = O$
	cvmlift3lem1.5	$⊢ φ \to M (1) = N (1)$
Assertion	cvmlift3lem1	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P)) (1)$

Proof

Step	Hyp	Ref	Expression
1		cvmlift3.b	$⊢ B = ⋃ C$
2		cvmlift3.y	$⊢ Y = ⋃ K$
3		cvmlift3.f	$⊢ φ \to F \in (C CovMap J)$
4		cvmlift3.k	$⊢ φ \to K \in SConn$
5		cvmlift3.l	$⊢ φ \to K \in N-LocallyPConn$
6		cvmlift3.o	$⊢ φ \to O \in Y$
7		cvmlift3.g	$⊢ φ \to G \in (K Cn J)$
8		cvmlift3.p	$⊢ φ \to P \in B$
9		cvmlift3.e	$⊢ φ \to F (P) = G (O)$
10		cvmlift3lem1.1	$⊢ φ \to M \in (II Cn K)$
11		cvmlift3lem1.2	$⊢ φ \to M (0) = O$
12		cvmlift3lem1.3	$⊢ φ \to N \in (II Cn K)$
13		cvmlift3lem1.4	$⊢ φ \to N (0) = O$
14		cvmlift3lem1.5	$⊢ φ \to M (1) = N (1)$
15		eqid	$⊢ (ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P))$
16		eqid	$⊢ (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P))$
17	11	fveq2d	$⊢ φ \to G (M (0)) = G (O)$
18	9 17	eqtr4d	$⊢ φ \to F (P) = G (M (0))$
19		iiuni	$⊢ [0, 1] = ⋃ II$
20	19 2	cnf	$⊢ M \in (II Cn K) \to M : [0, 1] ⟶ Y$
21	10 20	syl	$⊢ φ \to M : [0, 1] ⟶ Y$
22		0elunit	$⊢ 0 \in [0, 1]$
23		fvco3	$⊢ (M : [0, 1] ⟶ Y \land 0 \in [0, 1]) \to (G \circ M) (0) = G (M (0))$
24	21 22 23	sylancl	$⊢ φ \to (G \circ M) (0) = G (M (0))$
25	18 24	eqtr4d	$⊢ φ \to F (P) = (G \circ M) (0)$
26	11 13	eqtr4d	$⊢ φ \to M (0) = N (0)$
27	4 10 12 26 14	sconnpht2	$⊢ φ \to M ≃_{ph} (K) N$
28	27 7	phtpcco2	$⊢ φ \to (G \circ M) ≃_{ph} (J) (G \circ N)$
29	1 15 16 3 8 25 28	cvmliftpht	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) ≃_{ph} (C) (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P))$
30		phtpc01	$⊢ (ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) ≃_{ph} (C) (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P)) \to ((ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) (0) = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P)) (0) \land (ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P)) (1))$
31	29 30	syl	$⊢ φ \to ((ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) (0) = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P)) (0) \land (ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P)) (1))$
32	31	simprd	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ M \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = P)) (1)$

Metamath Proof Explorer

Theorem cvmlift3lem1

Proof