Definition df-cpmat 21763

Description: The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 21366). (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

Step	Hyp	Ref	Expression
1		ccpmat 21760	. 2 class ConstPolyMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8691	. . 3 class Fin
5		cvv 3422	. . 3 class V
6		vk	. . . . . . . . . 10 setvar 𝑘
7	6	cv 1538	. . . . . . . . 9 class 𝑘
8		vi	. . . . . . . . . . . 12 setvar 𝑖
9	8	cv 1538	. . . . . . . . . . 11 class 𝑖
10		vj	. . . . . . . . . . . 12 setvar 𝑗
11	10	cv 1538	. . . . . . . . . . 11 class 𝑗
12		vm	. . . . . . . . . . . 12 setvar 𝑚
13	12	cv 1538	. . . . . . . . . . 11 class 𝑚
14	9, 11, 13	co 7255	. . . . . . . . . 10 class (𝑖𝑚𝑗)
15		cco1 21259	. . . . . . . . . 10 class coe1
16	14, 15	cfv 6418	. . . . . . . . 9 class (coe1‘(𝑖𝑚𝑗))
17	7, 16	cfv 6418	. . . . . . . 8 class ((coe1‘(𝑖𝑚𝑗))‘𝑘)
18	3	cv 1538	. . . . . . . . 9 class 𝑟
19		c0g 17067	. . . . . . . . 9 class 0g
20	18, 19	cfv 6418	. . . . . . . 8 class (0g‘𝑟)
21	17, 20	wceq 1539	. . . . . . 7 wff ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)
22		cn 11903	. . . . . . 7 class ℕ
23	21, 6, 22	wral 3063	. . . . . 6 wff ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)
24	2	cv 1538	. . . . . 6 class 𝑛
25	23, 10, 24	wral 3063	. . . . 5 wff ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)
26	25, 8, 24	wral 3063	. . . 4 wff ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)
27		cpl1 21258	. . . . . . 7 class Poly1
28	18, 27	cfv 6418	. . . . . 6 class (Poly1‘𝑟)
29		cmat 21464	. . . . . 6 class Mat
30	24, 28, 29	co 7255	. . . . 5 class (𝑛 Mat (Poly1‘𝑟))
31		cbs 16840	. . . . 5 class Base
32	30, 31	cfv 6418	. . . 4 class (Base‘(𝑛 Mat (Poly1‘𝑟)))
33	26, 12, 32	crab 3067	. . 3 class {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)}
34	2, 3, 4, 5, 33	cmpo 7257	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)})
35	1, 34	wceq 1539	1 wff ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)})

This definition is referenced by:  cpmat  21766