pi1inv

Description: An inverse in the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015) (Revised by Mario Carneiro, 10-Aug-2015)

	Ref	Expression
Hypotheses	pi1grp.2	$⊢ G = J π_{1} Y$
	pi1inv.n	$⊢ N = {inv}_{g} (G)$
	pi1inv.j	$⊢ φ \to J \in TopOn (X)$
	pi1inv.y	$⊢ φ \to Y \in X$
	pi1inv.f	$⊢ φ \to F \in (II Cn J)$
	pi1inv.0	$⊢ φ \to F (0) = Y$
	pi1inv.1	$⊢ φ \to F (1) = Y$
	pi1inv.i	$⊢ I = (x \in [0, 1] ⟼ F (1 - x))$
Assertion	pi1inv	$⊢ φ \to N ([F] ≃_{ph} (J)) = [I] ≃_{ph} (J)$

Proof

Step	Hyp	Ref	Expression
1		pi1grp.2	$⊢ G = J π_{1} Y$
2		pi1inv.n	$⊢ N = {inv}_{g} (G)$
3		pi1inv.j	$⊢ φ \to J \in TopOn (X)$
4		pi1inv.y	$⊢ φ \to Y \in X$
5		pi1inv.f	$⊢ φ \to F \in (II Cn J)$
6		pi1inv.0	$⊢ φ \to F (0) = Y$
7		pi1inv.1	$⊢ φ \to F (1) = Y$
8		pi1inv.i	$⊢ I = (x \in [0, 1] ⟼ F (1 - x))$
9		eqid	$⊢ {Base}_{G} = {Base}_{G}$
10		eqid	$⊢ +_{G} = +_{G}$
11	8	pcorevcl	$⊢ F \in (II Cn J) \to (I \in (II Cn J) \land I (0) = F (1) \land I (1) = F (0))$
12	5 11	syl	$⊢ φ \to (I \in (II Cn J) \land I (0) = F (1) \land I (1) = F (0))$
13	12	simp1d	$⊢ φ \to I \in (II Cn J)$
14	12	simp2d	$⊢ φ \to I (0) = F (1)$
15	14 7	eqtrd	$⊢ φ \to I (0) = Y$
16	12	simp3d	$⊢ φ \to I (1) = F (0)$
17	16 6	eqtrd	$⊢ φ \to I (1) = Y$
18	9	a1i	$⊢ φ \to {Base}_{G} = {Base}_{G}$
19	1 3 4 18	pi1eluni	$⊢ φ \to (I \in ⋃ {Base}_{G} \leftrightarrow (I \in (II Cn J) \land I (0) = Y \land I (1) = Y))$
20	13 15 17 19	mpbir3and	$⊢ φ \to I \in ⋃ {Base}_{G}$
21	1 3 4 18	pi1eluni	$⊢ φ \to (F \in ⋃ {Base}_{G} \leftrightarrow (F \in (II Cn J) \land F (0) = Y \land F (1) = Y))$
22	5 6 7 21	mpbir3and	$⊢ φ \to F \in ⋃ {Base}_{G}$
23	1 9 3 4 10 20 22	pi1addval	$⊢ φ \to [I] ≃_{ph} (J) +_{G} [F] ≃_{ph} (J) = [(I *_{𝑝} (J) F)] ≃_{ph} (J)$
24		phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$
25	24	a1i	$⊢ φ \to ≃_{ph} (J) Er (II Cn J)$
26		eqid	$⊢ [0, 1] \times \{F (1)\} = [0, 1] \times \{F (1)\}$
27	8 26	pcorev	$⊢ F \in (II Cn J) \to (I *_{𝑝} (J) F) ≃_{ph} (J) ([0, 1] \times \{F (1)\})$
28	5 27	syl	$⊢ φ \to (I *_{𝑝} (J) F) ≃_{ph} (J) ([0, 1] \times \{F (1)\})$
29	7	sneqd	$⊢ φ \to \{F (1)\} = \{Y\}$
30	29	xpeq2d	$⊢ φ \to [0, 1] \times \{F (1)\} = [0, 1] \times \{Y\}$
31	28 30	breqtrd	$⊢ φ \to (I *_{𝑝} (J) F) ≃_{ph} (J) ([0, 1] \times \{Y\})$
32	25 31	erthi	$⊢ φ \to [(I *_{𝑝} (J) F)] ≃_{ph} (J) = [([0, 1] \times \{Y\})] ≃_{ph} (J)$
33		eqid	$⊢ [0, 1] \times \{Y\} = [0, 1] \times \{Y\}$
34	1 9 3 4 33	pi1grplem	$⊢ φ \to (G \in Grp \land [([0, 1] \times \{Y\})] ≃_{ph} (J) = 0_{G})$
35	34	simprd	$⊢ φ \to [([0, 1] \times \{Y\})] ≃_{ph} (J) = 0_{G}$
36	23 32 35	3eqtrd	$⊢ φ \to [I] ≃_{ph} (J) +_{G} [F] ≃_{ph} (J) = 0_{G}$
37	34	simpld	$⊢ φ \to G \in Grp$
38	1 9 3 4 5 6 7	elpi1i	$⊢ φ \to [F] ≃_{ph} (J) \in {Base}_{G}$
39	1 9 3 4 13 15 17	elpi1i	$⊢ φ \to [I] ≃_{ph} (J) \in {Base}_{G}$
40		eqid	$⊢ 0_{G} = 0_{G}$
41	9 10 40 2	grpinvid2	$⊢ (G \in Grp \land [F] ≃_{ph} (J) \in {Base}_{G} \land [I] ≃_{ph} (J) \in {Base}_{G}) \to (N ([F] ≃_{ph} (J)) = [I] ≃_{ph} (J) \leftrightarrow [I] ≃_{ph} (J) +_{G} [F] ≃_{ph} (J) = 0_{G})$
42	37 38 39 41	syl3anc	$⊢ φ \to (N ([F] ≃_{ph} (J)) = [I] ≃_{ph} (J) \leftrightarrow [I] ≃_{ph} (J) +_{G} [F] ≃_{ph} (J) = 0_{G})$
43	36 42	mpbird	$⊢ φ \to N ([F] ≃_{ph} (J)) = [I] ≃_{ph} (J)$

Metamath Proof Explorer

Theorem pi1inv

Proof