This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpsubcl

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

	Ref	Expression
Hypotheses	grpsubcl.b	$⊢ B = {Base}_{G}$
	grpsubcl.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	grpsubcl	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{-} Y \in B$

Step	Hyp	Ref	Expression
1		grpsubcl.b	$⊢ B = {Base}_{G}$
2		grpsubcl.m	$⊢ \underset{˙}{-} = -_{G}$
3	1 2	grpsubf	$⊢ G \in Grp \to \underset{˙}{-} : B \times B ⟶ B$
4		fovcdm	$⊢ (\underset{˙}{-} : B \times B ⟶ B \land X \in B \land Y \in B) \to X \underset{˙}{-} Y \in B$
5	3 4	syl3an1	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{-} Y \in B$