Metamath Proof Explorer


Theorem cpm2mfval

Description: Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 cpm2mfval.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
2 cpm2mfval.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
3 df-cpmat2mat cPolyMatToMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥𝑛 , 𝑦𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
4 3 a1i ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → cPolyMatToMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥𝑛 , 𝑦𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ) )
5 oveq12 ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑛 ConstPolyMat 𝑟 ) = ( 𝑁 ConstPolyMat 𝑅 ) )
6 5 2 eqtr4di ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑛 ConstPolyMat 𝑟 ) = 𝑆 )
7 simpl ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
8 eqidd ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) )
9 7 7 8 mpoeq123dv ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑥𝑛 , 𝑦𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) )
10 6 9 mpteq12dv ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥𝑛 , 𝑦𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
11 10 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) ∧ ( 𝑛 = 𝑁𝑟 = 𝑅 ) ) → ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥𝑛 , 𝑦𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
12 simpl ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑁 ∈ Fin )
13 elex ( 𝑅𝑉𝑅 ∈ V )
14 13 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑅 ∈ V )
15 2 ovexi 𝑆 ∈ V
16 mptexg ( 𝑆 ∈ V → ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ∈ V )
17 15 16 mp1i ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ∈ V )
18 4 11 12 14 17 ovmpod ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑁 cPolyMatToMat 𝑅 ) = ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
19 1 18 eqtrid ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝐼 = ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )