Metamath Proof Explorer

Theorem ply1tmcl

Description: Closure of the expression for a univariate polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015) (Proof shortened by AV, 25-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		ply1tmcl.k	$⊢ K = {Base}_{R}$
2		ply1tmcl.p	$⊢ P = {Poly}_{1} (R)$
3		ply1tmcl.x	$⊢ X = {var}_{1} (R)$
4		ply1tmcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		ply1tmcl.n	$⊢ N = {mulGrp}_{P}$
6		ply1tmcl.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
7		ply1tmcl.b	$⊢ B = {Base}_{P}$
8	2	ply1lmod	$⊢ R \in Ring \to P \in LMod$
9	8	3ad2ant1	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to P \in LMod$
10		simp2	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \in K$
11	2 3 5 6 7	ply1moncl	$⊢ (R \in Ring \land D \in ℕ_{0}) \to D \underset{˙}{\times} X \in B$
12	11	3adant2	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to D \underset{˙}{\times} X \in B$
13	2	ply1sca2	$⊢ I (R) = Scalar (P)$
14		df-base	$⊢ Base = Slot 1$
15	14 1	strfvi	$⊢ K = {Base}_{I (R)}$
16	7 13 4 15	lmodvscl	$⊢ (P \in LMod \land C \in K \land D \underset{˙}{\times} X \in B) \to C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in B$
17	9 10 12 16	syl3anc	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in B$