pi1cof

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

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		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
13		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
14	6 13	syl	$⊢ φ \to K \in Top$
15		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
16	14 15	sylib	$⊢ φ \to K \in TopOn (⋃ K)$
17	16	adantr	$⊢ (φ \land g \in ⋃ V) \to K \in TopOn (⋃ K)$
18		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (⋃ K) \land F \in (J Cn K)) \to F : X ⟶ ⋃ K$
19	5 16 6 18	syl3anc	$⊢ φ \to F : X ⟶ ⋃ K$
20	19 7	ffvelrnd	$⊢ φ \to F (A) \in ⋃ K$
21	8 20	eqeltrrd	$⊢ φ \to B \in ⋃ K$
22	21	adantr	$⊢ (φ \land g \in ⋃ V) \to B \in ⋃ K$
23	3	a1i	$⊢ φ \to V = {Base}_{P}$
24	1 5 7 23	pi1eluni	$⊢ φ \to (g \in ⋃ V \leftrightarrow (g \in (II Cn J) \land g (0) = A \land g (1) = A))$
25	24	biimpa	$⊢ (φ \land g \in ⋃ V) \to (g \in (II Cn J) \land g (0) = A \land g (1) = A)$
26	25	simp1d	$⊢ (φ \land g \in ⋃ V) \to g \in (II Cn J)$
27	6	adantr	$⊢ (φ \land g \in ⋃ V) \to F \in (J Cn K)$
28		cnco	$⊢ (g \in (II Cn J) \land F \in (J Cn K)) \to F \circ g \in (II Cn K)$
29	26 27 28	syl2anc	$⊢ (φ \land g \in ⋃ V) \to F \circ g \in (II Cn K)$
30		iitopon	$⊢ II \in TopOn ([0, 1])$
31		cnf2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (X) \land g \in (II Cn J)) \to g : [0, 1] ⟶ X$
32	30 5 26 31	mp3an2ani	$⊢ (φ \land g \in ⋃ V) \to g : [0, 1] ⟶ X$
33		0elunit	$⊢ 0 \in [0, 1]$
34		fvco3	$⊢ (g : [0, 1] ⟶ X \land 0 \in [0, 1]) \to (F \circ g) (0) = F (g (0))$
35	32 33 34	sylancl	$⊢ (φ \land g \in ⋃ V) \to (F \circ g) (0) = F (g (0))$
36	25	simp2d	$⊢ (φ \land g \in ⋃ V) \to g (0) = A$
37	36	fveq2d	$⊢ (φ \land g \in ⋃ V) \to F (g (0)) = F (A)$
38	8	adantr	$⊢ (φ \land g \in ⋃ V) \to F (A) = B$
39	35 37 38	3eqtrd	$⊢ (φ \land g \in ⋃ V) \to (F \circ g) (0) = B$
40		1elunit	$⊢ 1 \in [0, 1]$
41		fvco3	$⊢ (g : [0, 1] ⟶ X \land 1 \in [0, 1]) \to (F \circ g) (1) = F (g (1))$
42	32 40 41	sylancl	$⊢ (φ \land g \in ⋃ V) \to (F \circ g) (1) = F (g (1))$
43	25	simp3d	$⊢ (φ \land g \in ⋃ V) \to g (1) = A$
44	43	fveq2d	$⊢ (φ \land g \in ⋃ V) \to F (g (1)) = F (A)$
45	42 44 38	3eqtrd	$⊢ (φ \land g \in ⋃ V) \to (F \circ g) (1) = B$
46	2 12 17 22 29 39 45	elpi1i	$⊢ (φ \land g \in ⋃ V) \to [(F \circ g)] ≃_{ph} (K) \in {Base}_{Q}$
47		eceq1	$⊢ g = h \to [g] ≃_{ph} (J) = [h] ≃_{ph} (J)$
48		coeq2	$⊢ g = h \to F \circ g = F \circ h$
49	48	eceq1d	$⊢ g = h \to [(F \circ g)] ≃_{ph} (K) = [(F \circ h)] ≃_{ph} (K)$
50		phtpcer	$⊢ ≃_{ph} (K) Er (II Cn K)$
51	50	a1i	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to ≃_{ph} (K) Er (II Cn K)$
52		simpr3	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to [g] ≃_{ph} (J) = [h] ≃_{ph} (J)$
53		phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$
54	53	a1i	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to ≃_{ph} (J) Er (II Cn J)$
55		simpr1	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to g \in ⋃ V$
56	24	adantr	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to (g \in ⋃ V \leftrightarrow (g \in (II Cn J) \land g (0) = A \land g (1) = A))$
57	55 56	mpbid	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to (g \in (II Cn J) \land g (0) = A \land g (1) = A)$
58	57	simp1d	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to g \in (II Cn J)$
59	54 58	erth	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to (g ≃_{ph} (J) h \leftrightarrow [g] ≃_{ph} (J) = [h] ≃_{ph} (J))$
60	52 59	mpbird	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to g ≃_{ph} (J) h$
61	6	adantr	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to F \in (J Cn K)$
62	60 61	phtpcco2	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to (F \circ g) ≃_{ph} (K) (F \circ h)$
63	51 62	erthi	$⊢ (φ \land (g \in ⋃ V \land h \in ⋃ V \land [g] ≃_{ph} (J) = [h] ≃_{ph} (J))) \to [(F \circ g)] ≃_{ph} (K) = [(F \circ h)] ≃_{ph} (K)$
64	4 11 46 47 49 63	fliftfund	$⊢ φ \to Fun G$
65	4 11 46	fliftf	$⊢ φ \to (Fun G \leftrightarrow G : ran (g \in ⋃ V ⟼ [g] ≃_{ph} (J)) ⟶ {Base}_{Q})$
66	64 65	mpbid	$⊢ φ \to G : ran (g \in ⋃ V ⟼ [g] ≃_{ph} (J)) ⟶ {Base}_{Q}$
67	1 5 7 23	pi1bas2	$⊢ φ \to V = ⋃ V / ≃_{ph} (J)$
68		df-qs	$⊢ ⋃ V / ≃_{ph} (J) = \{s \| \exists g \in ⋃ V s = [g] ≃_{ph} (J)\}$
69		eqid	$⊢ (g \in ⋃ V ⟼ [g] ≃_{ph} (J)) = (g \in ⋃ V ⟼ [g] ≃_{ph} (J))$
70	69	rnmpt	$⊢ ran (g \in ⋃ V ⟼ [g] ≃_{ph} (J)) = \{s \| \exists g \in ⋃ V s = [g] ≃_{ph} (J)\}$
71	68 70	eqtr4i	$⊢ ⋃ V / ≃_{ph} (J) = ran (g \in ⋃ V ⟼ [g] ≃_{ph} (J))$
72	67 71	eqtrdi	$⊢ φ \to V = ran (g \in ⋃ V ⟼ [g] ≃_{ph} (J))$
73	72	feq2d	$⊢ φ \to (G : V ⟶ {Base}_{Q} \leftrightarrow G : ran (g \in ⋃ V ⟼ [g] ≃_{ph} (J)) ⟶ {Base}_{Q})$
74	66 73	mpbird	$⊢ φ \to G : V ⟶ {Base}_{Q}$

Metamath Proof Explorer

Theorem pi1cof

Proof