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 φxABV
fsumiunss.dj φDisjxAB
fsumiunss.c φxAkBC
fsumiunss.fi φDFin
Assertion fsumiunss φkxABDC=xxA|BDkBDC

Proof

Step Hyp Ref Expression
1 fsumiunss.b φxABV
2 fsumiunss.dj φDisjxAB
3 fsumiunss.c φxAkBC
4 fsumiunss.fi φDFin
5 nfcv _yBD
6 nfcsb1v _xy/xB
7 nfcv _xD
8 6 7 nfin _xy/xBD
9 csbeq1a x=yB=y/xB
10 9 ineq1d x=yBD=y/xBD
11 5 8 10 cbviun xABD=yAy/xBD
12 11 sumeq1i kxABDC=kyAy/xBDC
13 12 a1i φkxABDC=kyAy/xBDC
14 eliun zyAy/xBDyAzy/xBD
15 14 biimpi zyAy/xBDyAzy/xBD
16 df-rex yAzy/xBDyyAzy/xBD
17 15 16 sylib zyAy/xBDyyAzy/xBD
18 nfcv _yz
19 nfiu1 _yyAy/xBD
20 18 19 nfel yzyAy/xBD
21 simpl yAzy/xBDyA
22 ne0i zy/xBDy/xBD
23 22 adantl yAzy/xBDy/xBD
24 21 23 jca yAzy/xBDyAy/xBD
25 nfcv _xy
26 nfv xyA
27 26 nfci _xA
28 nfcv _x
29 8 28 nfne xy/xBD
30 10 neeq1d x=yBDy/xBD
31 25 27 29 30 elrabf yxA|BDyAy/xBD
32 24 31 sylibr yAzy/xBDyxA|BD
33 simpr yAzy/xBDzy/xBD
34 32 33 jca yAzy/xBDyxA|BDzy/xBD
35 34 a1i zyAy/xBDyAzy/xBDyxA|BDzy/xBD
36 20 35 eximd zyAy/xBDyyAzy/xBDyyxA|BDzy/xBD
37 17 36 mpd zyAy/xBDyyxA|BDzy/xBD
38 df-rex yxA|BDzy/xBDyyxA|BDzy/xBD
39 37 38 sylibr zyAy/xBDyxA|BDzy/xBD
40 eliun zyxA|BDy/xBDyxA|BDzy/xBD
41 39 40 sylibr zyAy/xBDzyxA|BDy/xBD
42 41 rgen zyAy/xBDzyxA|BDy/xBD
43 dfss3 yAy/xBDyxA|BDy/xBDzyAy/xBDzyxA|BDy/xBD
44 42 43 mpbir yAy/xBDyxA|BDy/xBD
45 elrabi yxA|BDyA
46 45 ssriv xA|BDA
47 iunss1 xA|BDAyxA|BDy/xBDyAy/xBD
48 46 47 ax-mp yxA|BDy/xBDyAy/xBD
49 44 48 eqssi yAy/xBD=yxA|BDy/xBD
50 49 sumeq1i kyAy/xBDC=kyxA|BDy/xBDC
51 50 a1i φkyAy/xBDC=kyxA|BDy/xBDC
52 1 2 4 disjinfi φxA|BDFin
53 inss2 y/xBDD
54 53 a1i φy/xBDD
55 ssfi DFiny/xBDDy/xBDFin
56 4 54 55 syl2anc φy/xBDFin
57 56 adantr φyxA|BDy/xBDFin
58 46 a1i φxA|BDA
59 inss1 y/xBDy/xB
60 59 rgenw yAy/xBDy/xB
61 60 a1i φyAy/xBDy/xB
62 nfcv _yB
63 eqcom x=yy=x
64 63 imbi1i x=yB=y/xBy=xB=y/xB
65 eqcom B=y/xBy/xB=B
66 65 imbi2i y=xB=y/xBy=xy/xB=B
67 64 66 bitri x=yB=y/xBy=xy/xB=B
68 9 67 mpbi y=xy/xB=B
69 6 62 68 cbvdisj DisjyAy/xBDisjxAB
70 2 69 sylibr φDisjyAy/xB
71 disjss2 yAy/xBDy/xBDisjyAy/xBDisjyAy/xBD
72 61 70 71 sylc φDisjyAy/xBD
73 disjss1 xA|BDADisjyAy/xBDDisjyxA|BDy/xBD
74 58 72 73 sylc φDisjyxA|BDy/xBD
75 simpl φyxA|BDky/xBDφ
76 45 ad2antrl φyxA|BDky/xBDyA
77 59 sseli ky/xBDky/xB
78 77 adantl yxA|BDky/xBDky/xB
79 78 adantl φyxA|BDky/xBDky/xB
80 nfv xφ
81 nfcv _xk
82 81 6 nfel xky/xB
83 80 26 82 nf3an xφyAky/xB
84 nfv xC
85 83 84 nfim xφyAky/xBC
86 eleq1w x=yxAyA
87 9 eleq2d x=ykBky/xB
88 86 87 3anbi23d x=yφxAkBφyAky/xB
89 88 imbi1d x=yφxAkBCφyAky/xBC
90 85 89 3 chvarfv φyAky/xBC
91 75 76 79 90 syl3anc φyxA|BDky/xBDC
92 52 57 74 91 fsumiun φkyxA|BDy/xBDC=yxA|BDky/xBDC
93 68 ineq1d y=xy/xBD=BD
94 93 sumeq1d y=xky/xBDC=kBDC
95 nfrab1 _xxA|BD
96 nfcv _yxA|BD
97 nfcv _xC
98 8 97 nfsum _xky/xBDC
99 nfcv _ykBDC
100 94 95 96 98 99 cbvsum yxA|BDky/xBDC=xxA|BDkBDC
101 100 a1i φyxA|BDky/xBDC=xxA|BDkBDC
102 92 101 eqtrd φkyxA|BDy/xBDC=xxA|BDkBDC
103 13 51 102 3eqtrd φkxABDC=xxA|BDkBDC