Theorem grpsubcl

Description: Closure of group subtraction. (Contributed by NM, 31-Mar-2014)

	Ref	Expression
Hypotheses	grpsubcl.b	$$⊢B={\mathrm{Base}}_G$$
	grpsubcl.m	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	grpsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		grpsubcl.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubcl.m	$$⊢\underset{\dot{}}{-}={-}_G$$
3	1 2	grpsubf	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{-}:B\times B⟶B$$
4		fovrn	$$⊢\left(\underset{\dot{}}{-}:B\times B⟶B\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y\in B$$
5	3 4	syl3an1	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y\in B$$