# Metamath Proof Explorer

## Theorem 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 𝐺 = ( 𝐽 π1 𝑌 )
pi1inv.n 𝑁 = ( invg𝐺 )
pi1inv.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1inv.y ( 𝜑𝑌𝑋 )
pi1inv.f ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
pi1inv.0 ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝑌 )
pi1inv.1 ( 𝜑 → ( 𝐹 ‘ 1 ) = 𝑌 )
pi1inv.i 𝐼 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
Assertion pi1inv ( 𝜑 → ( 𝑁 ‘ [ 𝐹 ] ( ≃ph𝐽 ) ) = [ 𝐼 ] ( ≃ph𝐽 ) )

### Proof

Step Hyp Ref Expression
1 pi1grp.2 𝐺 = ( 𝐽 π1 𝑌 )
2 pi1inv.n 𝑁 = ( invg𝐺 )
3 pi1inv.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 pi1inv.y ( 𝜑𝑌𝑋 )
5 pi1inv.f ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
6 pi1inv.0 ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝑌 )
7 pi1inv.1 ( 𝜑 → ( 𝐹 ‘ 1 ) = 𝑌 )
8 pi1inv.i 𝐼 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
9 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10 eqid ( +g𝐺 ) = ( +g𝐺 )
11 8 pcorevcl ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐼 ∈ ( II Cn 𝐽 ) ∧ ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
12 5 11 syl ( 𝜑 → ( 𝐼 ∈ ( II Cn 𝐽 ) ∧ ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )
13 12 simp1d ( 𝜑𝐼 ∈ ( II Cn 𝐽 ) )
14 12 simp2d ( 𝜑 → ( 𝐼 ‘ 0 ) = ( 𝐹 ‘ 1 ) )
15 14 7 eqtrd ( 𝜑 → ( 𝐼 ‘ 0 ) = 𝑌 )
16 12 simp3d ( 𝜑 → ( 𝐼 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
17 16 6 eqtrd ( 𝜑 → ( 𝐼 ‘ 1 ) = 𝑌 )
18 9 a1i ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
19 1 3 4 18 pi1eluni ( 𝜑 → ( 𝐼 ( Base ‘ 𝐺 ) ↔ ( 𝐼 ∈ ( II Cn 𝐽 ) ∧ ( 𝐼 ‘ 0 ) = 𝑌 ∧ ( 𝐼 ‘ 1 ) = 𝑌 ) ) )
20 13 15 17 19 mpbir3and ( 𝜑𝐼 ( Base ‘ 𝐺 ) )
21 1 3 4 18 pi1eluni ( 𝜑 → ( 𝐹 ( Base ‘ 𝐺 ) ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) )
22 5 6 7 21 mpbir3and ( 𝜑𝐹 ( Base ‘ 𝐺 ) )
23 1 9 3 4 10 20 22 pi1addval ( 𝜑 → ( [ 𝐼 ] ( ≃ph𝐽 ) ( +g𝐺 ) [ 𝐹 ] ( ≃ph𝐽 ) ) = [ ( 𝐼 ( *𝑝𝐽 ) 𝐹 ) ] ( ≃ph𝐽 ) )
24 phtpcer ( ≃ph𝐽 ) Er ( II Cn 𝐽 )
25 24 a1i ( 𝜑 → ( ≃ph𝐽 ) Er ( II Cn 𝐽 ) )
26 eqid ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 1 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 1 ) } )
27 8 26 pcorev ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐼 ( *𝑝𝐽 ) 𝐹 ) ( ≃ph𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 1 ) } ) )
28 5 27 syl ( 𝜑 → ( 𝐼 ( *𝑝𝐽 ) 𝐹 ) ( ≃ph𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 1 ) } ) )
29 7 sneqd ( 𝜑 → { ( 𝐹 ‘ 1 ) } = { 𝑌 } )
30 29 xpeq2d ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 1 ) } ) = ( ( 0 [,] 1 ) × { 𝑌 } ) )
31 28 30 breqtrd ( 𝜑 → ( 𝐼 ( *𝑝𝐽 ) 𝐹 ) ( ≃ph𝐽 ) ( ( 0 [,] 1 ) × { 𝑌 } ) )
32 25 31 erthi ( 𝜑 → [ ( 𝐼 ( *𝑝𝐽 ) 𝐹 ) ] ( ≃ph𝐽 ) = [ ( ( 0 [,] 1 ) × { 𝑌 } ) ] ( ≃ph𝐽 ) )
33 eqid ( ( 0 [,] 1 ) × { 𝑌 } ) = ( ( 0 [,] 1 ) × { 𝑌 } )
34 1 9 3 4 33 pi1grplem ( 𝜑 → ( 𝐺 ∈ Grp ∧ [ ( ( 0 [,] 1 ) × { 𝑌 } ) ] ( ≃ph𝐽 ) = ( 0g𝐺 ) ) )
35 34 simprd ( 𝜑 → [ ( ( 0 [,] 1 ) × { 𝑌 } ) ] ( ≃ph𝐽 ) = ( 0g𝐺 ) )
36 23 32 35 3eqtrd ( 𝜑 → ( [ 𝐼 ] ( ≃ph𝐽 ) ( +g𝐺 ) [ 𝐹 ] ( ≃ph𝐽 ) ) = ( 0g𝐺 ) )
37 34 simpld ( 𝜑𝐺 ∈ Grp )
38 1 9 3 4 5 6 7 elpi1i ( 𝜑 → [ 𝐹 ] ( ≃ph𝐽 ) ∈ ( Base ‘ 𝐺 ) )
39 1 9 3 4 13 15 17 elpi1i ( 𝜑 → [ 𝐼 ] ( ≃ph𝐽 ) ∈ ( Base ‘ 𝐺 ) )
40 eqid ( 0g𝐺 ) = ( 0g𝐺 )
41 9 10 40 2 grpinvid2 ( ( 𝐺 ∈ Grp ∧ [ 𝐹 ] ( ≃ph𝐽 ) ∈ ( Base ‘ 𝐺 ) ∧ [ 𝐼 ] ( ≃ph𝐽 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑁 ‘ [ 𝐹 ] ( ≃ph𝐽 ) ) = [ 𝐼 ] ( ≃ph𝐽 ) ↔ ( [ 𝐼 ] ( ≃ph𝐽 ) ( +g𝐺 ) [ 𝐹 ] ( ≃ph𝐽 ) ) = ( 0g𝐺 ) ) )
42 37 38 39 41 syl3anc ( 𝜑 → ( ( 𝑁 ‘ [ 𝐹 ] ( ≃ph𝐽 ) ) = [ 𝐼 ] ( ≃ph𝐽 ) ↔ ( [ 𝐼 ] ( ≃ph𝐽 ) ( +g𝐺 ) [ 𝐹 ] ( ≃ph𝐽 ) ) = ( 0g𝐺 ) ) )
43 36 42 mpbird ( 𝜑 → ( 𝑁 ‘ [ 𝐹 ] ( ≃ph𝐽 ) ) = [ 𝐼 ] ( ≃ph𝐽 ) )