Metamath Proof Explorer


Theorem cpm2mval

Description: The result of an inverse matrix transformation. (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

Ref Expression
Hypotheses cpm2mfval.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
cpm2mfval.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
Assertion cpm2mval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → ( 𝐼𝑀 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 cpm2mfval.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
2 cpm2mfval.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
3 1 2 cpm2mfval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝐼 = ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
4 3 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → 𝐼 = ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
5 oveq ( 𝑚 = 𝑀 → ( 𝑥 𝑚 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
6 5 fveq2d ( 𝑚 = 𝑀 → ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) = ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) )
7 6 fveq1d ( 𝑚 = 𝑀 → ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) )
8 7 mpoeq3dv ( 𝑚 = 𝑀 → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
9 8 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) ∧ 𝑚 = 𝑀 ) → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
10 simp3 ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → 𝑀𝑆 )
11 simp1 ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → 𝑁 ∈ Fin )
12 mpoexga ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ V )
13 11 11 12 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ V )
14 4 9 10 13 fvmptd ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → ( 𝐼𝑀 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )