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

Metamath Proof Explorer

Theorem esumrnmpt2

Proof