Theorem m2cpmf

Description: The matrix transformation is a function from the matrices to the constant polynomial matrices. (Contributed by AV, 18-Nov-2019)

	Ref	Expression
Hypotheses	m2cpm.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	m2cpm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	m2cpm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2cpm.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	m2cpmf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		m2cpm.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		m2cpm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3		m2cpm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		m2cpm.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
5		simpl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
6	5 5	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
7	6	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
8		mpoexga	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑖 𝑚 𝑗 ) ) ) ∈ V )
9	7 8	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑖 𝑚 𝑗 ) ) ) ∈ V )
10		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
11		eqid	⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
12	2 3 4 10 11	mat2pmatfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑖 𝑚 𝑗 ) ) ) ) )
13	1 2 3 4	m2cpm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑏 ) ∈ 𝑆 )
14	13	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑏 ) ∈ 𝑆 )
15	9 12 14	fmpt2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝑆 )