Theorem mulgcld

Description: Deduction associated with mulgcl . (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	mulgcld.1	$$⊢B={\mathrm{Base}}_G$$
	mulgcld.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgcld.3	$$⊢\phi \to G\in \mathrm{Grp}$$
	mulgcld.4	$$⊢\phi \to N\in \mathbb{Z}$$
	mulgcld.5	$$⊢\phi \to X\in B$$
Assertion	mulgcld	$$⊢\phi \to N\underset{\dot{}}{·}X\in B$$

Proof

Step	Hyp	Ref	Expression
1		mulgcld.1	$$⊢B={\mathrm{Base}}_G$$
2		mulgcld.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgcld.3	$$⊢\phi \to G\in \mathrm{Grp}$$
4		mulgcld.4	$$⊢\phi \to N\in \mathbb{Z}$$
5		mulgcld.5	$$⊢\phi \to X\in B$$
6	1 2	mulgcl	$$⊢\left(G\in \mathrm{Grp}\wedge N\in \mathbb{Z}\wedge X\in B\right)\to N\underset{\dot{}}{·}X\in B$$
7	3 4 5 6	syl3anc	$$⊢\phi \to N\underset{\dot{}}{·}X\in B$$