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	$$⊢\mathrm{ConstPolyMat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}|\forall i\in n\forall j\in n\forall k\in \mathbb{N}{\mathrm{coe}}_1\left(imj\right)\left(k\right)=0_r\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccpmat	$$class\mathrm{ConstPolyMat}$$
1		vn	$$setvarn$$
2		cfn	$$class\mathrm{Fin}$$
3		vr	$$setvarr$$
4		cvv	$$class\mathrm{V}$$
5		vm	$$setvarm$$
6		cbs	$$class\mathrm{Base}$$
7	1	cv	$$setvarn$$
8		cmat	$$class\mathrm{Mat}$$
9		cpl1	$$class{\mathrm{Poly}}_1$$
10	3	cv	$$setvarr$$
11	10 9	cfv	$$class{\mathrm{Poly}}_1\left(r\right)$$
12	7 11 8	co	$$class\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)$$
13	12 6	cfv	$$class{\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}$$
14		vi	$$setvari$$
15		vj	$$setvarj$$
16		vk	$$setvark$$
17		cn	$$class\mathbb{N}$$
18		cco1	$$class{\mathrm{coe}}_1$$
19	14	cv	$$setvari$$
20	5	cv	$$setvarm$$
21	15	cv	$$setvarj$$
22	19 21 20	co	$$class\left(imj\right)$$
23	22 18	cfv	$$class{\mathrm{coe}}_1\left(imj\right)$$
24	16	cv	$$setvark$$
25	24 23	cfv	$$class{\mathrm{coe}}_1\left(imj\right)\left(k\right)$$
26		c0g	$$class{0}_{𝑔}$$
27	10 26	cfv	$$class{0}_r$$
28	25 27	wceq	$$wff{\mathrm{coe}}_1\left(imj\right)\left(k\right)=0_r$$
29	28 16 17	wral	$$wff\forall k\in \mathbb{N}{\mathrm{coe}}_1\left(imj\right)\left(k\right)=0_r$$
30	29 15 7	wral	$$wff\forall j\in n\forall k\in \mathbb{N}{\mathrm{coe}}_1\left(imj\right)\left(k\right)=0_r$$
31	30 14 7	wral	$$wff\forall i\in n\forall j\in n\forall k\in \mathbb{N}{\mathrm{coe}}_1\left(imj\right)\left(k\right)=0_r$$
32	31 5 13	crab	$$class\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}|\forall i\in n\forall j\in n\forall k\in \mathbb{N}{\mathrm{coe}}_1\left(imj\right)\left(k\right)=0_r\right\}$$
33	1 3 2 4 32	cmpo	$$class\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}|\forall i\in n\forall j\in n\forall k\in \mathbb{N}{\mathrm{coe}}_1\left(imj\right)\left(k\right)=0_r\right\}\right)$$
34	0 33	wceq	$$wff\mathrm{ConstPolyMat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}|\forall i\in n\forall j\in n\forall k\in \mathbb{N}{\mathrm{coe}}_1\left(imj\right)\left(k\right)=0_r\right\}\right)$$