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	3 5	mgpbas	$$⊢B={\mathrm{Base}}_N$$
7	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
8	3	ringmgp	$$⊢P\in \mathrm{Ring}\to N\in \mathrm{Mnd}$$
9	7 8	syl	$$⊢R\in \mathrm{Ring}\to N\in \mathrm{Mnd}$$
10	9	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to N\in \mathrm{Mnd}$$
11		simpr	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to D\in {\mathbb{N}}_0$$
12	2 1 5	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
13	12	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to X\in B$$
14	6 4 10 11 13	mulgnn0cld	$$⊢\left(R\in \mathrm{Ring}\wedge D\in {\mathbb{N}}_0\right)\to D\underset{\dot{}}{\times }X\in B$$