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	|- P = ( Poly1 ` R )
	1pmatscmul.c	|- C = ( N Mat P )
	1pmatscmul.b	|- B = ( Base ` C )
	1pmatscmul.e	|- E = ( Base ` P )
	1pmatscmul.m	|- .* = ( .s ` C )
	1pmatscmul.1	|- .1. = ( 1r ` C )
Assertion	1pmatscmul	|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> ( Q .* .1. ) e. B )

Proof

Step	Hyp	Ref	Expression
1		1pmatscmul.p	|- P = ( Poly1 ` R )
2		1pmatscmul.c	|- C = ( N Mat P )
3		1pmatscmul.b	|- B = ( Base ` C )
4		1pmatscmul.e	|- E = ( Base ` P )
5		1pmatscmul.m	|- .* = ( .s ` C )
6		1pmatscmul.1	|- .1. = ( 1r ` C )
7	1	ply1ring	|- ( R e. Ring -> P e. Ring )
8	7	anim2i	|- ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ P e. Ring ) )
9	8	3adant3	|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> ( N e. Fin /\ P e. Ring ) )
10		simp3	|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> Q e. E )
11	1 2	pmatring	|- ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
12	11	3adant3	|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> C e. Ring )
13	3 6	ringidcl	|- ( C e. Ring -> .1. e. B )
14	12 13	syl	|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> .1. e. B )
15	4 2 3 5	matvscl	|- ( ( ( N e. Fin /\ P e. Ring ) /\ ( Q e. E /\ .1. e. B ) ) -> ( Q .* .1. ) e. B )
16	9 10 14 15	syl12anc	|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> ( Q .* .1. ) e. B )