m2cpminvid

Description: The inverse transformation applied to the transformation of a matrix over a ring R results in the matrix itself. (Contributed by AV, 12-Nov-2019) (Revised by AV, 13-Dec-2019)

	Ref	Expression
Hypotheses	m2cpminvid.i	$⊢ I = N cPolyMatToMat R$
	m2cpminvid.a	$⊢ A = N Mat R$
	m2cpminvid.k	$⊢ K = {Base}_{A}$
	m2cpminvid.t	$⊢ T = N matToPolyMat R$
Assertion	m2cpminvid	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to I (T (M)) = M$

Proof

Step	Hyp	Ref	Expression
1		m2cpminvid.i	$⊢ I = N cPolyMatToMat R$
2		m2cpminvid.a	$⊢ A = N Mat R$
3		m2cpminvid.k	$⊢ K = {Base}_{A}$
4		m2cpminvid.t	$⊢ T = N matToPolyMat R$
5		eqid	$⊢ N ConstPolyMat R = N ConstPolyMat R$
6	5 4 2 3	m2cpm	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to T (M) \in (N ConstPolyMat R)$
7	1 5	cpm2mval	$⊢ (N \in Fin \land R \in Ring \land T (M) \in (N ConstPolyMat R)) \to I (T (M)) = (x \in N, y \in N ⟼ {coe}_{1} (x T (M) y) (0))$
8	6 7	syld3an3	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to I (T (M)) = (x \in N, y \in N ⟼ {coe}_{1} (x T (M) y) (0))$
9		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
10		eqid	$⊢ algSc ({Poly}_{1} (R)) = algSc ({Poly}_{1} (R))$
11	4 2 3 9 10	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land (x \in N \land y \in N)) \to x T (M) y = algSc ({Poly}_{1} (R)) (x M y)$
12	11	3impb	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to x T (M) y = algSc ({Poly}_{1} (R)) (x M y)$
13	12	fveq2d	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to {coe}_{1} (x T (M) y) = {coe}_{1} (algSc ({Poly}_{1} (R)) (x M y))$
14	13	fveq1d	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to {coe}_{1} (x T (M) y) (0) = {coe}_{1} (algSc ({Poly}_{1} (R)) (x M y)) (0)$
15		simp12	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to R \in Ring$
16		eqid	$⊢ {Base}_{R} = {Base}_{R}$
17		simp2	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to x \in N$
18		simp3	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to y \in N$
19		simp13	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to M \in K$
20	2 16 3 17 18 19	matecld	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to x M y \in {Base}_{R}$
21	9 10 16	ply1sclid	$⊢ (R \in Ring \land x M y \in {Base}_{R}) \to x M y = {coe}_{1} (algSc ({Poly}_{1} (R)) (x M y)) (0)$
22	15 20 21	syl2anc	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to x M y = {coe}_{1} (algSc ({Poly}_{1} (R)) (x M y)) (0)$
23	14 22	eqtr4d	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land x \in N \land y \in N) \to {coe}_{1} (x T (M) y) (0) = x M y$
24	23	mpoeq3dva	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to (x \in N, y \in N ⟼ {coe}_{1} (x T (M) y) (0)) = (x \in N, y \in N ⟼ x M y)$
25		eqidd	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land (i \in N \land j \in N)) \to (x \in N, y \in N ⟼ x M y) = (x \in N, y \in N ⟼ x M y)$
26		oveq12	$⊢ (x = i \land y = j) \to x M y = i M j$
27	26	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in K) \land (i \in N \land j \in N)) \land (x = i \land y = j)) \to x M y = i M j$
28		simprl	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land (i \in N \land j \in N)) \to i \in N$
29		simprr	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land (i \in N \land j \in N)) \to j \in N$
30		ovexd	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land (i \in N \land j \in N)) \to i M j \in V$
31	25 27 28 29 30	ovmpod	$⊢ ((N \in Fin \land R \in Ring \land M \in K) \land (i \in N \land j \in N)) \to i (x \in N, y \in N ⟼ x M y) j = i M j$
32	31	ralrimivva	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to \forall i \in N \forall j \in N i (x \in N, y \in N ⟼ x M y) j = i M j$
33		simp1	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to N \in Fin$
34		simp2	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to R \in Ring$
35	2 16 3 33 34 20	matbas2d	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to (x \in N, y \in N ⟼ x M y) \in K$
36		simp3	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to M \in K$
37	2 3	eqmat	$⊢ ((x \in N, y \in N ⟼ x M y) \in K \land M \in K) \to ((x \in N, y \in N ⟼ x M y) = M \leftrightarrow \forall i \in N \forall j \in N i (x \in N, y \in N ⟼ x M y) j = i M j)$
38	35 36 37	syl2anc	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to ((x \in N, y \in N ⟼ x M y) = M \leftrightarrow \forall i \in N \forall j \in N i (x \in N, y \in N ⟼ x M y) j = i M j)$
39	32 38	mpbird	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to (x \in N, y \in N ⟼ x M y) = M$
40	8 24 39	3eqtrd	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to I (T (M)) = M$

Metamath Proof Explorer

Theorem m2cpminvid

Proof