ply1moncl

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

	Ref	Expression
Hypotheses	ply1moncl.p	$⊢ P = {Poly}_{1} (R)$
	ply1moncl.x	$⊢ X = {var}_{1} (R)$
	ply1moncl.n	$⊢ N = {mulGrp}_{P}$
	ply1moncl.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
	ply1moncl.b	$⊢ B = {Base}_{P}$
Assertion	ply1moncl	$⊢ (R \in Ring \land D \in ℕ_{0}) \to D \underset{˙}{\times} X \in B$

Step	Hyp	Ref	Expression
1		ply1moncl.p	$⊢ P = {Poly}_{1} (R)$
2		ply1moncl.x	$⊢ X = {var}_{1} (R)$
3		ply1moncl.n	$⊢ N = {mulGrp}_{P}$
4		ply1moncl.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
5		ply1moncl.b	$⊢ B = {Base}_{P}$
6	3 5	mgpbas	$⊢ B = {Base}_{N}$
7	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
8	3	ringmgp	$⊢ P \in Ring \to N \in Mnd$
9	7 8	syl	$⊢ R \in Ring \to N \in Mnd$
10	9	adantr	$⊢ (R \in Ring \land D \in ℕ_{0}) \to N \in Mnd$
11		simpr	$⊢ (R \in Ring \land D \in ℕ_{0}) \to D \in ℕ_{0}$
12	2 1 5	vr1cl	$⊢ R \in Ring \to X \in B$
13	12	adantr	$⊢ (R \in Ring \land D \in ℕ_{0}) \to X \in B$
14	6 4 10 11 13	mulgnn0cld	$⊢ (R \in Ring \land D \in ℕ_{0}) \to D \underset{˙}{\times} X \in B$

Metamath Proof Explorer