Theorem ply1moncl

Description: Closure of the expression for a univariate primitive monomial. (Contributed by AV, 14-Aug-2019)

	Ref	Expression
Hypotheses	ply1moncl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1moncl.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	ply1moncl.n	$$⊢N={\mathrm{mulGrp}}_P$$
	ply1moncl.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
	ply1moncl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	ply1moncl	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to D\underset{\dot{}}{\times }X\in B$$

Proof

Step	Hyp	Ref	Expression
1		ply1moncl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1moncl.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
3		ply1moncl.n	$$⊢N={\mathrm{mulGrp}}_P$$
4		ply1moncl.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
5		ply1moncl.b	$$⊢B={\mathrm{Base}}_P$$
6	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
7	3	ringmgp	$$⊢P\in \mathrm{Ring}\to N\in \mathrm{Mnd}$$
8	6 7	syl	$$⊢R\in \mathrm{Ring}\to N\in \mathrm{Mnd}$$
9	8	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to N\in \mathrm{Mnd}$$
10		simpr	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to D\in {\mathbb{N}}_0$$
11	2 1 5	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
12	11	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to X\in B$$
13	3 5	mgpbas	$$⊢B={\mathrm{Base}}_N$$
14	13 4	mulgnn0cl	$$⊢\left(N\in \mathrm{Mnd}\wedge D\in {\mathbb{N}}_0\wedge X\in B\right)\to D\underset{\dot{}}{\times }X\in B$$
15	9 10 12 14	syl3anc	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to D\underset{\dot{}}{\times }X\in B$$