m2cpminvid2

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

	Ref	Expression
Hypotheses	m2cpminvid2.s	$⊢ S = N ConstPolyMat R$
	m2cpminvid2.i	$⊢ I = N cPolyMatToMat R$
	m2cpminvid2.t	$⊢ T = N matToPolyMat R$
Assertion	m2cpminvid2	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to T (I (M)) = M$

Proof

Step	Hyp	Ref	Expression
1		m2cpminvid2.s	$⊢ S = N ConstPolyMat R$
2		m2cpminvid2.i	$⊢ I = N cPolyMatToMat R$
3		m2cpminvid2.t	$⊢ T = N matToPolyMat R$
4	2 1	cpm2mval	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to I (M) = (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0))$
5	4	fveq2d	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to T (I (M)) = T ((x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)))$
6		simp1	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to N \in Fin$
7		simp2	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to R \in Ring$
8		eqid	$⊢ N Mat R = N Mat R$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
11		eqid	$⊢ N Mat {Poly}_{1} (R) = N Mat {Poly}_{1} (R)$
12		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
13		eqid	$⊢ {Base}_{(N Mat {Poly}_{1} (R))} = {Base}_{(N Mat {Poly}_{1} (R))}$
14		simp2	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land x \in N \land y \in N) \to x \in N$
15		simp3	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land x \in N \land y \in N) \to y \in N$
16		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
17	1 16 11 13	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to M \in {Base}_{(N Mat {Poly}_{1} (R))}$
18	17	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land x \in N \land y \in N) \to M \in {Base}_{(N Mat {Poly}_{1} (R))}$
19	11 12 13 14 15 18	matecld	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land x \in N \land y \in N) \to x M y \in {Base}_{{Poly}_{1} (R)}$
20		0nn0	$⊢ 0 \in ℕ_{0}$
21		eqid	$⊢ {coe}_{1} (x M y) = {coe}_{1} (x M y)$
22	21 12 16 9	coe1fvalcl	$⊢ (x M y \in {Base}_{{Poly}_{1} (R)} \land 0 \in ℕ_{0}) \to {coe}_{1} (x M y) (0) \in {Base}_{R}$
23	19 20 22	sylancl	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land x \in N \land y \in N) \to {coe}_{1} (x M y) (0) \in {Base}_{R}$
24	8 9 10 6 7 23	matbas2d	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) \in {Base}_{(N Mat R)}$
25		eqid	$⊢ algSc ({Poly}_{1} (R)) = algSc ({Poly}_{1} (R))$
26	3 8 10 16 25	mat2pmatval	$⊢ (N \in Fin \land R \in Ring \land (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) \in {Base}_{(N Mat R)}) \to T ((x \in N, y \in N ⟼ {coe}_{1} (x M y) (0))) = (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) (i (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) j))$
27	6 7 24 26	syl3anc	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to T ((x \in N, y \in N ⟼ {coe}_{1} (x M y) (0))) = (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) (i (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) j))$
28		eqidd	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \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))$
29		oveq12	$⊢ (x = i \land y = j) \to x M y = i M j$
30	29	fveq2d	$⊢ (x = i \land y = j) \to {coe}_{1} (x M y) = {coe}_{1} (i M j)$
31	30	fveq1d	$⊢ (x = i \land y = j) \to {coe}_{1} (x M y) (0) = {coe}_{1} (i M j) (0)$
32	31	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \land (x = i \land y = j)) \to {coe}_{1} (x M y) (0) = {coe}_{1} (i M j) (0)$
33		simp2	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to i \in N$
34		simp3	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to j \in N$
35		fvexd	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to {coe}_{1} (i M j) (0) \in V$
36	28 32 33 34 35	ovmpod	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to i (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) j = {coe}_{1} (i M j) (0)$
37	36	fveq2d	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to algSc ({Poly}_{1} (R)) (i (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) j) = algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))$
38	37	mpoeq3dva	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) (i (x \in N, y \in N ⟼ {coe}_{1} (x M y) (0)) j)) = (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0)))$
39	27 38	eqtrd	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to T ((x \in N, y \in N ⟼ {coe}_{1} (x M y) (0))) = (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0)))$
40	1 16	m2cpminvid2lem	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to \forall n \in ℕ_{0} {coe}_{1} (algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n)$
41		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to R \in Ring$
42		simprl	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to x \in N$
43		simprr	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to y \in N$
44	17	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to M \in {Base}_{(N Mat {Poly}_{1} (R))}$
45	11 12 13 42 43 44	matecld	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to x M y \in {Base}_{{Poly}_{1} (R)}$
46	45 20 22	sylancl	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to {coe}_{1} (x M y) (0) \in {Base}_{R}$
47	16 25 9 12	ply1sclcl	$⊢ (R \in Ring \land {coe}_{1} (x M y) (0) \in {Base}_{R}) \to algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) \in {Base}_{{Poly}_{1} (R)}$
48	41 46 47	syl2anc	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) \in {Base}_{{Poly}_{1} (R)}$
49		eqid	$⊢ {coe}_{1} (algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0))) = {coe}_{1} (algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)))$
50	16 12 49 21	ply1coe1eq	$⊢ (R \in Ring \land algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) \in {Base}_{{Poly}_{1} (R)} \land x M y \in {Base}_{{Poly}_{1} (R)}) \to (\forall n \in ℕ_{0} {coe}_{1} (algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \leftrightarrow algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) = x M y)$
51	50	bicomd	$⊢ (R \in Ring \land algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) \in {Base}_{{Poly}_{1} (R)} \land x M y \in {Base}_{{Poly}_{1} (R)}) \to (algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) = x M y \leftrightarrow \forall n \in ℕ_{0} {coe}_{1} (algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n))$
52	41 48 45 51	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) = x M y \leftrightarrow \forall n \in ℕ_{0} {coe}_{1} (algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n))$
53	40 52	mpbird	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) = x M y$
54	53	ralrimivva	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to \forall x \in N \forall y \in N algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) = x M y$
55		eqidd	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land x \in N) \land y \in N) \to (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) = (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0)))$
56		oveq12	$⊢ (i = x \land j = y) \to i M j = x M y$
57	56	fveq2d	$⊢ (i = x \land j = y) \to {coe}_{1} (i M j) = {coe}_{1} (x M y)$
58	57	fveq1d	$⊢ (i = x \land j = y) \to {coe}_{1} (i M j) (0) = {coe}_{1} (x M y) (0)$
59	58	fveq2d	$⊢ (i = x \land j = y) \to algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0)) = algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0))$
60	59	adantl	$⊢ ((((N \in Fin \land R \in Ring \land M \in S) \land x \in N) \land y \in N) \land (i = x \land j = y)) \to algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0)) = algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0))$
61		simplr	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land x \in N) \land y \in N) \to x \in N$
62		simpr	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land x \in N) \land y \in N) \to y \in N$
63		fvexd	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land x \in N) \land y \in N) \to algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) \in V$
64	55 60 61 62 63	ovmpod	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land x \in N) \land y \in N) \to x (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) y = algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0))$
65	64	eqeq1d	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land x \in N) \land y \in N) \to (x (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) y = x M y \leftrightarrow algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) = x M y)$
66	65	anasss	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (x (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) y = x M y \leftrightarrow algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) = x M y)$
67	66	2ralbidva	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to (\forall x \in N \forall y \in N x (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) y = x M y \leftrightarrow \forall x \in N \forall y \in N algSc ({Poly}_{1} (R)) ({coe}_{1} (x M y) (0)) = x M y)$
68	54 67	mpbird	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) y = x M y$
69		fvexd	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to {Poly}_{1} (R) \in V$
70	7	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to R \in Ring$
71	17	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to M \in {Base}_{(N Mat {Poly}_{1} (R))}$
72	11 12 13 33 34 71	matecld	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to i M j \in {Base}_{{Poly}_{1} (R)}$
73		eqid	$⊢ {coe}_{1} (i M j) = {coe}_{1} (i M j)$
74	73 12 16 9	coe1fvalcl	$⊢ (i M j \in {Base}_{{Poly}_{1} (R)} \land 0 \in ℕ_{0}) \to {coe}_{1} (i M j) (0) \in {Base}_{R}$
75	72 20 74	sylancl	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to {coe}_{1} (i M j) (0) \in {Base}_{R}$
76	16 25 9 12	ply1sclcl	$⊢ (R \in Ring \land {coe}_{1} (i M j) (0) \in {Base}_{R}) \to algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0)) \in {Base}_{{Poly}_{1} (R)}$
77	70 75 76	syl2anc	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land i \in N \land j \in N) \to algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0)) \in {Base}_{{Poly}_{1} (R)}$
78	11 12 13 6 69 77	matbas2d	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) \in {Base}_{(N Mat {Poly}_{1} (R))}$
79	11 13	eqmat	$⊢ ((i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) \in {Base}_{(N Mat {Poly}_{1} (R))} \land M \in {Base}_{(N Mat {Poly}_{1} (R))}) \to ((i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) = M \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) y = x M y)$
80	78 17 79	syl2anc	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to ((i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) = M \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) y = x M y)$
81	68 80	mpbird	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to (i \in N, j \in N ⟼ algSc ({Poly}_{1} (R)) ({coe}_{1} (i M j) (0))) = M$
82	5 39 81	3eqtrd	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to T (I (M)) = M$

Metamath Proof Explorer

Theorem m2cpminvid2

Proof