fsumcom2

Description: Interchange order of summation. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Mario Carneiro, 28-Apr-2014) (Revised by Mario Carneiro, 8-Apr-2016) (Proof shortened by JJ, 2-Aug-2021)

	Ref	Expression
Hypotheses	fsumcom2.1	$⊢ φ \to A \in Fin$
	fsumcom2.2	$⊢ φ \to C \in Fin$
	fsumcom2.3	$⊢ (φ \land j \in A) \to B \in Fin$
	fsumcom2.4	$⊢ φ \to ((j \in A \land k \in B) \leftrightarrow (k \in C \land j \in D))$
	fsumcom2.5	$⊢ (φ \land (j \in A \land k \in B)) \to E \in ℂ$
Assertion	fsumcom2	$⊢ φ \to \sum_{j \in A} \sum_{k \in B} E = \sum_{k \in C} \sum_{j \in D} E$

Proof

Step	Hyp	Ref	Expression
1		fsumcom2.1	$⊢ φ \to A \in Fin$
2		fsumcom2.2	$⊢ φ \to C \in Fin$
3		fsumcom2.3	$⊢ (φ \land j \in A) \to B \in Fin$
4		fsumcom2.4	$⊢ φ \to ((j \in A \land k \in B) \leftrightarrow (k \in C \land j \in D))$
5		fsumcom2.5	$⊢ (φ \land (j \in A \land k \in B)) \to E \in ℂ$
6		relxp	$⊢ Rel (\{j\} \times B)$
7	6	rgenw	$⊢ \forall j \in A Rel (\{j\} \times B)$
8		reliun	$⊢ Rel ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \forall j \in A Rel (\{j\} \times B)$
9	7 8	mpbir	$⊢ Rel ⋃_{j \in A} (\{j\} \times B)$
10		relcnv	$⊢ Rel {⋃_{k \in C} (\{k\} \times D)}^{-1}$
11		ancom	$⊢ (x = j \land y = k) \leftrightarrow (y = k \land x = j)$
12		vex	$⊢ x \in V$
13		vex	$⊢ y \in V$
14	12 13	opth	$⊢ ⟨x, y⟩ = ⟨j, k⟩ \leftrightarrow (x = j \land y = k)$
15	13 12	opth	$⊢ ⟨y, x⟩ = ⟨k, j⟩ \leftrightarrow (y = k \land x = j)$
16	11 14 15	3bitr4i	$⊢ ⟨x, y⟩ = ⟨j, k⟩ \leftrightarrow ⟨y, x⟩ = ⟨k, j⟩$
17	16	a1i	$⊢ φ \to (⟨x, y⟩ = ⟨j, k⟩ \leftrightarrow ⟨y, x⟩ = ⟨k, j⟩)$
18	17 4	anbi12d	$⊢ φ \to ((⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in B)) \leftrightarrow (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D)))$
19	18	2exbidv	$⊢ φ \to (\exists j \exists k (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in B)) \leftrightarrow \exists j \exists k (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D)))$
20		eliunxp	$⊢ ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists j \exists k (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in B))$
21	12 13	opelcnv	$⊢ ⟨x, y⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1} \leftrightarrow ⟨y, x⟩ \in ⋃_{k \in C} (\{k\} \times D)$
22		eliunxp	$⊢ ⟨y, x⟩ \in ⋃_{k \in C} (\{k\} \times D) \leftrightarrow \exists k \exists j (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D))$
23		excom	$⊢ \exists k \exists j (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D)) \leftrightarrow \exists j \exists k (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D))$
24	21 22 23	3bitri	$⊢ ⟨x, y⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1} \leftrightarrow \exists j \exists k (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D))$
25	19 20 24	3bitr4g	$⊢ φ \to (⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow ⟨x, y⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1})$
26	9 10 25	eqrelrdv	$⊢ φ \to ⋃_{j \in A} (\{j\} \times B) = {⋃_{k \in C} (\{k\} \times D)}^{-1}$
27		nfcv	$⊢ \underline{Ⅎ} m (\{j\} \times B)$
28		nfcv	$⊢ \underline{Ⅎ} j \{m\}$
29		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ B$
30	28 29	nfxp	$⊢ \underline{Ⅎ} j (\{m\} \times ⦋ m / j ⦌ B)$
31		sneq	$⊢ j = m \to \{j\} = \{m\}$
32		csbeq1a	$⊢ j = m \to B = ⦋ m / j ⦌ B$
33	31 32	xpeq12d	$⊢ j = m \to \{j\} \times B = \{m\} \times ⦋ m / j ⦌ B$
34	27 30 33	cbviun	$⊢ ⋃_{j \in A} (\{j\} \times B) = ⋃_{m \in A} (\{m\} \times ⦋ m / j ⦌ B)$
35		nfcv	$⊢ \underline{Ⅎ} n (\{k\} \times D)$
36		nfcv	$⊢ \underline{Ⅎ} k \{n\}$
37		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ D$
38	36 37	nfxp	$⊢ \underline{Ⅎ} k (\{n\} \times ⦋ n / k ⦌ D)$
39		sneq	$⊢ k = n \to \{k\} = \{n\}$
40		csbeq1a	$⊢ k = n \to D = ⦋ n / k ⦌ D$
41	39 40	xpeq12d	$⊢ k = n \to \{k\} \times D = \{n\} \times ⦋ n / k ⦌ D$
42	35 38 41	cbviun	$⊢ ⋃_{k \in C} (\{k\} \times D) = ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)$
43	42	cnveqi	$⊢ {⋃_{k \in C} (\{k\} \times D)}^{-1} = {⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)}^{-1}$
44	26 34 43	3eqtr3g	$⊢ φ \to ⋃_{m \in A} (\{m\} \times ⦋ m / j ⦌ B) = {⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)}^{-1}$
45	44	sumeq1d	$⊢ φ \to \sum_{z \in ⋃_{m \in A} (\{m\} \times ⦋ m / j ⦌ B)} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = \sum_{z \in {⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)}^{-1}} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E$
46		vex	$⊢ n \in V$
47		vex	$⊢ m \in V$
48	46 47	op1std	$⊢ w = ⟨n, m⟩ \to 1^{st} (w) = n$
49	48	csbeq1d	$⊢ w = ⟨n, m⟩ \to ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E = ⦋ n / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
50	46 47	op2ndd	$⊢ w = ⟨n, m⟩ \to 2^{nd} (w) = m$
51	50	csbeq1d	$⊢ w = ⟨n, m⟩ \to ⦋ 2^{nd} (w) / j ⦌ E = ⦋ m / j ⦌ E$
52	51	csbeq2dv	$⊢ w = ⟨n, m⟩ \to ⦋ n / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
53	49 52	eqtrd	$⊢ w = ⟨n, m⟩ \to ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
54	47 46	op2ndd	$⊢ z = ⟨m, n⟩ \to 2^{nd} (z) = n$
55	54	csbeq1d	$⊢ z = ⟨m, n⟩ \to ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = ⦋ n / k ⦌ ⦋ 1^{st} (z) / j ⦌ E$
56	47 46	op1std	$⊢ z = ⟨m, n⟩ \to 1^{st} (z) = m$
57	56	csbeq1d	$⊢ z = ⟨m, n⟩ \to ⦋ 1^{st} (z) / j ⦌ E = ⦋ m / j ⦌ E$
58	57	csbeq2dv	$⊢ z = ⟨m, n⟩ \to ⦋ n / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
59	55 58	eqtrd	$⊢ z = ⟨m, n⟩ \to ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
60		snfi	$⊢ \{n\} \in Fin$
61	1	adantr	$⊢ (φ \land n \in C) \to A \in Fin$
62	47 46	opelcnv	$⊢ ⟨m, n⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1} \leftrightarrow ⟨n, m⟩ \in ⋃_{k \in C} (\{k\} \times D)$
63	37 40	opeliunxp2f	$⊢ ⟨n, m⟩ \in ⋃_{k \in C} (\{k\} \times D) \leftrightarrow (n \in C \land m \in ⦋ n / k ⦌ D)$
64	62 63	sylbbr	$⊢ (n \in C \land m \in ⦋ n / k ⦌ D) \to ⟨m, n⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1}$
65	64	adantl	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to ⟨m, n⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1}$
66	26	adantr	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to ⋃_{j \in A} (\{j\} \times B) = {⋃_{k \in C} (\{k\} \times D)}^{-1}$
67	65 66	eleqtrrd	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to ⟨m, n⟩ \in ⋃_{j \in A} (\{j\} \times B)$
68		eliun	$⊢ ⟨m, n⟩ \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists j \in A ⟨m, n⟩ \in (\{j\} \times B)$
69	67 68	sylib	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to \exists j \in A ⟨m, n⟩ \in (\{j\} \times B)$
70		opelxp	$⊢ ⟨m, n⟩ \in (\{j\} \times B) \leftrightarrow (m \in \{j\} \land n \in B)$
71	70	bilani	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to (m \in \{j\} \land n \in B)$
72	71	simpld	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to m \in \{j\}$
73		elsni	$⊢ m \in \{j\} \to m = j$
74	72 73	syl	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to m = j$
75		simpl	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to j \in A$
76	74 75	eqeltrd	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to m \in A$
77	76	rexlimiva	$⊢ \exists j \in A ⟨m, n⟩ \in (\{j\} \times B) \to m \in A$
78	69 77	syl	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to m \in A$
79	78	expr	$⊢ (φ \land n \in C) \to (m \in ⦋ n / k ⦌ D \to m \in A)$
80	79	ssrdv	$⊢ (φ \land n \in C) \to ⦋ n / k ⦌ D \subseteq A$
81	61 80	ssfid	$⊢ (φ \land n \in C) \to ⦋ n / k ⦌ D \in Fin$
82		xpfi	$⊢ (\{n\} \in Fin \land ⦋ n / k ⦌ D \in Fin) \to \{n\} \times ⦋ n / k ⦌ D \in Fin$
83	60 81 82	sylancr	$⊢ (φ \land n \in C) \to \{n\} \times ⦋ n / k ⦌ D \in Fin$
84	83	ralrimiva	$⊢ φ \to \forall n \in C \{n\} \times ⦋ n / k ⦌ D \in Fin$
85		iunfi	$⊢ (C \in Fin \land \forall n \in C \{n\} \times ⦋ n / k ⦌ D \in Fin) \to ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D) \in Fin$
86	2 84 85	syl2anc	$⊢ φ \to ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D) \in Fin$
87		reliun	$⊢ Rel ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D) \leftrightarrow \forall n \in C Rel (\{n\} \times ⦋ n / k ⦌ D)$
88		relxp	$⊢ Rel (\{n\} \times ⦋ n / k ⦌ D)$
89	88	a1i	$⊢ n \in C \to Rel (\{n\} \times ⦋ n / k ⦌ D)$
90	87 89	mprgbir	$⊢ Rel ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)$
91	90	a1i	$⊢ φ \to Rel ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)$
92		csbeq1	$⊢ m = 2^{nd} (w) \to ⦋ m / j ⦌ E = ⦋ 2^{nd} (w) / j ⦌ E$
93	92	csbeq2dv	$⊢ m = 2^{nd} (w) \to ⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E = ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
94	93	eleq1d	$⊢ m = 2^{nd} (w) \to (⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E \in ℂ \leftrightarrow ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E \in ℂ)$
95		csbeq1	$⊢ n = 1^{st} (w) \to ⦋ n / k ⦌ D = ⦋ 1^{st} (w) / k ⦌ D$
96		csbeq1	$⊢ n = 1^{st} (w) \to ⦋ n / k ⦌ ⦋ m / j ⦌ E = ⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E$
97	96	eleq1d	$⊢ n = 1^{st} (w) \to (⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ \leftrightarrow ⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
98	95 97	raleqbidv	$⊢ n = 1^{st} (w) \to (\forall m \in ⦋ n / k ⦌ D ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ \leftrightarrow \forall m \in ⦋ 1^{st} (w) / k ⦌ D ⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
99		simpl	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to φ$
100	29	nfcri	$⊢ Ⅎ j n \in ⦋ m / j ⦌ B$
101	73	equcomd	$⊢ m \in \{j\} \to j = m$
102	101 32	syl	$⊢ m \in \{j\} \to B = ⦋ m / j ⦌ B$
103	102	eleq2d	$⊢ m \in \{j\} \to (n \in B \leftrightarrow n \in ⦋ m / j ⦌ B)$
104	103	biimpa	$⊢ (m \in \{j\} \land n \in B) \to n \in ⦋ m / j ⦌ B$
105	70 104	sylbi	$⊢ ⟨m, n⟩ \in (\{j\} \times B) \to n \in ⦋ m / j ⦌ B$
106	105	a1i	$⊢ j \in A \to (⟨m, n⟩ \in (\{j\} \times B) \to n \in ⦋ m / j ⦌ B)$
107	100 106	rexlimi	$⊢ \exists j \in A ⟨m, n⟩ \in (\{j\} \times B) \to n \in ⦋ m / j ⦌ B$
108	69 107	syl	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to n \in ⦋ m / j ⦌ B$
109	5	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in B E \in ℂ$
110		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ E$
111	110	nfel1	$⊢ Ⅎ j ⦋ m / j ⦌ E \in ℂ$
112	29 111	nfralw	$⊢ Ⅎ j \forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ$
113		csbeq1a	$⊢ j = m \to E = ⦋ m / j ⦌ E$
114	113	eleq1d	$⊢ j = m \to (E \in ℂ \leftrightarrow ⦋ m / j ⦌ E \in ℂ)$
115	32 114	raleqbidv	$⊢ j = m \to (\forall k \in B E \in ℂ \leftrightarrow \forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ)$
116	112 115	rspc	$⊢ m \in A \to (\forall j \in A \forall k \in B E \in ℂ \to \forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ)$
117	109 116	mpan9	$⊢ (φ \land m \in A) \to \forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ$
118		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ ⦋ m / j ⦌ E$
119	118	nfel1	$⊢ Ⅎ k ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
120		csbeq1a	$⊢ k = n \to ⦋ m / j ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
121	120	eleq1d	$⊢ k = n \to (⦋ m / j ⦌ E \in ℂ \leftrightarrow ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
122	119 121	rspc	$⊢ n \in ⦋ m / j ⦌ B \to (\forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ \to ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
123	117 122	syl5com	$⊢ (φ \land m \in A) \to (n \in ⦋ m / j ⦌ B \to ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
124	123	impr	$⊢ (φ \land (m \in A \land n \in ⦋ m / j ⦌ B)) \to ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
125	99 78 108 124	syl12anc	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
126	125	ralrimivva	$⊢ φ \to \forall n \in C \forall m \in ⦋ n / k ⦌ D ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
127	126	adantr	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to \forall n \in C \forall m \in ⦋ n / k ⦌ D ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
128		eliun	$⊢ w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D) \leftrightarrow \exists n \in C w \in (\{n\} \times ⦋ n / k ⦌ D)$
129	128	bilani	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to \exists n \in C w \in (\{n\} \times ⦋ n / k ⦌ D)$
130		xp1st	$⊢ w \in (\{n\} \times ⦋ n / k ⦌ D) \to 1^{st} (w) \in \{n\}$
131	130	adantl	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 1^{st} (w) \in \{n\}$
132		elsni	$⊢ 1^{st} (w) \in \{n\} \to 1^{st} (w) = n$
133	131 132	syl	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 1^{st} (w) = n$
134		simpl	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to n \in C$
135	133 134	eqeltrd	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 1^{st} (w) \in C$
136	135	rexlimiva	$⊢ \exists n \in C w \in (\{n\} \times ⦋ n / k ⦌ D) \to 1^{st} (w) \in C$
137	129 136	syl	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to 1^{st} (w) \in C$
138	98 127 137	rspcdva	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to \forall m \in ⦋ 1^{st} (w) / k ⦌ D ⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E \in ℂ$
139		xp2nd	$⊢ w \in (\{n\} \times ⦋ n / k ⦌ D) \to 2^{nd} (w) \in ⦋ n / k ⦌ D$
140	139	adantl	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 2^{nd} (w) \in ⦋ n / k ⦌ D$
141	133	csbeq1d	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to ⦋ 1^{st} (w) / k ⦌ D = ⦋ n / k ⦌ D$
142	140 141	eleqtrrd	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
143	142	rexlimiva	$⊢ \exists n \in C w \in (\{n\} \times ⦋ n / k ⦌ D) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
144	129 143	syl	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
145	94 138 144	rspcdva	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E \in ℂ$
146	53 59 86 91 145	fsumcnv	$⊢ φ \to \sum_{w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)} ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E = \sum_{z \in {⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)}^{-1}} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E$
147	45 146	eqtr4d	$⊢ φ \to \sum_{z \in ⋃_{m \in A} (\{m\} \times ⦋ m / j ⦌ B)} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = \sum_{w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)} ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
148	3	ralrimiva	$⊢ φ \to \forall j \in A B \in Fin$
149	29	nfel1	$⊢ Ⅎ j ⦋ m / j ⦌ B \in Fin$
150	32	eleq1d	$⊢ j = m \to (B \in Fin \leftrightarrow ⦋ m / j ⦌ B \in Fin)$
151	149 150	rspc	$⊢ m \in A \to (\forall j \in A B \in Fin \to ⦋ m / j ⦌ B \in Fin)$
152	148 151	mpan9	$⊢ (φ \land m \in A) \to ⦋ m / j ⦌ B \in Fin$
153	59 1 152 124	fsum2d	$⊢ φ \to \sum_{m \in A} \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E = \sum_{z \in ⋃_{m \in A} (\{m\} \times ⦋ m / j ⦌ B)} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E$
154	53 2 81 125	fsum2d	$⊢ φ \to \sum_{n \in C} \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E = \sum_{w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)} ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
155	147 153 154	3eqtr4d	$⊢ φ \to \sum_{m \in A} \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E = \sum_{n \in C} \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
156		csbeq1a	$⊢ k = n \to E = ⦋ n / k ⦌ E$
157		nfcv	$⊢ \underline{Ⅎ} n E$
158		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ E$
159	156 157 158	cbvsum	$⊢ \sum_{k \in B} E = \sum_{n \in B} ⦋ n / k ⦌ E$
160	113	csbeq2dv	$⊢ j = m \to ⦋ n / k ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
161	160	adantr	$⊢ (j = m \land n \in B) \to ⦋ n / k ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
162	32 161	sumeq12dv	$⊢ j = m \to \sum_{n \in B} ⦋ n / k ⦌ E = \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
163	159 162	eqtrid	$⊢ j = m \to \sum_{k \in B} E = \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
164		nfcv	$⊢ \underline{Ⅎ} m \sum_{k \in B} E$
165		nfcv	$⊢ \underline{Ⅎ} j n$
166	165 110	nfcsbw	$⊢ \underline{Ⅎ} j ⦋ n / k ⦌ ⦋ m / j ⦌ E$
167	29 166	nfsum	$⊢ \underline{Ⅎ} j \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
168	163 164 167	cbvsum	$⊢ \sum_{j \in A} \sum_{k \in B} E = \sum_{m \in A} \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
169		nfcv	$⊢ \underline{Ⅎ} m E$
170	113 169 110	cbvsum	$⊢ \sum_{j \in D} E = \sum_{m \in D} ⦋ m / j ⦌ E$
171	120	adantr	$⊢ (k = n \land m \in D) \to ⦋ m / j ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
172	40 171	sumeq12dv	$⊢ k = n \to \sum_{m \in D} ⦋ m / j ⦌ E = \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
173	170 172	eqtrid	$⊢ k = n \to \sum_{j \in D} E = \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
174		nfcv	$⊢ \underline{Ⅎ} n \sum_{j \in D} E$
175	37 118	nfsum	$⊢ \underline{Ⅎ} k \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
176	173 174 175	cbvsum	$⊢ \sum_{k \in C} \sum_{j \in D} E = \sum_{n \in C} \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
177	155 168 176	3eqtr4g	$⊢ φ \to \sum_{j \in A} \sum_{k \in B} E = \sum_{k \in C} \sum_{j \in D} E$

Metamath Proof Explorer

Theorem fsumcom2

Proof