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	birani	$⊢ (U \in B \land W \in B) \to U \in {Base}_{C}$
112	111	3ad2ant2	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to U \in {Base}_{C}$
113	112	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}$
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)) \land (t \in N \land k \in (0 \dots K))) \to U \in {Base}_{C}$
115		eqid	$⊢ {Base}_{P} = {Base}_{P}$
116	2 115	matecl	$⊢ (i \in N \land t \in N \land U \in {Base}_{C}) \to i U t \in {Base}_{P}$
117	108 109 114 116	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}$
118	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}$
119		eqid	$⊢ {coe}_{1} (i U t) = {coe}_{1} (i U t)$
120	119 115 1 31	coe1fvalcl	$⊢ (i U t \in {Base}_{P} \land k \in ℕ_{0}) \to {coe}_{1} (i U t) (k) \in {Base}_{R}$
121	117 118 120	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}$
122		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$
123	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$
124	2 115 3 109 122 123	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}$
125	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}$
126		eqid	$⊢ {coe}_{1} (t W j) = {coe}_{1} (t W j)$
127	126 115 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}$
128	124 125 127	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}$
129	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}$
130	107 121 128 129	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}$
131	31 66 37 88 130	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)))$
132	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$
133	132	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)$
134	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)$
135	43 133 134	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)$
136		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$
137	136	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)$
138	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)$
139	53 137 138	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)$
140	135 139	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)$
141	140	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)$
142	141	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))$
143	142	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))$
144	143	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)))$
145	144	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)))$
146	106 131 145	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)))$
147	17 102 146	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$
148	147	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$
149	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
150	22 149	syl	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to C \in Ring$
151		simprl	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to U \in B$
152		simprr	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to W \in B$
153		eqid	$⊢ \cdot_{C} = \cdot_{C}$
154	3 153	ringcl	$⊢ (C \in Ring \land U \in B \land W \in B) \to U \cdot_{C} W \in B$
155	150 151 152 154	syl3anc	$⊢ (R \in Ring \land (U \in B \land W \in B)) \to U \cdot_{C} W \in B$
156	155	3adant3	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to U \cdot_{C} W \in B$
157	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}$
158	156 157	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}$
159	4	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
160	23 159	syl	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to A \in Ring$
161		ringcmn	$⊢ A \in Ring \to A \in CMnd$
162	160 161	syl	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to A \in CMnd$
163		fzfid	$⊢ (R \in Ring \land (U \in B \land W \in B) \land K \in ℕ_{0}) \to (0 \dots K) \in Fin$
164	160	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$
165	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$
166		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$
167	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}$
168	165 166 167	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})$
169	168 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}$
170		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$
171	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}$
172	165 170 171	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})$
173	172 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}$
174		eqid	$⊢ \cdot_{A} = \cdot_{A}$
175	44 174	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}$
176	164 169 173 175	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}$
177	176	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}$
178	44 162 163 177	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}$
179	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)$
180	158 178 179	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)$
181	148 180	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