Theorem decpmate

Description: An entry of the matrix consisting of the coefficients in the entries of a polynomial matrix is the corresponding coefficient in the polynomial entry of the given matrix. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	decpmate.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	decpmate.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	decpmate.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	decpmate	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑀 decompPMat 𝐾 ) 𝐽 ) = ( ( coe1 ‘ ( 𝐼 𝑀 𝐽 ) ) ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		decpmate.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		decpmate.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		decpmate.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4	2 3	decpmatval	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
5	4	3adant1	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
6	5	adantr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
7		oveq12	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝐼 𝑀 𝐽 ) )
8	7	fveq2d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe1 ‘ ( 𝐼 𝑀 𝐽 ) ) )
9	8	fveq1d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝐼 𝑀 𝐽 ) ) ‘ 𝐾 ) )
10	9	adantl	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝐼 𝑀 𝐽 ) ) ‘ 𝐾 ) )
11		simprl	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
12		simprr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐽 ∈ 𝑁 )
13		fvexd	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( coe1 ‘ ( 𝐼 𝑀 𝐽 ) ) ‘ 𝐾 ) ∈ V )
14	6 10 11 12 13	ovmpod	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑀 decompPMat 𝐾 ) 𝐽 ) = ( ( coe1 ‘ ( 𝐼 𝑀 𝐽 ) ) ‘ 𝐾 ) )