pmatcollpwfi

Description: Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-2019) (Revised by AV, 4-Dec-2019) (Proof shortened by AV, 3-Jul-2022)

	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	pmatcollpwfi	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ_{0} M = {\sum_{C}}_{n = 0}^{s} ((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	8	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
10		simp3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to M \in B$
11		eqid	$⊢ N Mat R = N Mat R$
12		eqid	$⊢ 0_{(N Mat R)} = 0_{(N Mat R)}$
13	1 2 3 11 12	decpmataa0	$⊢ (R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})$
14	9 10 13	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})$
15	1 2 3 4 5 6 7	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))$
16	15	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})) \to M = \underset{n \in ℕ_{0}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n))$
17		eqid	$⊢ 0_{C} = 0_{C}$
18		simp1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to N \in Fin$
19	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
20	18 9 19	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C \in Ring$
21		ringcmn	$⊢ C \in Ring \to C \in CMnd$
22	20 21	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C \in CMnd$
23	22	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})) \to C \in CMnd$
24	18	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to N \in Fin$
25	9	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to R \in Ring$
26	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
27	25 26	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to P \in Ring$
28	9	anim1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (R \in Ring \land n \in ℕ_{0})$
29		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
30		eqid	$⊢ {Base}_{P} = {Base}_{P}$
31	1 6 29 5 30	ply1moncl	$⊢ (R \in Ring \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{P}$
32	28 31	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{P}$
33		simpl2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to R \in CRing$
34	10	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to M \in B$
35		simpr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
36		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
37	1 2 3 11 36	decpmatcl	$⊢ (R \in CRing \land M \in B \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
38	33 34 35 37	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)}$
39	7 11 36 1 2 3	mat2pmatbas0	$⊢ (N \in Fin \land R \in Ring \land M decompPMat n \in {Base}_{(N Mat R)}) \to T (M decompPMat n) \in B$
40	24 25 38 39	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to T (M decompPMat n) \in B$
41	30 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$
42	24 27 32 40 41	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$
43	42	ralrimiva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \forall n \in ℕ_{0} (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) \in B$
44	43	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})) \to \forall n \in ℕ_{0} (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) \in B$
45		simplr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})) \to s \in ℕ_{0}$
46		fveq2	$⊢ M decompPMat n = 0_{(N Mat R)} \to T (M decompPMat n) = T (0_{(N Mat R)})$
47	9 18	jca	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (R \in Ring \land N \in Fin)$
48	47	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to (R \in Ring \land N \in Fin)$
49		eqid	$⊢ 0_{(N Mat P)} = 0_{(N Mat P)}$
50	7 1 12 49	0mat2pmat	$⊢ (R \in Ring \land N \in Fin) \to T (0_{(N Mat R)}) = 0_{(N Mat P)}$
51	48 50	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to T (0_{(N Mat R)}) = 0_{(N Mat P)}$
52	46 51	sylan9eqr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \land M decompPMat n = 0_{(N Mat R)}) \to T (M decompPMat n) = 0_{(N Mat P)}$
53	52	oveq2d	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \land M decompPMat n = 0_{(N Mat R)}) \to (n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n) = (n \underset{˙}{\times} X) \underset{˙}{} 0_{(N Mat P)}$
54	1 2	pmatlmod	$⊢ (N \in Fin \land R \in Ring) \to C \in LMod$
55	18 9 54	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C \in LMod$
56	55	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to C \in LMod$
57	28	adantlr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to (R \in Ring \land n \in ℕ_{0})$
58	57 31	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{P}$
59	1	ply1crng	$⊢ R \in CRing \to P \in CRing$
60	59	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
61	60	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
62	2	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (C)$
63	61 62	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (C)$
64	63	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (C) = P$
65	64	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to Scalar (C) = P$
66	65	fveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to {Base}_{Scalar (C)} = {Base}_{P}$
67	58 66	eleqtrrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{Scalar (C)}$
68	2	eqcomi	$⊢ N Mat P = C$
69	68	fveq2i	$⊢ 0_{(N Mat P)} = 0_{C}$
70	69	oveq2i	$⊢ (n \underset{˙}{\times} X) \underset{˙}{} 0_{(N Mat P)} = (n \underset{˙}{\times} X) \underset{˙}{} 0_{C}$
71		eqid	$⊢ Scalar (C) = Scalar (C)$
72		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
73	71 4 72 17	lmodvs0	$⊢ (C \in LMod \land n \underset{˙}{\times} X \in {Base}_{Scalar (C)}) \to (n \underset{˙}{\times} X) \underset{˙}{*} 0_{C} = 0_{C}$
74	70 73	eqtrid	$⊢ (C \in LMod \land n \underset{˙}{\times} X \in {Base}_{Scalar (C)}) \to (n \underset{˙}{\times} X) \underset{˙}{*} 0_{(N Mat P)} = 0_{C}$
75	56 67 74	syl2anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to (n \underset{˙}{\times} X) \underset{˙}{*} 0_{(N Mat P)} = 0_{C}$
76	75	adantr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \land M decompPMat n = 0_{(N Mat R)}) \to (n \underset{˙}{\times} X) \underset{˙}{*} 0_{(N Mat P)} = 0_{C}$
77	53 76	eqtrd	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \land M decompPMat n = 0_{(N Mat R)}) \to (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) = 0_{C}$
78	77	ex	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to (M decompPMat n = 0_{(N Mat R)} \to (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) = 0_{C})$
79	78	imim2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to ((s < n \to M decompPMat n = 0_{(N Mat R)}) \to (s < n \to (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) = 0_{C}))$
80	79	ralimdva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \to (\forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)}) \to \forall n \in ℕ_{0} (s < n \to (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) = 0_{C}))$
81	80	imp	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})) \to \forall n \in ℕ_{0} (s < n \to (n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n) = 0_{C})$
82	3 17 23 44 45 81	gsummptnn0fz	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})) \to \underset{n \in ℕ_{0}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)) = {\sum_{C}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n))$
83	16 82	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \land \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)})) \to M = {\sum_{C}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n))$
84	83	ex	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ_{0}) \to (\forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)}) \to M = {\sum_{C}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)))$
85	84	reximdva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to M decompPMat n = 0_{(N Mat R)}) \to \exists s \in ℕ_{0} M = {\sum_{C}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)))$
86	14 85	mpd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ_{0} M = {\sum_{C}}_{n = 0}^{s} ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n))$

Metamath Proof Explorer

Theorem pmatcollpwfi

Proof