Metamath Proof Explorer


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𝑟 ) } )