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	⊢ ConstPolyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccpmat	⊢ ConstPolyMat
1		vn	⊢ 𝑛
2		cfn	⊢ Fin
3		vr	⊢ 𝑟
4		cvv	⊢ V
5		vm	⊢ 𝑚
6		cbs	⊢ Base
7	1	cv	⊢ 𝑛
8		cmat	⊢ Mat
9		cpl1	⊢ Poly1
10	3	cv	⊢ 𝑟
11	10 9	cfv	⊢ ( Poly1 ‘ 𝑟 )
12	7 11 8	co	⊢ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) )
13	12 6	cfv	⊢ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) )
14		vi	⊢ 𝑖
15		vj	⊢ 𝑗
16		vk	⊢ 𝑘
17		cn	⊢ ℕ
18		cco1	⊢ coe1
19	14	cv	⊢ 𝑖
20	5	cv	⊢ 𝑚
21	15	cv	⊢ 𝑗
22	19 21 20	co	⊢ ( 𝑖 𝑚 𝑗 )
23	22 18	cfv	⊢ ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) )
24	16	cv	⊢ 𝑘
25	24 23	cfv	⊢ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 )
26		c0g	⊢ 0g
27	10 26	cfv	⊢ ( 0g ‘ 𝑟 )
28	25 27	wceq	⊢ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 )
29	28 16 17	wral	⊢ ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 )
30	29 15 7	wral	⊢ ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 )
31	30 14 7	wral	⊢ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 )
32	31 5 13	crab	⊢ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) }
33	1 3 2 4 32	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) } )
34	0 33	wceq	⊢ ConstPolyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) } )