This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 nfcv ⊢ Ⅎ 𝑥 𝐶
96 8 95 nfsum ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶
97 nfcv ⊢ Ⅎ 𝑦 Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶
98 94 96 97 cbvsum ⊢ Σ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶
99 98 a1i ⊢ ( 𝜑 → Σ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶 )
100 92 99 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶 )
101 13 51 100 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐷 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐷 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝐷 ) 𝐶 )