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 𝐴 = ( 𝑁 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𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )