Theorem mat2pmatval

Description: 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	mat2pmatval	⊢ ( ( 𝑁 ∈ 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	mat2pmatfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑇 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
7	6	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → 𝑇 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
8		oveq	⊢ ( 𝑚 = 𝑀 → ( 𝑥 𝑚 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
9	8	fveq2d	⊢ ( 𝑚 = 𝑀 → ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) )
10	9	mpoeq3dv	⊢ ( 𝑚 = 𝑀 → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )
11	10	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )
12		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
13		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
14		mpoexga	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) ∈ V )
15	13 13 14	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) ∈ V )
16	7 11 12 15	fvmptd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑀 𝑦 ) ) ) )