pmatcollpw2

Description: Write a polynomial matrix as a sum of matrices whose entries are products of variable powers and constant polynomials collecting like powers. (Contributed by AV, 3-Oct-2019) (Revised by AV, 3-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw1.p	$⊢ P = {Poly}_{1} (R)$
	pmatcollpw1.c	$⊢ C = N Mat P$
	pmatcollpw1.b	$⊢ B = {Base}_{C}$
	pmatcollpw1.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
	pmatcollpw1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	pmatcollpw1.x	$⊢ X = {var}_{1} (R)$
Assertion	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) \underset{˙}{\times} (n \underset{˙}{\times} X))$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw1.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcollpw1.c	$⊢ C = N Mat P$
3		pmatcollpw1.b	$⊢ B = {Base}_{C}$
4		pmatcollpw1.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
5		pmatcollpw1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
6		pmatcollpw1.x	$⊢ X = {var}_{1} (R)$
7	1 2 3 4 5 6	pmatcollpw1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to M = (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)))$
8		eqid	$⊢ 0_{C} = 0_{C}$
9		simp1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to N \in Fin$
10		nn0ex	$⊢ ℕ_{0} \in V$
11	10	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ℕ_{0} \in V$
12	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
13	12	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to P \in Ring$
14		eqid	$⊢ {Base}_{P} = {Base}_{P}$
15	9	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \to N \in Fin$
16	13	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \to P \in Ring$
17		simp1l2	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to R \in Ring$
18		eqid	$⊢ N Mat R = N Mat R$
19		eqid	$⊢ {Base}_{R} = {Base}_{R}$
20		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
21		simp2	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to i \in N$
22		simp3	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to j \in N$
23		simp2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to R \in Ring$
24	23	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \to R \in Ring$
25		simp3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to M \in B$
26	25	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \to M \in B$
27		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
28	24 26 27	3jca	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \to (R \in Ring \land M \in B \land n \in ℕ_{0})$
29	28	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to (R \in Ring \land M \in B \land n \in ℕ_{0})$
30	1 2 3 18 20	decpmatcl	$⊢ (R \in Ring \land M \in B \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
31	29 30	syl	$⊢ (((N \in Fin \land R \in Ring \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)}$
32	18 19 20 21 22 31	matecld	$⊢ (((N \in Fin \land R \in Ring \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}$
33		simp1r	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to n \in ℕ_{0}$
34		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
35	19 1 6 4 34 5 14	ply1tmcl	$⊢ (R \in Ring \land i (M decompPMat n) j \in {Base}_{R} \land n \in ℕ_{0}) \to (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X) \in {Base}_{P}$
36	17 32 33 35	syl3anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X) \in {Base}_{P}$
37	2 14 3 15 16 36	matbas2d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) \in B$
38	1 2 3 4 5 6	pmatcollpw2lem	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {finSupp}_{0_{C}} ((n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))))$
39	2 3 8 9 11 13 37 38	matgsum	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{n \in ℕ_{0}}{\sum_{C}} (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)))$
40	7 39	eqtr4d	$⊢ (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) \underset{˙}{\times} (n \underset{˙}{\times} X))$

Metamath Proof Explorer

Theorem pmatcollpw2

Proof