esumrnmpt2

Description: Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020)

	Ref	Expression
Hypotheses	esumrnmpt2.1	$⊢ y = B \to C = D$
	esumrnmpt2.2	$⊢ φ \to A \in V$
	esumrnmpt2.3	$⊢ (φ \land k \in A) \to D \in [0, +∞]$
	esumrnmpt2.4	$⊢ (φ \land k \in A) \to B \in W$
	esumrnmpt2.5	$⊢ ((φ \land k \in A) \land B = \emptyset) \to D = 0$
	esumrnmpt2.6	$⊢ φ \to \underset{k \in A}{Disj} B$
Assertion	esumrnmpt2	$⊢ φ \to \underset{y \in ran (k \in A ⟼ B)}{\sum^{}} C = \underset{k \in A}{\sum^{}} D$

Proof

Step	Hyp	Ref	Expression
1		esumrnmpt2.1	$⊢ y = B \to C = D$
2		esumrnmpt2.2	$⊢ φ \to A \in V$
3		esumrnmpt2.3	$⊢ (φ \land k \in A) \to D \in [0, +∞]$
4		esumrnmpt2.4	$⊢ (φ \land k \in A) \to B \in W$
5		esumrnmpt2.5	$⊢ ((φ \land k \in A) \land B = \emptyset) \to D = 0$
6		esumrnmpt2.6	$⊢ φ \to \underset{k \in A}{Disj} B$
7		nfrab1	$⊢ \underline{Ⅎ} k \{k \in A \| \neg B = \emptyset\}$
8		ssrab2	$⊢ \{k \in A \| \neg B = \emptyset\} \subseteq A$
9	8	a1i	$⊢ φ \to \{k \in A \| \neg B = \emptyset\} \subseteq A$
10	2 9	ssexd	$⊢ φ \to \{k \in A \| \neg B = \emptyset\} \in V$
11	9	sselda	$⊢ (φ \land k \in \{k \in A \| \neg B = \emptyset\}) \to k \in A$
12	11 3	syldan	$⊢ (φ \land k \in \{k \in A \| \neg B = \emptyset\}) \to D \in [0, +∞]$
13	11 4	syldan	$⊢ (φ \land k \in \{k \in A \| \neg B = \emptyset\}) \to B \in W$
14		rabid	$⊢ k \in \{k \in A \| \neg B = \emptyset\} \leftrightarrow (k \in A \land \neg B = \emptyset)$
15	14	simprbi	$⊢ k \in \{k \in A \| \neg B = \emptyset\} \to \neg B = \emptyset$
16	15	adantl	$⊢ (φ \land k \in \{k \in A \| \neg B = \emptyset\}) \to \neg B = \emptyset$
17		elsng	$⊢ B \in W \to (B \in \{\emptyset\} \leftrightarrow B = \emptyset)$
18	13 17	syl	$⊢ (φ \land k \in \{k \in A \| \neg B = \emptyset\}) \to (B \in \{\emptyset\} \leftrightarrow B = \emptyset)$
19	16 18	mtbird	$⊢ (φ \land k \in \{k \in A \| \neg B = \emptyset\}) \to \neg B \in \{\emptyset\}$
20	13 19	eldifd	$⊢ (φ \land k \in \{k \in A \| \neg B = \emptyset\}) \to B \in (W ∖ \{\emptyset\})$
21		nfcv	$⊢ \underline{Ⅎ} k A$
22	7 21	disjss1f	$⊢ \{k \in A \| \neg B = \emptyset\} \subseteq A \to (\underset{k \in A}{Disj} B \to \underset{k \in \{k \in A \| \neg B = \emptyset\}}{Disj} B)$
23	9 6 22	sylc	$⊢ φ \to \underset{k \in \{k \in A \| \neg B = \emptyset\}}{Disj} B$
24	7 1 10 12 20 23	esumrnmpt	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C = \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D$
25		nfv	$⊢ Ⅎ y (φ \land \exists k \in A B = \emptyset)$
26		snex	$⊢ \{\emptyset\} \in V$
27	26	a1i	$⊢ (φ \land \exists k \in A B = \emptyset) \to \{\emptyset\} \in V$
28		velsn	$⊢ y \in \{\emptyset\} \leftrightarrow y = \emptyset$
29	28	bilani	$⊢ ((φ \land \exists k \in A B = \emptyset) \land y \in \{\emptyset\}) \to y = \emptyset$
30		nfv	$⊢ Ⅎ k φ$
31		nfre1	$⊢ Ⅎ k \exists k \in A B = \emptyset$
32	30 31	nfan	$⊢ Ⅎ k (φ \land \exists k \in A B = \emptyset)$
33		nfv	$⊢ Ⅎ k y = \emptyset$
34	32 33	nfan	$⊢ Ⅎ k ((φ \land \exists k \in A B = \emptyset) \land y = \emptyset)$
35		nfv	$⊢ Ⅎ k C = 0$
36		simpllr	$⊢ ((((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \land k \in A) \land B = \emptyset) \to y = \emptyset$
37		simpr	$⊢ ((((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \land k \in A) \land B = \emptyset) \to B = \emptyset$
38	36 37	eqtr4d	$⊢ ((((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \land k \in A) \land B = \emptyset) \to y = B$
39	38 1	syl	$⊢ ((((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \land k \in A) \land B = \emptyset) \to C = D$
40		simp-4l	$⊢ ((((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \land k \in A) \land B = \emptyset) \to φ$
41		simplr	$⊢ ((((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \land k \in A) \land B = \emptyset) \to k \in A$
42	40 41 37 5	syl21anc	$⊢ ((((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \land k \in A) \land B = \emptyset) \to D = 0$
43	39 42	eqtrd	$⊢ ((((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \land k \in A) \land B = \emptyset) \to C = 0$
44		simplr	$⊢ ((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \to \exists k \in A B = \emptyset$
45	34 35 43 44	r19.29af2	$⊢ ((φ \land \exists k \in A B = \emptyset) \land y = \emptyset) \to C = 0$
46	29 45	syldan	$⊢ ((φ \land \exists k \in A B = \emptyset) \land y \in \{\emptyset\}) \to C = 0$
47		0e0iccpnf	$⊢ 0 \in [0, +∞]$
48	46 47	eqeltrdi	$⊢ ((φ \land \exists k \in A B = \emptyset) \land y \in \{\emptyset\}) \to C \in [0, +∞]$
49		nfcv	$⊢ \underline{Ⅎ} k y$
50		nfmpt1	$⊢ \underline{Ⅎ} k (k \in \{k \in A \| B = \emptyset\} ⟼ B)$
51	50	nfrn	$⊢ \underline{Ⅎ} k ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)$
52	49 51	nfel	$⊢ Ⅎ k y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)$
53	30 52	nfan	$⊢ Ⅎ k (φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B))$
54		simpr	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to y = B$
55		rabid	$⊢ k \in \{k \in A \| B = \emptyset\} \leftrightarrow (k \in A \land B = \emptyset)$
56	55	simprbi	$⊢ k \in \{k \in A \| B = \emptyset\} \to B = \emptyset$
57	56	ad2antlr	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to B = \emptyset$
58	54 57	eqtrd	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to y = \emptyset$
59	58 28	sylibr	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to y \in \{\emptyset\}$
60		vex	$⊢ y \in V$
61		eqid	$⊢ (k \in \{k \in A \| B = \emptyset\} ⟼ B) = (k \in \{k \in A \| B = \emptyset\} ⟼ B)$
62	61	elrnmpt	$⊢ y \in V \to (y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \leftrightarrow \exists k \in \{k \in A \| B = \emptyset\} y = B)$
63	60 62	ax-mp	$⊢ y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \leftrightarrow \exists k \in \{k \in A \| B = \emptyset\} y = B$
64	63	bilani	$⊢ (φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \to \exists k \in \{k \in A \| B = \emptyset\} y = B$
65	53 59 64	r19.29af	$⊢ (φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \to y \in \{\emptyset\}$
66	65	ex	$⊢ φ \to (y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \to y \in \{\emptyset\})$
67	66	ssrdv	$⊢ φ \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \subseteq \{\emptyset\}$
68	67	adantr	$⊢ (φ \land \exists k \in A B = \emptyset) \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \subseteq \{\emptyset\}$
69	25 27 48 68	esummono	$⊢ (φ \land \exists k \in A B = \emptyset) \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \leq \underset{y \in \{\emptyset\}}{\sum^{}} C$
70		0ex	$⊢ \emptyset \in V$
71	70	a1i	$⊢ (φ \land \exists k \in A B = \emptyset) \to \emptyset \in V$
72	47	a1i	$⊢ (φ \land \exists k \in A B = \emptyset) \to 0 \in [0, +∞]$
73	45 71 72	esumsn	$⊢ (φ \land \exists k \in A B = \emptyset) \to \underset{y \in \{\emptyset\}}{\sum^{*}} C = 0$
74	69 73	breqtrd	$⊢ (φ \land \exists k \in A B = \emptyset) \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C \leq 0$
75		simpr	$⊢ (φ \land \neg \exists k \in A B = \emptyset) \to \neg \exists k \in A B = \emptyset$
76		nfv	$⊢ Ⅎ y \neg \exists k \in A B = \emptyset$
77	31	nfn	$⊢ Ⅎ k \neg \exists k \in A B = \emptyset$
78		rabn0	$⊢ \{k \in A \| B = \emptyset\} \neq \emptyset \leftrightarrow \exists k \in A B = \emptyset$
79	78	biimpi	$⊢ \{k \in A \| B = \emptyset\} \neq \emptyset \to \exists k \in A B = \emptyset$
80	79	necon1bi	$⊢ \neg \exists k \in A B = \emptyset \to \{k \in A \| B = \emptyset\} = \emptyset$
81		eqid	$⊢ B = B$
82	81	a1i	$⊢ \neg \exists k \in A B = \emptyset \to B = B$
83	77 80 82	mpteq12df	$⊢ \neg \exists k \in A B = \emptyset \to (k \in \{k \in A \| B = \emptyset\} ⟼ B) = (k \in \emptyset ⟼ B)$
84		mpt0	$⊢ (k \in \emptyset ⟼ B) = \emptyset$
85	83 84	eqtrdi	$⊢ \neg \exists k \in A B = \emptyset \to (k \in \{k \in A \| B = \emptyset\} ⟼ B) = \emptyset$
86	85	rneqd	$⊢ \neg \exists k \in A B = \emptyset \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) = ran \emptyset$
87		rn0	$⊢ ran \emptyset = \emptyset$
88	86 87	eqtrdi	$⊢ \neg \exists k \in A B = \emptyset \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) = \emptyset$
89	76 88	esumeq1d	$⊢ \neg \exists k \in A B = \emptyset \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C = \underset{y \in \emptyset}{\sum^{}} C$
90		esumnul	$⊢ \underset{y \in \emptyset}{\sum^{*}} C = 0$
91	89 90	eqtrdi	$⊢ \neg \exists k \in A B = \emptyset \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C = 0$
92		0le0	$⊢ 0 \leq 0$
93	91 92	eqbrtrdi	$⊢ \neg \exists k \in A B = \emptyset \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C \leq 0$
94	75 93	syl	$⊢ (φ \land \neg \exists k \in A B = \emptyset) \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C \leq 0$
95	74 94	pm2.61dan	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C \leq 0$
96		ssrab2	$⊢ \{k \in A \| B = \emptyset\} \subseteq A$
97	96	a1i	$⊢ φ \to \{k \in A \| B = \emptyset\} \subseteq A$
98	2 97	ssexd	$⊢ φ \to \{k \in A \| B = \emptyset\} \in V$
99		nfrab1	$⊢ \underline{Ⅎ} k \{k \in A \| B = \emptyset\}$
100	99	mptexgf	$⊢ \{k \in A \| B = \emptyset\} \in V \to (k \in \{k \in A \| B = \emptyset\} ⟼ B) \in V$
101		rnexg	$⊢ (k \in \{k \in A \| B = \emptyset\} ⟼ B) \in V \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \in V$
102	98 100 101	3syl	$⊢ φ \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \in V$
103	1	adantl	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to C = D$
104		simplll	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to φ$
105	97	sselda	$⊢ (φ \land k \in \{k \in A \| B = \emptyset\}) \to k \in A$
106	105	adantlr	$⊢ ((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \to k \in A$
107	106	adantr	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to k \in A$
108	104 107 3	syl2anc	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to D \in [0, +∞]$
109	103 108	eqeltrd	$⊢ (((φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| B = \emptyset\}) \land y = B) \to C \in [0, +∞]$
110	53 109 64	r19.29af	$⊢ (φ \land y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)) \to C \in [0, +∞]$
111	110	ralrimiva	$⊢ φ \to \forall y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) C \in [0, +∞]$
112		nfcv	$⊢ \underline{Ⅎ} y ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)$
113	112	esumcl	$⊢ (ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \in V \land \forall y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) C \in [0, +∞]) \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C \in [0, +∞]$
114	102 111 113	syl2anc	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C \in [0, +∞]$
115		elxrge0	$⊢ \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \in [0, +∞] \leftrightarrow (\underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \in ℝ^{} \land 0 \leq \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C)$
116	115	simprbi	$⊢ \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \in [0, +∞] \to 0 \leq \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C$
117	114 116	syl	$⊢ φ \to 0 \leq \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C$
118	95 117	jca	$⊢ φ \to (\underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \leq 0 \land 0 \leq \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C)$
119		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
120	119 114	sselid	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \in ℝ^{}$
121	119 47	sselii	$⊢ 0 \in ℝ^{*}$
122	121	a1i	$⊢ φ \to 0 \in ℝ^{*}$
123		xrletri3	$⊢ (\underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \in ℝ^{} \land 0 \in ℝ^{}) \to (\underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C = 0 \leftrightarrow (\underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \leq 0 \land 0 \leq \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C))$
124	120 122 123	syl2anc	$⊢ φ \to (\underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C = 0 \leftrightarrow (\underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C \leq 0 \land 0 \leq \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C))$
125	118 124	mpbird	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{*}} C = 0$
126	125	oveq1d	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C +_{𝑒} \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C = 0 +_{𝑒} \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{*}} C$
127	12	ralrimiva	$⊢ φ \to \forall k \in \{k \in A \| \neg B = \emptyset\} D \in [0, +∞]$
128	7	esumcl	$⊢ (\{k \in A \| \neg B = \emptyset\} \in V \land \forall k \in \{k \in A \| \neg B = \emptyset\} D \in [0, +∞]) \to \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{*}} D \in [0, +∞]$
129	10 127 128	syl2anc	$⊢ φ \to \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{*}} D \in [0, +∞]$
130	119 129	sselid	$⊢ φ \to \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D \in ℝ^{}$
131	24 130	eqeltrd	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C \in ℝ^{}$
132		xaddlid	$⊢ \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C \in ℝ^{} \to 0 +_{𝑒} \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C = \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C$
133	131 132	syl	$⊢ φ \to 0 +_{𝑒} \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C = \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C$
134	126 133	eqtrd	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C +_{𝑒} \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C = \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{*}} C$
135		simpl	$⊢ (φ \land k \in \{k \in A \| B = \emptyset\}) \to φ$
136	56	adantl	$⊢ (φ \land k \in \{k \in A \| B = \emptyset\}) \to B = \emptyset$
137	135 105 136 5	syl21anc	$⊢ (φ \land k \in \{k \in A \| B = \emptyset\}) \to D = 0$
138	137	ralrimiva	$⊢ φ \to \forall k \in \{k \in A \| B = \emptyset\} D = 0$
139	30 138	esumeq2d	$⊢ φ \to \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{}} D = \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{}} 0$
140	99	esum0	$⊢ \{k \in A \| B = \emptyset\} \in V \to \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{*}} 0 = 0$
141	98 140	syl	$⊢ φ \to \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{*}} 0 = 0$
142	139 141	eqtrd	$⊢ φ \to \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{*}} D = 0$
143	142	oveq1d	$⊢ φ \to \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{}} D +_{𝑒} \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D = 0 +_{𝑒} \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{*}} D$
144		xaddlid	$⊢ \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D \in ℝ^{} \to 0 +_{𝑒} \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D = \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D$
145	130 144	syl	$⊢ φ \to 0 +_{𝑒} \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D = \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D$
146	143 145	eqtrd	$⊢ φ \to \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{}} D +_{𝑒} \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D = \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{*}} D$
147	24 134 146	3eqtr4d	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C +_{𝑒} \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C = \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{}} D +_{𝑒} \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D$
148		nfv	$⊢ Ⅎ y φ$
149		nfcv	$⊢ \underline{Ⅎ} y ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
150	7	mptexgf	$⊢ \{k \in A \| \neg B = \emptyset\} \in V \to (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \in V$
151		rnexg	$⊢ (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \in V \to ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \in V$
152	10 150 151	3syl	$⊢ φ \to ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \in V$
153	67	ssrind	$⊢ φ \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cap ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \subseteq \{\emptyset\} \cap ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
154		incom	$⊢ ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \cap \{\emptyset\} = \{\emptyset\} \cap ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
155	15	neqned	$⊢ k \in \{k \in A \| \neg B = \emptyset\} \to B \neq \emptyset$
156	155	necomd	$⊢ k \in \{k \in A \| \neg B = \emptyset\} \to \emptyset \neq B$
157	156	neneqd	$⊢ k \in \{k \in A \| \neg B = \emptyset\} \to \neg \emptyset = B$
158	157	nrex	$⊢ \neg \exists k \in \{k \in A \| \neg B = \emptyset\} \emptyset = B$
159		eqid	$⊢ (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) = (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
160	159	elrnmpt	$⊢ \emptyset \in V \to (\emptyset \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \leftrightarrow \exists k \in \{k \in A \| \neg B = \emptyset\} \emptyset = B)$
161	70 160	ax-mp	$⊢ \emptyset \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \leftrightarrow \exists k \in \{k \in A \| \neg B = \emptyset\} \emptyset = B$
162	158 161	mtbir	$⊢ \neg \emptyset \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
163		disjsn	$⊢ ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \cap \{\emptyset\} = \emptyset \leftrightarrow \neg \emptyset \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
164	162 163	mpbir	$⊢ ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \cap \{\emptyset\} = \emptyset$
165	154 164	eqtr3i	$⊢ \{\emptyset\} \cap ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) = \emptyset$
166	153 165	sseqtrdi	$⊢ φ \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cap ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \subseteq \emptyset$
167		ss0	$⊢ ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cap ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \subseteq \emptyset \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cap ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) = \emptyset$
168	166 167	syl	$⊢ φ \to ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cap ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) = \emptyset$
169		nfmpt1	$⊢ \underline{Ⅎ} k (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
170	169	nfrn	$⊢ \underline{Ⅎ} k ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
171	49 170	nfel	$⊢ Ⅎ k y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
172	30 171	nfan	$⊢ Ⅎ k (φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B))$
173	1	adantl	$⊢ (((φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| \neg B = \emptyset\}) \land y = B) \to C = D$
174		simplll	$⊢ (((φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| \neg B = \emptyset\}) \land y = B) \to φ$
175	11	adantlr	$⊢ ((φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| \neg B = \emptyset\}) \to k \in A$
176	175	adantr	$⊢ (((φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| \neg B = \emptyset\}) \land y = B) \to k \in A$
177	174 176 3	syl2anc	$⊢ (((φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| \neg B = \emptyset\}) \land y = B) \to D \in [0, +∞]$
178	173 177	eqeltrd	$⊢ (((φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) \land k \in \{k \in A \| \neg B = \emptyset\}) \land y = B) \to C \in [0, +∞]$
179	159	elrnmpt	$⊢ y \in V \to (y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \leftrightarrow \exists k \in \{k \in A \| \neg B = \emptyset\} y = B)$
180	60 179	ax-mp	$⊢ y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B) \leftrightarrow \exists k \in \{k \in A \| \neg B = \emptyset\} y = B$
181	180	bilani	$⊢ (φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) \to \exists k \in \{k \in A \| \neg B = \emptyset\} y = B$
182	172 178 181	r19.29af	$⊢ (φ \land y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) \to C \in [0, +∞]$
183	148 112 149 102 152 168 110 182	esumsplit	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C = \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B)}{\sum^{}} C +_{𝑒} \underset{y \in ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{*}} C$
184		rabnc	$⊢ \{k \in A \| B = \emptyset\} \cap \{k \in A \| \neg B = \emptyset\} = \emptyset$
185	184	a1i	$⊢ φ \to \{k \in A \| B = \emptyset\} \cap \{k \in A \| \neg B = \emptyset\} = \emptyset$
186	105 3	syldan	$⊢ (φ \land k \in \{k \in A \| B = \emptyset\}) \to D \in [0, +∞]$
187	30 99 7 98 10 185 186 12	esumsplit	$⊢ φ \to \underset{k \in \{k \in A \| B = \emptyset\} \cup \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D = \underset{k \in \{k \in A \| B = \emptyset\}}{\sum^{}} D +_{𝑒} \underset{k \in \{k \in A \| \neg B = \emptyset\}}{\sum^{*}} D$
188	147 183 187	3eqtr4d	$⊢ φ \to \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C = \underset{k \in \{k \in A \| B = \emptyset\} \cup \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D$
189		rabxm	$⊢ A = \{k \in A \| B = \emptyset\} \cup \{k \in A \| \neg B = \emptyset\}$
190	189 81	mpteq12i	$⊢ (k \in A ⟼ B) = (k \in (\{k \in A \| B = \emptyset\} \cup \{k \in A \| \neg B = \emptyset\}) ⟼ B)$
191		mptun	$⊢ (k \in (\{k \in A \| B = \emptyset\} \cup \{k \in A \| \neg B = \emptyset\}) ⟼ B) = (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
192	190 191	eqtri	$⊢ (k \in A ⟼ B) = (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
193	192	rneqi	$⊢ ran (k \in A ⟼ B) = ran ((k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B))$
194		rnun	$⊢ ran ((k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)) = ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
195	193 194	eqtri	$⊢ ran (k \in A ⟼ B) = ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
196	195	a1i	$⊢ φ \to ran (k \in A ⟼ B) = ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)$
197	148 196	esumeq1d	$⊢ φ \to \underset{y \in ran (k \in A ⟼ B)}{\sum^{}} C = \underset{y \in ran (k \in \{k \in A \| B = \emptyset\} ⟼ B) \cup ran (k \in \{k \in A \| \neg B = \emptyset\} ⟼ B)}{\sum^{}} C$
198	189	a1i	$⊢ φ \to A = \{k \in A \| B = \emptyset\} \cup \{k \in A \| \neg B = \emptyset\}$
199	30 198	esumeq1d	$⊢ φ \to \underset{k \in A}{\sum^{}} D = \underset{k \in \{k \in A \| B = \emptyset\} \cup \{k \in A \| \neg B = \emptyset\}}{\sum^{}} D$
200	188 197 199	3eqtr4d	$⊢ φ \to \underset{y \in ran (k \in A ⟼ B)}{\sum^{}} C = \underset{k \in A}{\sum^{}} D$

Metamath Proof Explorer

Theorem esumrnmpt2

Proof