Theorem mat2pmatf

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

	Ref	Expression
Hypotheses	mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
Assertion	mat2pmatf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2		mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
6		mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
7		simpl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
8	7 7	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
9	8	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
10		mpoexga	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ∈ V )
11	9 10	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ∈ V )
12		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
13	1 2 3 4 12	mat2pmatfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
14	1 2 3 4 5 6	mat2pmatbas0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑚 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑚 ) ∈ 𝐻 )
15	14	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑚 ) ∈ 𝐻 )
16	11 13 15	fmpt2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝐻 )