Metamath Proof Explorer

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 = {Poly}_{1} (R)$
		1pmatscmul.c	$⊢ C = N Mat P$
		1pmatscmul.b	$⊢ B = {Base}_{C}$
		1pmatscmul.e	$⊢ E = {Base}_{P}$
		1pmatscmul.m	$⊢ \underset{˙}{*} = \cdot_{C}$
		1pmatscmul.1	$⊢ \underset{˙}{1} = 1_{C}$
	Assertion	1pmatscmul	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \to Q \underset{˙}{*} \underset{˙}{1} \in B$

Proof

Step	Hyp	Ref	Expression
1		1pmatscmul.p	$⊢ P = {Poly}_{1} (R)$
2		1pmatscmul.c	$⊢ C = N Mat P$
3		1pmatscmul.b	$⊢ B = {Base}_{C}$
4		1pmatscmul.e	$⊢ E = {Base}_{P}$
5		1pmatscmul.m	$⊢ \underset{˙}{*} = \cdot_{C}$
6		1pmatscmul.1	$⊢ \underset{˙}{1} = 1_{C}$
7	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
8	7	anim2i	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land P \in Ring)$
9	8	3adant3	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \to (N \in Fin \land P \in Ring)$
10		simp3	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \to Q \in E$
11	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
12	11	3adant3	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \to C \in Ring$
13	3 6	ringidcl	$⊢ C \in Ring \to \underset{˙}{1} \in B$
14	12 13	syl	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \to \underset{˙}{1} \in B$
15	4 2 3 5	matvscl	$⊢ ((N \in Fin \land P \in Ring) \land (Q \in E \land \underset{˙}{1} \in B)) \to Q \underset{˙}{*} \underset{˙}{1} \in B$
16	9 10 14 15	syl12anc	$⊢ (N \in Fin \land R \in Ring \land Q \in E) \to Q \underset{˙}{*} \underset{˙}{1} \in B$