Metamath Proof Explorer


Theorem mat2pmatval

Description: The result of a matrix transformation. (Contributed by AV, 31-Jul-2019)

Ref Expression
Hypotheses mat2pmatfval.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
mat2pmatfval.a 𝐴 = ( 𝑁 Mat 𝑅 )
mat2pmatfval.b 𝐵 = ( Base ‘ 𝐴 )
mat2pmatfval.p 𝑃 = ( Poly1𝑅 )
mat2pmatfval.s 𝑆 = ( algSc ‘ 𝑃 )
Assertion mat2pmatval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → ( 𝑇𝑀 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 mat2pmatfval.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2 mat2pmatfval.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 mat2pmatfval.b 𝐵 = ( Base ‘ 𝐴 )
4 mat2pmatfval.p 𝑃 = ( Poly1𝑅 )
5 mat2pmatfval.s 𝑆 = ( algSc ‘ 𝑃 )
6 1 2 3 4 5 mat2pmatfval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑇 = ( 𝑚𝐵 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
7 6 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → 𝑇 = ( 𝑚𝐵 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
8 oveq ( 𝑚 = 𝑀 → ( 𝑥 𝑚 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
9 8 fveq2d ( 𝑚 = 𝑀 → ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) )
10 9 mpoeq3dv ( 𝑚 = 𝑀 → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )
11 10 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) ∧ 𝑚 = 𝑀 ) → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )
12 simp3 ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → 𝑀𝐵 )
13 simp1 ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → 𝑁 ∈ Fin )
14 mpoexga ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) ∈ V )
15 13 13 14 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) ∈ V )
16 7 11 12 15 fvmptd ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → ( 𝑇𝑀 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )