Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cpmat Structured version   Visualization version   GIF version

Definition df-cpmat 20730
 Description: The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 19869). (Contributed by AV, 15-Nov-2019.)
Assertion
Ref Expression
df-cpmat ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ∣ ∀𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)})
Distinct variable group:   𝑖,𝑗,𝑘,𝑚,𝑛,𝑟

Detailed syntax breakdown of Definition df-cpmat
StepHypRef Expression
1 ccpmat 20727 . 2 class ConstPolyMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8108 . . 3 class Fin
5 cvv 3349 . . 3 class V
6 vk . . . . . . . . . 10 setvar 𝑘
76cv 1629 . . . . . . . . 9 class 𝑘
8 vi . . . . . . . . . . . 12 setvar 𝑖
98cv 1629 . . . . . . . . . . 11 class 𝑖
10 vj . . . . . . . . . . . 12 setvar 𝑗
1110cv 1629 . . . . . . . . . . 11 class 𝑗
12 vm . . . . . . . . . . . 12 setvar 𝑚
1312cv 1629 . . . . . . . . . . 11 class 𝑚
149, 11, 13co 6792 . . . . . . . . . 10 class (𝑖𝑚𝑗)
15 cco1 19762 . . . . . . . . . 10 class coe1
1614, 15cfv 6031 . . . . . . . . 9 class (coe1‘(𝑖𝑚𝑗))
177, 16cfv 6031 . . . . . . . 8 class ((coe1‘(𝑖𝑚𝑗))‘𝑘)
183cv 1629 . . . . . . . . 9 class 𝑟
19 c0g 16307 . . . . . . . . 9 class 0g
2018, 19cfv 6031 . . . . . . . 8 class (0g𝑟)
2117, 20wceq 1630 . . . . . . 7 wff ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)
22 cn 11221 . . . . . . 7 class
2321, 6, 22wral 3060 . . . . . 6 wff 𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)
242cv 1629 . . . . . 6 class 𝑛
2523, 10, 24wral 3060 . . . . 5 wff 𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)
2625, 8, 24wral 3060 . . . 4 wff 𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)
27 cpl1 19761 . . . . . . 7 class Poly1
2818, 27cfv 6031 . . . . . 6 class (Poly1𝑟)
29 cmat 20429 . . . . . 6 class Mat
3024, 28, 29co 6792 . . . . 5 class (𝑛 Mat (Poly1𝑟))
31 cbs 16063 . . . . 5 class Base
3230, 31cfv 6031 . . . 4 class (Base‘(𝑛 Mat (Poly1𝑟)))
3326, 12, 32crab 3064 . . 3 class {𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ∣ ∀𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)}
342, 3, 4, 5, 33cmpt2 6794 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ∣ ∀𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)})
351, 34wceq 1630 1 wff ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ∣ ∀𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)})
 Colors of variables: wff setvar class This definition is referenced by:  cpmat  20733
 Copyright terms: Public domain W3C validator