Metamath Proof Explorer

Definition df-cpmat

Description: The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf ). (Contributed by AV, 15-Nov-2019)

Ref Expression
Assertion df-cpmat ⊢ ConstPolyMat = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat Poly 1 ⁡ r | ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccpmat class ConstPolyMat
1 vn setvar n
2 cfn class Fin
3 vr setvar r
4 cvv class V
5 vm setvar m
6 cbs class Base
7 1 cv setvar n
8 cmat class Mat
9 cpl1 class Poly 1
10 3 cv setvar r
11 10 9 cfv class Poly 1 ⁡ r
12 7 11 8 co class n Mat Poly 1 ⁡ r
13 12 6 cfv class Base n Mat Poly 1 ⁡ r
14 vi setvar i
15 vj setvar j
16 vk setvar k
17 cn class ℕ
18 cco1 class coe 1
19 14 cv setvar i
20 5 cv setvar m
21 15 cv setvar j
22 19 21 20 co class i m j
23 22 18 cfv class coe 1 ⁡ i m j
24 16 cv setvar k
25 24 23 cfv class coe 1 ⁡ i m j ⁡ k
26 c0g class 0 𝑔
27 10 26 cfv class 0 r
28 25 27 wceq wff coe 1 ⁡ i m j ⁡ k = 0 r
29 28 16 17 wral wff ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r
30 29 15 7 wral wff ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r
31 30 14 7 wral wff ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r
32 31 5 13 crab class m ∈ Base n Mat Poly 1 ⁡ r | ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r
33 1 3 2 4 32 cmpo class n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat Poly 1 ⁡ r | ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r
34 0 33 wceq wff ConstPolyMat = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat Poly 1 ⁡ r | ∀ i ∈ n ∀ j ∈ n ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 r