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 ) )