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 
|- ( ( ph /\ x e. A ) -> B e. V )
fsumiunss.dj 
|- ( ph -> Disj_ x e. A B )
fsumiunss.c 
|- ( ( ph /\ x e. A /\ k e. B ) -> C e. CC )
fsumiunss.fi 
|- ( ph -> D e. Fin )
Assertion fsumiunss 
|- ( ph -> sum_ k e. U_ x e. A ( B i^i D ) C = sum_ x e. { x e. A | ( B i^i D ) =/= (/) } sum_ k e. ( B i^i D ) C )

Proof

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