This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpinvf

Description: The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015)

Ref Expression
Hypotheses grpinvcl.b 
|- B = ( Base ` G )
grpinvcl.n 
|- N = ( invg ` G )
Assertion grpinvf 
|- ( G e. Grp -> N : B --> B )

Proof

Step Hyp Ref Expression
1 grpinvcl.b 
 |-  B = ( Base ` G )
2 grpinvcl.n 
 |-  N = ( invg ` G )
3 eqid 
 |-  ( +g ` G ) = ( +g ` G )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 1 3 4 grpinveu 
 |-  ( ( G e. Grp /\ x e. B ) -> E! y e. B ( y ( +g ` G ) x ) = ( 0g ` G ) )
6 riotacl 
 |-  ( E! y e. B ( y ( +g ` G ) x ) = ( 0g ` G ) -> ( iota_ y e. B ( y ( +g ` G ) x ) = ( 0g ` G ) ) e. B )
7 5 6 syl 
 |-  ( ( G e. Grp /\ x e. B ) -> ( iota_ y e. B ( y ( +g ` G ) x ) = ( 0g ` G ) ) e. B )
8 1 3 4 2 grpinvfval 
 |-  N = ( x e. B |-> ( iota_ y e. B ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
9 7 8 fmptd 
 |-  ( G e. Grp -> N : B --> B )