Theorem decpmatval

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power, general version for arbitrary matrices. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	decpmatval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	decpmatval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	decpmatval	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		decpmatval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		decpmatval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		decpmatval0	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	1 4 2	matbas2i	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
6		elmapi	⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
7		fdm	⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) → dom 𝑀 = ( 𝑁 × 𝑁 ) )
8	7	dmeqd	⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) → dom dom 𝑀 = dom ( 𝑁 × 𝑁 ) )
9		dmxpid	⊢ dom ( 𝑁 × 𝑁 ) = 𝑁
10	8 9	eqtrdi	⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) → dom dom 𝑀 = 𝑁 )
11	5 6 10	3syl	⊢ ( 𝑀 ∈ 𝐵 → dom dom 𝑀 = 𝑁 )
12	11	adantr	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → dom dom 𝑀 = 𝑁 )
13		eqidd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) )
14	12 12 13	mpoeq123dv	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
15	3 14	eqtrd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )