pm2mpval

Description: Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpval.p	$⊢ P = {Poly}_{1} (R)$
	pm2mpval.c	$⊢ C = N Mat P$
	pm2mpval.b	$⊢ B = {Base}_{C}$
	pm2mpval.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
	pm2mpval.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	pm2mpval.x	$⊢ X = {var}_{1} (A)$
	pm2mpval.a	$⊢ A = N Mat R$
	pm2mpval.q	$⊢ Q = {Poly}_{1} (A)$
	pm2mpval.t	$⊢ T = N pMatToMatPoly R$
Assertion	pm2mpval	$⊢ (N \in Fin \land R \in V) \to T = (m \in B ⟼ \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpval.c	$⊢ C = N Mat P$
3		pm2mpval.b	$⊢ B = {Base}_{C}$
4		pm2mpval.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
5		pm2mpval.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
6		pm2mpval.x	$⊢ X = {var}_{1} (A)$
7		pm2mpval.a	$⊢ A = N Mat R$
8		pm2mpval.q	$⊢ Q = {Poly}_{1} (A)$
9		pm2mpval.t	$⊢ T = N pMatToMatPoly R$
10		df-pm2mp	$⊢ pMatToMatPoly = (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat {Poly}_{1} (r))} ⟼ ⦋ (n Mat r) / a ⦌ ⦋ {Poly}_{1} (a) / q ⦌ (\underset{k \in ℕ_{0}}{\sum_{q}}, ((m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a))))))$
11	10	a1i	$⊢ (N \in Fin \land R \in V) \to pMatToMatPoly = (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat {Poly}_{1} (r))} ⟼ ⦋ (n Mat r) / a ⦌ ⦋ {Poly}_{1} (a) / q ⦌ (\underset{k \in ℕ_{0}}{\sum_{q}}, ((m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a))))))$
12		simpl	$⊢ (n = N \land r = R) \to n = N$
13		fveq2	$⊢ r = R \to {Poly}_{1} (r) = {Poly}_{1} (R)$
14	13	adantl	$⊢ (n = N \land r = R) \to {Poly}_{1} (r) = {Poly}_{1} (R)$
15	12 14	oveq12d	$⊢ (n = N \land r = R) \to n Mat {Poly}_{1} (r) = N Mat {Poly}_{1} (R)$
16	15	fveq2d	$⊢ (n = N \land r = R) \to {Base}_{(n Mat {Poly}_{1} (r))} = {Base}_{(N Mat {Poly}_{1} (R))}$
17	1	oveq2i	$⊢ N Mat P = N Mat {Poly}_{1} (R)$
18	2 17	eqtri	$⊢ C = N Mat {Poly}_{1} (R)$
19	18	fveq2i	$⊢ {Base}_{C} = {Base}_{(N Mat {Poly}_{1} (R))}$
20	3 19	eqtri	$⊢ B = {Base}_{(N Mat {Poly}_{1} (R))}$
21	16 20	eqtr4di	$⊢ (n = N \land r = R) \to {Base}_{(n Mat {Poly}_{1} (r))} = B$
22	21	adantl	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to {Base}_{(n Mat {Poly}_{1} (r))} = B$
23		ovex	$⊢ n Mat r \in V$
24		fvexd	$⊢ a = n Mat r \to {Poly}_{1} (a) \in V$
25		simpr	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to q = {Poly}_{1} (a)$
26		fveq2	$⊢ a = n Mat r \to {Poly}_{1} (a) = {Poly}_{1} (n Mat r)$
27	26	adantr	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to {Poly}_{1} (a) = {Poly}_{1} (n Mat r)$
28	25 27	eqtrd	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to q = {Poly}_{1} (n Mat r)$
29	28	fveq2d	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to \cdot_{q} = \cdot_{{Poly}_{1} (n Mat r)}$
30		eqidd	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to m decompPMat k = m decompPMat k$
31	28	fveq2d	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to {mulGrp}_{q} = {mulGrp}_{{Poly}_{1} (n Mat r)}$
32	31	fveq2d	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to \cdot_{{mulGrp}_{q}} = \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}}$
33		eqidd	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to k = k$
34		fveq2	$⊢ a = n Mat r \to {var}_{1} (a) = {var}_{1} (n Mat r)$
35	34	adantr	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to {var}_{1} (a) = {var}_{1} (n Mat r)$
36	32 33 35	oveq123d	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to k \cdot_{{mulGrp}_{q}} {var}_{1} (a) = k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r)$
37	29 30 36	oveq123d	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to (m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a)) = (m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r))$
38	37	mpteq2dv	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to (k \in ℕ_{0} ⟼ (m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a))) = (k \in ℕ_{0} ⟼ (m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r)))$
39	28 38	oveq12d	$⊢ (a = n Mat r \land q = {Poly}_{1} (a)) \to \underset{k \in ℕ_{0}}{\sum_{q}} ((m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a))) = \underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (n Mat r)}} ((m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r)))$
40	24 39	csbied	$⊢ a = n Mat r \to ⦋ {Poly}_{1} (a) / q ⦌ (\underset{k \in ℕ_{0}}{\sum_{q}}, ((m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a)))) = \underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (n Mat r)}} ((m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r)))$
41	23 40	csbie	$⊢ ⦋ (n Mat r) / a ⦌ ⦋ {Poly}_{1} (a) / q ⦌ (\underset{k \in ℕ_{0}}{\sum_{q}}, ((m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a)))) = \underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (n Mat r)}} ((m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r)))$
42		oveq12	$⊢ (n = N \land r = R) \to n Mat r = N Mat R$
43	42	fveq2d	$⊢ (n = N \land r = R) \to {Poly}_{1} (n Mat r) = {Poly}_{1} (N Mat R)$
44	7	fveq2i	$⊢ {Poly}_{1} (A) = {Poly}_{1} (N Mat R)$
45	8 44	eqtri	$⊢ Q = {Poly}_{1} (N Mat R)$
46	43 45	eqtr4di	$⊢ (n = N \land r = R) \to {Poly}_{1} (n Mat r) = Q$
47	43	fveq2d	$⊢ (n = N \land r = R) \to \cdot_{{Poly}_{1} (n Mat r)} = \cdot_{{Poly}_{1} (N Mat R)}$
48	45	fveq2i	$⊢ \cdot_{Q} = \cdot_{{Poly}_{1} (N Mat R)}$
49	4 48	eqtri	$⊢ \underset{˙}{*} = \cdot_{{Poly}_{1} (N Mat R)}$
50	47 49	eqtr4di	$⊢ (n = N \land r = R) \to \cdot_{{Poly}_{1} (n Mat r)} = \underset{˙}{*}$
51		eqidd	$⊢ (n = N \land r = R) \to m decompPMat k = m decompPMat k$
52	43	fveq2d	$⊢ (n = N \land r = R) \to {mulGrp}_{{Poly}_{1} (n Mat r)} = {mulGrp}_{{Poly}_{1} (N Mat R)}$
53	52	fveq2d	$⊢ (n = N \land r = R) \to \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} = \cdot_{{mulGrp}_{{Poly}_{1} (N Mat R)}}$
54	45	fveq2i	$⊢ {mulGrp}_{Q} = {mulGrp}_{{Poly}_{1} (N Mat R)}$
55	54	fveq2i	$⊢ \cdot_{{mulGrp}_{Q}} = \cdot_{{mulGrp}_{{Poly}_{1} (N Mat R)}}$
56	5 55	eqtri	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (N Mat R)}}$
57	53 56	eqtr4di	$⊢ (n = N \land r = R) \to \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} = \underset{˙}{\times}$
58		eqidd	$⊢ (n = N \land r = R) \to k = k$
59	42	fveq2d	$⊢ (n = N \land r = R) \to {var}_{1} (n Mat r) = {var}_{1} (N Mat R)$
60	7	fveq2i	$⊢ {var}_{1} (A) = {var}_{1} (N Mat R)$
61	6 60	eqtri	$⊢ X = {var}_{1} (N Mat R)$
62	59 61	eqtr4di	$⊢ (n = N \land r = R) \to {var}_{1} (n Mat r) = X$
63	57 58 62	oveq123d	$⊢ (n = N \land r = R) \to k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r) = k \underset{˙}{\times} X$
64	50 51 63	oveq123d	$⊢ (n = N \land r = R) \to (m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r)) = (m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)$
65	64	mpteq2dv	$⊢ (n = N \land r = R) \to (k \in ℕ_{0} ⟼ (m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r))) = (k \in ℕ_{0} ⟼ (m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
66	46 65	oveq12d	$⊢ (n = N \land r = R) \to \underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (n Mat r)}} ((m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r))) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
67	66	adantl	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to \underset{k \in ℕ_{0}}{\sum_{{Poly}_{1} (n Mat r)}} ((m decompPMat k) \cdot_{{Poly}_{1} (n Mat r)} (k \cdot_{{mulGrp}_{{Poly}_{1} (n Mat r)}} {var}_{1} (n Mat r))) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
68	41 67	eqtrid	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to ⦋ (n Mat r) / a ⦌ ⦋ {Poly}_{1} (a) / q ⦌ (\underset{k \in ℕ_{0}}{\sum_{q}}, ((m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a)))) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
69	22 68	mpteq12dv	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to (m \in {Base}_{(n Mat {Poly}_{1} (r))} ⟼ ⦋ (n Mat r) / a ⦌ ⦋ {Poly}_{1} (a) / q ⦌ (\underset{k \in ℕ_{0}}{\sum_{q}}, ((m decompPMat k) \cdot_{q} (k \cdot_{{mulGrp}_{q}} {var}_{1} (a))))) = (m \in B ⟼ \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
70		simpl	$⊢ (N \in Fin \land R \in V) \to N \in Fin$
71		elex	$⊢ R \in V \to R \in V$
72	71	adantl	$⊢ (N \in Fin \land R \in V) \to R \in V$
73	3	fvexi	$⊢ B \in V$
74	73	mptex	$⊢ (m \in B ⟼ \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) \in V$
75	74	a1i	$⊢ (N \in Fin \land R \in V) \to (m \in B ⟼ \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) \in V$
76	11 69 70 72 75	ovmpod	$⊢ (N \in Fin \land R \in V) \to N pMatToMatPoly R = (m \in B ⟼ \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
77	9 76	eqtrid	$⊢ (N \in Fin \land R \in V) \to T = (m \in B ⟼ \underset{k \in ℕ_{0}}{\sum_{Q}} ((m decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem pm2mpval

Proof