Definition df-cpmat 20511

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

Assertion

Ref	Expression
df-cpmat	|- ConstPolyMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( (coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } )

Distinct variable group:   i, j, k, m, n, r

Detailed syntax breakdown of Definition df-cpmat

Step	Hyp	Ref	Expression
1		ccpmat 20508	. 2 class ConstPolyMat
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cfn 7955	. . 3 class Fin
5		cvv 3200	. . 3 class _V
6		vk	. . . . . . . . . 10 setvar k
7	6	cv 1482	. . . . . . . . 9 class k
8		vi	. . . . . . . . . . . 12 setvar i
9	8	cv 1482	. . . . . . . . . . 11 class i
10		vj	. . . . . . . . . . . 12 setvar j
11	10	cv 1482	. . . . . . . . . . 11 class j
12		vm	. . . . . . . . . . . 12 setvar m
13	12	cv 1482	. . . . . . . . . . 11 class m
14	9, 11, 13	co 6650	. . . . . . . . . 10 class ( i m j )
15		cco1 19548	. . . . . . . . . 10 class coe1
16	14, 15	cfv 5888	. . . . . . . . 9 class (coe1 ` ( i m j ) )
17	7, 16	cfv 5888	. . . . . . . 8 class ( (coe1 ` ( i m j ) ) ` k )
18	3	cv 1482	. . . . . . . . 9 class r
19		c0g 16100	. . . . . . . . 9 class 0g
20	18, 19	cfv 5888	. . . . . . . 8 class ( 0g ` r )
21	17, 20	wceq 1483	. . . . . . 7 wff ( (coe1 ` ( i m j ) ) ` k ) = ( 0g ` r )
22		cn 11020	. . . . . . 7 class NN
23	21, 6, 22	wral 2912	. . . . . 6 wff A. k e. NN ( (coe1 ` ( i m j ) ) ` k ) = ( 0g ` r )
24	2	cv 1482	. . . . . 6 class n
25	23, 10, 24	wral 2912	. . . . 5 wff A. j e. n A. k e. NN ( (coe1 ` ( i m j ) ) ` k ) = ( 0g ` r )
26	25, 8, 24	wral 2912	. . . 4 wff A. i e. n A. j e. n A. k e. NN ( (coe1 ` ( i m j ) ) ` k ) = ( 0g ` r )
27		cpl1 19547	. . . . . . 7 class Poly1
28	18, 27	cfv 5888	. . . . . 6 class (Poly1 ` r )
29		cmat 20213	. . . . . 6 class Mat
30	24, 28, 29	co 6650	. . . . 5 class ( n Mat (Poly1 ` r ) )
31		cbs 15857	. . . . 5 class Base
32	30, 31	cfv 5888	. . . 4 class ( Base ` ( n Mat (Poly1 ` r ) ) )
33	26, 12, 32	crab 2916	. . 3 class { m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( (coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) }
34	2, 3, 4, 5, 33	cmpt2 6652	. 2 class ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( (coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } )
35	1, 34	wceq 1483	1 wff ConstPolyMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( (coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } )

This definition is referenced by:  cpmat  20514