pi1xfr

Description: Given a path F and its inverse I between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015)

	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)$
	pi1xfr.i	$⊢ I = (x \in [0, 1] ⟼ F (1 - x))$
Assertion	pi1xfr	$⊢ φ \to G \in (P GrpHom 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		pi1xfr.i	$⊢ I = (x \in [0, 1] ⟼ F (1 - x))$
8		iitopon	$⊢ II \in TopOn ([0, 1])$
9		cnf2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (X) \land F \in (II Cn J)) \to F : [0, 1] ⟶ X$
10	8 5 6 9	mp3an2i	$⊢ φ \to F : [0, 1] ⟶ X$
11		0elunit	$⊢ 0 \in [0, 1]$
12		ffvelcdm	$⊢ (F : [0, 1] ⟶ X \land 0 \in [0, 1]) \to F (0) \in X$
13	10 11 12	sylancl	$⊢ φ \to F (0) \in X$
14	1	pi1grp	$⊢ (J \in TopOn (X) \land F (0) \in X) \to P \in Grp$
15	5 13 14	syl2anc	$⊢ φ \to P \in Grp$
16		1elunit	$⊢ 1 \in [0, 1]$
17		ffvelcdm	$⊢ (F : [0, 1] ⟶ X \land 1 \in [0, 1]) \to F (1) \in X$
18	10 16 17	sylancl	$⊢ φ \to F (1) \in X$
19	2	pi1grp	$⊢ (J \in TopOn (X) \land F (1) \in X) \to Q \in Grp$
20	5 18 19	syl2anc	$⊢ φ \to Q \in Grp$
21	7	pcorevcl	$⊢ F \in (II Cn J) \to (I \in (II Cn J) \land I (0) = F (1) \land I (1) = F (0))$
22	6 21	syl	$⊢ φ \to (I \in (II Cn J) \land I (0) = F (1) \land I (1) = F (0))$
23	22	simp1d	$⊢ φ \to I \in (II Cn J)$
24	22	simp2d	$⊢ φ \to I (0) = F (1)$
25	24	eqcomd	$⊢ φ \to F (1) = I (0)$
26	22	simp3d	$⊢ φ \to I (1) = F (0)$
27	1 2 3 4 5 6 23 25 26	pi1xfrf	$⊢ φ \to G : B ⟶ {Base}_{Q}$
28	3	a1i	$⊢ φ \to B = {Base}_{P}$
29	1 5 13 28	pi1bas2	$⊢ φ \to B = ⋃ B / ≃_{ph} (J)$
30	29	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in (⋃ B / ≃_{ph} (J)))$
31	30	biimpa	$⊢ (φ \land y \in B) \to y \in (⋃ B / ≃_{ph} (J))$
32		eqid	$⊢ ⋃ B / ≃_{ph} (J) = ⋃ B / ≃_{ph} (J)$
33		fvoveq1	$⊢ [f] ≃_{ph} (J) = y \to G ([f] ≃_{ph} (J) +_{P} z) = G (y +_{P} z)$
34		fveq2	$⊢ [f] ≃_{ph} (J) = y \to G ([f] ≃_{ph} (J)) = G (y)$
35	34	oveq1d	$⊢ [f] ≃_{ph} (J) = y \to G ([f] ≃_{ph} (J)) +_{Q} G (z) = G (y) +_{Q} G (z)$
36	33 35	eqeq12d	$⊢ [f] ≃_{ph} (J) = y \to (G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z) \leftrightarrow G (y +_{P} z) = G (y) +_{Q} G (z))$
37	36	ralbidv	$⊢ [f] ≃_{ph} (J) = y \to (\forall z \in B G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z) \leftrightarrow \forall z \in B G (y +_{P} z) = G (y) +_{Q} G (z))$
38	29	eleq2d	$⊢ φ \to (z \in B \leftrightarrow z \in (⋃ B / ≃_{ph} (J)))$
39	38	biimpa	$⊢ (φ \land z \in B) \to z \in (⋃ B / ≃_{ph} (J))$
40	39	adantlr	$⊢ ((φ \land f \in ⋃ B) \land z \in B) \to z \in (⋃ B / ≃_{ph} (J))$
41		oveq2	$⊢ [h] ≃_{ph} (J) = z \to [f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J) = [f] ≃_{ph} (J) +_{P} z$
42	41	fveq2d	$⊢ [h] ≃_{ph} (J) = z \to G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J) +_{P} z)$
43		fveq2	$⊢ [h] ≃_{ph} (J) = z \to G ([h] ≃_{ph} (J)) = G (z)$
44	43	oveq2d	$⊢ [h] ≃_{ph} (J) = z \to G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J)) +_{Q} G (z)$
45	42 44	eqeq12d	$⊢ [h] ≃_{ph} (J) = z \to (G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J)) \leftrightarrow G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z))$
46		phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$
47	46	a1i	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ≃_{ph} (J) Er (II Cn J)$
48	1 5 13 28	pi1eluni	$⊢ φ \to (f \in ⋃ B \leftrightarrow (f \in (II Cn J) \land f (0) = F (0) \land f (1) = F (0)))$
49	48	biimpa	$⊢ (φ \land f \in ⋃ B) \to (f \in (II Cn J) \land f (0) = F (0) \land f (1) = F (0))$
50	49	simp1d	$⊢ (φ \land f \in ⋃ B) \to f \in (II Cn J)$
51	50	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f \in (II Cn J)$
52	1 5 13 28	pi1eluni	$⊢ φ \to (h \in ⋃ B \leftrightarrow (h \in (II Cn J) \land h (0) = F (0) \land h (1) = F (0)))$
53	52	adantr	$⊢ (φ \land f \in ⋃ B) \to (h \in ⋃ B \leftrightarrow (h \in (II Cn J) \land h (0) = F (0) \land h (1) = F (0)))$
54	53	biimp3a	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (h \in (II Cn J) \land h (0) = F (0) \land h (1) = F (0))$
55	54	simp1d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to h \in (II Cn J)$
56	51 55	pco0	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f *_{𝑝} (J) h) (0) = f (0)$
57	49	simp2d	$⊢ (φ \land f \in ⋃ B) \to f (0) = F (0)$
58	57	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f (0) = F (0)$
59	56 58	eqtrd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f *_{𝑝} (J) h) (0) = F (0)$
60	49	simp3d	$⊢ (φ \land f \in ⋃ B) \to f (1) = F (0)$
61	60	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f (1) = F (0)$
62	54	simp2d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to h (0) = F (0)$
63	61 62	eqtr4d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f (1) = h (0)$
64	51 55 63	pcocn	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f *_{𝑝} (J) h \in (II Cn J)$
65	6	3ad2ant1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to F \in (II Cn J)$
66	64 65	pco0	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ((f _{𝑝} (J) h) _{𝑝} (J) F) (0) = (f *_{𝑝} (J) h) (0)$
67	26	3ad2ant1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I (1) = F (0)$
68	59 66 67	3eqtr4rd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I (1) = ((f _{𝑝} (J) h) _{𝑝} (J) F) (0)$
69	23	3ad2ant1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I \in (II Cn J)$
70	47 69	erref	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I ≃_{ph} (J) I$
71	54	simp3d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to h (1) = F (0)$
72		eqid	$⊢ (u \in [0, 1] ⟼ if (u \leq \frac{1}{2}, if (u \leq \frac{1}{4}, 2 u, u + (\frac{1}{4})), (\frac{u}{2}) + (\frac{1}{2}))) = (u \in [0, 1] ⟼ if (u \leq \frac{1}{2}, if (u \leq \frac{1}{4}, 2 u, u + (\frac{1}{4})), (\frac{u}{2}) + (\frac{1}{2})))$
73	51 55 65 63 71 72	pcoass	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ((f _{𝑝} (J) h) _{𝑝} (J) F) ≃_{ph} (J) (f _{𝑝} (J) (h _{𝑝} (J) F))$
74	55 65	pco0	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (h *_{𝑝} (J) F) (0) = h (0)$
75	63 74	eqtr4d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f (1) = (h *_{𝑝} (J) F) (0)$
76	47 51	erref	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f ≃_{ph} (J) f$
77	65 69	pco1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (F *_{𝑝} (J) I) (1) = I (1)$
78	62 74 67	3eqtr4rd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I (1) = (h *_{𝑝} (J) F) (0)$
79	77 78	eqtrd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (F _{𝑝} (J) I) (1) = (h _{𝑝} (J) F) (0)$
80		eqid	$⊢ [0, 1] \times \{F (0)\} = [0, 1] \times \{F (0)\}$
81	7 80	pcorev2	$⊢ F \in (II Cn J) \to (F *_{𝑝} (J) I) ≃_{ph} (J) ([0, 1] \times \{F (0)\})$
82	65 81	syl	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (F *_{𝑝} (J) I) ≃_{ph} (J) ([0, 1] \times \{F (0)\})$
83	55 65 71	pcocn	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to h *_{𝑝} (J) F \in (II Cn J)$
84	47 83	erref	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (h _{𝑝} (J) F) ≃_{ph} (J) (h _{𝑝} (J) F)$
85	79 82 84	pcohtpy	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ((F _{𝑝} (J) I) _{𝑝} (J) (h _{𝑝} (J) F)) ≃_{ph} (J) (([0, 1] \times \{F (0)\}) _{𝑝} (J) (h *_{𝑝} (J) F))$
86	74 62	eqtrd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (h *_{𝑝} (J) F) (0) = F (0)$
87	80	pcopt	$⊢ (h _{𝑝} (J) F \in (II Cn J) \land (h _{𝑝} (J) F) (0) = F (0)) \to (([0, 1] \times \{F (0)\}) _{𝑝} (J) (h _{𝑝} (J) F)) ≃_{ph} (J) (h *_{𝑝} (J) F)$
88	83 86 87	syl2anc	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (([0, 1] \times \{F (0)\}) _{𝑝} (J) (h _{𝑝} (J) F)) ≃_{ph} (J) (h *_{𝑝} (J) F)$
89	47 85 88	ertrd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ((F _{𝑝} (J) I) _{𝑝} (J) (h _{𝑝} (J) F)) ≃_{ph} (J) (h _{𝑝} (J) F)$
90	24	3ad2ant1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I (0) = F (1)$
91	90	eqcomd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to F (1) = I (0)$
92	65 69 83 91 78 72	pcoass	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ((F _{𝑝} (J) I) _{𝑝} (J) (h _{𝑝} (J) F)) ≃_{ph} (J) (F _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F)))$
93	47 89 92	ertr3d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (h _{𝑝} (J) F) ≃_{ph} (J) (F _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F)))$
94	75 76 93	pcohtpy	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f _{𝑝} (J) (h _{𝑝} (J) F)) ≃_{ph} (J) (f _{𝑝} (J) (F _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F))))$
95	69 83 78	pcocn	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I _{𝑝} (J) (h _{𝑝} (J) F) \in (II Cn J)$
96	69 83	pco0	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) (h _{𝑝} (J) F)) (0) = I (0)$
97	96 90	eqtrd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) (h _{𝑝} (J) F)) (0) = F (1)$
98	97	eqcomd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to F (1) = (I _{𝑝} (J) (h _{𝑝} (J) F)) (0)$
99	51 65 95 61 98 72	pcoass	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ((f _{𝑝} (J) F) _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F))) ≃_{ph} (J) (f _{𝑝} (J) (F _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F))))$
100	47 94 99	ertr4d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f _{𝑝} (J) (h _{𝑝} (J) F)) ≃_{ph} (J) ((f _{𝑝} (J) F) _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F)))$
101	47 73 100	ertrd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ((f _{𝑝} (J) h) _{𝑝} (J) F) ≃_{ph} (J) ((f _{𝑝} (J) F) _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F)))$
102	68 70 101	pcohtpy	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) ((f _{𝑝} (J) h) _{𝑝} (J) F)) ≃_{ph} (J) (I _{𝑝} (J) ((f _{𝑝} (J) F) _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F))))$
103	6	adantr	$⊢ (φ \land f \in ⋃ B) \to F \in (II Cn J)$
104	50 103 60	pcocn	$⊢ (φ \land f \in ⋃ B) \to f *_{𝑝} (J) F \in (II Cn J)$
105	104	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f *_{𝑝} (J) F \in (II Cn J)$
106	50 103	pco0	$⊢ (φ \land f \in ⋃ B) \to (f *_{𝑝} (J) F) (0) = f (0)$
107	26	adantr	$⊢ (φ \land f \in ⋃ B) \to I (1) = F (0)$
108	57 106 107	3eqtr4rd	$⊢ (φ \land f \in ⋃ B) \to I (1) = (f *_{𝑝} (J) F) (0)$
109	108	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I (1) = (f *_{𝑝} (J) F) (0)$
110	51 65	pco1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f *_{𝑝} (J) F) (1) = F (1)$
111	110 97	eqtr4d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f _{𝑝} (J) F) (1) = (I _{𝑝} (J) (h *_{𝑝} (J) F)) (0)$
112	69 105 95 109 111 72	pcoass	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to ((I _{𝑝} (J) (f _{𝑝} (J) F)) _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F))) ≃_{ph} (J) (I _{𝑝} (J) ((f _{𝑝} (J) F) _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F))))$
113	47 102 112	ertr4d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) ((f _{𝑝} (J) h) _{𝑝} (J) F)) ≃_{ph} (J) ((I _{𝑝} (J) (f _{𝑝} (J) F)) _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F)))$
114	47 113	erthi	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to [(I _{𝑝} (J) ((f _{𝑝} (J) h) _{𝑝} (J) F))] ≃_{ph} (J) = [((I _{𝑝} (J) (f _{𝑝} (J) F)) _{𝑝} (J) (I _{𝑝} (J) (h _{𝑝} (J) F)))] ≃_{ph} (J)$
115	5	3ad2ant1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to J \in TopOn (X)$
116	51 55	pco1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f *_{𝑝} (J) h) (1) = h (1)$
117	116 71	eqtrd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f *_{𝑝} (J) h) (1) = F (0)$
118	1 5 13 28	pi1eluni	$⊢ φ \to (f _{𝑝} (J) h \in ⋃ B \leftrightarrow (f _{𝑝} (J) h \in (II Cn J) \land (f _{𝑝} (J) h) (0) = F (0) \land (f _{𝑝} (J) h) (1) = F (0)))$
119	118	3ad2ant1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (f _{𝑝} (J) h \in ⋃ B \leftrightarrow (f _{𝑝} (J) h \in (II Cn J) \land (f _{𝑝} (J) h) (0) = F (0) \land (f _{𝑝} (J) h) (1) = F (0)))$
120	64 59 117 119	mpbir3and	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f *_{𝑝} (J) h \in ⋃ B$
121	1 2 3 4 115 65 69 91 67 120	pi1xfrval	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to G ([(f _{𝑝} (J) h)] ≃_{ph} (J)) = [(I _{𝑝} (J) ((f _{𝑝} (J) h) _{𝑝} (J) F))] ≃_{ph} (J)$
122		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
123	18	3ad2ant1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to F (1) \in X$
124		eqid	$⊢ +_{Q} = +_{Q}$
125	23	adantr	$⊢ (φ \land f \in ⋃ B) \to I \in (II Cn J)$
126	125 104 108	pcocn	$⊢ (φ \land f \in ⋃ B) \to I _{𝑝} (J) (f _{𝑝} (J) F) \in (II Cn J)$
127	126	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I _{𝑝} (J) (f _{𝑝} (J) F) \in (II Cn J)$
128	125 104	pco0	$⊢ (φ \land f \in ⋃ B) \to (I _{𝑝} (J) (f _{𝑝} (J) F)) (0) = I (0)$
129	24	adantr	$⊢ (φ \land f \in ⋃ B) \to I (0) = F (1)$
130	128 129	eqtrd	$⊢ (φ \land f \in ⋃ B) \to (I _{𝑝} (J) (f _{𝑝} (J) F)) (0) = F (1)$
131	130	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) (f _{𝑝} (J) F)) (0) = F (1)$
132	125 104	pco1	$⊢ (φ \land f \in ⋃ B) \to (I _{𝑝} (J) (f _{𝑝} (J) F)) (1) = (f *_{𝑝} (J) F) (1)$
133	50 103	pco1	$⊢ (φ \land f \in ⋃ B) \to (f *_{𝑝} (J) F) (1) = F (1)$
134	132 133	eqtrd	$⊢ (φ \land f \in ⋃ B) \to (I _{𝑝} (J) (f _{𝑝} (J) F)) (1) = F (1)$
135	134	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) (f _{𝑝} (J) F)) (1) = F (1)$
136		eqidd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to {Base}_{Q} = {Base}_{Q}$
137	2 115 123 136	pi1eluni	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) (f _{𝑝} (J) F) \in ⋃ {Base}_{Q} \leftrightarrow (I _{𝑝} (J) (f _{𝑝} (J) F) \in (II Cn J) \land (I _{𝑝} (J) (f _{𝑝} (J) F)) (0) = F (1) \land (I _{𝑝} (J) (f _{𝑝} (J) F)) (1) = F (1)))$
138	127 131 135 137	mpbir3and	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I _{𝑝} (J) (f _{𝑝} (J) F) \in ⋃ {Base}_{Q}$
139	69 83	pco1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) (h _{𝑝} (J) F)) (1) = (h *_{𝑝} (J) F) (1)$
140	55 65	pco1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (h *_{𝑝} (J) F) (1) = F (1)$
141	139 140	eqtrd	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) (h _{𝑝} (J) F)) (1) = F (1)$
142	2 115 123 136	pi1eluni	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to (I _{𝑝} (J) (h _{𝑝} (J) F) \in ⋃ {Base}_{Q} \leftrightarrow (I _{𝑝} (J) (h _{𝑝} (J) F) \in (II Cn J) \land (I _{𝑝} (J) (h _{𝑝} (J) F)) (0) = F (1) \land (I _{𝑝} (J) (h _{𝑝} (J) F)) (1) = F (1)))$
143	95 97 141 142	mpbir3and	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to I _{𝑝} (J) (h _{𝑝} (J) F) \in ⋃ {Base}_{Q}$
144	2 122 115 123 124 138 143	pi1addval	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to [(I _{𝑝} (J) (f _{𝑝} (J) F))] ≃_{ph} (J) +_{Q} [(I _{𝑝} (J) (h _{𝑝} (J) F))] ≃_{ph} (J) = [((I _{𝑝} (J) (f _{𝑝} (J) F)) _{𝑝} (J) (I _{𝑝} (J) (h *_{𝑝} (J) F)))] ≃_{ph} (J)$
145	114 121 144	3eqtr4d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to G ([(f _{𝑝} (J) h)] ≃_{ph} (J)) = [(I _{𝑝} (J) (f _{𝑝} (J) F))] ≃_{ph} (J) +_{Q} [(I _{𝑝} (J) (h *_{𝑝} (J) F))] ≃_{ph} (J)$
146	13	3ad2ant1	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to F (0) \in X$
147		eqid	$⊢ +_{P} = +_{P}$
148		simp2	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to f \in ⋃ B$
149		simp3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to h \in ⋃ B$
150	1 3 115 146 147 148 149	pi1addval	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to [f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J) = [(f *_{𝑝} (J) h)] ≃_{ph} (J)$
151	150	fveq2d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([(f *_{𝑝} (J) h)] ≃_{ph} (J))$
152	5	adantr	$⊢ (φ \land f \in ⋃ B) \to J \in TopOn (X)$
153	25	adantr	$⊢ (φ \land f \in ⋃ B) \to F (1) = I (0)$
154		simpr	$⊢ (φ \land f \in ⋃ B) \to f \in ⋃ B$
155	1 2 3 4 152 103 125 153 107 154	pi1xfrval	$⊢ (φ \land f \in ⋃ B) \to G ([f] ≃_{ph} (J)) = [(I _{𝑝} (J) (f _{𝑝} (J) F))] ≃_{ph} (J)$
156	155	3adant3	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to G ([f] ≃_{ph} (J)) = [(I _{𝑝} (J) (f _{𝑝} (J) F))] ≃_{ph} (J)$
157	1 2 3 4 115 65 69 91 67 149	pi1xfrval	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to G ([h] ≃_{ph} (J)) = [(I _{𝑝} (J) (h _{𝑝} (J) F))] ≃_{ph} (J)$
158	156 157	oveq12d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J)) = [(I _{𝑝} (J) (f _{𝑝} (J) F))] ≃_{ph} (J) +_{Q} [(I _{𝑝} (J) (h _{𝑝} (J) F))] ≃_{ph} (J)$
159	145 151 158	3eqtr4d	$⊢ (φ \land f \in ⋃ B \land h \in ⋃ B) \to G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J))$
160	159	3expa	$⊢ ((φ \land f \in ⋃ B) \land h \in ⋃ B) \to G ([f] ≃_{ph} (J) +_{P} [h] ≃_{ph} (J)) = G ([f] ≃_{ph} (J)) +_{Q} G ([h] ≃_{ph} (J))$
161	32 45 160	ectocld	$⊢ ((φ \land f \in ⋃ B) \land z \in (⋃ B / ≃_{ph} (J))) \to G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z)$
162	40 161	syldan	$⊢ ((φ \land f \in ⋃ B) \land z \in B) \to G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z)$
163	162	ralrimiva	$⊢ (φ \land f \in ⋃ B) \to \forall z \in B G ([f] ≃_{ph} (J) +_{P} z) = G ([f] ≃_{ph} (J)) +_{Q} G (z)$
164	32 37 163	ectocld	$⊢ (φ \land y \in (⋃ B / ≃_{ph} (J))) \to \forall z \in B G (y +_{P} z) = G (y) +_{Q} G (z)$
165	31 164	syldan	$⊢ (φ \land y \in B) \to \forall z \in B G (y +_{P} z) = G (y) +_{Q} G (z)$
166	165	ralrimiva	$⊢ φ \to \forall y \in B \forall z \in B G (y +_{P} z) = G (y) +_{Q} G (z)$
167	27 166	jca	$⊢ φ \to (G : B ⟶ {Base}_{Q} \land \forall y \in B \forall z \in B G (y +_{P} z) = G (y) +_{Q} G (z))$
168	3 122 147 124	isghm	$⊢ G \in (P GrpHom Q) \leftrightarrow ((P \in Grp \land Q \in Grp) \land (G : B ⟶ {Base}_{Q} \land \forall y \in B \forall z \in B G (y +_{P} z) = G (y) +_{Q} G (z)))$
169	15 20 167 168	syl21anbrc	$⊢ φ \to G \in (P GrpHom Q)$

Metamath Proof Explorer

Theorem pi1xfr

Proof