mat2pmatvalel

Description: A (matrix) element of 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	mat2pmatvalel	$⊢ ((N \in Fin \land R \in V \land M \in B) \land (X \in N \land Y \in N)) \to X T (M) Y = 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	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))$
7	6	adantr	$⊢ ((N \in Fin \land R \in V \land M \in B) \land (X \in N \land Y \in N)) \to T (M) = (x \in N, y \in N ⟼ S (x M y))$
8		oveq12	$⊢ (x = X \land y = Y) \to x M y = X M Y$
9	8	fveq2d	$⊢ (x = X \land y = Y) \to S (x M y) = S (X M Y)$
10	9	adantl	$⊢ (((N \in Fin \land R \in V \land M \in B) \land (X \in N \land Y \in N)) \land (x = X \land y = Y)) \to S (x M y) = S (X M Y)$
11		simprl	$⊢ ((N \in Fin \land R \in V \land M \in B) \land (X \in N \land Y \in N)) \to X \in N$
12		simprr	$⊢ ((N \in Fin \land R \in V \land M \in B) \land (X \in N \land Y \in N)) \to Y \in N$
13		fvexd	$⊢ ((N \in Fin \land R \in V \land M \in B) \land (X \in N \land Y \in N)) \to S (X M Y) \in V$
14	7 10 11 12 13	ovmpod	$⊢ ((N \in Fin \land R \in V \land M \in B) \land (X \in N \land Y \in N)) \to X T (M) Y = S (X M Y)$

Metamath Proof Explorer