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

Metamath Proof Explorer

Theorem grpcl

Description: Closure of the operation of a group. (Contributed by NM, 14-Aug-2011)

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

Step	Hyp	Ref	Expression
1		grpcl.b	$⊢ B = {Base}_{G}$
2		grpcl.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpmnd	$⊢ G \in Grp \to G \in Mnd$
4	1 2	mndcl	$⊢ (G \in Mnd \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$