Theorem 1pmatscmul

Description: The scalar product of the identity polynomial matrix with a polynomial is a polynomial matrix. (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	1pmatscmul.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	1pmatscmul.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	1pmatscmul.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	1pmatscmul.e	⊢ 𝐸 = ( Base ‘ 𝑃 )
	1pmatscmul.m	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
	1pmatscmul.1	⊢ 1 = ( 1r ‘ 𝐶 )
Assertion	1pmatscmul	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → ( 𝑄 ∗ 1 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		1pmatscmul.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		1pmatscmul.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		1pmatscmul.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		1pmatscmul.e	⊢ 𝐸 = ( Base ‘ 𝑃 )
5		1pmatscmul.m	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
6		1pmatscmul.1	⊢ 1 = ( 1r ‘ 𝐶 )
7	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
8	7	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
9	8	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
10		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → 𝑄 ∈ 𝐸 )
11	1 2	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
12	11	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → 𝐶 ∈ Ring )
13	3 6	ringidcl	⊢ ( 𝐶 ∈ Ring → 1 ∈ 𝐵 )
14	12 13	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → 1 ∈ 𝐵 )
15	4 2 3 5	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( 𝑄 ∈ 𝐸 ∧ 1 ∈ 𝐵 ) ) → ( 𝑄 ∗ 1 ) ∈ 𝐵 )
16	9 10 14 15	syl12anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → ( 𝑄 ∗ 1 ) ∈ 𝐵 )