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

Definition df-cpmat 20430
Description: The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 19574). (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 20427 . 2 class ConstPolyMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 7899 . . 3 class Fin
5 cvv 3186 . . 3 class V
6 vk . . . . . . . . . 10 setvar 𝑘
76cv 1479 . . . . . . . . 9 class 𝑘
8 vi . . . . . . . . . . . 12 setvar 𝑖
98cv 1479 . . . . . . . . . . 11 class 𝑖
10 vj . . . . . . . . . . . 12 setvar 𝑗
1110cv 1479 . . . . . . . . . . 11 class 𝑗
12 vm . . . . . . . . . . . 12 setvar 𝑚
1312cv 1479 . . . . . . . . . . 11 class 𝑚
149, 11, 13co 6604 . . . . . . . . . 10 class (𝑖𝑚𝑗)
15 cco1 19467 . . . . . . . . . 10 class coe1
1614, 15cfv 5847 . . . . . . . . 9 class (coe1‘(𝑖𝑚𝑗))
177, 16cfv 5847 . . . . . . . 8 class ((coe1‘(𝑖𝑚𝑗))‘𝑘)
183cv 1479 . . . . . . . . 9 class 𝑟
19 c0g 16021 . . . . . . . . 9 class 0g
2018, 19cfv 5847 . . . . . . . 8 class (0g𝑟)
2117, 20wceq 1480 . . . . . . 7 wff ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)
22 cn 10964 . . . . . . 7 class
2321, 6, 22wral 2907 . . . . . 6 wff 𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)
242cv 1479 . . . . . 6 class 𝑛
2523, 10, 24wral 2907 . . . . 5 wff 𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)
2625, 8, 24wral 2907 . . . 4 wff 𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)
27 cpl1 19466 . . . . . . 7 class Poly1
2818, 27cfv 5847 . . . . . 6 class (Poly1𝑟)
29 cmat 20132 . . . . . 6 class Mat
3024, 28, 29co 6604 . . . . 5 class (𝑛 Mat (Poly1𝑟))
31 cbs 15781 . . . . 5 class Base
3230, 31cfv 5847 . . . 4 class (Base‘(𝑛 Mat (Poly1𝑟)))
3326, 12, 32crab 2911 . . 3 class {𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ∣ ∀𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)}
342, 3, 4, 5, 33cmpt2 6606 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ∣ ∀𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)})
351, 34wceq 1480 1 wff ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ∣ ∀𝑖𝑛𝑗𝑛𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g𝑟)})
Colors of variables: wff setvar class
This definition is referenced by:  cpmat  20433
  Copyright terms: Public domain W3C validator