Theorem mat2pmatfval

Description: Value of the 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	mat2pmatfval	⊢ ( ( 𝑁 ∈ 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		df-mat2pmat	⊢ matToPolyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
7	6	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → matToPolyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) ) )
8		oveq12	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
9	8	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
10	2	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
11	3 10	eqtr2i	⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = 𝐵
12	9 11	eqtrdi	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = 𝐵 )
13		simpl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
14		2fveq3	⊢ ( 𝑟 = 𝑅 → ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) )
15	14	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) )
16	4	fveq2i	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
17	5 16	eqtr2i	⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = 𝑆
18	15 17	eqtrdi	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) = 𝑆 )
19	18	fveq1d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) )
20	13 13 19	mpoeq123dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) )
21	12 20	mpteq12dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
22	21	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
23		simpl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ Fin )
24		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
25	24	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ V )
26	3	fvexi	⊢ 𝐵 ∈ V
27		mptexg	⊢ ( 𝐵 ∈ V → ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) ∈ V )
28	26 27	mp1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) ∈ V )
29	7 22 23 25 28	ovmpod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 matToPolyMat 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
30	1 29	syl5eq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑇 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )