pi1xfrf

Description: Functionality of the loop transfer function on the equivalence class of a path. (Contributed 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)$
Assertion	pi1xfrf	$⊢ φ \to G : B ⟶ {Base}_{Q}$

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	5	adantr	$⊢ (φ \land g \in ⋃ B) \to J \in TopOn (X)$
11		iitopon	$⊢ II \in TopOn ([0, 1])$
12		cnf2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (X) \land F \in (II Cn J)) \to F : [0, 1] ⟶ X$
13	11 5 6 12	mp3an2i	$⊢ φ \to F : [0, 1] ⟶ X$
14		0elunit	$⊢ 0 \in [0, 1]$
15		ffvelrn	$⊢ (F : [0, 1] ⟶ X \land 0 \in [0, 1]) \to F (0) \in X$
16	13 14 15	sylancl	$⊢ φ \to F (0) \in X$
17	16	adantr	$⊢ (φ \land g \in ⋃ B) \to F (0) \in X$
18	3	a1i	$⊢ φ \to B = {Base}_{P}$
19	1 5 16 18	pi1eluni	$⊢ φ \to (g \in ⋃ B \leftrightarrow (g \in (II Cn J) \land g (0) = F (0) \land g (1) = F (0)))$
20	19	biimpa	$⊢ (φ \land g \in ⋃ B) \to (g \in (II Cn J) \land g (0) = F (0) \land g (1) = F (0))$
21	20	simp1d	$⊢ (φ \land g \in ⋃ B) \to g \in (II Cn J)$
22	20	simp2d	$⊢ (φ \land g \in ⋃ B) \to g (0) = F (0)$
23	20	simp3d	$⊢ (φ \land g \in ⋃ B) \to g (1) = F (0)$
24	1 3 10 17 21 22 23	elpi1i	$⊢ (φ \land g \in ⋃ B) \to [g] ≃_{ph} (J) \in B$
25		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
26		1elunit	$⊢ 1 \in [0, 1]$
27		ffvelrn	$⊢ (F : [0, 1] ⟶ X \land 1 \in [0, 1]) \to F (1) \in X$
28	13 26 27	sylancl	$⊢ φ \to F (1) \in X$
29	28	adantr	$⊢ (φ \land g \in ⋃ B) \to F (1) \in X$
30	7	adantr	$⊢ (φ \land g \in ⋃ B) \to I \in (II Cn J)$
31	6	adantr	$⊢ (φ \land g \in ⋃ B) \to F \in (II Cn J)$
32	21 31 23	pcocn	$⊢ (φ \land g \in ⋃ B) \to g *_{𝑝} (J) F \in (II Cn J)$
33	21 31	pco0	$⊢ (φ \land g \in ⋃ B) \to (g *_{𝑝} (J) F) (0) = g (0)$
34	9	adantr	$⊢ (φ \land g \in ⋃ B) \to I (1) = F (0)$
35	22 33 34	3eqtr4rd	$⊢ (φ \land g \in ⋃ B) \to I (1) = (g *_{𝑝} (J) F) (0)$
36	30 32 35	pcocn	$⊢ (φ \land g \in ⋃ B) \to I _{𝑝} (J) (g _{𝑝} (J) F) \in (II Cn J)$
37	30 32	pco0	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) (0) = I (0)$
38	8	adantr	$⊢ (φ \land g \in ⋃ B) \to F (1) = I (0)$
39	37 38	eqtr4d	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) (0) = F (1)$
40	30 32	pco1	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) (1) = (g *_{𝑝} (J) F) (1)$
41	21 31	pco1	$⊢ (φ \land g \in ⋃ B) \to (g *_{𝑝} (J) F) (1) = F (1)$
42	40 41	eqtrd	$⊢ (φ \land g \in ⋃ B) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) (1) = F (1)$
43	2 25 10 29 36 39 42	elpi1i	$⊢ (φ \land g \in ⋃ B) \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) \in {Base}_{Q}$
44		eceq1	$⊢ g = h \to [g] ≃_{ph} (J) = [h] ≃_{ph} (J)$
45		oveq1	$⊢ g = h \to g _{𝑝} (J) F = h _{𝑝} (J) F$
46	45	oveq2d	$⊢ g = h \to I _{𝑝} (J) (g _{𝑝} (J) F) = I _{𝑝} (J) (h _{𝑝} (J) F)$
47	46	eceq1d	$⊢ g = h \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) = [(I _{𝑝} (J) (h _{𝑝} (J) F))] ≃_{ph} (J)$
48		phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$
49	48	a1i	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to ≃_{ph} (J) Er (II Cn J)$
50	22	3ad2antr1	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to g (0) = F (0)$
51	21	3ad2antr1	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to g \in (II Cn J)$
52	6	adantr	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to F \in (II Cn J)$
53	51 52	pco0	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to (g *_{𝑝} (J) F) (0) = g (0)$
54	9	adantr	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to I (1) = F (0)$
55	50 53 54	3eqtr4rd	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to I (1) = (g *_{𝑝} (J) F) (0)$
56	7	adantr	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to I \in (II Cn J)$
57	49 56	erref	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to I ≃_{ph} (J) I$
58	23	3ad2antr1	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to g (1) = F (0)$
59		simpr3	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to [g] ≃_{ph} (J) = [h] ≃_{ph} (J)$
60	49 51	erth	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to (g ≃_{ph} (J) h \leftrightarrow [g] ≃_{ph} (J) = [h] ≃_{ph} (J))$
61	59 60	mpbird	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to g ≃_{ph} (J) h$
62	49 52	erref	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to F ≃_{ph} (J) F$
63	58 61 62	pcohtpy	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to (g _{𝑝} (J) F) ≃_{ph} (J) (h _{𝑝} (J) F)$
64	55 57 63	pcohtpy	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to (I _{𝑝} (J) (g _{𝑝} (J) F)) ≃_{ph} (J) (I _{𝑝} (J) (h _{𝑝} (J) F))$
65	49 64	erthi	$⊢ (φ \land (g \in ⋃ B \land h \in ⋃ B \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to [(I _{𝑝} (J) (g _{𝑝} (J) F))] ≃_{ph} (J) = [(I _{𝑝} (J) (h _{𝑝} (J) F))] ≃_{ph} (J)$
66	4 24 43 44 47 65	fliftfund	$⊢ φ \to Fun G$
67	4 24 43	fliftf	$⊢ φ \to (Fun G \leftrightarrow G : ran (g \in ⋃ B ⟼ [g] ≃_{ph} (J)) ⟶ {Base}_{Q})$
68	66 67	mpbid	$⊢ φ \to G : ran (g \in ⋃ B ⟼ [g] ≃_{ph} (J)) ⟶ {Base}_{Q}$
69	1 5 16 18	pi1bas2	$⊢ φ \to B = ⋃ B / ≃_{ph} (J)$
70		df-qs	$⊢ ⋃ B / ≃_{ph} (J) = \{s \| \exists g \in ⋃ B s = [g] ≃_{ph} (J)\}$
71		eqid	$⊢ (g \in ⋃ B ⟼ [g] ≃_{ph} (J)) = (g \in ⋃ B ⟼ [g] ≃_{ph} (J))$
72	71	rnmpt	$⊢ ran (g \in ⋃ B ⟼ [g] ≃_{ph} (J)) = \{s \| \exists g \in ⋃ B s = [g] ≃_{ph} (J)\}$
73	70 72	eqtr4i	$⊢ ⋃ B / ≃_{ph} (J) = ran (g \in ⋃ B ⟼ [g] ≃_{ph} (J))$
74	69 73	eqtrdi	$⊢ φ \to B = ran (g \in ⋃ B ⟼ [g] ≃_{ph} (J))$
75	74	feq2d	$⊢ φ \to (G : B ⟶ {Base}_{Q} \leftrightarrow G : ran (g \in ⋃ B ⟼ [g] ≃_{ph} (J)) ⟶ {Base}_{Q})$
76	68 75	mpbird	$⊢ φ \to G : B ⟶ {Base}_{Q}$

Metamath Proof Explorer

Theorem pi1xfrf

Proof