pmatcollpw

Description: Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 26-Oct-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
	pmatcollpw.c	$⊢ C = N Mat P$
	pmatcollpw.b	$⊢ B = {Base}_{C}$
	pmatcollpw.m	$⊢ \underset{˙}{*} = \cdot_{C}$
	pmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	pmatcollpw.x	$⊢ X = {var}_{1} (R)$
	pmatcollpw.t	$⊢ T = N matToPolyMat R$
Assertion	pmatcollpw	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to M = \underset{n \in ℕ_{0}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n))$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcollpw.c	$⊢ C = N Mat P$
3		pmatcollpw.b	$⊢ B = {Base}_{C}$
4		pmatcollpw.m	$⊢ \underset{˙}{*} = \cdot_{C}$
5		pmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
6		pmatcollpw.x	$⊢ X = {var}_{1} (R)$
7		pmatcollpw.t	$⊢ T = N matToPolyMat R$
8		crngring	$⊢ R \in CRing \to R \in Ring$
9		eqid	$⊢ \cdot_{P} = \cdot_{P}$
10	1 2 3 9 5 6	pmatcollpw2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to M = \underset{n \in ℕ_{0}}{\sum_{C}} (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X))$
11	8 10	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to M = \underset{n \in ℕ_{0}}{\sum_{C}} (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X))$
12		eqidd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X))$
13		oveq12	$⊢ (i = a \land j = b) \to i (M decompPMat n) j = a (M decompPMat n) b$
14	13	oveq1d	$⊢ (i = a \land j = b) \to (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X) = (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X)$
15	14	adantl	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \land (i = a \land j = b)) \to (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X) = (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X)$
16		simprl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to a \in N$
17		simpr	$⊢ (a \in N \land b \in N) \to b \in N$
18	17	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to b \in N$
19		simp2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in CRing$
20	19	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to R \in CRing$
21	20 8	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to R \in Ring$
22	21	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to R \in Ring$
23		eqid	$⊢ N Mat R = N Mat R$
24		eqid	$⊢ {Base}_{R} = {Base}_{R}$
25		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
26		simp3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to M \in B$
27	26	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to M \in B$
28		simpr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
29	1 2 3 23 25	decpmatcl	$⊢ (R \in CRing \land M \in B \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
30	20 27 28 29	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
31	30	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to M decompPMat n \in {Base}_{(N Mat R)}$
32	23 24 25 16 18 31	matecld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to a (M decompPMat n) b \in {Base}_{R}$
33		simplr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to n \in ℕ_{0}$
34		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
35		eqid	$⊢ {Base}_{P} = {Base}_{P}$
36	24 1 6 9 34 5 35	ply1tmcl	$⊢ (R \in Ring \land a (M decompPMat n) b \in {Base}_{R} \land n \in ℕ_{0}) \to (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X) \in {Base}_{P}$
37	22 32 33 36	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X) \in {Base}_{P}$
38	12 15 16 18 37	ovmpod	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to a (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) b = (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X)$
39	1 2 3 4 5 6 7	pmatcollpwlem	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X) = a ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)) b$
40	39	3expb	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X) = a ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)) b$
41	38 40	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to a (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) b = a ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)) b$
42	41	ralrimivva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) b = a ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)) b$
43		simpl1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to N \in Fin$
44	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
45	8 44	syl	$⊢ R \in CRing \to P \in Ring$
46	45	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
47	46	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to P \in Ring$
48	21	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to R \in Ring$
49		simp2	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to i \in N$
50		simp3	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to j \in N$
51	30	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to M decompPMat n \in {Base}_{(N Mat R)}$
52	23 24 25 49 50 51	matecld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to i (M decompPMat n) j \in {Base}_{R}$
53	28	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to n \in ℕ_{0}$
54	24 1 6 9 34 5 35	ply1tmcl	$⊢ (R \in Ring \land i (M decompPMat n) j \in {Base}_{R} \land n \in ℕ_{0}) \to (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X) \in {Base}_{P}$
55	48 52 53 54	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X) \in {Base}_{P}$
56	2 35 3 43 47 55	matbas2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) \in B$
57	8	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
58	1 6 34 5 35	ply1moncl	$⊢ (R \in Ring \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{P}$
59	57 58	sylan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{P}$
60	57	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to R \in Ring$
61	7 23 25 1 2	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M decompPMat n \in {Base}_{(N Mat R)}) \to T (M decompPMat n) \in {Base}_{C}$
62	43 60 30 61	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to T (M decompPMat n) \in {Base}_{C}$
63	62 3	eleqtrrdi	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to T (M decompPMat n) \in B$
64	35 2 3 4	matvscl	$⊢ ((N \in Fin \land P \in Ring) \land (n \underset{˙}{\times} X \in {Base}_{P} \land T (M decompPMat n) \in B)) \to (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) \in B$
65	43 47 59 63 64	syl22anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) \in B$
66	2 3	eqmat	$⊢ ((i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) \in B \land (n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n) \in B) \to ((i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) = (n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n) \leftrightarrow \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) b = a ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)) b)$
67	56 65 66	syl2anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to ((i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) = (n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n) \leftrightarrow \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) b = a ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)) b)$
68	42 67	mpbird	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) = (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)$
69	68	mpteq2dva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X))) = (n \in ℕ_{0} ⟼ (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n))$
70	69	oveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{n \in ℕ_{0}}{\sum_{C}} (i \in N, j \in N ⟼ (i (M decompPMat n) j) \cdot_{P} (n \underset{˙}{\times} X)) = \underset{n \in ℕ_{0}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n))$
71	11 70	eqtrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to M = \underset{n \in ℕ_{0}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n))$

Metamath Proof Explorer

Theorem pmatcollpw

Proof