Theorem grpsubf

Description: Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Hypotheses	grpsubcl.b	$$⊢B={\mathrm{Base}}_G$$
	grpsubcl.m	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	grpsubf	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{-}:B\times B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		grpsubcl.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubcl.m	$$⊢\underset{\dot{}}{-}={-}_G$$
3		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
4	1 3	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge y\in B\right)\to {inv}_g\left(G\right)\left(y\right)\in B$$
5	4	3adant2	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\wedge y\in B\right)\to {inv}_g\left(G\right)\left(y\right)\in B$$
6		eqid	$$⊢{+}_G={+}_G$$
7	1 6	grpcl	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\wedge {inv}_g\left(G\right)\left(y\right)\in B\right)\to x{+}_G{inv}_g\left(G\right)\left(y\right)\in B$$
8	5 7	syld3an3	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\wedge y\in B\right)\to x{+}_G{inv}_g\left(G\right)\left(y\right)\in B$$
9	8	3expb	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_G{inv}_g\left(G\right)\left(y\right)\in B$$
10	9	ralrimivva	$$⊢G\in \mathrm{Grp}\to \forall x\in B\forall y\in Bx{+}_G{inv}_g\left(G\right)\left(y\right)\in B$$
11	1 6 3 2	grpsubfval	$$⊢\underset{\dot{}}{-}=\left(x\in B,y\in B⟼x{+}_G{inv}_g\left(G\right)\left(y\right)\right)$$
12	11	fmpo	$$⊢\forall x\in B\forall y\in Bx{+}_G{inv}_g\left(G\right)\left(y\right)\in B\leftrightarrow \underset{\dot{}}{-}:B\times B⟶B$$
13	10 12	sylib	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{-}:B\times B⟶B$$