m2cpmf

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

Step	Hyp	Ref	Expression
1		m2cpm.s	$⊢ S = N ConstPolyMat R$
2		m2cpm.t	$⊢ T = N matToPolyMat R$
3		m2cpm.a	$⊢ A = N Mat R$
4		m2cpm.b	$⊢ B = {Base}_{A}$
5		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
6	5 5	jca	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land N \in Fin)$
7	6	adantr	$⊢ ((N \in Fin \land R \in Ring) \land m \in B) \to (N \in Fin \land N \in Fin)$
8		mpoexga	$⊢ (N \in Fin \land N \in Fin) \to (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) (i m j)) \in V$
9	7 8	syl	$⊢ ((N \in Fin \land R \in Ring) \land m \in B) \to (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) (i m j)) \in V$
10		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
11		eqid	$⊢ algSc ({Poly}_{1} (R)) = algSc ({Poly}_{1} (R))$
12	2 3 4 10 11	mat2pmatfval	$⊢ (N \in Fin \land R \in Ring) \to T = (m \in B ⟼ (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) (i m j)))$
13	1 2 3 4	m2cpm	$⊢ (N \in Fin \land R \in Ring \land b \in B) \to T (b) \in S$
14	13	3expa	$⊢ ((N \in Fin \land R \in Ring) \land b \in B) \to T (b) \in S$
15	9 12 14	fmpt2d	$⊢ (N \in Fin \land R \in Ring) \to T : B ⟶ S$

Metamath Proof Explorer