Metamath Proof Explorer

Theorem pmatassa

Description: The set of polynomial matrices over a commutative ring is an associative algebra. (Contributed by AV, 16-Jun-2024)

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

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