Theorem grpinvfn

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

	Ref	Expression
Hypotheses	grpinvfn.b	$$⊢B={\mathrm{Base}}_G$$
	grpinvfn.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	grpinvfn	$$⊢NFnB$$

Proof

Step	Hyp	Ref	Expression
1		grpinvfn.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinvfn.n	$$⊢N={inv}_g\left(G\right)$$
3		riotaex	$$⊢\left(\iota y\in B|y{+}_{G}x=0_G\right)\in \mathrm{V}$$
4		eqid	$$⊢{+}_G={+}_G$$
5		eqid	$$⊢0_G=0_G$$
6	1 4 5 2	grpinvfval	$$⊢N=\left(x\in B⟼\left(\iota y\in B|y{+}_{G}x=0_G\right)\right)$$
7	3 6	fnmpti	$$⊢NFnB$$