Metamath Proof Explorer


Theorem cpmatpmat

Description: A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses cpmat.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpmat.p 𝑃 = ( Poly1𝑅 )
cpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
cpmat.b 𝐵 = ( Base ‘ 𝐶 )
Assertion cpmatpmat ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → 𝑀𝐵 )

Proof

Step Hyp Ref Expression
1 cpmat.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 cpmat.p 𝑃 = ( Poly1𝑅 )
3 cpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
4 cpmat.b 𝐵 = ( Base ‘ 𝐶 )
5 1 2 3 4 cpmat ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑆 = { 𝑚𝐵 ∣ ∀ 𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g𝑅 ) } )
6 5 eleq2d ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑀𝑆𝑀 ∈ { 𝑚𝐵 ∣ ∀ 𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g𝑅 ) } ) )
7 elrabi ( 𝑀 ∈ { 𝑚𝐵 ∣ ∀ 𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g𝑅 ) } → 𝑀𝐵 )
8 6 7 syl6bi ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑀𝑆𝑀𝐵 ) )
9 8 3impia ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → 𝑀𝐵 )