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 )