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 ⊢ S = N ConstPolyMat R
cpmat.p ⊢ P = Poly 1 ⁡ R
cpmat.c ⊢ C = N Mat P
cpmat.b ⊢ B = Base C
Assertion cpmatpmat ⊢ N ∈ Fin ∧ R ∈ V ∧ M ∈ S → M ∈ B

Proof

Step Hyp Ref Expression
1 cpmat.s ⊢ S = N ConstPolyMat R
2 cpmat.p ⊢ P = Poly 1 ⁡ R
3 cpmat.c ⊢ C = N Mat P
4 cpmat.b ⊢ B = Base C
5 1 2 3 4 cpmat ⊢ N ∈ Fin ∧ R ∈ V → S = m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
6 5 eleq2d ⊢ N ∈ Fin ∧ R ∈ V → M ∈ S ↔ M ∈ m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
7 elrabi ⊢ M ∈ m ∈ B | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R → M ∈ B
8 6 7 biimtrdi ⊢ N ∈ Fin ∧ R ∈ V → M ∈ S → M ∈ B
9 8 3impia ⊢ N ∈ Fin ∧ R ∈ V ∧ M ∈ S → M ∈ B