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 𝑃 = ( 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 ) ∈ 𝐵 )