Metamath Proof Explorer

Theorem pmatlmod

Description: The set of polynomial matrices over a ring is a left module. (Contributed by AV, 6-Nov-2019)

	Ref	Expression
Hypotheses	pmatring.p	$⊢ P = {Poly}_{1} (R)$
	pmatring.c	$⊢ C = N Mat P$
Assertion	pmatlmod	$⊢ (N \in Fin \land R \in Ring) \to C \in LMod$

Step	Hyp	Ref	Expression
1		pmatring.p	$⊢ P = {Poly}_{1} (R)$
2		pmatring.c	$⊢ C = N Mat P$
3	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
4	2	matlmod	$⊢ (N \in Fin \land P \in Ring) \to C \in LMod$
5	3 4	sylan2	$⊢ (N \in Fin \land R \in Ring) \to C \in LMod$