Theorem mply1topmatval

Description: A polynomial over matrices transformed into a polynomial matrix. I is the inverse function of the transformation T of polynomial matrices into polynomials over matrices: ( T( IO ) ) = O ) (see mp2pm2mp ). (Contributed by AV, 6-Oct-2019)

	Ref	Expression
Hypotheses	mply1topmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mply1topmat.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	mply1topmat.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
	mply1topmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mply1topmat.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	mply1topmat.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	mply1topmat.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
	mply1topmat.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
Assertion	mply1topmatval	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mply1topmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mply1topmat.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
3		mply1topmat.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
4		mply1topmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mply1topmat.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
6		mply1topmat.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7		mply1topmat.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
8		mply1topmat.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
9		fveq2	⊢ ( 𝑝 = 𝑂 → ( coe1 ‘ 𝑝 ) = ( coe1 ‘ 𝑂 ) )
10	9	fveq1d	⊢ ( 𝑝 = 𝑂 → ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) )
11	10	oveqd	⊢ ( 𝑝 = 𝑂 → ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) )
12	11	oveq1d	⊢ ( 𝑝 = 𝑂 → ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) )
13	12	mpteq2dv	⊢ ( 𝑝 = 𝑂 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) )
14	13	oveq2d	⊢ ( 𝑝 = 𝑂 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) )
15	14	mpoeq3dv	⊢ ( 𝑝 = 𝑂 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
16		simpr	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑂 ∈ 𝐿 ) → 𝑂 ∈ 𝐿 )
17		simpl	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑂 ∈ 𝐿 ) → 𝑁 ∈ 𝑉 )
18		mpoexga	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ V )
19	17 18	syldan	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑂 ∈ 𝐿 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ V )
20	8 15 16 19	fvmptd3	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )