Theorem grpinvfn

Description: Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	grpinvfn.b	|- B = ( Base ` G )
	grpinvfn.n	|- N = ( invg ` G )
Assertion	grpinvfn	|- N Fn B

Proof

Step	Hyp	Ref	Expression
1		grpinvfn.b	|- B = ( Base ` G )
2		grpinvfn.n	|- N = ( invg ` G )
3		riotaex	|- ( iota_ y e. B ( y ( +g ` G ) x ) = ( 0g ` G ) ) e. _V
4		eqid	|- ( +g ` G ) = ( +g ` G )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6	1 4 5 2	grpinvfval	|- N = ( x e. B |-> ( iota_ y e. B ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
7	3 6	fnmpti	|- N Fn B