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 = ( Poly1 ` R )
	pmatring.c	|- C = ( N Mat P )
Assertion	pmatassa	|- ( ( N e. Fin /\ R e. CRing ) -> C e. AssAlg )

Proof

Step	Hyp	Ref	Expression
1		pmatring.p	|- P = ( Poly1 ` R )
2		pmatring.c	|- C = ( N Mat P )
3	1	ply1crng	|- ( R e. CRing -> P e. CRing )
4	2	matassa	|- ( ( N e. Fin /\ P e. CRing ) -> C e. AssAlg )
5	3 4	sylan2	|- ( ( N e. Fin /\ R e. CRing ) -> C e. AssAlg )