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

Metamath Proof Explorer

Theorem mulgnncl

Description: Closure of the group multiple (exponentiation) operation for a positive multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014) (Revised by AV, 29-Aug-2021)

	Ref	Expression
Hypotheses	mulgnncl.b	$⊢ B = {Base}_{G}$
	mulgnncl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mulgnncl	$⊢ (G \in Mgm \land N \in ℕ \land X \in B) \to N \underset{˙}{\cdot} X \in B$

Proof

Step	Hyp	Ref	Expression
1		mulgnncl.b	$⊢ B = {Base}_{G}$
2		mulgnncl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		eqid	$⊢ +_{G} = +_{G}$
4		id	$⊢ G \in Mgm \to G \in Mgm$
5		ssidd	$⊢ G \in Mgm \to B \subseteq B$
6	1 3	mgmcl	$⊢ (G \in Mgm \land x \in B \land y \in B) \to x +_{G} y \in B$
7	1 2 3 4 5 6	mulgnnsubcl	$⊢ (G \in Mgm \land N \in ℕ \land X \in B) \to N \underset{˙}{\cdot} X \in B$