Metamath Proof Explorer

Theorem grpodivcl

Description: Closure of group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdivf.1	$⊢ X = ran G$
	grpdivf.3	$⊢ D = /_{g} (G)$
Assertion	grpodivcl	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D B \in X$

Step	Hyp	Ref	Expression
1		grpdivf.1	$⊢ X = ran G$
2		grpdivf.3	$⊢ D = /_{g} (G)$
3	1 2	grpodivf	$⊢ G \in GrpOp \to D : X \times X ⟶ X$
4		fovcdm	$⊢ (D : X \times X ⟶ X \land A \in X \land B \in X) \to A D B \in X$
5	3 4	syl3an1	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D B \in X$