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 ‘ 𝐽 ) )