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={\mathrm{Base}}_G$$
	grpinvcl.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	grpinvf	$$⊢G\in \mathrm{Grp}\to N:B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		grpinvcl.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinvcl.n	$$⊢N={inv}_g\left(G\right)$$
3		eqid	$$⊢{+}_G={+}_G$$
4		eqid	$$⊢0_G=0_G$$
5	1 3 4	grpinveu	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \exists !y\in By{+}_{G}x=0_G$$
6		riotacl	$$⊢\exists !y\in By{+}_{G}x=0_G\to \left(\iota y\in B|y{+}_{G}x=0_G\right)\in B$$
7	5 6	syl	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \left(\iota y\in B|y{+}_{G}x=0_G\right)\in B$$
8	1 3 4 2	grpinvfval	$$⊢N=\left(x\in B⟼\left(\iota y\in B|y{+}_{G}x=0_G\right)\right)$$
9	7 8	fmptd	$$⊢G\in \mathrm{Grp}\to N:B⟶B$$