Metamath Proof Explorer


Theorem cpm2mvalel

Description: A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019)

Ref Expression
Hypotheses cpm2mfval.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
cpm2mfval.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
Assertion cpm2mvalel ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) ∧ ( 𝑋𝑁𝑌𝑁 ) ) → ( 𝑋 ( 𝐼𝑀 ) 𝑌 ) = ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 cpm2mfval.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
2 cpm2mfval.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
3 1 2 cpm2mval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) → ( 𝐼𝑀 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
4 3 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) ∧ ( 𝑋𝑁𝑌𝑁 ) ) → ( 𝐼𝑀 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
5 oveq12 ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑋 𝑀 𝑌 ) )
6 5 fveq2d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) = ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) )
7 6 fveq1d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) )
8 7 adantl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) ∧ ( 𝑋𝑁𝑌𝑁 ) ) ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) )
9 simprl ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) ∧ ( 𝑋𝑁𝑌𝑁 ) ) → 𝑋𝑁 )
10 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) ∧ ( 𝑋𝑁𝑌𝑁 ) ) → 𝑌𝑁 )
11 fvexd ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) ∧ ( 𝑋𝑁𝑌𝑁 ) ) → ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) ∈ V )
12 4 8 9 10 11 ovmpod ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝑆 ) ∧ ( 𝑋𝑁𝑌𝑁 ) ) → ( 𝑋 ( 𝐼𝑀 ) 𝑌 ) = ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) )