Definition df-decpmat

Description: Define the decomposition of polynomial matrices. This function collects the coefficients of a polynomial matrix m belong to the k th power of the polynomial variable for each entry of m . (Contributed by AV, 2-Dec-2019)

	Ref	Expression
Assertion	df-decpmat	⊢ decompPMat = ( 𝑚 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑚 , 𝑗 ∈ dom dom 𝑚 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdecpmat	⊢ decompPMat
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		vk	⊢ 𝑘
4		cn0	⊢ ℕ0
5		vi	⊢ 𝑖
6	1	cv	⊢ 𝑚
7	6	cdm	⊢ dom 𝑚
8	7	cdm	⊢ dom dom 𝑚
9		vj	⊢ 𝑗
10		cco1	⊢ coe1
11	5	cv	⊢ 𝑖
12	9	cv	⊢ 𝑗
13	11 12 6	co	⊢ ( 𝑖 𝑚 𝑗 )
14	13 10	cfv	⊢ ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) )
15	3	cv	⊢ 𝑘
16	15 14	cfv	⊢ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 )
17	5 9 8 8 16	cmpo	⊢ ( 𝑖 ∈ dom dom 𝑚 , 𝑗 ∈ dom dom 𝑚 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) )
18	1 3 2 4 17	cmpo	⊢ ( 𝑚 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑚 , 𝑗 ∈ dom dom 𝑚 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) )
19	0 18	wceq	⊢ decompPMat = ( 𝑚 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑚 , 𝑗 ∈ dom dom 𝑚 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) )