cpm2mval

Description: The result of an inverse matrix transformation. (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

	Ref	Expression
Hypotheses	cpm2mfval.i	$⊢ I = N cPolyMatToMat R$
	cpm2mfval.s	$⊢ S = N ConstPolyMat R$
Assertion	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))$

Step	Hyp	Ref	Expression
1		cpm2mfval.i	$⊢ I = N cPolyMatToMat R$
2		cpm2mfval.s	$⊢ S = N ConstPolyMat R$
3	1 2	cpm2mfval	$⊢ (N \in Fin \land R \in V) \to I = (m \in S ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0)))$
4	3	3adant3	$⊢ (N \in Fin \land R \in V \land M \in S) \to I = (m \in S ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0)))$
5		oveq	$⊢ m = M \to x m y = x M y$
6	5	fveq2d	$⊢ m = M \to {coe}_{1} (x m y) = {coe}_{1} (x M y)$
7	6	fveq1d	$⊢ m = M \to {coe}_{1} (x m y) (0) = {coe}_{1} (x M y) (0)$
8	7	mpoeq3dv	$⊢ m = M \to (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0)) = (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0))$
9	8	adantl	$⊢ ((N \in Fin \land R \in V \land M \in S) \land m = M) \to (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0)) = (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0))$
10		simp3	$⊢ (N \in Fin \land R \in V \land M \in S) \to M \in S$
11		simp1	$⊢ (N \in Fin \land R \in V \land M \in S) \to N \in Fin$
12		mpoexga	$⊢ (N \in Fin \land N \in Fin) \to (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) \in V$
13	11 11 12	syl2anc	$⊢ (N \in Fin \land R \in V \land M \in S) \to (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) \in V$
14	4 9 10 13	fvmptd	$⊢ (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))$

Metamath Proof Explorer