Theorem mat2pmatvalel

Description: A (matrix) element of 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	mat2pmatvalel	⊢ ( ( ( 𝑁 ∈ 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	mat2pmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )
7	6	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )
8		oveq12	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑋 𝑀 𝑌 ) )
9	8	fveq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) = ( 𝑆 ‘ ( 𝑋 𝑀 𝑌 ) ) )
10	9	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) = ( 𝑆 ‘ ( 𝑋 𝑀 𝑌 ) ) )
11		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → 𝑋 ∈ 𝑁 )
12		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → 𝑌 ∈ 𝑁 )
13		fvexd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑋 𝑀 𝑌 ) ) ∈ V )
14	7 10 11 12 13	ovmpod	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( 𝑋 ( 𝑇 ‘ 𝑀 ) 𝑌 ) = ( 𝑆 ‘ ( 𝑋 𝑀 𝑌 ) ) )