cpm2mvalel

Description: A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019)

	Ref	Expression
Hypotheses	cpm2mfval.i	$⊢ I = N cPolyMatToMat R$
	cpm2mfval.s	$⊢ S = N ConstPolyMat R$
Assertion	cpm2mvalel	$⊢ ((N \in Fin \land R \in V \land M \in S) \land (X \in N \land Y \in N)) \to X I (M) Y = {coe}_{1} (X M Y) (0)$

Step	Hyp	Ref	Expression
1		cpm2mfval.i	$⊢ I = N cPolyMatToMat R$
2		cpm2mfval.s	$⊢ S = N ConstPolyMat R$
3	1 2	cpm2mval	$⊢ (N \in Fin \land R \in V \land M \in S) \to I (M) = (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0))$
4	3	adantr	$⊢ ((N \in Fin \land R \in V \land M \in S) \land (X \in N \land Y \in N)) \to I (M) = (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0))$
5		oveq12	$⊢ (x = X \land y = Y) \to x M y = X M Y$
6	5	fveq2d	$⊢ (x = X \land y = Y) \to {coe}_{1} (x M y) = {coe}_{1} (X M Y)$
7	6	fveq1d	$⊢ (x = X \land y = Y) \to {coe}_{1} (x M y) (0) = {coe}_{1} (X M Y) (0)$
8	7	adantl	$⊢ (((N \in Fin \land R \in V \land M \in S) \land (X \in N \land Y \in N)) \land (x = X \land y = Y)) \to {coe}_{1} (x M y) (0) = {coe}_{1} (X M Y) (0)$
9		simprl	$⊢ ((N \in Fin \land R \in V \land M \in S) \land (X \in N \land Y \in N)) \to X \in N$
10		simprr	$⊢ ((N \in Fin \land R \in V \land M \in S) \land (X \in N \land Y \in N)) \to Y \in N$
11		fvexd	$⊢ ((N \in Fin \land R \in V \land M \in S) \land (X \in N \land Y \in N)) \to {coe}_{1} (X M Y) (0) \in V$
12	4 8 9 10 11	ovmpod	$⊢ ((N \in Fin \land R \in V \land M \in S) \land (X \in N \land Y \in N)) \to X I (M) Y = {coe}_{1} (X M Y) (0)$

Metamath Proof Explorer