mp2pm2mp

Description: A polynomial over matrices transformed into a polynomial matrix transformed back into the polynomial over matrices. (Contributed by AV, 12-Oct-2019)

	Ref	Expression
Hypotheses	mp2pm2mp.a	$⊢ A = N Mat R$
	mp2pm2mp.q	$⊢ Q = {Poly}_{1} (A)$
	mp2pm2mp.l	$⊢ L = {Base}_{Q}$
	mp2pm2mp.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	mp2pm2mp.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
	mp2pm2mp.y	$⊢ Y = {var}_{1} (R)$
	mp2pm2mp.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
	mp2pm2mplem2.p	$⊢ P = {Poly}_{1} (R)$
	mp2pm2mp.t	$⊢ T = N pMatToMatPoly R$
Assertion	mp2pm2mp	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to T (I (O)) = O$

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	$⊢ A = N Mat R$
2		mp2pm2mp.q	$⊢ Q = {Poly}_{1} (A)$
3		mp2pm2mp.l	$⊢ L = {Base}_{Q}$
4		mp2pm2mp.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		mp2pm2mp.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
6		mp2pm2mp.y	$⊢ Y = {var}_{1} (R)$
7		mp2pm2mp.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
8		mp2pm2mplem2.p	$⊢ P = {Poly}_{1} (R)$
9		mp2pm2mp.t	$⊢ T = N pMatToMatPoly R$
10		eqid	$⊢ N Mat P = N Mat P$
11		eqid	$⊢ {Base}_{(N Mat P)} = {Base}_{(N Mat P)}$
12	1 2 3 8 4 5 6 7 10 11	mply1topmatcl	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to I (O) \in {Base}_{(N Mat P)}$
13		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
14		eqid	$⊢ \cdot_{{mulGrp}_{Q}} = \cdot_{{mulGrp}_{Q}}$
15		eqid	$⊢ {var}_{1} (A) = {var}_{1} (A)$
16	8 10 11 13 14 15 1 2 9	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land I (O) \in {Base}_{(N Mat P)}) \to T (I (O)) = \underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
17	12 16	syld3an3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to T (I (O)) = \underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
18	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
19	18	3adant3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to A \in Ring$
20		eqid	$⊢ 0_{Q} = 0_{Q}$
21	2	ply1ring	$⊢ A \in Ring \to Q \in Ring$
22		ringcmn	$⊢ Q \in Ring \to Q \in CMnd$
23	18 21 22	3syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in CMnd$
24	23	3adant3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to Q \in CMnd$
25		nn0ex	$⊢ ℕ_{0} \in V$
26	25	a1i	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to ℕ_{0} \in V$
27	19	adantr	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land n \in ℕ_{0}) \to A \in Ring$
28		simpl2	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land n \in ℕ_{0}) \to R \in Ring$
29	12	adantr	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land n \in ℕ_{0}) \to I (O) \in {Base}_{(N Mat P)}$
30		simpr	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
31		eqid	$⊢ {Base}_{A} = {Base}_{A}$
32	8 10 11 1 31	decpmatcl	$⊢ (R \in Ring \land I (O) \in {Base}_{(N Mat P)} \land n \in ℕ_{0}) \to I (O) decompPMat n \in {Base}_{A}$
33	28 29 30 32	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land n \in ℕ_{0}) \to I (O) decompPMat n \in {Base}_{A}$
34		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
35	31 2 15 13 34 14 3	ply1tmcl	$⊢ (A \in Ring \land I (O) decompPMat n \in {Base}_{A} \land n \in ℕ_{0}) \to (I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in L$
36	27 33 30 35	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land n \in ℕ_{0}) \to (I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in L$
37	36	fmpttd	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (n \in ℕ_{0} ⟼ (I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) : ℕ_{0} ⟶ L$
38		fveq2	$⊢ k = n \to {coe}_{1} (p) (k) = {coe}_{1} (p) (n)$
39	38	oveqd	$⊢ k = n \to i {coe}_{1} (p) (k) j = i {coe}_{1} (p) (n) j$
40		oveq1	$⊢ k = n \to k E Y = n E Y$
41	39 40	oveq12d	$⊢ k = n \to (i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y) = (i {coe}_{1} (p) (n) j) \underset{˙}{\cdot} (n E Y)$
42	41	cbvmptv	$⊢ (k \in ℕ_{0} ⟼ (i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)) = (n \in ℕ_{0} ⟼ (i {coe}_{1} (p) (n) j) \underset{˙}{\cdot} (n E Y))$
43	42	a1i	$⊢ (i \in N \land j \in N) \to (k \in ℕ_{0} ⟼ (i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)) = (n \in ℕ_{0} ⟼ (i {coe}_{1} (p) (n) j) \underset{˙}{\cdot} (n E Y))$
44	43	oveq2d	$⊢ (i \in N \land j \in N) \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)) = \underset{n \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (n) j) \underset{˙}{\cdot} (n E Y))$
45	44	mpoeq3ia	$⊢ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))) = (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (n) j) \underset{˙}{\cdot} (n E Y)))$
46	45	mpteq2i	$⊢ (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y)))) = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (n) j) \underset{˙}{\cdot} (n E Y))))$
47	7 46	eqtri	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (n) j) \underset{˙}{\cdot} (n E Y))))$
48	1 2 3 4 5 6 47 8 13 14 15	mp2pm2mplem5	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {finSupp}_{0_{Q}} ((n \in ℕ_{0} ⟼ (I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
49	3 20 24 26 37 48	gsumcl	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to \underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in L$
50		simp3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to O \in L$
51	19 49 50	3jca	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (A \in Ring \land \underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in L \land O \in L)$
52	1 2 3 4 5 6 7 8	mp2pm2mplem4	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land n \in ℕ_{0}) \to I (O) decompPMat n = {coe}_{1} (O) (n)$
53	52	oveq1d	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land n \in ℕ_{0}) \to (I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) = {coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))$
54	53	adantlr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \land n \in ℕ_{0}) \to (I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) = {coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))$
55	54	mpteq2dva	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ (I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = (n \in ℕ_{0} ⟼ {coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
56	55	oveq2d	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to \underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = \underset{n \in ℕ_{0}}{\sum_{Q}} ({coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
57	56	fveq2d	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) = {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ({coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
58	57	fveq1d	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) = {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ({coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l)$
59	19 50	jca	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (A \in Ring \land O \in L)$
60	59	adantr	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to (A \in Ring \land O \in L)$
61		eqid	$⊢ {coe}_{1} (O) = {coe}_{1} (O)$
62	2 15 3 13 34 14 61	ply1coe	$⊢ (A \in Ring \land O \in L) \to O = \underset{n \in ℕ_{0}}{\sum_{Q}} ({coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
63	60 62	syl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to O = \underset{n \in ℕ_{0}}{\sum_{Q}} ({coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
64	63	eqcomd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to \underset{n \in ℕ_{0}}{\sum_{Q}} ({coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = O$
65	64	fveq2d	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ({coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) = {coe}_{1} (O)$
66	65	fveq1d	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ({coe}_{1} (O) (n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) = {coe}_{1} (O) (l)$
67	58 66	eqtrd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land l \in ℕ_{0}) \to {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) = {coe}_{1} (O) (l)$
68	67	ralrimiva	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to \forall l \in ℕ_{0} {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) = {coe}_{1} (O) (l)$
69		eqid	$⊢ {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) = {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
70	2 3 69 61	eqcoe1ply1eq	$⊢ (A \in Ring \land \underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in L \land O \in L) \to (\forall l \in ℕ_{0} {coe}_{1} (\underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) = {coe}_{1} (O) (l) \to \underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = O)$
71	51 68 70	sylc	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to \underset{n \in ℕ_{0}}{\sum_{Q}} ((I (O) decompPMat n) \cdot_{Q} (n \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = O$
72	17 71	eqtrd	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to T (I (O)) = O$

Metamath Proof Explorer

Theorem mp2pm2mp

Proof