pmatcollpw1

Description: Write a polynomial matrix as a matrix of sums of scaled monomials. (Contributed by AV, 29-Sep-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	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)))$

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	pmatcollpw1lem2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a M b = \underset{n \in ℕ_{0}}{\sum_{P}} ((a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$
8		eqidd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((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)))$
9		oveq12	$⊢ (i = a \land j = b) \to i (M decompPMat n) j = a (M decompPMat n) b$
10	9	oveq1d	$⊢ (i = a \land j = b) \to (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X) = (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X)$
11	10	mpteq2dv	$⊢ (i = a \land j = b) \to (n \in ℕ_{0} ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) = (n \in ℕ_{0} ⟼ (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$
12	11	oveq2d	$⊢ (i = a \land j = b) \to \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) = \underset{n \in ℕ_{0}}{\sum_{P}} ((a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$
13	12	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land (i = a \land j = b)) \to \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) = \underset{n \in ℕ_{0}}{\sum_{P}} ((a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$
14		simprl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a \in N$
15		simprr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to b \in N$
16		eqid	$⊢ {Base}_{P} = {Base}_{P}$
17		eqid	$⊢ 0_{P} = 0_{P}$
18	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
19		ringcmn	$⊢ P \in Ring \to P \in CMnd$
20	18 19	syl	$⊢ R \in Ring \to P \in CMnd$
21	20	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to P \in CMnd$
22	21	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to P \in CMnd$
23		nn0ex	$⊢ ℕ_{0} \in V$
24	23	a1i	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to ℕ_{0} \in V$
25		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to R \in Ring$
26	25	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to R \in Ring$
27		eqid	$⊢ N Mat R = N Mat R$
28		eqid	$⊢ {Base}_{R} = {Base}_{R}$
29		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
30		simplrl	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to a \in N$
31	15	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to b \in N$
32		simpl3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to M \in B$
33	32	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to M \in B$
34		simpr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
35	1 2 3 27 29	decpmatcl	$⊢ (R \in Ring \land M \in B \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
36	26 33 34 35	syl3anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
37	27 28 29 30 31 36	matecld	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to a (M decompPMat n) b \in {Base}_{R}$
38		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
39	28 1 6 4 38 5 16	ply1tmcl	$⊢ (R \in Ring \land a (M decompPMat n) b \in {Base}_{R} \land n \in ℕ_{0}) \to (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X) \in {Base}_{P}$
40	26 37 34 39	syl3anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X) \in {Base}_{P}$
41	40	fmpttd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to (n \in ℕ_{0} ⟼ (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X)) : ℕ_{0} ⟶ {Base}_{P}$
42	1 2 3 4 5 6	pmatcollpw1lem1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land a \in N \land b \in N) \to {finSupp}_{0_{P}} ((n \in ℕ_{0} ⟼ (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X)))$
43	42	3expb	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to {finSupp}_{0_{P}} ((n \in ℕ_{0} ⟼ (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X)))$
44	16 17 22 24 41 43	gsumcl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to \underset{n \in ℕ_{0}}{\sum_{P}} ((a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X)) \in {Base}_{P}$
45	8 13 14 15 44	ovmpod	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) b = \underset{n \in ℕ_{0}}{\sum_{P}} ((a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$
46	7 45	eqtr4d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a M b = a (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) b$
47	46	ralrimivva	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \forall a \in N \forall b \in N a M b = a (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) b$
48		simp3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to M \in B$
49		simp1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to N \in Fin$
50	18	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to P \in Ring$
51	21	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \to P \in CMnd$
52	23	a1i	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \to ℕ_{0} \in V$
53		simpl12	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \land n \in ℕ_{0}) \to R \in Ring$
54		simpl2	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \land n \in ℕ_{0}) \to i \in N$
55		simpl3	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \land n \in ℕ_{0}) \to j \in N$
56	48	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \to M \in B$
57	56	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \land n \in ℕ_{0}) \to M \in B$
58		simpr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
59	53 57 58 35	syl3anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
60	27 28 29 54 55 59	matecld	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \land n \in ℕ_{0}) \to i (M decompPMat n) j \in {Base}_{R}$
61	28 1 6 4 38 5 16	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}$
62	53 60 58 61	syl3anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \land n \in ℕ_{0}) \to (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X) \in {Base}_{P}$
63	62	fmpttd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \to (n \in ℕ_{0} ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) : ℕ_{0} ⟶ {Base}_{P}$
64	1 2 3 4 5 6	pmatcollpw1lem1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \to {finSupp}_{0_{P}} ((n \in ℕ_{0} ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)))$
65	16 17 51 52 63 64	gsumcl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land i \in N \land j \in N) \to \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) \in {Base}_{P}$
66	2 16 3 49 50 65	matbas2d	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) \in B$
67	2 3	eqmat	$⊢ (M \in B \land (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) \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))) \leftrightarrow \forall a \in N \forall b \in N a M b = a (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) b)$
68	48 66 67	syl2anc	$⊢ (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))) \leftrightarrow \forall a \in N \forall b \in N a M b = a (i \in N, j \in N ⟼ \underset{n \in ℕ_{0}}{\sum_{P}} ((i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) b)$
69	47 68	mpbird	$⊢ (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)))$

Metamath Proof Explorer

Theorem pmatcollpw1

Proof