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	biimtrdi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑀 ∈ 𝑆 → 𝑀 ∈ 𝐵 ) )
9	8	3impia	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) → 𝑀 ∈ 𝐵 )