decpmatmulsumfsupp

	Ref	Expression
Hypotheses	decpmatmul.p	$⊢ P = {Poly}_{1} (R)$
	decpmatmul.c	$⊢ C = N Mat P$
	decpmatmul.b	$⊢ B = {Base}_{C}$
	decpmatmul.a	$⊢ A = N Mat R$
	decpmatmulsumfsupp.m	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
	decpmatmulsumfsupp.0	$⊢ \underset{˙}{0} = 0_{A}$
Assertion	decpmatmulsumfsupp	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to {finSupp}_{\underset{˙}{0}} ((l \in ℕ_{0} ⟼ {\sum_{A}}_{k = 0}^{l} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (l - k)))))$

Proof

Step	Hyp	Ref	Expression
1		decpmatmul.p	$⊢ P = {Poly}_{1} (R)$
2		decpmatmul.c	$⊢ C = N Mat P$
3		decpmatmul.b	$⊢ B = {Base}_{C}$
4		decpmatmul.a	$⊢ A = N Mat R$
5		decpmatmulsumfsupp.m	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
6		decpmatmulsumfsupp.0	$⊢ \underset{˙}{0} = 0_{A}$
7	6	fvexi	$⊢ \underset{˙}{0} \in V$
8	7	a1i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \underset{˙}{0} \in V$
9		ovexd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land l \in ℕ_{0}) \to {\sum_{A}}_{k = 0}^{l} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (l - k))) \in V$
10		oveq2	$⊢ l = n \to (0 \dots l) = (0 \dots n)$
11		oveq1	$⊢ l = n \to l - k = n - k$
12	11	oveq2d	$⊢ l = n \to y decompPMat (l - k) = y decompPMat (n - k)$
13	12	oveq2d	$⊢ l = n \to (x decompPMat k) \underset{˙}{\cdot} (y decompPMat (l - k)) = (x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))$
14	10 13	mpteq12dv	$⊢ l = n \to (k \in (0 \dots l) ⟼ (x decompPMat k) \underset{˙}{\cdot} (y decompPMat (l - k))) = (k \in (0 \dots n) ⟼ (x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k)))$
15	14	oveq2d	$⊢ l = n \to {\sum_{A}}_{k = 0}^{l} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (l - k))) = {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k)))$
16		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to N \in Fin$
17		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to R \in Ring$
18	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
19	18	anim1i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (C \in Ring \land (x \in B \land y \in B))$
20		3anass	$⊢ (C \in Ring \land x \in B \land y \in B) \leftrightarrow (C \in Ring \land (x \in B \land y \in B))$
21	19 20	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (C \in Ring \land x \in B \land y \in B)$
22		eqid	$⊢ \cdot_{C} = \cdot_{C}$
23	3 22	ringcl	$⊢ (C \in Ring \land x \in B \land y \in B) \to x \cdot_{C} y \in B$
24	21 23	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to x \cdot_{C} y \in B$
25		eqid	$⊢ 0_{R} = 0_{R}$
26	1 2 3 25	pmatcoe1fsupp	$⊢ (N \in Fin \land R \in Ring \land x \cdot_{C} y \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R})$
27	16 17 24 26	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R})$
28		fvoveq1	$⊢ a = i \to {coe}_{1} (a (x \cdot_{C} y) b) = {coe}_{1} (i (x \cdot_{C} y) b)$
29	28	fveq1d	$⊢ a = i \to {coe}_{1} (a (x \cdot_{C} y) b) (n) = {coe}_{1} (i (x \cdot_{C} y) b) (n)$
30	29	eqeq1d	$⊢ a = i \to ({coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R} \leftrightarrow {coe}_{1} (i (x \cdot_{C} y) b) (n) = 0_{R})$
31		oveq2	$⊢ b = j \to i (x \cdot_{C} y) b = i (x \cdot_{C} y) j$
32	31	fveq2d	$⊢ b = j \to {coe}_{1} (i (x \cdot_{C} y) b) = {coe}_{1} (i (x \cdot_{C} y) j)$
33	32	fveq1d	$⊢ b = j \to {coe}_{1} (i (x \cdot_{C} y) b) (n) = {coe}_{1} (i (x \cdot_{C} y) j) (n)$
34	33	eqeq1d	$⊢ b = j \to ({coe}_{1} (i (x \cdot_{C} y) b) (n) = 0_{R} \leftrightarrow {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R})$
35	30 34	rspc2va	$⊢ ((i \in N \land j \in N) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R}$
36	35	expcom	$⊢ \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R} \to ((i \in N \land j \in N) \to {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R})$
37	36	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to ((i \in N \land j \in N) \to {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R})$
38	37	3impib	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \land i \in N \land j \in N) \to {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R}$
39	38	mpoeq3dva	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = (i \in N, j \in N ⟼ 0_{R})$
40	4 25	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (i \in N, j \in N ⟼ 0_{R})$
41	6 40	syl5eq	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} = (i \in N, j \in N ⟼ 0_{R})$
42	41	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to \underset{˙}{0} = (i \in N, j \in N ⟼ 0_{R})$
43	39 42	eqtr4d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0}$
44	43	ex	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (\forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R} \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0})$
45	44	imim2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ((s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0}))$
46	45	ralimdva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\forall n \in ℕ_{0} (s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0}))$
47	46	reximdv	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0}))$
48	27 47	mpd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0})$
49	5	oveqi	$⊢ (x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k)) = (x decompPMat k) \cdot_{A} (y decompPMat (n - k))$
50	49	a1i	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k)) = (x decompPMat k) \cdot_{A} (y decompPMat (n - k))$
51	50	mpteq2dv	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (k \in (0 \dots n) ⟼ (x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))) = (k \in (0 \dots n) ⟼ (x decompPMat k) \cdot_{A} (y decompPMat (n - k)))$
52	51	oveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))) = {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))$
53	1 2 3 4	decpmatmul	$⊢ (R \in Ring \land (x \in B \land y \in B) \land n \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat n = {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))$
54	53	ad4ant234	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat n = {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))$
55	2 3	decpmatval	$⊢ (x \cdot_{C} y \in B \land n \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat n = (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n))$
56	24 55	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat n = (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n))$
57	52 54 56	3eqtr2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))) = (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n))$
58	57	eqeq1d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ({\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))) = \underset{˙}{0} \leftrightarrow (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0})$
59	58	imbi2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ((s < n \to {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))) = \underset{˙}{0}) \leftrightarrow (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0}))$
60	59	ralbidva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\forall n \in ℕ_{0} (s < n \to {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))) = \underset{˙}{0}) \leftrightarrow \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0}))$
61	60	rexbidv	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))) = \underset{˙}{0}) \leftrightarrow \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = \underset{˙}{0}))$
62	48 61	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (n - k))) = \underset{˙}{0})$
63	8 9 15 62	mptnn0fsuppd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to {finSupp}_{\underset{˙}{0}} ((l \in ℕ_{0} ⟼ {\sum_{A}}_{k = 0}^{l} ((x decompPMat k) \underset{˙}{\cdot} (y decompPMat (l - k)))))$

Metamath Proof Explorer

Theorem decpmatmulsumfsupp

Proof