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=Poly1R
1pmatscmul.c C=NMatP
1pmatscmul.b B=BaseC
1pmatscmul.e E=BaseP
1pmatscmul.m ˙=C
1pmatscmul.1 1˙=1C
Assertion 1pmatscmul NFinRRingQEQ˙1˙B

Proof

Step Hyp Ref Expression
1 1pmatscmul.p P=Poly1R
2 1pmatscmul.c C=NMatP
3 1pmatscmul.b B=BaseC
4 1pmatscmul.e E=BaseP
5 1pmatscmul.m ˙=C
6 1pmatscmul.1 1˙=1C
7 1 ply1ring RRingPRing
8 7 anim2i NFinRRingNFinPRing
9 8 3adant3 NFinRRingQENFinPRing
10 simp3 NFinRRingQEQE
11 1 2 pmatring NFinRRingCRing
12 11 3adant3 NFinRRingQECRing
13 3 6 ringidcl CRing1˙B
14 12 13 syl NFinRRingQE1˙B
15 4 2 3 5 matvscl NFinPRingQE1˙BQ˙1˙B
16 9 10 14 15 syl12anc NFinRRingQEQ˙1˙B