Theorem pm2mpfval

Description: A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-Oct-2019) (Revised by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pm2mpval.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pm2mpval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pm2mpval.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	pm2mpval.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	pm2mpval.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
	pm2mpval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pm2mpval.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	pm2mpval.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpval.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pm2mpval.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5		pm2mpval.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6		pm2mpval.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
7		pm2mpval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8		pm2mpval.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9		pm2mpval.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
10	1 2 3 4 5 6 7 8 9	pm2mpval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑇 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
11	10	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → 𝑇 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
12		oveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 decompPMat 𝑘 ) = ( 𝑀 decompPMat 𝑘 ) )
13	12	oveq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
14	13	mpteq2dv	⊢ ( 𝑚 = 𝑀 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
15	14	oveq2d	⊢ ( 𝑚 = 𝑀 → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
16	15	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
17		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
18		ovexd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ V )
19	11 16 17 18	fvmptd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )