pconnpi1

Description: All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015)

	Ref	Expression
Hypotheses	pconnpi1.x	$⊢ X = ⋃ J$
	pconnpi1.p	$⊢ P = J π_{1} A$
	pconnpi1.q	$⊢ Q = J π_{1} B$
	pconnpi1.s	$⊢ S = {Base}_{P}$
	pconnpi1.t	$⊢ T = {Base}_{Q}$
Assertion	pconnpi1	$⊢ (J \in PConn \land A \in X \land B \in X) \to P ≃_{𝑔} Q$

Proof

Step	Hyp	Ref	Expression
1		pconnpi1.x	$⊢ X = ⋃ J$
2		pconnpi1.p	$⊢ P = J π_{1} A$
3		pconnpi1.q	$⊢ Q = J π_{1} B$
4		pconnpi1.s	$⊢ S = {Base}_{P}$
5		pconnpi1.t	$⊢ T = {Base}_{Q}$
6	1	pconncn	$⊢ (J \in PConn \land A \in X \land B \in X) \to \exists f \in (II Cn J) (f (0) = A \land f (1) = B)$
7		eqid	$⊢ J π_{1} f (0) = J π_{1} f (0)$
8		eqid	$⊢ J π_{1} f (1) = J π_{1} f (1)$
9		eqid	$⊢ {Base}_{(J π_{1} f (0))} = {Base}_{(J π_{1} f (0))}$
10		eqid	$⊢ ran (h \in ⋃ {Base}_{(J π_{1} f (0))} ⟼ ⟨[h] ≃_{ph} (J), [((x \in [0, 1] ⟼ f (1 - x)) _{𝑝} (J) (h _{𝑝} (J) f))] ≃_{ph} (J)⟩) = ran (h \in ⋃ {Base}_{(J π_{1} f (0))} ⟼ ⟨[h] ≃_{ph} (J), [((x \in [0, 1] ⟼ f (1 - x)) _{𝑝} (J) (h _{𝑝} (J) f))] ≃_{ph} (J)⟩)$
11		simpl1	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to J \in PConn$
12		pconntop	$⊢ J \in PConn \to J \in Top$
13	11 12	syl	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to J \in Top$
14	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
15	13 14	sylib	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to J \in TopOn (X)$
16		simprl	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to f \in (II Cn J)$
17		oveq2	$⊢ x = y \to 1 - x = 1 - y$
18	17	fveq2d	$⊢ x = y \to f (1 - x) = f (1 - y)$
19	18	cbvmptv	$⊢ (x \in [0, 1] ⟼ f (1 - x)) = (y \in [0, 1] ⟼ f (1 - y))$
20	7 8 9 10 15 16 19	pi1xfrgim	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to ran (h \in ⋃ {Base}_{(J π_{1} f (0))} ⟼ ⟨[h] ≃_{ph} (J), [((x \in [0, 1] ⟼ f (1 - x)) _{𝑝} (J) (h _{𝑝} (J) f))] ≃_{ph} (J)⟩) \in ((J π_{1} f (0)) GrpIso (J π_{1} f (1)))$
21		simprrl	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to f (0) = A$
22	21	oveq2d	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to J π_{1} f (0) = J π_{1} A$
23	22 2	eqtr4di	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to J π_{1} f (0) = P$
24		simprrr	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to f (1) = B$
25	24	oveq2d	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to J π_{1} f (1) = J π_{1} B$
26	25 3	eqtr4di	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to J π_{1} f (1) = Q$
27	23 26	oveq12d	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to (J π_{1} f (0)) GrpIso (J π_{1} f (1)) = P GrpIso Q$
28	20 27	eleqtrd	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to ran (h \in ⋃ {Base}_{(J π_{1} f (0))} ⟼ ⟨[h] ≃_{ph} (J), [((x \in [0, 1] ⟼ f (1 - x)) _{𝑝} (J) (h _{𝑝} (J) f))] ≃_{ph} (J)⟩) \in (P GrpIso Q)$
29		brgici	$⊢ ran (h \in ⋃ {Base}_{(J π_{1} f (0))} ⟼ ⟨[h] ≃_{ph} (J), [((x \in [0, 1] ⟼ f (1 - x)) _{𝑝} (J) (h _{𝑝} (J) f))] ≃_{ph} (J)⟩) \in (P GrpIso Q) \to P ≃_{𝑔} Q$
30	28 29	syl	$⊢ ((J \in PConn \land A \in X \land B \in X) \land (f \in (II Cn J) \land (f (0) = A \land f (1) = B))) \to P ≃_{𝑔} Q$
31	6 30	rexlimddv	$⊢ (J \in PConn \land A \in X \land B \in X) \to P ≃_{𝑔} Q$

Metamath Proof Explorer

Theorem pconnpi1

Proof