decpmatmul

Description: The matrix consisting of the coefficients in the polynomial entries of the product of two polynomial matrices is a sum of products of the matrices consisting of the coefficients in the polynomial entries of the polynomial matrices for the same power. (Contributed by AV, 21-Oct-2019) (Revised by AV, 3-Dec-2019)

	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$
Assertion	decpmatmul	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to (U \cdot_{C} W) decompPMat K = {\sum_{A}}_{k = 0}^{K} ((U decompPMat k) \cdot_{A} (W decompPMat (K - 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		eqidd	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to (x \in N, y \in N ⟼ {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)))) = (x \in N, y \in N ⟼ {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))))$
6		oveq1	$⊢ x = i \to x (U decompPMat k) t = i (U decompPMat k) t$
7		oveq2	$⊢ y = j \to t (W decompPMat (K - k)) y = t (W decompPMat (K - k)) j$
8	6 7	oveqan12d	$⊢ (x = i \land y = j) \to (x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y) = (i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)$
9	8	mpteq2dv	$⊢ (x = i \land y = j) \to (t \in N ⟼ (x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)) = (t \in N ⟼ (i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j))$
10	9	oveq2d	$⊢ (x = i \land y = j) \to \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)) = \underset{t \in N}{\sum_{R}} ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j))$
11	10	mpteq2dv	$⊢ (x = i \land y = j) \to (k \in (0 \dots K) ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))) = (k \in (0 \dots K) ⟼ \underset{t \in N}{\sum_{R}} ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)))$
12	11	oveq2d	$⊢ (x = i \land y = j) \to {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))) = {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)))$
13	12	adantl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (x = i \land y = j)) \to {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))) = {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)))$
14		simprl	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to i \in N$
15		simprr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to j \in N$
16		ovexd	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j))) \in V$
17	5 13 14 15 16	ovmpod	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to i (x \in N, y \in N ⟼ {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)))) j = {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)))$
18	2 3	matrcl	$⊢ U \in B \to (N \in Fin \land P \in V)$
19	18	simpld	$⊢ U \in B \to N \in Fin$
20	19	adantr	$⊢ (U \in B \land W \in B) \to N \in Fin$
21	20	anim2i	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to (R \in Ring \land N \in Fin)$
22	21	ancomd	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to (N \in Fin \land R \in Ring)$
23	22	3adant3	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to (N \in Fin \land R \in Ring)$
24		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
25	4 24	matmulr	$⊢ (N \in Fin \land R \in Ring) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
26	23 25	syl	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
27	26	adantr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
28	27	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
29	28	eqcomd	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to \cdot_{A} = R maMul ⟨N, N, N⟩$
30	29	oveqd	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (U decompPMat k) \cdot_{A} (W decompPMat (K - k)) = (U decompPMat k) (R maMul ⟨N, N, N⟩) (W decompPMat (K - k))$
31		eqid	$⊢ {Base}_{R} = {Base}_{R}$
32		eqid	$⊢ \cdot_{R} = \cdot_{R}$
33		simp1	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to R \in Ring$
34	33	adantr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to R \in Ring$
35	34	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to R \in Ring$
36	23	simpld	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to N \in Fin$
37	36	adantr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to N \in Fin$
38	37	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to N \in Fin$
39		simpl2l	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to U \in B$
40	39	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to U \in B$
41		elfznn0	$⊢ k \in (0 \dots K) \to k \in ℕ_{0}$
42	41	adantl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to k \in ℕ_{0}$
43	35 40 42	3jca	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (R \in Ring \land U \in B \land k \in ℕ_{0})$
44		eqid	$⊢ {Base}_{A} = {Base}_{A}$
45	1 2 3 4 44	decpmatcl	$⊢ (R \in Ring \land U \in B \land k \in ℕ_{0}) \to U decompPMat k \in {Base}_{A}$
46	43 45	syl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to U decompPMat k \in {Base}_{A}$
47	4 31 44	matbas2i	$⊢ U decompPMat k \in {Base}_{A} \to U decompPMat k \in ({Base}_{R}^{(N \times N)})$
48	46 47	syl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to U decompPMat k \in ({Base}_{R}^{(N \times N)})$
49		simpl2r	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to W \in B$
50	49	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to W \in B$
51		fznn0sub	$⊢ k \in (0 \dots K) \to K - k \in ℕ_{0}$
52	51	adantl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to K - k \in ℕ_{0}$
53	35 50 52	3jca	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (R \in Ring \land W \in B \land K - k \in ℕ_{0})$
54	1 2 3 4 44	decpmatcl	$⊢ (R \in Ring \land W \in B \land K - k \in ℕ_{0}) \to W decompPMat (K - k) \in {Base}_{A}$
55	53 54	syl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to W decompPMat (K - k) \in {Base}_{A}$
56	4 31 44	matbas2i	$⊢ W decompPMat (K - k) \in {Base}_{A} \to W decompPMat (K - k) \in ({Base}_{R}^{(N \times N)})$
57	55 56	syl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to W decompPMat (K - k) \in ({Base}_{R}^{(N \times N)})$
58	24 31 32 35 38 38 38 48 57	mamuval	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (U decompPMat k) (R maMul ⟨N, N, N⟩) (W decompPMat (K - k)) = (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)))$
59	30 58	eqtrd	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (U decompPMat k) \cdot_{A} (W decompPMat (K - k)) = (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)))$
60	59	mpteq2dva	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to (k \in (0 \dots K) ⟼ (U decompPMat k) \cdot_{A} (W decompPMat (K - k))) = (k \in (0 \dots K) ⟼ (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))))$
61	60	oveq2d	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to {\sum_{A}}_{k = 0}^{K} ((U decompPMat k) \cdot_{A} (W decompPMat (K - k))) = {\sum_{A}}_{k = 0}^{K} (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)))$
62		eqid	$⊢ 0_{A} = 0_{A}$
63		ovexd	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to (0 \dots K) \in V$
64		ringcmn	$⊢ R \in Ring \to R \in CMnd$
65	33 64	syl	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to R \in CMnd$
66	65	adantr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to R \in CMnd$
67	66	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to R \in CMnd$
68	67	3ad2ant1	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \to R \in CMnd$
69	38	3ad2ant1	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \to N \in Fin$
70	35	3ad2ant1	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \to R \in Ring$
71	70	adantr	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to R \in Ring$
72		simpl2	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to x \in N$
73		simpr	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to t \in N$
74	43	3ad2ant1	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \to (R \in Ring \land U \in B \land k \in ℕ_{0})$
75	74	adantr	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to (R \in Ring \land U \in B \land k \in ℕ_{0})$
76	75 45	syl	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to U decompPMat k \in {Base}_{A}$
77	4 31 44 72 73 76	matecld	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to x (U decompPMat k) t \in {Base}_{R}$
78		simpl3	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to y \in N$
79	55	3ad2ant1	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \to W decompPMat (K - k) \in {Base}_{A}$
80	79	adantr	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to W decompPMat (K - k) \in {Base}_{A}$
81	4 31 44 73 78 80	matecld	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to t (W decompPMat (K - k)) y \in {Base}_{R}$
82	31 32	ringcl	$⊢ (R \in Ring \land x (U decompPMat k) t \in {Base}_{R} \land t (W decompPMat (K - k)) y \in {Base}_{R}) \to (x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y) \in {Base}_{R}$
83	71 77 81 82	syl3anc	$⊢ (((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \land t \in N) \to (x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y) \in {Base}_{R}$
84	83	ralrimiva	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \to \forall t \in N (x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y) \in {Base}_{R}$
85	31 68 69 84	gsummptcl	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land x \in N \land y \in N) \to \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)) \in {Base}_{R}$
86	4 31 44 38 35 85	matbas2d	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))) \in {Base}_{A}$
87		eqid	$⊢ (k \in (0 \dots K) ⟼ (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)))) = (k \in (0 \dots K) ⟼ (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))))$
88		fzfid	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to (0 \dots K) \in Fin$
89		simpl	$⊢ (N \in Fin \land P \in V) \to N \in Fin$
90	89 89	jca	$⊢ (N \in Fin \land P \in V) \to (N \in Fin \land N \in Fin)$
91	18 90	syl	$⊢ U \in B \to (N \in Fin \land N \in Fin)$
92	91	adantr	$⊢ (U \in B \land W \in B) \to (N \in Fin \land N \in Fin)$
93	92	3ad2ant2	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to (N \in Fin \land N \in Fin)$
94	93	adantr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to (N \in Fin \land N \in Fin)$
95	94	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (N \in Fin \land N \in Fin)$
96		mpoexga	$⊢ (N \in Fin \land N \in Fin) \to (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))) \in V$
97	95 96	syl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))) \in V$
98		fvexd	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to 0_{A} \in V$
99	87 88 97 98	fsuppmptdm	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to {finSupp}_{0_{A}} ((k \in (0 \dots K) ⟼ (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)))))$
100	4 44 62 37 63 34 86 99	matgsum	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to {\sum_{A}}_{k = 0}^{K} (x \in N, y \in N ⟼ \underset{t \in N}{\sum_{R}} ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))) = (x \in N, y \in N ⟼ {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))))$
101	61 100	eqtrd	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to {\sum_{A}}_{k = 0}^{K} ((U decompPMat k) \cdot_{A} (W decompPMat (K - k))) = (x \in N, y \in N ⟼ {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y))))$
102	101	oveqd	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to i ({\sum_{A}}_{k = 0}^{K}, ((U decompPMat k) \cdot_{A} (W decompPMat (K - k)))) j = i (x \in N, y \in N ⟼ {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((x (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) y)))) j$
103		simpl2	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to (U \in B \land W \in B)$
104		simpl3	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to K \in ℕ_{0}$
105	1 2 3	decpmatmullem	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (i \in N \land j \in N \land K \in ℕ_{0})) \to i ((U \cdot_{C} W) decompPMat K) j = \underset{t \in N}{\sum_{R}} ({\sum_{R}}_{k = 0}^{K}, ({coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k)))$
106	37 34 103 14 15 104 105	syl213anc	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to i ((U \cdot_{C} W) decompPMat K) j = \underset{t \in N}{\sum_{R}} ({\sum_{R}}_{k = 0}^{K}, ({coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k)))$
107		simpll1	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to R \in Ring$
108		simplrl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to i \in N$
109		simprl	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to t \in N$
110	3	eleq2i	$⊢ U \in B \leftrightarrow U \in {Base}_{C}$
111	110	biimpi	$⊢ U \in B \to U \in {Base}_{C}$
112	111	adantr	$⊢ (U \in B \land W \in B) \to U \in {Base}_{C}$
113	112	3ad2ant2	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to U \in {Base}_{C}$
114	113	adantr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to U \in {Base}_{C}$
115	114	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to U \in {Base}_{C}$
116		eqid	$⊢ {Base}_{P} = {Base}_{P}$
117	2 116	matecl	$⊢ (i \in N \land t \in N \land U \in {Base}_{C}) \to i U t \in {Base}_{P}$
118	108 109 115 117	syl3anc	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to i U t \in {Base}_{P}$
119	41	ad2antll	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to k \in ℕ_{0}$
120		eqid	$⊢ {coe}_{1} (i U t) = {coe}_{1} (i U t)$
121	120 116 1 31	coe1fvalcl	$⊢ (i U t \in {Base}_{P} \land k \in ℕ_{0}) \to {coe}_{1} (i U t) (k) \in {Base}_{R}$
122	118 119 121	syl2anc	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to {coe}_{1} (i U t) (k) \in {Base}_{R}$
123		simplrr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to j \in N$
124	49	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to W \in B$
125	2 116 3 109 123 124	matecld	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to t W j \in {Base}_{P}$
126	51	ad2antll	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to K - k \in ℕ_{0}$
127		eqid	$⊢ {coe}_{1} (t W j) = {coe}_{1} (t W j)$
128	127 116 1 31	coe1fvalcl	$⊢ (t W j \in {Base}_{P} \land K - k \in ℕ_{0}) \to {coe}_{1} (t W j) (K - k) \in {Base}_{R}$
129	125 126 128	syl2anc	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to {coe}_{1} (t W j) (K - k) \in {Base}_{R}$
130	31 32	ringcl	$⊢ (R \in Ring \land {coe}_{1} (i U t) (k) \in {Base}_{R} \land {coe}_{1} (t W j) (K - k) \in {Base}_{R}) \to {coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k) \in {Base}_{R}$
131	107 122 129 130	syl3anc	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land (t \in N \land k \in (0 \dots K))) \to {coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k) \in {Base}_{R}$
132	31 66 37 88 131	gsumcom3fi	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to \underset{t \in N}{\sum_{R}} ({\sum_{R}}_{k = 0}^{K}, ({coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k))) = {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ({coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k)))$
133	14	adantr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to i \in N$
134	133	anim1i	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land t \in N) \to (i \in N \land t \in N)$
135	1 2 3	decpmate	$⊢ ((R \in Ring \land U \in B \land k \in ℕ_{0}) \land (i \in N \land t \in N)) \to i (U decompPMat k) t = {coe}_{1} (i U t) (k)$
136	43 134 135	syl2an2r	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land t \in N) \to i (U decompPMat k) t = {coe}_{1} (i U t) (k)$
137		simplrr	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to j \in N$
138	137	anim1ci	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land t \in N) \to (t \in N \land j \in N)$
139	1 2 3	decpmate	$⊢ ((R \in Ring \land W \in B \land K - k \in ℕ_{0}) \land (t \in N \land j \in N)) \to t (W decompPMat (K - k)) j = {coe}_{1} (t W j) (K - k)$
140	53 138 139	syl2an2r	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land t \in N) \to t (W decompPMat (K - k)) j = {coe}_{1} (t W j) (K - k)$
141	136 140	oveq12d	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land t \in N) \to (i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j) = {coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k)$
142	141	eqcomd	$⊢ ((((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \land t \in N) \to {coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k) = (i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)$
143	142	mpteq2dva	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to (t \in N ⟼ {coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k)) = (t \in N ⟼ (i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j))$
144	143	oveq2d	$⊢ (((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \land k \in (0 \dots K)) \to \underset{t \in N}{\sum_{R}} ({coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k)) = \underset{t \in N}{\sum_{R}} ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j))$
145	144	mpteq2dva	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to (k \in (0 \dots K) ⟼ \underset{t \in N}{\sum_{R}} ({coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k))) = (k \in (0 \dots K) ⟼ \underset{t \in N}{\sum_{R}} ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)))$
146	145	oveq2d	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ({coe}_{1} (i U t) (k) \cdot_{R} {coe}_{1} (t W j) (K - k))) = {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)))$
147	106 132 146	3eqtrd	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to i ((U \cdot_{C} W) decompPMat K) j = {\sum_{R}}_{k = 0}^{K} (\underset{t \in N}{\sum_{R}}, ((i (U decompPMat k) t) \cdot_{R} (t (W decompPMat (K - k)) j)))$
148	17 102 147	3eqtr4rd	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land (i \in N \land j \in N)) \to i ((U \cdot_{C} W) decompPMat K) j = i ({\sum_{A}}_{k = 0}^{K}, ((U decompPMat k) \cdot_{A} (W decompPMat (K - k)))) j$
149	148	ralrimivva	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to \forall i \in N \forall j \in N i ((U \cdot_{C} W) decompPMat K) j = i ({\sum_{A}}_{k = 0}^{K}, ((U decompPMat k) \cdot_{A} (W decompPMat (K - k)))) j$
150	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
151	22 150	syl	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to C \in Ring$
152		simprl	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to U \in B$
153		simprr	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to W \in B$
154		eqid	$⊢ \cdot_{C} = \cdot_{C}$
155	3 154	ringcl	$⊢ (C \in Ring \land U \in B \land W \in B) \to U \cdot_{C} W \in B$
156	151 152 153 155	syl3anc	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to U \cdot_{C} W \in B$
157	156	3adant3	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to U \cdot_{C} W \in B$
158	1 2 3 4 44	decpmatcl	$⊢ (R \in Ring \land U \cdot_{C} W \in B \land K \in ℕ_{0}) \to (U \cdot_{C} W) decompPMat K \in {Base}_{A}$
159	157 158	syld3an2	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to (U \cdot_{C} W) decompPMat K \in {Base}_{A}$
160	4	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
161	23 160	syl	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to A \in Ring$
162		ringcmn	$⊢ A \in Ring \to A \in CMnd$
163	161 162	syl	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to A \in CMnd$
164		fzfid	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to (0 \dots K) \in Fin$
165	161	adantr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to A \in Ring$
166	33	adantr	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to R \in Ring$
167		simpl2l	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to U \in B$
168	41	adantl	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to k \in ℕ_{0}$
169	166 167 168	3jca	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to (R \in Ring \land U \in B \land k \in ℕ_{0})$
170	169 45	syl	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to U decompPMat k \in {Base}_{A}$
171		simpl2r	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to W \in B$
172	51	adantl	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to K - k \in ℕ_{0}$
173	166 171 172	3jca	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to (R \in Ring \land W \in B \land K - k \in ℕ_{0})$
174	173 54	syl	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to W decompPMat (K - k) \in {Base}_{A}$
175		eqid	$⊢ \cdot_{A} = \cdot_{A}$
176	44 175	ringcl	$⊢ (A \in Ring \land U decompPMat k \in {Base}_{A} \land W decompPMat (K - k) \in {Base}_{A}) \to (U decompPMat k) \cdot_{A} (W decompPMat (K - k)) \in {Base}_{A}$
177	165 170 174 176	syl3anc	$⊢ ((R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \land k \in (0 \dots K)) \to (U decompPMat k) \cdot_{A} (W decompPMat (K - k)) \in {Base}_{A}$
178	177	ralrimiva	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to \forall k \in (0 \dots K) (U decompPMat k) \cdot_{A} (W decompPMat (K - k)) \in {Base}_{A}$
179	44 163 164 178	gsummptcl	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to {\sum_{A}}_{k = 0}^{K} ((U decompPMat k) \cdot_{A} (W decompPMat (K - k))) \in {Base}_{A}$
180	4 44	eqmat	$⊢ ((U \cdot_{C} W) decompPMat K \in {Base}_{A} \land {\sum_{A}}_{k = 0}^{K} ((U decompPMat k) \cdot_{A} (W decompPMat (K - k))) \in {Base}_{A}) \to ((U \cdot_{C} W) decompPMat K = {\sum_{A}}_{k = 0}^{K} ((U decompPMat k) \cdot_{A} (W decompPMat (K - k))) \leftrightarrow \forall i \in N \forall j \in N i ((U \cdot_{C} W) decompPMat K) j = i ({\sum_{A}}_{k = 0}^{K}, ((U decompPMat k) \cdot_{A} (W decompPMat (K - k)))) j)$
181	159 179 180	syl2anc	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to ((U \cdot_{C} W) decompPMat K = {\sum_{A}}_{k = 0}^{K} ((U decompPMat k) \cdot_{A} (W decompPMat (K - k))) \leftrightarrow \forall i \in N \forall j \in N i ((U \cdot_{C} W) decompPMat K) j = i ({\sum_{A}}_{k = 0}^{K}, ((U decompPMat k) \cdot_{A} (W decompPMat (K - k)))) j)$
182	149 181	mpbird	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to (U \cdot_{C} W) decompPMat K = {\sum_{A}}_{k = 0}^{K} ((U decompPMat k) \cdot_{A} (W decompPMat (K - k)))$

Metamath Proof Explorer

Theorem decpmatmul

Proof