pi1coval

Description: The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 10-Aug-2015) (Proof shortened by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	pi1co.p	$⊢ P = J π_{1} A$
	pi1co.q	$⊢ Q = K π_{1} B$
	pi1co.v	$⊢ V = {Base}_{P}$
	pi1co.g	$⊢ G = ran (g \in ⋃ V ⟼ ⟨[g] ≃_{ph} (J), [(F \circ g)] ≃_{ph} (K)⟩)$
	pi1co.j	$⊢ φ \to J \in TopOn (X)$
	pi1co.f	$⊢ φ \to F \in (J Cn K)$
	pi1co.a	$⊢ φ \to A \in X$
	pi1co.b	$⊢ φ \to F (A) = B$
Assertion	pi1coval	$⊢ (φ \land T \in ⋃ V) \to G ([T] ≃_{ph} (J)) = [(F \circ T)] ≃_{ph} (K)$

Proof

Step	Hyp	Ref	Expression
1		pi1co.p	$⊢ P = J π_{1} A$
2		pi1co.q	$⊢ Q = K π_{1} B$
3		pi1co.v	$⊢ V = {Base}_{P}$
4		pi1co.g	$⊢ G = ran (g \in ⋃ V ⟼ ⟨[g] ≃_{ph} (J), [(F \circ g)] ≃_{ph} (K)⟩)$
5		pi1co.j	$⊢ φ \to J \in TopOn (X)$
6		pi1co.f	$⊢ φ \to F \in (J Cn K)$
7		pi1co.a	$⊢ φ \to A \in X$
8		pi1co.b	$⊢ φ \to F (A) = B$
9		fvex	$⊢ ≃_{ph} (J) \in V$
10		ecexg	$⊢ ≃_{ph} (J) \in V \to [g] ≃_{ph} (J) \in V$
11	9 10	mp1i	$⊢ (φ \land g \in ⋃ V) \to [g] ≃_{ph} (J) \in V$
12		fvex	$⊢ ≃_{ph} (K) \in V$
13		ecexg	$⊢ ≃_{ph} (K) \in V \to [(F \circ g)] ≃_{ph} (K) \in V$
14	12 13	mp1i	$⊢ (φ \land g \in ⋃ V) \to [(F \circ g)] ≃_{ph} (K) \in V$
15		eceq1	$⊢ g = T \to [g] ≃_{ph} (J) = [T] ≃_{ph} (J)$
16		coeq2	$⊢ g = T \to F \circ g = F \circ T$
17	16	eceq1d	$⊢ g = T \to [(F \circ g)] ≃_{ph} (K) = [(F \circ T)] ≃_{ph} (K)$
18	1 2 3 4 5 6 7 8	pi1cof	$⊢ φ \to G : V ⟶ {Base}_{Q}$
19	18	ffund	$⊢ φ \to Fun G$
20	4 11 14 15 17 19	fliftval	$⊢ (φ \land T \in ⋃ V) \to G ([T] ≃_{ph} (J)) = [(F \circ T)] ≃_{ph} (K)$

Metamath Proof Explorer

Theorem pi1coval

Proof