matgsum

Description: Finite commutative sums in a matrix algebra are taken componentwise. (Contributed by AV, 26-Sep-2019)

	Ref	Expression
Hypotheses	matgsum.a	$⊢ A = N Mat R$
	matgsum.b	$⊢ B = {Base}_{A}$
	matgsum.z	$⊢ \underset{˙}{0} = 0_{A}$
	matgsum.i	$⊢ φ \to N \in Fin$
	matgsum.j	$⊢ φ \to J \in W$
	matgsum.r	$⊢ φ \to R \in Ring$
	matgsum.f	$⊢ (φ \land y \in J) \to (i \in N, j \in N ⟼ U) \in B$
	matgsum.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((y \in J ⟼ (i \in N, j \in N ⟼ U)))$
Assertion	matgsum	$⊢ φ \to \underset{y \in J}{\sum_{A}} (i \in N, j \in N ⟼ U) = (i \in N, j \in N ⟼ \underset{y \in J}{\sum_{R}} U)$

Proof

Step	Hyp	Ref	Expression
1		matgsum.a	$⊢ A = N Mat R$
2		matgsum.b	$⊢ B = {Base}_{A}$
3		matgsum.z	$⊢ \underset{˙}{0} = 0_{A}$
4		matgsum.i	$⊢ φ \to N \in Fin$
5		matgsum.j	$⊢ φ \to J \in W$
6		matgsum.r	$⊢ φ \to R \in Ring$
7		matgsum.f	$⊢ (φ \land y \in J) \to (i \in N, j \in N ⟼ U) \in B$
8		matgsum.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((y \in J ⟼ (i \in N, j \in N ⟼ U)))$
9	5	mptexd	$⊢ φ \to (y \in J ⟼ (i \in N, j \in N ⟼ U)) \in V$
10	1	ovexi	$⊢ A \in V$
11	10	a1i	$⊢ φ \to A \in V$
12		ovexd	$⊢ φ \to R freeLMod (N \times N) \in V$
13		eqid	$⊢ R freeLMod (N \times N) = R freeLMod (N \times N)$
14	1 13	matbas	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
15	4 6 14	syl2anc	$⊢ φ \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
16	15	eqcomd	$⊢ φ \to {Base}_{A} = {Base}_{(R freeLMod (N \times N))}$
17	1 13	matplusg	$⊢ (N \in Fin \land R \in Ring) \to +_{(R freeLMod (N \times N))} = +_{A}$
18	4 6 17	syl2anc	$⊢ φ \to +_{(R freeLMod (N \times N))} = +_{A}$
19	18	eqcomd	$⊢ φ \to +_{A} = +_{(R freeLMod (N \times N))}$
20	9 11 12 16 19	gsumpropd	$⊢ φ \to \underset{y \in J}{\sum_{A}} (i \in N, j \in N ⟼ U) = \underset{y \in J}{\sum_{R freeLMod (N \times N)}} (i \in N, j \in N ⟼ U)$
21		mpompts	$⊢ (i \in N, j \in N ⟼ U) = (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)$
22	21	a1i	$⊢ φ \to (i \in N, j \in N ⟼ U) = (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)$
23	22	mpteq2dv	$⊢ φ \to (y \in J ⟼ (i \in N, j \in N ⟼ U)) = (y \in J ⟼ (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U))$
24	23	oveq2d	$⊢ φ \to \underset{y \in J}{\sum_{R freeLMod (N \times N)}} (i \in N, j \in N ⟼ U) = \underset{y \in J}{\sum_{R freeLMod (N \times N)}} (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)$
25		eqid	$⊢ {Base}_{(R freeLMod (N \times N))} = {Base}_{(R freeLMod (N \times N))}$
26		eqid	$⊢ 0_{(R freeLMod (N \times N))} = 0_{(R freeLMod (N \times N))}$
27		xpfi	$⊢ (N \in Fin \land N \in Fin) \to N \times N \in Fin$
28	4 4 27	syl2anc	$⊢ φ \to N \times N \in Fin$
29	7 2	eleqtrdi	$⊢ (φ \land y \in J) \to (i \in N, j \in N ⟼ U) \in {Base}_{A}$
30	21	eqcomi	$⊢ (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U) = (i \in N, j \in N ⟼ U)$
31	30	a1i	$⊢ (φ \land y \in J) \to (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U) = (i \in N, j \in N ⟼ U)$
32	4 6	jca	$⊢ φ \to (N \in Fin \land R \in Ring)$
33	32	adantr	$⊢ (φ \land y \in J) \to (N \in Fin \land R \in Ring)$
34	33 14	syl	$⊢ (φ \land y \in J) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
35	29 31 34	3eltr4d	$⊢ (φ \land y \in J) \to (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U) \in {Base}_{(R freeLMod (N \times N))}$
36	30	mpteq2i	$⊢ (y \in J ⟼ (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)) = (y \in J ⟼ (i \in N, j \in N ⟼ U))$
37	3	eqcomi	$⊢ 0_{A} = \underset{˙}{0}$
38	8 36 37	3brtr4g	$⊢ φ \to {finSupp}_{0_{A}} ((y \in J ⟼ (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)))$
39	1 13	mat0	$⊢ (N \in Fin \land R \in Ring) \to 0_{(R freeLMod (N \times N))} = 0_{A}$
40	4 6 39	syl2anc	$⊢ φ \to 0_{(R freeLMod (N \times N))} = 0_{A}$
41	38 40	breqtrrd	$⊢ φ \to {finSupp}_{0_{(R freeLMod (N \times N))}} ((y \in J ⟼ (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)))$
42	13 25 26 28 5 6 35 41	frlmgsum	$⊢ φ \to \underset{y \in J}{\sum_{R freeLMod (N \times N)}} (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U) = (z \in (N \times N) ⟼ \underset{y \in J}{\sum_{R}} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)$
43	24 42	eqtrd	$⊢ φ \to \underset{y \in J}{\sum_{R freeLMod (N \times N)}} (i \in N, j \in N ⟼ U) = (z \in (N \times N) ⟼ \underset{y \in J}{\sum_{R}} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)$
44		fvex	$⊢ 2^{nd} (z) \in V$
45		csbov2g	$⊢ 2^{nd} (z) \in V \to ⦋ 2^{nd} (z) / j ⦌ (\underset{y \in J}{\sum_{R}}, U) = \sum_{R} ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U)$
46	44 45	ax-mp	$⊢ ⦋ 2^{nd} (z) / j ⦌ (\underset{y \in J}{\sum_{R}}, U) = \sum_{R} ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U)$
47	46	csbeq2i	$⊢ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (\underset{y \in J}{\sum_{R}}, U) = ⦋ 1^{st} (z) / i ⦌ (\sum_{R}, ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U))$
48		fvex	$⊢ 1^{st} (z) \in V$
49		csbov2g	$⊢ 1^{st} (z) \in V \to ⦋ 1^{st} (z) / i ⦌ (\sum_{R}, ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U)) = \sum_{R} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U)$
50	48 49	ax-mp	$⊢ ⦋ 1^{st} (z) / i ⦌ (\sum_{R}, ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U)) = \sum_{R} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U)$
51		csbmpt2	$⊢ 2^{nd} (z) \in V \to ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U) = (y \in J ⟼ ⦋ 2^{nd} (z) / j ⦌ U)$
52	44 51	ax-mp	$⊢ ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U) = (y \in J ⟼ ⦋ 2^{nd} (z) / j ⦌ U)$
53	52	csbeq2i	$⊢ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U) = ⦋ 1^{st} (z) / i ⦌ (y \in J ⟼ ⦋ 2^{nd} (z) / j ⦌ U)$
54		csbmpt2	$⊢ 1^{st} (z) \in V \to ⦋ 1^{st} (z) / i ⦌ (y \in J ⟼ ⦋ 2^{nd} (z) / j ⦌ U) = (y \in J ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)$
55	48 54	ax-mp	$⊢ ⦋ 1^{st} (z) / i ⦌ (y \in J ⟼ ⦋ 2^{nd} (z) / j ⦌ U) = (y \in J ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)$
56	53 55	eqtri	$⊢ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U) = (y \in J ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U)$
57	56	oveq2i	$⊢ \sum_{R} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (y \in J ⟼ U) = \underset{y \in J}{\sum_{R}} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U$
58	47 50 57	3eqtrri	$⊢ \underset{y \in J}{\sum_{R}} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U = ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (\underset{y \in J}{\sum_{R}}, U)$
59	58	mpteq2i	$⊢ (z \in (N \times N) ⟼ \underset{y \in J}{\sum_{R}} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U) = (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (\underset{y \in J}{\sum_{R}}, U))$
60		mpompts	$⊢ (i \in N, j \in N ⟼ \underset{y \in J}{\sum_{R}} U) = (z \in (N \times N) ⟼ ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ (\underset{y \in J}{\sum_{R}}, U))$
61	59 60	eqtr4i	$⊢ (z \in (N \times N) ⟼ \underset{y \in J}{\sum_{R}} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U) = (i \in N, j \in N ⟼ \underset{y \in J}{\sum_{R}} U)$
62	61	a1i	$⊢ φ \to (z \in (N \times N) ⟼ \underset{y \in J}{\sum_{R}} ⦋ 1^{st} (z) / i ⦌ ⦋ 2^{nd} (z) / j ⦌ U) = (i \in N, j \in N ⟼ \underset{y \in J}{\sum_{R}} U)$
63	20 43 62	3eqtrd	$⊢ φ \to \underset{y \in J}{\sum_{A}} (i \in N, j \in N ⟼ U) = (i \in N, j \in N ⟼ \underset{y \in J}{\sum_{R}} U)$

Metamath Proof Explorer

Theorem matgsum

Proof