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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatring.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion	pmatassa	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ AssAlg )

Proof

Step	Hyp	Ref	Expression
1		pmatring.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmatring.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3	1	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
4	2	matassa	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝐶 ∈ AssAlg )
5	3 4	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ AssAlg )