pi1xfrval

Description: The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 12-Feb-2015) (Revised by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	pi1xfr.p	$⊢ P = J π_{1} F (0)$
	pi1xfr.q	$⊢ Q = J π_{1} F (1)$
	pi1xfr.b	$⊢ B = {Base}_{P}$
	pi1xfr.g	$⊢ G = ran (g \in ⋃ B ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J)⟩)$
	pi1xfr.j	$⊢ φ \to J \in TopOn (X)$
	pi1xfr.f	$⊢ φ \to F \in (II Cn J)$
	pi1xfrval.i	$⊢ φ \to I \in (II Cn J)$
	pi1xfrval.1	$⊢ φ \to F (1) = I (0)$
	pi1xfrval.2	$⊢ φ \to I (1) = F (0)$
	pi1xfrval.a	$⊢ φ \to A \in ⋃ B$
Assertion	pi1xfrval	$⊢ φ \to G ([A] ≃_{ph} (J)) = [(I _{𝑝} (J) (A _{𝑝} (J) F))] ≃_{ph} (J)$

Proof

Step	Hyp	Ref	Expression
1		pi1xfr.p	$⊢ P = J π_{1} F (0)$
2		pi1xfr.q	$⊢ Q = J π_{1} F (1)$
3		pi1xfr.b	$⊢ B = {Base}_{P}$
4		pi1xfr.g	$⊢ G = ran (g \in ⋃ B ⟼ ⟨[g] ≃_{ph} (J), [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J)⟩)$
5		pi1xfr.j	$⊢ φ \to J \in TopOn (X)$
6		pi1xfr.f	$⊢ φ \to F \in (II Cn J)$
7		pi1xfrval.i	$⊢ φ \to I \in (II Cn J)$
8		pi1xfrval.1	$⊢ φ \to F (1) = I (0)$
9		pi1xfrval.2	$⊢ φ \to I (1) = F (0)$
10		pi1xfrval.a	$⊢ φ \to A \in ⋃ B$
11		fvex	$⊢ ≃_{ph} (J) \in V$
12		ecexg	$⊢ ≃_{ph} (J) \in V \to [g] ≃_{ph} (J) \in V$
13	11 12	mp1i	$⊢ (φ \land g \in ⋃ B) \to [g] ≃_{ph} (J) \in V$
14		ecexg	$⊢ ≃_{ph} (J) \in V \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) \in V$
15	11 14	mp1i	$⊢ (φ \land g \in ⋃ B) \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) \in V$
16		eceq1	$⊢ g = A \to [g] ≃_{ph} (J) = [A] ≃_{ph} (J)$
17		oveq1	$⊢ g = A \to g _{𝑝} (J) F = A _{𝑝} (J) F$
18	17	oveq2d	$⊢ g = A \to I _{𝑝} (J) (g _{𝑝} (J) F) = I _{𝑝} (J) (A _{𝑝} (J) F)$
19	18	eceq1d	$⊢ g = A \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) = [(I _{𝑝} (J) (A _{𝑝} (J) F))] ≃_{ph} (J)$
20	1 2 3 4 5 6 7 8 9	pi1xfrf	$⊢ φ \to G : B ⟶ {Base}_{Q}$
21	20	ffund	$⊢ φ \to Fun G$
22	4 13 15 16 19 21	fliftval	$⊢ (φ \land A \in ⋃ B) \to G ([A] ≃_{ph} (J)) = [(I _{𝑝} (J) (A _{𝑝} (J) F))] ≃_{ph} (J)$
23	10 22	mpdan	$⊢ φ \to G ([A] ≃_{ph} (J)) = [(I _{𝑝} (J) (A _{𝑝} (J) F))] ≃_{ph} (J)$

Metamath Proof Explorer

Theorem pi1xfrval

Proof