mat2pmatval

Description: The result of a matrix transformation. (Contributed by AV, 31-Jul-2019)

	Ref	Expression
Hypotheses	mat2pmatfval.t	$⊢ T = N matToPolyMat R$
	mat2pmatfval.a	$⊢ A = N Mat R$
	mat2pmatfval.b	$⊢ B = {Base}_{A}$
	mat2pmatfval.p	$⊢ P = {Poly}_{1} (R)$
	mat2pmatfval.s	$⊢ S = algSc (P)$
Assertion	mat2pmatval	$⊢ (N \in Fin \land R \in V \land M \in B) \to T (M) = (x \in N, y \in N ⟼ S (x M y))$

Step	Hyp	Ref	Expression
1		mat2pmatfval.t	$⊢ T = N matToPolyMat R$
2		mat2pmatfval.a	$⊢ A = N Mat R$
3		mat2pmatfval.b	$⊢ B = {Base}_{A}$
4		mat2pmatfval.p	$⊢ P = {Poly}_{1} (R)$
5		mat2pmatfval.s	$⊢ S = algSc (P)$
6	1 2 3 4 5	mat2pmatfval	$⊢ (N \in Fin \land R \in V) \to T = (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y)))$
7	6	3adant3	$⊢ (N \in Fin \land R \in V \land M \in B) \to T = (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y)))$
8		oveq	$⊢ m = M \to x m y = x M y$
9	8	fveq2d	$⊢ m = M \to S (x m y) = S (x M y)$
10	9	mpoeq3dv	$⊢ m = M \to (x \in N, y \in N ⟼ S (x m y)) = (x \in N, y \in N ⟼ S (x M y))$
11	10	adantl	$⊢ ((N \in Fin \land R \in V \land M \in B) \land m = M) \to (x \in N, y \in N ⟼ S (x m y)) = (x \in N, y \in N ⟼ S (x M y))$
12		simp3	$⊢ (N \in Fin \land R \in V \land M \in B) \to M \in B$
13		simp1	$⊢ (N \in Fin \land R \in V \land M \in B) \to N \in Fin$
14		mpoexga	$⊢ (N \in Fin \land N \in Fin) \to (x \in N, y \in N ⟼ S (x M y)) \in V$
15	13 13 14	syl2anc	$⊢ (N \in Fin \land R \in V \land M \in B) \to (x \in N, y \in N ⟼ S (x M y)) \in V$
16	7 11 12 15	fvmptd	$⊢ (N \in Fin \land R \in V \land M \in B) \to T (M) = (x \in N, y \in N ⟼ S (x M y))$

Metamath Proof Explorer