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		simpr	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to ⟨m, n⟩ \in (\{j\} \times B)$
71		opelxp	$⊢ ⟨m, n⟩ \in (\{j\} \times B) \leftrightarrow (m \in \{j\} \land n \in B)$
72	70 71	sylib	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to (m \in \{j\} \land n \in B)$
73	72	simpld	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to m \in \{j\}$
74		elsni	$⊢ m \in \{j\} \to m = j$
75	73 74	syl	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to m = j$
76		simpl	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to j \in A$
77	75 76	eqeltrd	$⊢ (j \in A \land ⟨m, n⟩ \in (\{j\} \times B)) \to m \in A$
78	77	rexlimiva	$⊢ \exists j \in A ⟨m, n⟩ \in (\{j\} \times B) \to m \in A$
79	69 78	syl	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to m \in A$
80	79	expr	$⊢ (φ \land n \in C) \to (m \in ⦋ n / k ⦌ D \to m \in A)$
81	80	ssrdv	$⊢ (φ \land n \in C) \to ⦋ n / k ⦌ D \subseteq A$
82	61 81	ssfid	$⊢ (φ \land n \in C) \to ⦋ n / k ⦌ D \in Fin$
83		xpfi	$⊢ (\{n\} \in Fin \land ⦋ n / k ⦌ D \in Fin) \to \{n\} \times ⦋ n / k ⦌ D \in Fin$
84	60 82 83	sylancr	$⊢ (φ \land n \in C) \to \{n\} \times ⦋ n / k ⦌ D \in Fin$
85	84	ralrimiva	$⊢ φ \to \forall n \in C \{n\} \times ⦋ n / k ⦌ D \in Fin$
86		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$
87	2 85 86	syl2anc	$⊢ φ \to ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D) \in Fin$
88		reliun	$⊢ Rel ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D) \leftrightarrow \forall n \in C Rel (\{n\} \times ⦋ n / k ⦌ D)$
89		relxp	$⊢ Rel (\{n\} \times ⦋ n / k ⦌ D)$
90	89	a1i	$⊢ n \in C \to Rel (\{n\} \times ⦋ n / k ⦌ D)$
91	88 90	mprgbir	$⊢ Rel ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)$
92	91	a1i	$⊢ φ \to Rel ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)$
93		csbeq1	$⊢ m = 2^{nd} (w) \to ⦋ m / j ⦌ E = ⦋ 2^{nd} (w) / j ⦌ E$
94	93	csbeq2dv	$⊢ m = 2^{nd} (w) \to ⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E = ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
95	94	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 ℂ)$
96		csbeq1	$⊢ n = 1^{st} (w) \to ⦋ n / k ⦌ D = ⦋ 1^{st} (w) / k ⦌ D$
97		csbeq1	$⊢ n = 1^{st} (w) \to ⦋ n / k ⦌ ⦋ m / j ⦌ E = ⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E$
98	97	eleq1d	$⊢ n = 1^{st} (w) \to (⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ \leftrightarrow ⦋ 1^{st} (w) / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
99	96 98	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 ℂ)$
100		simpl	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to φ$
101	29	nfcri	$⊢ Ⅎ j n \in ⦋ m / j ⦌ B$
102	74	equcomd	$⊢ m \in \{j\} \to j = m$
103	102 32	syl	$⊢ m \in \{j\} \to B = ⦋ m / j ⦌ B$
104	103	eleq2d	$⊢ m \in \{j\} \to (n \in B \leftrightarrow n \in ⦋ m / j ⦌ B)$
105	104	biimpa	$⊢ (m \in \{j\} \land n \in B) \to n \in ⦋ m / j ⦌ B$
106	71 105	sylbi	$⊢ ⟨m, n⟩ \in (\{j\} \times B) \to n \in ⦋ m / j ⦌ B$
107	106	a1i	$⊢ j \in A \to (⟨m, n⟩ \in (\{j\} \times B) \to n \in ⦋ m / j ⦌ B)$
108	101 107	rexlimi	$⊢ \exists j \in A ⟨m, n⟩ \in (\{j\} \times B) \to n \in ⦋ m / j ⦌ B$
109	69 108	syl	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to n \in ⦋ m / j ⦌ B$
110	5	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in B E \in ℂ$
111		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ E$
112	111	nfel1	$⊢ Ⅎ j ⦋ m / j ⦌ E \in ℂ$
113	29 112	nfralw	$⊢ Ⅎ j \forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ$
114		csbeq1a	$⊢ j = m \to E = ⦋ m / j ⦌ E$
115	114	eleq1d	$⊢ j = m \to (E \in ℂ \leftrightarrow ⦋ m / j ⦌ E \in ℂ)$
116	32 115	raleqbidv	$⊢ j = m \to (\forall k \in B E \in ℂ \leftrightarrow \forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ)$
117	113 116	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 ℂ)$
118	110 117	mpan9	$⊢ (φ \land m \in A) \to \forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ$
119		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ ⦋ m / j ⦌ E$
120	119	nfel1	$⊢ Ⅎ k ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
121		csbeq1a	$⊢ k = n \to ⦋ m / j ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
122	121	eleq1d	$⊢ k = n \to (⦋ m / j ⦌ E \in ℂ \leftrightarrow ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
123	120 122	rspc	$⊢ n \in ⦋ m / j ⦌ B \to (\forall k \in ⦋ m / j ⦌ B ⦋ m / j ⦌ E \in ℂ \to ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
124	118 123	syl5com	$⊢ (φ \land m \in A) \to (n \in ⦋ m / j ⦌ B \to ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ)$
125	124	impr	$⊢ (φ \land (m \in A \land n \in ⦋ m / j ⦌ B)) \to ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
126	100 79 109 125	syl12anc	$⊢ (φ \land (n \in C \land m \in ⦋ n / k ⦌ D)) \to ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
127	126	ralrimivva	$⊢ φ \to \forall n \in C \forall m \in ⦋ n / k ⦌ D ⦋ n / k ⦌ ⦋ m / j ⦌ E \in ℂ$
128	127	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 ℂ$
129		simpr	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)$
130		eliun	$⊢ w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D) \leftrightarrow \exists n \in C w \in (\{n\} \times ⦋ n / k ⦌ D)$
131	129 130	sylib	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to \exists n \in C w \in (\{n\} \times ⦋ n / k ⦌ D)$
132		xp1st	$⊢ w \in (\{n\} \times ⦋ n / k ⦌ D) \to 1^{st} (w) \in \{n\}$
133	132	adantl	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 1^{st} (w) \in \{n\}$
134		elsni	$⊢ 1^{st} (w) \in \{n\} \to 1^{st} (w) = n$
135	133 134	syl	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 1^{st} (w) = n$
136		simpl	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to n \in C$
137	135 136	eqeltrd	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 1^{st} (w) \in C$
138	137	rexlimiva	$⊢ \exists n \in C w \in (\{n\} \times ⦋ n / k ⦌ D) \to 1^{st} (w) \in C$
139	131 138	syl	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to 1^{st} (w) \in C$
140	99 128 139	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 ℂ$
141		xp2nd	$⊢ w \in (\{n\} \times ⦋ n / k ⦌ D) \to 2^{nd} (w) \in ⦋ n / k ⦌ D$
142	141	adantl	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 2^{nd} (w) \in ⦋ n / k ⦌ D$
143	135	csbeq1d	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to ⦋ 1^{st} (w) / k ⦌ D = ⦋ n / k ⦌ D$
144	142 143	eleqtrrd	$⊢ (n \in C \land w \in (\{n\} \times ⦋ n / k ⦌ D)) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
145	144	rexlimiva	$⊢ \exists n \in C w \in (\{n\} \times ⦋ n / k ⦌ D) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
146	131 145	syl	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
147	95 140 146	rspcdva	$⊢ (φ \land w \in ⋃_{n \in C} (\{n\} \times ⦋ n / k ⦌ D)) \to ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E \in ℂ$
148	53 59 87 92 147	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$
149	45 148	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$
150	3	ralrimiva	$⊢ φ \to \forall j \in A B \in Fin$
151	29	nfel1	$⊢ Ⅎ j ⦋ m / j ⦌ B \in Fin$
152	32	eleq1d	$⊢ j = m \to (B \in Fin \leftrightarrow ⦋ m / j ⦌ B \in Fin)$
153	151 152	rspc	$⊢ m \in A \to (\forall j \in A B \in Fin \to ⦋ m / j ⦌ B \in Fin)$
154	150 153	mpan9	$⊢ (φ \land m \in A) \to ⦋ m / j ⦌ B \in Fin$
155	59 1 154 125	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$
156	53 2 82 126	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$
157	149 155 156	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$
158		nfcv	$⊢ \underline{Ⅎ} m \sum_{k \in B} E$
159		nfcv	$⊢ \underline{Ⅎ} j n$
160	159 111	nfcsbw	$⊢ \underline{Ⅎ} j ⦋ n / k ⦌ ⦋ m / j ⦌ E$
161	29 160	nfsum	$⊢ \underline{Ⅎ} j \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
162		nfcv	$⊢ \underline{Ⅎ} n E$
163		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ E$
164		csbeq1a	$⊢ k = n \to E = ⦋ n / k ⦌ E$
165	162 163 164	cbvsumi	$⊢ \sum_{k \in B} E = \sum_{n \in B} ⦋ n / k ⦌ E$
166	114	csbeq2dv	$⊢ j = m \to ⦋ n / k ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
167	166	adantr	$⊢ (j = m \land n \in B) \to ⦋ n / k ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
168	32 167	sumeq12dv	$⊢ j = m \to \sum_{n \in B} ⦋ n / k ⦌ E = \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
169	165 168	syl5eq	$⊢ j = m \to \sum_{k \in B} E = \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
170	158 161 169	cbvsumi	$⊢ \sum_{j \in A} \sum_{k \in B} E = \sum_{m \in A} \sum_{n \in ⦋ m / j ⦌ B} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
171		nfcv	$⊢ \underline{Ⅎ} n \sum_{j \in D} E$
172	37 119	nfsum	$⊢ \underline{Ⅎ} k \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
173		nfcv	$⊢ \underline{Ⅎ} m E$
174	173 111 114	cbvsumi	$⊢ \sum_{j \in D} E = \sum_{m \in D} ⦋ m / j ⦌ E$
175	121	adantr	$⊢ (k = n \land m \in D) \to ⦋ m / j ⦌ E = ⦋ n / k ⦌ ⦋ m / j ⦌ E$
176	40 175	sumeq12dv	$⊢ k = n \to \sum_{m \in D} ⦋ m / j ⦌ E = \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
177	174 176	syl5eq	$⊢ k = n \to \sum_{j \in D} E = \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
178	171 172 177	cbvsumi	$⊢ \sum_{k \in C} \sum_{j \in D} E = \sum_{n \in C} \sum_{m \in ⦋ n / k ⦌ D} ⦋ n / k ⦌ ⦋ m / j ⦌ E$
179	157 170 178	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