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 
|- G = ( J pi1 Y )
pi1inv.n 
|- N = ( invg ` G )
pi1inv.j 
|- ( ph -> J e. ( TopOn ` X ) )
pi1inv.y 
|- ( ph -> Y e. X )
pi1inv.f 
|- ( ph -> F e. ( II Cn J ) )
pi1inv.0 
|- ( ph -> ( F ` 0 ) = Y )
pi1inv.1 
|- ( ph -> ( F ` 1 ) = Y )
pi1inv.i 
|- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
Assertion pi1inv 
|- ( ph -> ( N ` [ F ] ( ~=ph ` J ) ) = [ I ] ( ~=ph ` J ) )

Proof

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