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

Metamath Proof Explorer

Theorem mulgnn0cld

Description: Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl . (Contributed by SN, 1-Feb-2025)

	Ref	Expression
Hypotheses	mulgnn0cld.b	$⊢ B = {Base}_{G}$
	mulgnn0cld.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnn0cld.m	$⊢ φ \to G \in Mnd$
	mulgnn0cld.n	$⊢ φ \to N \in ℕ_{0}$
	mulgnn0cld.x	$⊢ φ \to X \in B$
Assertion	mulgnn0cld	$⊢ φ \to N \underset{˙}{\cdot} X \in B$

Proof

Step	Hyp	Ref	Expression
1		mulgnn0cld.b	$⊢ B = {Base}_{G}$
2		mulgnn0cld.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgnn0cld.m	$⊢ φ \to G \in Mnd$
4		mulgnn0cld.n	$⊢ φ \to N \in ℕ_{0}$
5		mulgnn0cld.x	$⊢ φ \to X \in B$
6	1 2	mulgnn0cl	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to N \underset{˙}{\cdot} X \in B$
7	3 4 5 6	syl3anc	$⊢ φ \to N \underset{˙}{\cdot} X \in B$