Theorem 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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	fsumiunss.dj	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
	fsumiunss.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
	fsumiunss.fi	⊢ ( 𝜑 → 𝐷 ∈ Fin )
Assertion	fsumiunss	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fsumiunss.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		fsumiunss.dj	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
3		fsumiunss.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
4		fsumiunss.fi	⊢ ( 𝜑 → 𝐷 ∈ Fin )
5		nfcv	⊢ Ⅎ 𝑦 ( 𝐵 ∩ 𝐷 )
6		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
7		nfcv	⊢ Ⅎ 𝑥 𝐷
8	6 7	nfin	⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 )
9		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10	9	ineq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∩ 𝐷 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
11	5 8 10	cbviun	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐷 ) = ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 )
12	11	sumeq1i	⊢ Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑘 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶
13	12	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑘 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 )
14		eliun	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
15	14	biimpi	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → ∃ 𝑦 ∈ 𝐴 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
16		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) )
17	15 16	sylib	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) )
18		nfcv	⊢ Ⅎ 𝑦 𝑧
19		nfiu1	⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 )
20	18 19	nfel	⊢ Ⅎ 𝑦 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 )
21		simpl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → 𝑦 ∈ 𝐴 )
22		ne0i	⊢ ( 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ≠ ∅ )
23	22	adantl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ≠ ∅ )
24	21 23	jca	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → ( 𝑦 ∈ 𝐴 ∧ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
25		nfcv	⊢ Ⅎ 𝑥 𝑦
26		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
27	26	nfci	⊢ Ⅎ 𝑥 𝐴
28		nfcv	⊢ Ⅎ 𝑥 ∅
29	8 28	nfne	⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ≠ ∅
30	10	neeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 ∩ 𝐷 ) ≠ ∅ ↔ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
31	25 27 29 30	elrabf	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ↔ ( 𝑦 ∈ 𝐴 ∧ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
32	24 31	sylibr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } )
33		simpr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
34	32 33	jca	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) )
35	34	a1i	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) ) )
36	20 35	eximd	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → ∃ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) ) )
37	17 36	mpd	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → ∃ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) )
38		df-rex	⊢ ( ∃ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ↔ ∃ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) )
39	37 38	sylibr	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → ∃ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
40		eliun	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ↔ ∃ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } 𝑧 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
41	39 40	sylibr	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → 𝑧 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
42	41	rgen	⊢ ∀ 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝑧 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 )
43		dfss3	⊢ ( ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ↔ ∀ 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝑧 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
44	42 43	mpbir	⊢ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 )
45		elrabi	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } → 𝑦 ∈ 𝐴 )
46	45	ssriv	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ⊆ 𝐴
47		iunss1	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ⊆ 𝐴 → ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
48	46 47	ax-mp	⊢ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 )
49	44 48	eqssi	⊢ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) = ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 )
50	49	sumeq1i	⊢ Σ 𝑘 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑘 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶
51	50	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑘 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 )
52	1 2 4	disjinfi	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∈ Fin )
53		inss2	⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ 𝐷
54	53	a1i	⊢ ( 𝜑 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ 𝐷 )
55		ssfi	⊢ ( ( 𝐷 ∈ Fin ∧ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ 𝐷 ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ∈ Fin )
56	4 54 55	syl2anc	⊢ ( 𝜑 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ∈ Fin )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ∈ Fin )
58	46	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ⊆ 𝐴 )
59		inss1	⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
60	59	rgenw	⊢ ∀ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
61	60	a1i	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
62		nfcv	⊢ Ⅎ 𝑦 𝐵
63		eqcom	⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
64	63	imbi1i	⊢ ( ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
65		eqcom	⊢ ( 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
66	65	imbi2i	⊢ ( ( 𝑦 = 𝑥 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
67	64 66	bitri	⊢ ( ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
68	9 67	mpbi	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
69	6 62 68	cbvdisj	⊢ ( Disj 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐵 )
70	2 69	sylibr	⊢ ( 𝜑 → Disj 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
71		disjss2	⊢ ( ∀ 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ⊆ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 → ( Disj 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 → Disj 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) )
72	61 70 71	sylc	⊢ ( 𝜑 → Disj 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
73		disjss1	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ⊆ 𝐴 → ( Disj 𝑦 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → Disj 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) )
74	58 72 73	sylc	⊢ ( 𝜑 → Disj 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) )
75		simpl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) ) → 𝜑 )
76	45	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) ) → 𝑦 ∈ 𝐴 )
77	59	sseli	⊢ ( 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) → 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
78	77	adantl	⊢ ( ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) → 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
79	78	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) ) → 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
80		nfv	⊢ Ⅎ 𝑥 𝜑
81		nfcv	⊢ Ⅎ 𝑥 𝑘
82	81 6	nfel	⊢ Ⅎ 𝑥 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
83	80 26 82	nf3an	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
84		nfv	⊢ Ⅎ 𝑥 𝐶 ∈ ℂ
85	83 84	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ℂ )
86		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
87	9	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
88	86 87	3anbi23d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
89	88	imbi1d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ℂ ) ) )
90	85 89 3	chvarfv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ℂ )
91	75 76 79 90	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ∧ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) ) ) → 𝐶 ∈ ℂ )
92	52 57 74 91	fsumiun	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 )
93	68	ineq1d	⊢ ( 𝑦 = 𝑥 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) = ( 𝐵 ∩ 𝐷 ) )
94	93	sumeq1d	⊢ ( 𝑦 = 𝑥 → Σ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶 )
95		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ }
96		nfcv	⊢ Ⅎ 𝑦 { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ }
97		nfcv	⊢ Ⅎ 𝑥 𝐶
98	8 97	nfsum	⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶
99		nfcv	⊢ Ⅎ 𝑦 Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶
100	94 95 96 98 99	cbvsum	⊢ Σ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶
101	100	a1i	⊢ ( 𝜑 → Σ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶 )
102	92 101	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶 )
103	13 51 102	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶 )