esum2dlem

Description: Lemma for esum2d (finite case). (Contributed by Thierry Arnoux, 17-May-2020) (Proof shortened by AV, 17-Sep-2021)

	Ref	Expression
Hypotheses	esum2d.0	$⊢ \underline{Ⅎ} k F$
	esum2d.1	$⊢ z = ⟨j, k⟩ \to F = C$
	esum2d.2	$⊢ φ \to A \in V$
	esum2d.3	$⊢ (φ \land j \in A) \to B \in W$
	esum2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in [0, +∞]$
	esum2dlem.e	$⊢ φ \to A \in Fin$
Assertion	esum2dlem	$⊢ φ \to \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$

Proof

Step	Hyp	Ref	Expression
1		esum2d.0	$⊢ \underline{Ⅎ} k F$
2		esum2d.1	$⊢ z = ⟨j, k⟩ \to F = C$
3		esum2d.2	$⊢ φ \to A \in V$
4		esum2d.3	$⊢ (φ \land j \in A) \to B \in W$
5		esum2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in [0, +∞]$
6		esum2dlem.e	$⊢ φ \to A \in Fin$
7		esumeq1	$⊢ a = \emptyset \to \underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{j \in \emptyset}{\sum^{}} \underset{k \in B}{\sum^{}} C$
8		nfv	$⊢ Ⅎ z a = \emptyset$
9		iuneq1	$⊢ a = \emptyset \to ⋃_{j \in a} (\{j\} \times B) = ⋃_{j \in \emptyset} (\{j\} \times B)$
10	8 9	esumeq1d	$⊢ a = \emptyset \to \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F = \underset{z \in ⋃_{j \in \emptyset} (\{j\} \times B)}{\sum^{}} F$
11	7 10	eqeq12d	$⊢ a = \emptyset \to (\underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F \leftrightarrow \underset{j \in \emptyset}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in \emptyset} (\{j\} \times B)}{\sum^{}} F)$
12		esumeq1	$⊢ a = b \to \underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C$
13		nfv	$⊢ Ⅎ z a = b$
14		iuneq1	$⊢ a = b \to ⋃_{j \in a} (\{j\} \times B) = ⋃_{j \in b} (\{j\} \times B)$
15	13 14	esumeq1d	$⊢ a = b \to \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F$
16	12 15	eqeq12d	$⊢ a = b \to (\underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F \leftrightarrow \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F)$
17		esumeq1	$⊢ a = b \cup \{l\} \to \underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{j \in b \cup \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C$
18		nfv	$⊢ Ⅎ z a = b \cup \{l\}$
19		iuneq1	$⊢ a = b \cup \{l\} \to ⋃_{j \in a} (\{j\} \times B) = ⋃_{j \in b \cup \{l\}} (\{j\} \times B)$
20	18 19	esumeq1d	$⊢ a = b \cup \{l\} \to \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F = \underset{z \in ⋃_{j \in b \cup \{l\}} (\{j\} \times B)}{\sum^{}} F$
21	17 20	eqeq12d	$⊢ a = b \cup \{l\} \to (\underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F \leftrightarrow \underset{j \in b \cup \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b \cup \{l\}} (\{j\} \times B)}{\sum^{}} F)$
22		esumeq1	$⊢ a = A \to \underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C$
23		nfv	$⊢ Ⅎ z a = A$
24		iuneq1	$⊢ a = A \to ⋃_{j \in a} (\{j\} \times B) = ⋃_{j \in A} (\{j\} \times B)$
25	23 24	esumeq1d	$⊢ a = A \to \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F$
26	22 25	eqeq12d	$⊢ a = A \to (\underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F \leftrightarrow \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F)$
27		esumnul	$⊢ \underset{z \in \emptyset}{\sum^{*}} F = 0$
28		0iun	$⊢ ⋃_{j \in \emptyset} (\{j\} \times B) = \emptyset$
29		esumeq1	$⊢ ⋃_{j \in \emptyset} (\{j\} \times B) = \emptyset \to \underset{z \in ⋃_{j \in \emptyset} (\{j\} \times B)}{\sum^{}} F = \underset{z \in \emptyset}{\sum^{}} F$
30	28 29	ax-mp	$⊢ \underset{z \in ⋃_{j \in \emptyset} (\{j\} \times B)}{\sum^{}} F = \underset{z \in \emptyset}{\sum^{}} F$
31		esumnul	$⊢ \underset{j \in \emptyset}{\sum^{}} \underset{k \in B}{\sum^{}} C = 0$
32	27 30 31	3eqtr4ri	$⊢ \underset{j \in \emptyset}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in \emptyset} (\{j\} \times B)}{\sum^{*}} F$
33	32	a1i	$⊢ φ \to \underset{j \in \emptyset}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in \emptyset} (\{j\} \times B)}{\sum^{*}} F$
34		simpr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F) \to \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F$
35		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ l / j ⦌ B$
36		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ l / j ⦌ C$
37	35 36	nfesum2	$⊢ \underline{Ⅎ} j \underset{k \in ⦋ l / j ⦌ B}{\sum^{*}} ⦋ l / j ⦌ C$
38		csbeq1a	$⊢ j = l \to B = ⦋ l / j ⦌ B$
39		csbeq1a	$⊢ j = l \to C = ⦋ l / j ⦌ C$
40	38 39	esumeq12d	$⊢ j = l \to \underset{k \in B}{\sum^{}} C = \underset{k \in ⦋ l / j ⦌ B}{\sum^{}} ⦋ l / j ⦌ C$
41	40	adantl	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j = l) \to \underset{k \in B}{\sum^{}} C = \underset{k \in ⦋ l / j ⦌ B}{\sum^{}} ⦋ l / j ⦌ C$
42		simprr	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to l \in (A ∖ b)$
43	42	eldifad	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to l \in A$
44	4	adantlr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in A) \to B \in W$
45	44	ralrimiva	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \forall j \in A B \in W$
46		rspcsbela	$⊢ (l \in A \land \forall j \in A B \in W) \to ⦋ l / j ⦌ B \in W$
47	43 45 46	syl2anc	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to ⦋ l / j ⦌ B \in W$
48		simpll	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land k \in ⦋ l / j ⦌ B) \to φ$
49	43	adantr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land k \in ⦋ l / j ⦌ B) \to l \in A$
50		simpr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land k \in ⦋ l / j ⦌ B) \to k \in ⦋ l / j ⦌ B$
51	5	ex	$⊢ φ \to ((j \in A \land k \in B) \to C \in [0, +∞])$
52	51	sbcimdv	$⊢ φ \to (\underset{˙}{[} l / j \underset{˙}{]} (j \in A \land k \in B) \to \underset{˙}{[} l / j \underset{˙}{]} C \in [0, +∞])$
53		sbcan	$⊢ \underset{˙}{[} l / j \underset{˙}{]} (j \in A \land k \in B) \leftrightarrow (\underset{˙}{[} l / j \underset{˙}{]} j \in A \land \underset{˙}{[} l / j \underset{˙}{]} k \in B)$
54		sbcel1v	$⊢ \underset{˙}{[} l / j \underset{˙}{]} j \in A \leftrightarrow l \in A$
55		sbcel2	$⊢ \underset{˙}{[} l / j \underset{˙}{]} k \in B \leftrightarrow k \in ⦋ l / j ⦌ B$
56	54 55	anbi12i	$⊢ (\underset{˙}{[} l / j \underset{˙}{]} j \in A \land \underset{˙}{[} l / j \underset{˙}{]} k \in B) \leftrightarrow (l \in A \land k \in ⦋ l / j ⦌ B)$
57	53 56	bitri	$⊢ \underset{˙}{[} l / j \underset{˙}{]} (j \in A \land k \in B) \leftrightarrow (l \in A \land k \in ⦋ l / j ⦌ B)$
58		vex	$⊢ l \in V$
59		sbcel1g	$⊢ l \in V \to (\underset{˙}{[} l / j \underset{˙}{]} C \in [0, +∞] \leftrightarrow ⦋ l / j ⦌ C \in [0, +∞])$
60	58 59	ax-mp	$⊢ \underset{˙}{[} l / j \underset{˙}{]} C \in [0, +∞] \leftrightarrow ⦋ l / j ⦌ C \in [0, +∞]$
61	52 57 60	3imtr3g	$⊢ φ \to ((l \in A \land k \in ⦋ l / j ⦌ B) \to ⦋ l / j ⦌ C \in [0, +∞])$
62	61	imp	$⊢ (φ \land (l \in A \land k \in ⦋ l / j ⦌ B)) \to ⦋ l / j ⦌ C \in [0, +∞]$
63	48 49 50 62	syl12anc	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land k \in ⦋ l / j ⦌ B) \to ⦋ l / j ⦌ C \in [0, +∞]$
64	63	ralrimiva	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \forall k \in ⦋ l / j ⦌ B ⦋ l / j ⦌ C \in [0, +∞]$
65		nfcv	$⊢ \underline{Ⅎ} k ⦋ l / j ⦌ B$
66	65	esumcl	$⊢ (⦋ l / j ⦌ B \in W \land \forall k \in ⦋ l / j ⦌ B ⦋ l / j ⦌ C \in [0, +∞]) \to \underset{k \in ⦋ l / j ⦌ B}{\sum^{*}} ⦋ l / j ⦌ C \in [0, +∞]$
67	47 64 66	syl2anc	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \underset{k \in ⦋ l / j ⦌ B}{\sum^{*}} ⦋ l / j ⦌ C \in [0, +∞]$
68	37 41 42 67	esumsnf	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \underset{j \in \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{k \in ⦋ l / j ⦌ B}{\sum^{*}} ⦋ l / j ⦌ C$
69		nfv	$⊢ Ⅎ k (φ \land (b \subseteq A \land l \in (A ∖ b)))$
70		nfv	$⊢ Ⅎ j z = ⟨l, k⟩$
71	36	nfeq2	$⊢ Ⅎ j F = ⦋ l / j ⦌ C$
72	70 71	nfim	$⊢ Ⅎ j (z = ⟨l, k⟩ \to F = ⦋ l / j ⦌ C)$
73		opeq1	$⊢ j = l \to ⟨j, k⟩ = ⟨l, k⟩$
74	73	eqeq2d	$⊢ j = l \to (z = ⟨j, k⟩ \leftrightarrow z = ⟨l, k⟩)$
75	39	eqeq2d	$⊢ j = l \to (F = C \leftrightarrow F = ⦋ l / j ⦌ C)$
76	74 75	imbi12d	$⊢ j = l \to ((z = ⟨j, k⟩ \to F = C) \leftrightarrow (z = ⟨l, k⟩ \to F = ⦋ l / j ⦌ C))$
77	72 76 2	chvarfv	$⊢ z = ⟨l, k⟩ \to F = ⦋ l / j ⦌ C$
78		vsnid	$⊢ j \in \{j\}$
79	78	a1i	$⊢ ((φ \land j \in A) \land k \in B) \to j \in \{j\}$
80		simpr	$⊢ ((φ \land j \in A) \land k \in B) \to k \in B$
81	79 80	opelxpd	$⊢ ((φ \land j \in A) \land k \in B) \to ⟨j, k⟩ \in (\{j\} \times B)$
82		xp2nd	$⊢ z \in (\{j\} \times B) \to 2^{nd} (z) \in B$
83		xp1st	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) \in \{j\}$
84		fvex	$⊢ 1^{st} (z) \in V$
85	84	elsn	$⊢ 1^{st} (z) \in \{j\} \leftrightarrow 1^{st} (z) = j$
86	83 85	sylib	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) = j$
87		eqop	$⊢ z \in (\{j\} \times B) \to (z = ⟨j, k⟩ \leftrightarrow (1^{st} (z) = j \land 2^{nd} (z) = k))$
88	86 87	mpbirand	$⊢ z \in (\{j\} \times B) \to (z = ⟨j, k⟩ \leftrightarrow 2^{nd} (z) = k)$
89		eqcom	$⊢ 2^{nd} (z) = k \leftrightarrow k = 2^{nd} (z)$
90	88 89	syl6bb	$⊢ z \in (\{j\} \times B) \to (z = ⟨j, k⟩ \leftrightarrow k = 2^{nd} (z))$
91	90	ad2antlr	$⊢ (((φ \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \to (z = ⟨j, k⟩ \leftrightarrow k = 2^{nd} (z))$
92	91	ralrimiva	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to \forall k \in B (z = ⟨j, k⟩ \leftrightarrow k = 2^{nd} (z))$
93		reu6i	$⊢ (2^{nd} (z) \in B \land \forall k \in B (z = ⟨j, k⟩ \leftrightarrow k = 2^{nd} (z))) \to \exists! k \in B z = ⟨j, k⟩$
94	82 92 93	syl2an2	$⊢ ((φ \land j \in A) \land z \in (\{j\} \times B)) \to \exists! k \in B z = ⟨j, k⟩$
95	81 94	f1mptrn	$⊢ (φ \land j \in A) \to Fun {(k \in B ⟼ ⟨j, k⟩)}^{-1}$
96	95	ex	$⊢ φ \to (j \in A \to Fun {(k \in B ⟼ ⟨j, k⟩)}^{-1})$
97	96	sbcimdv	$⊢ φ \to (\underset{˙}{[} l / j \underset{˙}{]} j \in A \to \underset{˙}{[} l / j \underset{˙}{]} Fun {(k \in B ⟼ ⟨j, k⟩)}^{-1})$
98		sbcfung	$⊢ l \in V \to (\underset{˙}{[} l / j \underset{˙}{]} Fun {(k \in B ⟼ ⟨j, k⟩)}^{-1} \leftrightarrow Fun ⦋ l / j ⦌ {(k \in B ⟼ ⟨j, k⟩)}^{-1})$
99		csbcnv	$⊢ {⦋ l / j ⦌ (k \in B ⟼ ⟨j, k⟩)}^{-1} = ⦋ l / j ⦌ {(k \in B ⟼ ⟨j, k⟩)}^{-1}$
100		csbmpt12	$⊢ l \in V \to ⦋ l / j ⦌ (k \in B ⟼ ⟨j, k⟩) = (k \in ⦋ l / j ⦌ B ⟼ ⦋ l / j ⦌ ⟨j, k⟩)$
101		csbopg	$⊢ l \in V \to ⦋ l / j ⦌ ⟨j, k⟩ = ⟨⦋ l / j ⦌ j, ⦋ l / j ⦌ k⟩$
102		csbvarg	$⊢ l \in V \to ⦋ l / j ⦌ j = l$
103		csbconstg	$⊢ l \in V \to ⦋ l / j ⦌ k = k$
104	102 103	opeq12d	$⊢ l \in V \to ⟨⦋ l / j ⦌ j, ⦋ l / j ⦌ k⟩ = ⟨l, k⟩$
105	101 104	eqtrd	$⊢ l \in V \to ⦋ l / j ⦌ ⟨j, k⟩ = ⟨l, k⟩$
106	105	mpteq2dv	$⊢ l \in V \to (k \in ⦋ l / j ⦌ B ⟼ ⦋ l / j ⦌ ⟨j, k⟩) = (k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)$
107	100 106	eqtrd	$⊢ l \in V \to ⦋ l / j ⦌ (k \in B ⟼ ⟨j, k⟩) = (k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)$
108	107	cnveqd	$⊢ l \in V \to {⦋ l / j ⦌ (k \in B ⟼ ⟨j, k⟩)}^{-1} = {(k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)}^{-1}$
109	99 108	syl5eqr	$⊢ l \in V \to ⦋ l / j ⦌ {(k \in B ⟼ ⟨j, k⟩)}^{-1} = {(k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)}^{-1}$
110	109	funeqd	$⊢ l \in V \to (Fun ⦋ l / j ⦌ {(k \in B ⟼ ⟨j, k⟩)}^{-1} \leftrightarrow Fun {(k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)}^{-1})$
111	98 110	bitrd	$⊢ l \in V \to (\underset{˙}{[} l / j \underset{˙}{]} Fun {(k \in B ⟼ ⟨j, k⟩)}^{-1} \leftrightarrow Fun {(k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)}^{-1})$
112	58 111	ax-mp	$⊢ \underset{˙}{[} l / j \underset{˙}{]} Fun {(k \in B ⟼ ⟨j, k⟩)}^{-1} \leftrightarrow Fun {(k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)}^{-1}$
113	97 54 112	3imtr3g	$⊢ φ \to (l \in A \to Fun {(k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)}^{-1})$
114	113	imp	$⊢ (φ \land l \in A) \to Fun {(k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)}^{-1}$
115	43 114	syldan	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to Fun {(k \in ⦋ l / j ⦌ B ⟼ ⟨l, k⟩)}^{-1}$
116		vsnid	$⊢ l \in \{l\}$
117	116	a1i	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land k \in ⦋ l / j ⦌ B) \to l \in \{l\}$
118	117 50	opelxpd	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land k \in ⦋ l / j ⦌ B) \to ⟨l, k⟩ \in (\{l\} \times ⦋ l / j ⦌ B)$
119	1 69 65 77 47 115 63 118	esumc	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \underset{k \in ⦋ l / j ⦌ B}{\sum^{}} ⦋ l / j ⦌ C = \underset{z \in \{t \| \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩\}}{\sum^{}} F$
120		nfab1	$⊢ \underline{Ⅎ} t \{t \| \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩\}$
121		nfcv	$⊢ \underline{Ⅎ} t (\{l\} \times ⦋ l / j ⦌ B)$
122		opeq1	$⊢ i = l \to ⟨i, k⟩ = ⟨l, k⟩$
123	122	eqeq2d	$⊢ i = l \to (t = ⟨i, k⟩ \leftrightarrow t = ⟨l, k⟩)$
124	123	rexbidv	$⊢ i = l \to (\exists k \in ⦋ l / j ⦌ B t = ⟨i, k⟩ \leftrightarrow \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩)$
125	58 124	rexsn	$⊢ \exists i \in \{l\} \exists k \in ⦋ l / j ⦌ B t = ⟨i, k⟩ \leftrightarrow \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩$
126		elxp2	$⊢ t \in (\{l\} \times ⦋ l / j ⦌ B) \leftrightarrow \exists i \in \{l\} \exists k \in ⦋ l / j ⦌ B t = ⟨i, k⟩$
127		abid	$⊢ t \in \{t \| \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩\} \leftrightarrow \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩$
128	125 126 127	3bitr4ri	$⊢ t \in \{t \| \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩\} \leftrightarrow t \in (\{l\} \times ⦋ l / j ⦌ B)$
129	120 121 128	eqri	$⊢ \{t \| \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩\} = \{l\} \times ⦋ l / j ⦌ B$
130		esumeq1	$⊢ \{t \| \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩\} = \{l\} \times ⦋ l / j ⦌ B \to \underset{z \in \{t \| \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩\}}{\sum^{}} F = \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{}} F$
131	129 130	ax-mp	$⊢ \underset{z \in \{t \| \exists k \in ⦋ l / j ⦌ B t = ⟨l, k⟩\}}{\sum^{}} F = \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{}} F$
132	119 131	eqtrdi	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \underset{k \in ⦋ l / j ⦌ B}{\sum^{}} ⦋ l / j ⦌ C = \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{}} F$
133	68 132	eqtrd	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \underset{j \in \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{*}} F$
134	133	adantr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F) \to \underset{j \in \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{}} F$
135	34 134	oveq12d	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F) \to \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C +_{𝑒} \underset{j \in \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F +_{𝑒} \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{*}} F$
136		nfv	$⊢ Ⅎ j (φ \land (b \subseteq A \land l \in (A ∖ b)))$
137		nfcv	$⊢ \underline{Ⅎ} j b$
138		nfcv	$⊢ \underline{Ⅎ} j \{l\}$
139		vex	$⊢ b \in V$
140	139	a1i	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to b \in V$
141		snex	$⊢ \{l\} \in V$
142	141	a1i	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \{l\} \in V$
143	42	eldifbd	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \neg l \in b$
144		disjsn	$⊢ b \cap \{l\} = \emptyset \leftrightarrow \neg l \in b$
145	143 144	sylibr	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to b \cap \{l\} = \emptyset$
146		simpll	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to φ$
147		simprl	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to b \subseteq A$
148	147	sselda	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to j \in A$
149	5	anassrs	$⊢ ((φ \land j \in A) \land k \in B) \to C \in [0, +∞]$
150	149	ralrimiva	$⊢ (φ \land j \in A) \to \forall k \in B C \in [0, +∞]$
151		nfcv	$⊢ \underline{Ⅎ} k B$
152	151	esumcl	$⊢ (B \in W \land \forall k \in B C \in [0, +∞]) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
153	4 150 152	syl2anc	$⊢ (φ \land j \in A) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
154	146 148 153	syl2anc	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
155		simpll	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in \{l\}) \to φ$
156	43	snssd	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \{l\} \subseteq A$
157	156	sselda	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in \{l\}) \to j \in A$
158	155 157 153	syl2anc	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in \{l\}) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
159	136 137 138 140 142 145 154 158	esumsplit	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \underset{j \in b \cup \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C +_{𝑒} \underset{j \in \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C$
160	159	adantr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F) \to \underset{j \in b \cup \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C +_{𝑒} \underset{j \in \{l\}}{\sum^{}} \underset{k \in B}{\sum^{*}} C$
161		iunxun	$⊢ ⋃_{j \in b \cup \{l\}} (\{j\} \times B) = ⋃_{j \in b} (\{j\} \times B) \cup ⋃_{j \in \{l\}} (\{j\} \times B)$
162	138 35	nfxp	$⊢ \underline{Ⅎ} j (\{l\} \times ⦋ l / j ⦌ B)$
163		sneq	$⊢ j = l \to \{j\} = \{l\}$
164	163 38	xpeq12d	$⊢ j = l \to \{j\} \times B = \{l\} \times ⦋ l / j ⦌ B$
165	162 164	iunxsngf	$⊢ l \in V \to ⋃_{j \in \{l\}} (\{j\} \times B) = \{l\} \times ⦋ l / j ⦌ B$
166	58 165	ax-mp	$⊢ ⋃_{j \in \{l\}} (\{j\} \times B) = \{l\} \times ⦋ l / j ⦌ B$
167	166	uneq2i	$⊢ ⋃_{j \in b} (\{j\} \times B) \cup ⋃_{j \in \{l\}} (\{j\} \times B) = ⋃_{j \in b} (\{j\} \times B) \cup (\{l\} \times ⦋ l / j ⦌ B)$
168	161 167	eqtri	$⊢ ⋃_{j \in b \cup \{l\}} (\{j\} \times B) = ⋃_{j \in b} (\{j\} \times B) \cup (\{l\} \times ⦋ l / j ⦌ B)$
169		esumeq1	$⊢ ⋃_{j \in b \cup \{l\}} (\{j\} \times B) = ⋃_{j \in b} (\{j\} \times B) \cup (\{l\} \times ⦋ l / j ⦌ B) \to \underset{z \in ⋃_{j \in b \cup \{l\}} (\{j\} \times B)}{\sum^{}} F = \underset{z \in ⋃_{j \in b} (\{j\} \times B) \cup (\{l\} \times ⦋ l / j ⦌ B)}{\sum^{}} F$
170	168 169	ax-mp	$⊢ \underset{z \in ⋃_{j \in b \cup \{l\}} (\{j\} \times B)}{\sum^{}} F = \underset{z \in ⋃_{j \in b} (\{j\} \times B) \cup (\{l\} \times ⦋ l / j ⦌ B)}{\sum^{}} F$
171		nfv	$⊢ Ⅎ z (φ \land (b \subseteq A \land l \in (A ∖ b)))$
172		nfcv	$⊢ \underline{Ⅎ} z ⋃_{j \in b} (\{j\} \times B)$
173		nfcv	$⊢ \underline{Ⅎ} z (\{l\} \times ⦋ l / j ⦌ B)$
174		snex	$⊢ \{j\} \in V$
175	148 44	syldan	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to B \in W$
176		xpexg	$⊢ (\{j\} \in V \land B \in W) \to \{j\} \times B \in V$
177	174 175 176	sylancr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to \{j\} \times B \in V$
178	177	ralrimiva	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \forall j \in b \{j\} \times B \in V$
179		iunexg	$⊢ (b \in V \land \forall j \in b \{j\} \times B \in V) \to ⋃_{j \in b} (\{j\} \times B) \in V$
180	139 178 179	sylancr	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to ⋃_{j \in b} (\{j\} \times B) \in V$
181		xpexg	$⊢ (\{l\} \in V \land ⦋ l / j ⦌ B \in W) \to \{l\} \times ⦋ l / j ⦌ B \in V$
182	141 47 181	sylancr	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \{l\} \times ⦋ l / j ⦌ B \in V$
183		simpr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to j \in b$
184	143	adantr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to \neg l \in b$
185		nelne2	$⊢ (j \in b \land \neg l \in b) \to j \neq l$
186	183 184 185	syl2anc	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to j \neq l$
187		disjsn2	$⊢ j \neq l \to \{j\} \cap \{l\} = \emptyset$
188		xpdisj1	$⊢ \{j\} \cap \{l\} = \emptyset \to (\{j\} \times B) \cap (\{l\} \times ⦋ l / j ⦌ B) = \emptyset$
189	186 187 188	3syl	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land j \in b) \to (\{j\} \times B) \cap (\{l\} \times ⦋ l / j ⦌ B) = \emptyset$
190	189	iuneq2dv	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to ⋃_{j \in b} ((\{j\} \times B) \cap (\{l\} \times ⦋ l / j ⦌ B)) = ⋃_{j \in b} \emptyset$
191	162	iunin1f	$⊢ ⋃_{j \in b} ((\{j\} \times B) \cap (\{l\} \times ⦋ l / j ⦌ B)) = ⋃_{j \in b} (\{j\} \times B) \cap (\{l\} \times ⦋ l / j ⦌ B)$
192		iun0	$⊢ ⋃_{j \in b} \emptyset = \emptyset$
193	190 191 192	3eqtr3g	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to ⋃_{j \in b} (\{j\} \times B) \cap (\{l\} \times ⦋ l / j ⦌ B) = \emptyset$
194		simpll	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land z \in ⋃_{j \in b} (\{j\} \times B)) \to φ$
195		iunss1	$⊢ b \subseteq A \to ⋃_{j \in b} (\{j\} \times B) \subseteq ⋃_{j \in A} (\{j\} \times B)$
196	147 195	syl	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to ⋃_{j \in b} (\{j\} \times B) \subseteq ⋃_{j \in A} (\{j\} \times B)$
197	196	sselda	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land z \in ⋃_{j \in b} (\{j\} \times B)) \to z \in ⋃_{j \in A} (\{j\} \times B)$
198		nfv	$⊢ Ⅎ j φ$
199		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} (\{j\} \times B)$
200	199	nfcri	$⊢ Ⅎ j z \in ⋃_{j \in A} (\{j\} \times B)$
201	198 200	nfan	$⊢ Ⅎ j (φ \land z \in ⋃_{j \in A} (\{j\} \times B))$
202		nfv	$⊢ Ⅎ k (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B))$
203		nfcv	$⊢ \underline{Ⅎ} k [0, +∞]$
204	1 203	nfel	$⊢ Ⅎ k F \in [0, +∞]$
205	2	adantl	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to F = C$
206		simp-5l	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to φ$
207		simp-4r	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to j \in A$
208		simplr	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to k \in B$
209	206 207 208 5	syl12anc	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to C \in [0, +∞]$
210	205 209	eqeltrd	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to F \in [0, +∞]$
211		elsnxp	$⊢ j \in A \to (z \in (\{j\} \times B) \leftrightarrow \exists k \in B z = ⟨j, k⟩)$
212	211	biimpa	$⊢ (j \in A \land z \in (\{j\} \times B)) \to \exists k \in B z = ⟨j, k⟩$
213	212	adantll	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \to \exists k \in B z = ⟨j, k⟩$
214	202 204 210 213	r19.29af2	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \to F \in [0, +∞]$
215		simpr	$⊢ (φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \to z \in ⋃_{j \in A} (\{j\} \times B)$
216		eliun	$⊢ z \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists j \in A z \in (\{j\} \times B)$
217	215 216	sylib	$⊢ (φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \to \exists j \in A z \in (\{j\} \times B)$
218	201 214 217	r19.29af	$⊢ (φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \to F \in [0, +∞]$
219	194 197 218	syl2anc	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land z \in ⋃_{j \in b} (\{j\} \times B)) \to F \in [0, +∞]$
220		simpll	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land z \in (\{l\} \times ⦋ l / j ⦌ B)) \to φ$
221		nfcv	$⊢ \underline{Ⅎ} j A$
222		nfcv	$⊢ \underline{Ⅎ} j l$
223	221 222 162 164	ssiun2sf	$⊢ l \in A \to \{l\} \times ⦋ l / j ⦌ B \subseteq ⋃_{j \in A} (\{j\} \times B)$
224	43 223	syl	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \{l\} \times ⦋ l / j ⦌ B \subseteq ⋃_{j \in A} (\{j\} \times B)$
225	224	sselda	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land z \in (\{l\} \times ⦋ l / j ⦌ B)) \to z \in ⋃_{j \in A} (\{j\} \times B)$
226	220 225 218	syl2anc	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land z \in (\{l\} \times ⦋ l / j ⦌ B)) \to F \in [0, +∞]$
227	171 172 173 180 182 193 219 226	esumsplit	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \underset{z \in ⋃_{j \in b} (\{j\} \times B) \cup (\{l\} \times ⦋ l / j ⦌ B)}{\sum^{}} F = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F +_{𝑒} \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{*}} F$
228	170 227	syl5eq	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to \underset{z \in ⋃_{j \in b \cup \{l\}} (\{j\} \times B)}{\sum^{}} F = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F +_{𝑒} \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{*}} F$
229	228	adantr	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F) \to \underset{z \in ⋃_{j \in b \cup \{l\}} (\{j\} \times B)}{\sum^{}} F = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F +_{𝑒} \underset{z \in \{l\} \times ⦋ l / j ⦌ B}{\sum^{}} F$
230	135 160 229	3eqtr4d	$⊢ ((φ \land (b \subseteq A \land l \in (A ∖ b))) \land \underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F) \to \underset{j \in b \cup \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b \cup \{l\}} (\{j\} \times B)}{\sum^{}} F$
231	230	ex	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to (\underset{j \in b}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b} (\{j\} \times B)}{\sum^{}} F \to \underset{j \in b \cup \{l\}}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in b \cup \{l\}} (\{j\} \times B)}{\sum^{}} F)$
232	11 16 21 26 33 231 6	findcard2d	$⊢ φ \to \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$

Metamath Proof Explorer

Theorem esum2dlem

Proof