Metamath Proof Explorer

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 ⊢A=NMatR
mply1topmat.q ⊢Q=Poly1⁡A
mply1topmat.l ⊢L=BaseQ
mply1topmat.p ⊢P=Poly1⁡R
mply1topmat.m ⊢·˙=⋅P
mply1topmat.e ⊢E=⋅mulGrpP
mply1topmat.y ⊢Y=var1⁡R
mply1topmat.i ⊢I=p∈L⟼i∈N,j∈N⟼∑Pk∈ℕ0icoe1⁡p⁡kj·˙kEY
Assertion mply1topmatval ⊢N∈V∧O∈L→I⁡O=i∈N,j∈N⟼∑Pk∈ℕ0icoe1⁡O⁡kj·˙kEY

Proof

Step Hyp Ref Expression
1 mply1topmat.a ⊢A=NMatR
2 mply1topmat.q ⊢Q=Poly1⁡A
3 mply1topmat.l ⊢L=BaseQ
4 mply1topmat.p ⊢P=Poly1⁡R
5 mply1topmat.m ⊢·˙=⋅P
6 mply1topmat.e ⊢E=⋅mulGrpP
7 mply1topmat.y ⊢Y=var1⁡R
8 mply1topmat.i ⊢I=p∈L⟼i∈N,j∈N⟼∑Pk∈ℕ0icoe1⁡p⁡kj·˙kEY
9 fveq2 ⊢p=O→coe1⁡p=coe1⁡O
10 9 fveq1d ⊢p=O→coe1⁡p⁡k=coe1⁡O⁡k
11 10 oveqd ⊢p=O→icoe1⁡p⁡kj=icoe1⁡O⁡kj
12 11 oveq1d ⊢p=O→icoe1⁡p⁡kj·˙kEY=icoe1⁡O⁡kj·˙kEY
13 12 mpteq2dv ⊢p=O→k∈ℕ0⟼icoe1⁡p⁡kj·˙kEY=k∈ℕ0⟼icoe1⁡O⁡kj·˙kEY
14 13 oveq2d ⊢p=O→∑Pk∈ℕ0icoe1⁡p⁡kj·˙kEY=∑Pk∈ℕ0icoe1⁡O⁡kj·˙kEY
15 14 mpoeq3dv ⊢p=O→i∈N,j∈N⟼∑Pk∈ℕ0icoe1⁡p⁡kj·˙kEY=i∈N,j∈N⟼∑Pk∈ℕ0icoe1⁡O⁡kj·˙kEY
16 simpr ⊢N∈V∧O∈L→O∈L
17 simpl ⊢N∈V∧O∈L→N∈V
18 mpoexga ⊢N∈V∧N∈V→i∈N,j∈N⟼∑Pk∈ℕ0icoe1⁡O⁡kj·˙kEY∈V
19 17 18 syldan ⊢N∈V∧O∈L→i∈N,j∈N⟼∑Pk∈ℕ0icoe1⁡O⁡kj·˙kEY∈V
20 8 15 16 19 fvmptd3 ⊢N∈V∧O∈L→I⁡O=i∈N,j∈N⟼∑Pk∈ℕ0icoe1⁡O⁡kj·˙kEY