fsumiunss

Description: Sum over a disjoint indexed union, intersected with a finite set D . Similar to fsumiun , but here A and B need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	fsumiunss.b	$⊢ (φ \land x \in A) \to B \in V$
	fsumiunss.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
	fsumiunss.c	$⊢ (φ \land x \in A \land k \in B) \to C \in ℂ$
	fsumiunss.fi	$⊢ φ \to D \in Fin$
Assertion	fsumiunss	$⊢ φ \to \sum_{k \in ⋃_{x \in A} (B \cap D)} C = \sum_{x \in \{x \in A \| B \cap D \neq \emptyset\}} \sum_{k \in B \cap D} C$

Proof

Step	Hyp	Ref	Expression
1		fsumiunss.b	$⊢ (φ \land x \in A) \to B \in V$
2		fsumiunss.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
3		fsumiunss.c	$⊢ (φ \land x \in A \land k \in B) \to C \in ℂ$
4		fsumiunss.fi	$⊢ φ \to D \in Fin$
5		nfcv	$⊢ \underline{Ⅎ} y (B \cap D)$
6		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
7		nfcv	$⊢ \underline{Ⅎ} x D$
8	6 7	nfin	$⊢ \underline{Ⅎ} x (⦋ y / x ⦌ B \cap D)$
9		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
10	9	ineq1d	$⊢ x = y \to B \cap D = ⦋ y / x ⦌ B \cap D$
11	5 8 10	cbviun	$⊢ ⋃_{x \in A} (B \cap D) = ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)$
12	11	sumeq1i	$⊢ \sum_{k \in ⋃_{x \in A} (B \cap D)} C = \sum_{k \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)} C$
13	12	a1i	$⊢ φ \to \sum_{k \in ⋃_{x \in A} (B \cap D)} C = \sum_{k \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)} C$
14		eliun	$⊢ z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \leftrightarrow \exists y \in A z \in (⦋ y / x ⦌ B \cap D)$
15	14	biimpi	$⊢ z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \to \exists y \in A z \in (⦋ y / x ⦌ B \cap D)$
16		df-rex	$⊢ \exists y \in A z \in (⦋ y / x ⦌ B \cap D) \leftrightarrow \exists y (y \in A \land z \in (⦋ y / x ⦌ B \cap D))$
17	15 16	sylib	$⊢ z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \to \exists y (y \in A \land z \in (⦋ y / x ⦌ B \cap D))$
18		nfcv	$⊢ \underline{Ⅎ} y z$
19		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)$
20	18 19	nfel	$⊢ Ⅎ y z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)$
21		simpl	$⊢ (y \in A \land z \in (⦋ y / x ⦌ B \cap D)) \to y \in A$
22		ne0i	$⊢ z \in (⦋ y / x ⦌ B \cap D) \to ⦋ y / x ⦌ B \cap D \neq \emptyset$
23	22	adantl	$⊢ (y \in A \land z \in (⦋ y / x ⦌ B \cap D)) \to ⦋ y / x ⦌ B \cap D \neq \emptyset$
24	21 23	jca	$⊢ (y \in A \land z \in (⦋ y / x ⦌ B \cap D)) \to (y \in A \land ⦋ y / x ⦌ B \cap D \neq \emptyset)$
25		nfcv	$⊢ \underline{Ⅎ} x y$
26		nfv	$⊢ Ⅎ x y \in A$
27	26	nfci	$⊢ \underline{Ⅎ} x A$
28		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
29	8 28	nfne	$⊢ Ⅎ x ⦋ y / x ⦌ B \cap D \neq \emptyset$
30	10	neeq1d	$⊢ x = y \to (B \cap D \neq \emptyset \leftrightarrow ⦋ y / x ⦌ B \cap D \neq \emptyset)$
31	25 27 29 30	elrabf	$⊢ y \in \{x \in A \| B \cap D \neq \emptyset\} \leftrightarrow (y \in A \land ⦋ y / x ⦌ B \cap D \neq \emptyset)$
32	24 31	sylibr	$⊢ (y \in A \land z \in (⦋ y / x ⦌ B \cap D)) \to y \in \{x \in A \| B \cap D \neq \emptyset\}$
33		simpr	$⊢ (y \in A \land z \in (⦋ y / x ⦌ B \cap D)) \to z \in (⦋ y / x ⦌ B \cap D)$
34	32 33	jca	$⊢ (y \in A \land z \in (⦋ y / x ⦌ B \cap D)) \to (y \in \{x \in A \| B \cap D \neq \emptyset\} \land z \in (⦋ y / x ⦌ B \cap D))$
35	34	a1i	$⊢ z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \to ((y \in A \land z \in (⦋ y / x ⦌ B \cap D)) \to (y \in \{x \in A \| B \cap D \neq \emptyset\} \land z \in (⦋ y / x ⦌ B \cap D)))$
36	20 35	eximd	$⊢ z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \to (\exists y (y \in A \land z \in (⦋ y / x ⦌ B \cap D)) \to \exists y (y \in \{x \in A \| B \cap D \neq \emptyset\} \land z \in (⦋ y / x ⦌ B \cap D)))$
37	17 36	mpd	$⊢ z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \to \exists y (y \in \{x \in A \| B \cap D \neq \emptyset\} \land z \in (⦋ y / x ⦌ B \cap D))$
38		df-rex	$⊢ \exists y \in \{x \in A \| B \cap D \neq \emptyset\} z \in (⦋ y / x ⦌ B \cap D) \leftrightarrow \exists y (y \in \{x \in A \| B \cap D \neq \emptyset\} \land z \in (⦋ y / x ⦌ B \cap D))$
39	37 38	sylibr	$⊢ z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \to \exists y \in \{x \in A \| B \cap D \neq \emptyset\} z \in (⦋ y / x ⦌ B \cap D)$
40		eliun	$⊢ z \in ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D) \leftrightarrow \exists y \in \{x \in A \| B \cap D \neq \emptyset\} z \in (⦋ y / x ⦌ B \cap D)$
41	39 40	sylibr	$⊢ z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \to z \in ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)$
42	41	rgen	$⊢ \forall z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) z \in ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)$
43		dfss3	$⊢ ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \subseteq ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D) \leftrightarrow \forall z \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) z \in ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)$
44	42 43	mpbir	$⊢ ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) \subseteq ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)$
45		elrabi	$⊢ y \in \{x \in A \| B \cap D \neq \emptyset\} \to y \in A$
46	45	ssriv	$⊢ \{x \in A \| B \cap D \neq \emptyset\} \subseteq A$
47		iunss1	$⊢ \{x \in A \| B \cap D \neq \emptyset\} \subseteq A \to ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D) \subseteq ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)$
48	46 47	ax-mp	$⊢ ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D) \subseteq ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)$
49	44 48	eqssi	$⊢ ⋃_{y \in A} (⦋ y / x ⦌ B \cap D) = ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)$
50	49	sumeq1i	$⊢ \sum_{k \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)} C = \sum_{k \in ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)} C$
51	50	a1i	$⊢ φ \to \sum_{k \in ⋃_{y \in A} (⦋ y / x ⦌ B \cap D)} C = \sum_{k \in ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)} C$
52	1 2 4	disjinfi	$⊢ φ \to \{x \in A \| B \cap D \neq \emptyset\} \in Fin$
53		inss2	$⊢ ⦋ y / x ⦌ B \cap D \subseteq D$
54	53	a1i	$⊢ φ \to ⦋ y / x ⦌ B \cap D \subseteq D$
55		ssfi	$⊢ (D \in Fin \land ⦋ y / x ⦌ B \cap D \subseteq D) \to ⦋ y / x ⦌ B \cap D \in Fin$
56	4 54 55	syl2anc	$⊢ φ \to ⦋ y / x ⦌ B \cap D \in Fin$
57	56	adantr	$⊢ (φ \land y \in \{x \in A \| B \cap D \neq \emptyset\}) \to ⦋ y / x ⦌ B \cap D \in Fin$
58	46	a1i	$⊢ φ \to \{x \in A \| B \cap D \neq \emptyset\} \subseteq A$
59		inss1	$⊢ ⦋ y / x ⦌ B \cap D \subseteq ⦋ y / x ⦌ B$
60	59	rgenw	$⊢ \forall y \in A ⦋ y / x ⦌ B \cap D \subseteq ⦋ y / x ⦌ B$
61	60	a1i	$⊢ φ \to \forall y \in A ⦋ y / x ⦌ B \cap D \subseteq ⦋ y / x ⦌ B$
62		nfcv	$⊢ \underline{Ⅎ} y B$
63		eqcom	$⊢ x = y \leftrightarrow y = x$
64	63	imbi1i	$⊢ (x = y \to B = ⦋ y / x ⦌ B) \leftrightarrow (y = x \to B = ⦋ y / x ⦌ B)$
65		eqcom	$⊢ B = ⦋ y / x ⦌ B \leftrightarrow ⦋ y / x ⦌ B = B$
66	65	imbi2i	$⊢ (y = x \to B = ⦋ y / x ⦌ B) \leftrightarrow (y = x \to ⦋ y / x ⦌ B = B)$
67	64 66	bitri	$⊢ (x = y \to B = ⦋ y / x ⦌ B) \leftrightarrow (y = x \to ⦋ y / x ⦌ B = B)$
68	9 67	mpbi	$⊢ y = x \to ⦋ y / x ⦌ B = B$
69	6 62 68	cbvdisj	$⊢ \underset{y \in A}{Disj} ⦋ y / x ⦌ B \leftrightarrow \underset{x \in A}{Disj} B$
70	2 69	sylibr	$⊢ φ \to \underset{y \in A}{Disj} ⦋ y / x ⦌ B$
71		disjss2	$⊢ \forall y \in A ⦋ y / x ⦌ B \cap D \subseteq ⦋ y / x ⦌ B \to (\underset{y \in A}{Disj} ⦋ y / x ⦌ B \to \underset{y \in A}{Disj} (⦋ y / x ⦌ B \cap D))$
72	61 70 71	sylc	$⊢ φ \to \underset{y \in A}{Disj} (⦋ y / x ⦌ B \cap D)$
73		disjss1	$⊢ \{x \in A \| B \cap D \neq \emptyset\} \subseteq A \to (\underset{y \in A}{Disj} (⦋ y / x ⦌ B \cap D) \to \underset{y \in \{x \in A \| B \cap D \neq \emptyset\}}{Disj} (⦋ y / x ⦌ B \cap D))$
74	58 72 73	sylc	$⊢ φ \to \underset{y \in \{x \in A \| B \cap D \neq \emptyset\}}{Disj} (⦋ y / x ⦌ B \cap D)$
75		simpl	$⊢ (φ \land (y \in \{x \in A \| B \cap D \neq \emptyset\} \land k \in (⦋ y / x ⦌ B \cap D))) \to φ$
76	45	ad2antrl	$⊢ (φ \land (y \in \{x \in A \| B \cap D \neq \emptyset\} \land k \in (⦋ y / x ⦌ B \cap D))) \to y \in A$
77	59	sseli	$⊢ k \in (⦋ y / x ⦌ B \cap D) \to k \in ⦋ y / x ⦌ B$
78	77	adantl	$⊢ (y \in \{x \in A \| B \cap D \neq \emptyset\} \land k \in (⦋ y / x ⦌ B \cap D)) \to k \in ⦋ y / x ⦌ B$
79	78	adantl	$⊢ (φ \land (y \in \{x \in A \| B \cap D \neq \emptyset\} \land k \in (⦋ y / x ⦌ B \cap D))) \to k \in ⦋ y / x ⦌ B$
80		nfv	$⊢ Ⅎ x φ$
81		nfcv	$⊢ \underline{Ⅎ} x k$
82	81 6	nfel	$⊢ Ⅎ x k \in ⦋ y / x ⦌ B$
83	80 26 82	nf3an	$⊢ Ⅎ x (φ \land y \in A \land k \in ⦋ y / x ⦌ B)$
84		nfv	$⊢ Ⅎ x C \in ℂ$
85	83 84	nfim	$⊢ Ⅎ x ((φ \land y \in A \land k \in ⦋ y / x ⦌ B) \to C \in ℂ)$
86		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
87	9	eleq2d	$⊢ x = y \to (k \in B \leftrightarrow k \in ⦋ y / x ⦌ B)$
88	86 87	3anbi23d	$⊢ x = y \to ((φ \land x \in A \land k \in B) \leftrightarrow (φ \land y \in A \land k \in ⦋ y / x ⦌ B))$
89	88	imbi1d	$⊢ x = y \to (((φ \land x \in A \land k \in B) \to C \in ℂ) \leftrightarrow ((φ \land y \in A \land k \in ⦋ y / x ⦌ B) \to C \in ℂ))$
90	85 89 3	chvarfv	$⊢ (φ \land y \in A \land k \in ⦋ y / x ⦌ B) \to C \in ℂ$
91	75 76 79 90	syl3anc	$⊢ (φ \land (y \in \{x \in A \| B \cap D \neq \emptyset\} \land k \in (⦋ y / x ⦌ B \cap D))) \to C \in ℂ$
92	52 57 74 91	fsumiun	$⊢ φ \to \sum_{k \in ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)} C = \sum_{y \in \{x \in A \| B \cap D \neq \emptyset\}} \sum_{k \in ⦋ y / x ⦌ B \cap D} C$
93	68	ineq1d	$⊢ y = x \to ⦋ y / x ⦌ B \cap D = B \cap D$
94	93	sumeq1d	$⊢ y = x \to \sum_{k \in ⦋ y / x ⦌ B \cap D} C = \sum_{k \in B \cap D} C$
95		nfcv	$⊢ \underline{Ⅎ} x C$
96	8 95	nfsum	$⊢ \underline{Ⅎ} x \sum_{k \in ⦋ y / x ⦌ B \cap D} C$
97		nfcv	$⊢ \underline{Ⅎ} y \sum_{k \in B \cap D} C$
98	94 96 97	cbvsum	$⊢ \sum_{y \in \{x \in A \| B \cap D \neq \emptyset\}} \sum_{k \in ⦋ y / x ⦌ B \cap D} C = \sum_{x \in \{x \in A \| B \cap D \neq \emptyset\}} \sum_{k \in B \cap D} C$
99	98	a1i	$⊢ φ \to \sum_{y \in \{x \in A \| B \cap D \neq \emptyset\}} \sum_{k \in ⦋ y / x ⦌ B \cap D} C = \sum_{x \in \{x \in A \| B \cap D \neq \emptyset\}} \sum_{k \in B \cap D} C$
100	92 99	eqtrd	$⊢ φ \to \sum_{k \in ⋃_{y \in \{x \in A \| B \cap D \neq \emptyset\}} (⦋ y / x ⦌ B \cap D)} C = \sum_{x \in \{x \in A \| B \cap D \neq \emptyset\}} \sum_{k \in B \cap D} C$
101	13 51 100	3eqtrd	$⊢ φ \to \sum_{k \in ⋃_{x \in A} (B \cap D)} C = \sum_{x \in \{x \in A \| B \cap D \neq \emptyset\}} \sum_{k \in B \cap D} C$

Metamath Proof Explorer

Theorem fsumiunss

Proof