Metamath Proof Explorer

Theorem esumrnmpt2

Description: Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020)

Ref Expression
Hypotheses esumrnmpt2.1 
|- ( y = B -> C = D )
esumrnmpt2.2 
|- ( ph -> A e. V )
esumrnmpt2.3 
|- ( ( ph /\ k e. A ) -> D e. ( 0 [,] +oo ) )
esumrnmpt2.4 
|- ( ( ph /\ k e. A ) -> B e. W )
esumrnmpt2.5 
|- ( ( ( ph /\ k e. A ) /\ B = (/) ) -> D = 0 )
esumrnmpt2.6 
|- ( ph -> Disj_ k e. A B )
Assertion esumrnmpt2 
|- ( ph -> sum* y e. ran ( k e. A |-> B ) C = sum* k e. A D )

Proof

Step Hyp Ref Expression
1 esumrnmpt2.1 
 |-  ( y = B -> C = D )
2 esumrnmpt2.2 
 |-  ( ph -> A e. V )
3 esumrnmpt2.3 
 |-  ( ( ph /\ k e. A ) -> D e. ( 0 [,] +oo ) )
4 esumrnmpt2.4 
 |-  ( ( ph /\ k e. A ) -> B e. W )
5 esumrnmpt2.5 
 |-  ( ( ( ph /\ k e. A ) /\ B = (/) ) -> D = 0 )
6 esumrnmpt2.6 
 |-  ( ph -> Disj_ k e. A B )
7 nfrab1 
 |-  F/_ k { k e. A | -. B = (/) }
8 ssrab2 
 |-  { k e. A | -. B = (/) } C_ A
9 8 a1i 
 |-  ( ph -> { k e. A | -. B = (/) } C_ A )
10 2 9 ssexd 
 |-  ( ph -> { k e. A | -. B = (/) } e. _V )
11 9 sselda 
 |-  ( ( ph /\ k e. { k e. A | -. B = (/) } ) -> k e. A )
12 11 3 syldan 
 |-  ( ( ph /\ k e. { k e. A | -. B = (/) } ) -> D e. ( 0 [,] +oo ) )
13 11 4 syldan 
 |-  ( ( ph /\ k e. { k e. A | -. B = (/) } ) -> B e. W )
14 rabid 
 |-  ( k e. { k e. A | -. B = (/) } <-> ( k e. A /\ -. B = (/) ) )
15 14 simprbi 
 |-  ( k e. { k e. A | -. B = (/) } -> -. B = (/) )
16 15 adantl 
 |-  ( ( ph /\ k e. { k e. A | -. B = (/) } ) -> -. B = (/) )
17 elsng 
 |-  ( B e. W -> ( B e. { (/) } <-> B = (/) ) )
18 13 17 syl 
 |-  ( ( ph /\ k e. { k e. A | -. B = (/) } ) -> ( B e. { (/) } <-> B = (/) ) )
19 16 18 mtbird 
 |-  ( ( ph /\ k e. { k e. A | -. B = (/) } ) -> -. B e. { (/) } )
20 13 19 eldifd 
 |-  ( ( ph /\ k e. { k e. A | -. B = (/) } ) -> B e. ( W \ { (/) } ) )
21 nfcv 
 |-  F/_ k A
22 7 21 disjss1f 
 |-  ( { k e. A | -. B = (/) } C_ A -> ( Disj_ k e. A B -> Disj_ k e. { k e. A | -. B = (/) } B ) )
23 9 6 22 sylc 
 |-  ( ph -> Disj_ k e. { k e. A | -. B = (/) } B )
24 7 1 10 12 20 23 esumrnmpt 
 |-  ( ph -> sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C = sum* k e. { k e. A | -. B = (/) } D )
25 nfv 
 |-  F/ y ( ph /\ E. k e. A B = (/) )
26 snex 
 |-  { (/) } e. _V
27 26 a1i 
 |-  ( ( ph /\ E. k e. A B = (/) ) -> { (/) } e. _V )
28 velsn 
 |-  ( y e. { (/) } <-> y = (/) )
29 28 bilani 
 |-  ( ( ( ph /\ E. k e. A B = (/) ) /\ y e. { (/) } ) -> y = (/) )
30 nfv 
 |-  F/ k ph
31 nfre1 
 |-  F/ k E. k e. A B = (/)
32 30 31 nfan 
 |-  F/ k ( ph /\ E. k e. A B = (/) )
33 nfv 
 |-  F/ k y = (/)
34 32 33 nfan 
 |-  F/ k ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) )
35 nfv 
 |-  F/ k C = 0
36 simpllr 
 |-  ( ( ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) /\ k e. A ) /\ B = (/) ) -> y = (/) )
37 simpr 
 |-  ( ( ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) /\ k e. A ) /\ B = (/) ) -> B = (/) )
38 36 37 eqtr4d 
 |-  ( ( ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) /\ k e. A ) /\ B = (/) ) -> y = B )
39 38 1 syl 
 |-  ( ( ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) /\ k e. A ) /\ B = (/) ) -> C = D )
40 simp-4l 
 |-  ( ( ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) /\ k e. A ) /\ B = (/) ) -> ph )
41 simplr 
 |-  ( ( ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) /\ k e. A ) /\ B = (/) ) -> k e. A )
42 40 41 37 5 syl21anc 
 |-  ( ( ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) /\ k e. A ) /\ B = (/) ) -> D = 0 )
43 39 42 eqtrd 
 |-  ( ( ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) /\ k e. A ) /\ B = (/) ) -> C = 0 )
44 simplr 
 |-  ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) -> E. k e. A B = (/) )
45 34 35 43 44 r19.29af2 
 |-  ( ( ( ph /\ E. k e. A B = (/) ) /\ y = (/) ) -> C = 0 )
46 29 45 syldan 
 |-  ( ( ( ph /\ E. k e. A B = (/) ) /\ y e. { (/) } ) -> C = 0 )
47 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
48 46 47 eqeltrdi 
 |-  ( ( ( ph /\ E. k e. A B = (/) ) /\ y e. { (/) } ) -> C e. ( 0 [,] +oo ) )
49 nfcv 
 |-  F/_ k y
50 nfmpt1 
 |-  F/_ k ( k e. { k e. A | B = (/) } |-> B )
51 50 nfrn 
 |-  F/_ k ran ( k e. { k e. A | B = (/) } |-> B )
52 49 51 nfel 
 |-  F/ k y e. ran ( k e. { k e. A | B = (/) } |-> B )
53 30 52 nfan 
 |-  F/ k ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) )
54 simpr 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> y = B )
55 rabid 
 |-  ( k e. { k e. A | B = (/) } <-> ( k e. A /\ B = (/) ) )
56 55 simprbi 
 |-  ( k e. { k e. A | B = (/) } -> B = (/) )
57 56 ad2antlr 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> B = (/) )
58 54 57 eqtrd 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> y = (/) )
59 58 28 sylibr 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> y e. { (/) } )
60 vex 
 |-  y e. _V
61 eqid 
 |-  ( k e. { k e. A | B = (/) } |-> B ) = ( k e. { k e. A | B = (/) } |-> B )
62 61 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( k e. { k e. A | B = (/) } |-> B ) <-> E. k e. { k e. A | B = (/) } y = B ) )
63 60 62 ax-mp 
 |-  ( y e. ran ( k e. { k e. A | B = (/) } |-> B ) <-> E. k e. { k e. A | B = (/) } y = B )
64 63 bilani 
 |-  ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) -> E. k e. { k e. A | B = (/) } y = B )
65 53 59 64 r19.29af 
 |-  ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) -> y e. { (/) } )
66 65 ex 
 |-  ( ph -> ( y e. ran ( k e. { k e. A | B = (/) } |-> B ) -> y e. { (/) } ) )
67 66 ssrdv 
 |-  ( ph -> ran ( k e. { k e. A | B = (/) } |-> B ) C_ { (/) } )
68 67 adantr 
 |-  ( ( ph /\ E. k e. A B = (/) ) -> ran ( k e. { k e. A | B = (/) } |-> B ) C_ { (/) } )
69 25 27 48 68 esummono 
 |-  ( ( ph /\ E. k e. A B = (/) ) -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C <_ sum* y e. { (/) } C )
70 0ex 
 |-  (/) e. _V
71 70 a1i 
 |-  ( ( ph /\ E. k e. A B = (/) ) -> (/) e. _V )
72 47 a1i 
 |-  ( ( ph /\ E. k e. A B = (/) ) -> 0 e. ( 0 [,] +oo ) )
73 45 71 72 esumsn 
 |-  ( ( ph /\ E. k e. A B = (/) ) -> sum* y e. { (/) } C = 0 )
74 69 73 breqtrd 
 |-  ( ( ph /\ E. k e. A B = (/) ) -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C <_ 0 )
75 simpr 
 |-  ( ( ph /\ -. E. k e. A B = (/) ) -> -. E. k e. A B = (/) )
76 nfv 
 |-  F/ y -. E. k e. A B = (/)
77 31 nfn 
 |-  F/ k -. E. k e. A B = (/)
78 rabn0 
 |-  ( { k e. A | B = (/) } =/= (/) <-> E. k e. A B = (/) )
79 78 biimpi 
 |-  ( { k e. A | B = (/) } =/= (/) -> E. k e. A B = (/) )
80 79 necon1bi 
 |-  ( -. E. k e. A B = (/) -> { k e. A | B = (/) } = (/) )
81 eqid 
 |-  B = B
82 81 a1i 
 |-  ( -. E. k e. A B = (/) -> B = B )
83 77 80 82 mpteq12df 
 |-  ( -. E. k e. A B = (/) -> ( k e. { k e. A | B = (/) } |-> B ) = ( k e. (/) |-> B ) )
84 mpt0 
 |-  ( k e. (/) |-> B ) = (/)
85 83 84 eqtrdi 
 |-  ( -. E. k e. A B = (/) -> ( k e. { k e. A | B = (/) } |-> B ) = (/) )
86 85 rneqd 
 |-  ( -. E. k e. A B = (/) -> ran ( k e. { k e. A | B = (/) } |-> B ) = ran (/) )
87 rn0 
 |-  ran (/) = (/)
88 86 87 eqtrdi 
 |-  ( -. E. k e. A B = (/) -> ran ( k e. { k e. A | B = (/) } |-> B ) = (/) )
89 76 88 esumeq1d 
 |-  ( -. E. k e. A B = (/) -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C = sum* y e. (/) C )
90 esumnul 
 |-  sum* y e. (/) C = 0
91 89 90 eqtrdi 
 |-  ( -. E. k e. A B = (/) -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C = 0 )
92 0le0 
 |-  0 <_ 0
93 91 92 eqbrtrdi 
 |-  ( -. E. k e. A B = (/) -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C <_ 0 )
94 75 93 syl 
 |-  ( ( ph /\ -. E. k e. A B = (/) ) -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C <_ 0 )
95 74 94 pm2.61dan 
 |-  ( ph -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C <_ 0 )
96 ssrab2 
 |-  { k e. A | B = (/) } C_ A
97 96 a1i 
 |-  ( ph -> { k e. A | B = (/) } C_ A )
98 2 97 ssexd 
 |-  ( ph -> { k e. A | B = (/) } e. _V )
99 nfrab1 
 |-  F/_ k { k e. A | B = (/) }
100 99 mptexgf 
 |-  ( { k e. A | B = (/) } e. _V -> ( k e. { k e. A | B = (/) } |-> B ) e. _V )
101 rnexg 
 |-  ( ( k e. { k e. A | B = (/) } |-> B ) e. _V -> ran ( k e. { k e. A | B = (/) } |-> B ) e. _V )
102 98 100 101 3syl 
 |-  ( ph -> ran ( k e. { k e. A | B = (/) } |-> B ) e. _V )
103 1 adantl 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> C = D )
104 simplll 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> ph )
105 97 sselda 
 |-  ( ( ph /\ k e. { k e. A | B = (/) } ) -> k e. A )
106 105 adantlr 
 |-  ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) -> k e. A )
107 106 adantr 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> k e. A )
108 104 107 3 syl2anc 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> D e. ( 0 [,] +oo ) )
109 103 108 eqeltrd 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) /\ k e. { k e. A | B = (/) } ) /\ y = B ) -> C e. ( 0 [,] +oo ) )
110 53 109 64 r19.29af 
 |-  ( ( ph /\ y e. ran ( k e. { k e. A | B = (/) } |-> B ) ) -> C e. ( 0 [,] +oo ) )
111 110 ralrimiva 
 |-  ( ph -> A. y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. ( 0 [,] +oo ) )
112 nfcv 
 |-  F/_ y ran ( k e. { k e. A | B = (/) } |-> B )
113 112 esumcl 
 |-  ( ( ran ( k e. { k e. A | B = (/) } |-> B ) e. _V /\ A. y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. ( 0 [,] +oo ) ) -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. ( 0 [,] +oo ) )
114 102 111 113 syl2anc 
 |-  ( ph -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. ( 0 [,] +oo ) )
115 elxrge0 
 |-  ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. ( 0 [,] +oo ) <-> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. RR* /\ 0 <_ sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C ) )
116 115 simprbi 
 |-  ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. ( 0 [,] +oo ) -> 0 <_ sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C )
117 114 116 syl 
 |-  ( ph -> 0 <_ sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C )
118 95 117 jca 
 |-  ( ph -> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C <_ 0 /\ 0 <_ sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C ) )
119 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
120 119 114 sselid 
 |-  ( ph -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. RR* )
121 119 47 sselii 
 |-  0 e. RR*
122 121 a1i 
 |-  ( ph -> 0 e. RR* )
123 xrletri3 
 |-  ( ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C e. RR* /\ 0 e. RR* ) -> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C = 0 <-> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C <_ 0 /\ 0 <_ sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C ) ) )
124 120 122 123 syl2anc 
 |-  ( ph -> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C = 0 <-> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C <_ 0 /\ 0 <_ sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C ) ) )
125 118 124 mpbird 
 |-  ( ph -> sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C = 0 )
126 125 oveq1d 
 |-  ( ph -> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C +e sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C ) = ( 0 +e sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C ) )
127 12 ralrimiva 
 |-  ( ph -> A. k e. { k e. A | -. B = (/) } D e. ( 0 [,] +oo ) )
128 7 esumcl 
 |-  ( ( { k e. A | -. B = (/) } e. _V /\ A. k e. { k e. A | -. B = (/) } D e. ( 0 [,] +oo ) ) -> sum* k e. { k e. A | -. B = (/) } D e. ( 0 [,] +oo ) )
129 10 127 128 syl2anc 
 |-  ( ph -> sum* k e. { k e. A | -. B = (/) } D e. ( 0 [,] +oo ) )
130 119 129 sselid 
 |-  ( ph -> sum* k e. { k e. A | -. B = (/) } D e. RR* )
131 24 130 eqeltrd 
 |-  ( ph -> sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C e. RR* )
132 xaddlid 
 |-  ( sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C e. RR* -> ( 0 +e sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C ) = sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C )
133 131 132 syl 
 |-  ( ph -> ( 0 +e sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C ) = sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C )
134 126 133 eqtrd 
 |-  ( ph -> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C +e sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C ) = sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C )
135 simpl 
 |-  ( ( ph /\ k e. { k e. A | B = (/) } ) -> ph )
136 56 adantl 
 |-  ( ( ph /\ k e. { k e. A | B = (/) } ) -> B = (/) )
137 135 105 136 5 syl21anc 
 |-  ( ( ph /\ k e. { k e. A | B = (/) } ) -> D = 0 )
138 137 ralrimiva 
 |-  ( ph -> A. k e. { k e. A | B = (/) } D = 0 )
139 30 138 esumeq2d 
 |-  ( ph -> sum* k e. { k e. A | B = (/) } D = sum* k e. { k e. A | B = (/) } 0 )
140 99 esum0 
 |-  ( { k e. A | B = (/) } e. _V -> sum* k e. { k e. A | B = (/) } 0 = 0 )
141 98 140 syl 
 |-  ( ph -> sum* k e. { k e. A | B = (/) } 0 = 0 )
142 139 141 eqtrd 
 |-  ( ph -> sum* k e. { k e. A | B = (/) } D = 0 )
143 142 oveq1d 
 |-  ( ph -> ( sum* k e. { k e. A | B = (/) } D +e sum* k e. { k e. A | -. B = (/) } D ) = ( 0 +e sum* k e. { k e. A | -. B = (/) } D ) )
144 xaddlid 
 |-  ( sum* k e. { k e. A | -. B = (/) } D e. RR* -> ( 0 +e sum* k e. { k e. A | -. B = (/) } D ) = sum* k e. { k e. A | -. B = (/) } D )
145 130 144 syl 
 |-  ( ph -> ( 0 +e sum* k e. { k e. A | -. B = (/) } D ) = sum* k e. { k e. A | -. B = (/) } D )
146 143 145 eqtrd 
 |-  ( ph -> ( sum* k e. { k e. A | B = (/) } D +e sum* k e. { k e. A | -. B = (/) } D ) = sum* k e. { k e. A | -. B = (/) } D )
147 24 134 146 3eqtr4d 
 |-  ( ph -> ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C +e sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C ) = ( sum* k e. { k e. A | B = (/) } D +e sum* k e. { k e. A | -. B = (/) } D ) )
148 nfv 
 |-  F/ y ph
149 nfcv 
 |-  F/_ y ran ( k e. { k e. A | -. B = (/) } |-> B )
150 7 mptexgf 
 |-  ( { k e. A | -. B = (/) } e. _V -> ( k e. { k e. A | -. B = (/) } |-> B ) e. _V )
151 rnexg 
 |-  ( ( k e. { k e. A | -. B = (/) } |-> B ) e. _V -> ran ( k e. { k e. A | -. B = (/) } |-> B ) e. _V )
152 10 150 151 3syl 
 |-  ( ph -> ran ( k e. { k e. A | -. B = (/) } |-> B ) e. _V )
153 67 ssrind 
 |-  ( ph -> ( ran ( k e. { k e. A | B = (/) } |-> B ) i^i ran ( k e. { k e. A | -. B = (/) } |-> B ) ) C_ ( { (/) } i^i ran ( k e. { k e. A | -. B = (/) } |-> B ) ) )
154 incom 
 |-  ( ran ( k e. { k e. A | -. B = (/) } |-> B ) i^i { (/) } ) = ( { (/) } i^i ran ( k e. { k e. A | -. B = (/) } |-> B ) )
155 15 neqned 
 |-  ( k e. { k e. A | -. B = (/) } -> B =/= (/) )
156 155 necomd 
 |-  ( k e. { k e. A | -. B = (/) } -> (/) =/= B )
157 156 neneqd 
 |-  ( k e. { k e. A | -. B = (/) } -> -. (/) = B )
158 157 nrex 
 |-  -. E. k e. { k e. A | -. B = (/) } (/) = B
159 eqid 
 |-  ( k e. { k e. A | -. B = (/) } |-> B ) = ( k e. { k e. A | -. B = (/) } |-> B )
160 159 elrnmpt 
 |-  ( (/) e. _V -> ( (/) e. ran ( k e. { k e. A | -. B = (/) } |-> B ) <-> E. k e. { k e. A | -. B = (/) } (/) = B ) )
161 70 160 ax-mp 
 |-  ( (/) e. ran ( k e. { k e. A | -. B = (/) } |-> B ) <-> E. k e. { k e. A | -. B = (/) } (/) = B )
162 158 161 mtbir 
 |-  -. (/) e. ran ( k e. { k e. A | -. B = (/) } |-> B )
163 disjsn 
 |-  ( ( ran ( k e. { k e. A | -. B = (/) } |-> B ) i^i { (/) } ) = (/) <-> -. (/) e. ran ( k e. { k e. A | -. B = (/) } |-> B ) )
164 162 163 mpbir 
 |-  ( ran ( k e. { k e. A | -. B = (/) } |-> B ) i^i { (/) } ) = (/)
165 154 164 eqtr3i 
 |-  ( { (/) } i^i ran ( k e. { k e. A | -. B = (/) } |-> B ) ) = (/)
166 153 165 sseqtrdi 
 |-  ( ph -> ( ran ( k e. { k e. A | B = (/) } |-> B ) i^i ran ( k e. { k e. A | -. B = (/) } |-> B ) ) C_ (/) )
167 ss0 
 |-  ( ( ran ( k e. { k e. A | B = (/) } |-> B ) i^i ran ( k e. { k e. A | -. B = (/) } |-> B ) ) C_ (/) -> ( ran ( k e. { k e. A | B = (/) } |-> B ) i^i ran ( k e. { k e. A | -. B = (/) } |-> B ) ) = (/) )
168 166 167 syl 
 |-  ( ph -> ( ran ( k e. { k e. A | B = (/) } |-> B ) i^i ran ( k e. { k e. A | -. B = (/) } |-> B ) ) = (/) )
169 nfmpt1 
 |-  F/_ k ( k e. { k e. A | -. B = (/) } |-> B )
170 169 nfrn 
 |-  F/_ k ran ( k e. { k e. A | -. B = (/) } |-> B )
171 49 170 nfel 
 |-  F/ k y e. ran ( k e. { k e. A | -. B = (/) } |-> B )
172 30 171 nfan 
 |-  F/ k ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) )
173 1 adantl 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) /\ k e. { k e. A | -. B = (/) } ) /\ y = B ) -> C = D )
174 simplll 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) /\ k e. { k e. A | -. B = (/) } ) /\ y = B ) -> ph )
175 11 adantlr 
 |-  ( ( ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) /\ k e. { k e. A | -. B = (/) } ) -> k e. A )
176 175 adantr 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) /\ k e. { k e. A | -. B = (/) } ) /\ y = B ) -> k e. A )
177 174 176 3 syl2anc 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) /\ k e. { k e. A | -. B = (/) } ) /\ y = B ) -> D e. ( 0 [,] +oo ) )
178 173 177 eqeltrd 
 |-  ( ( ( ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) /\ k e. { k e. A | -. B = (/) } ) /\ y = B ) -> C e. ( 0 [,] +oo ) )
179 159 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) <-> E. k e. { k e. A | -. B = (/) } y = B ) )
180 60 179 ax-mp 
 |-  ( y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) <-> E. k e. { k e. A | -. B = (/) } y = B )
181 180 bilani 
 |-  ( ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) -> E. k e. { k e. A | -. B = (/) } y = B )
182 172 178 181 r19.29af 
 |-  ( ( ph /\ y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) -> C e. ( 0 [,] +oo ) )
183 148 112 149 102 152 168 110 182 esumsplit 
 |-  ( ph -> sum* y e. ( ran ( k e. { k e. A | B = (/) } |-> B ) u. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) C = ( sum* y e. ran ( k e. { k e. A | B = (/) } |-> B ) C +e sum* y e. ran ( k e. { k e. A | -. B = (/) } |-> B ) C ) )
184 rabnc 
 |-  ( { k e. A | B = (/) } i^i { k e. A | -. B = (/) } ) = (/)
185 184 a1i 
 |-  ( ph -> ( { k e. A | B = (/) } i^i { k e. A | -. B = (/) } ) = (/) )
186 105 3 syldan 
 |-  ( ( ph /\ k e. { k e. A | B = (/) } ) -> D e. ( 0 [,] +oo ) )
187 30 99 7 98 10 185 186 12 esumsplit 
 |-  ( ph -> sum* k e. ( { k e. A | B = (/) } u. { k e. A | -. B = (/) } ) D = ( sum* k e. { k e. A | B = (/) } D +e sum* k e. { k e. A | -. B = (/) } D ) )
188 147 183 187 3eqtr4d 
 |-  ( ph -> sum* y e. ( ran ( k e. { k e. A | B = (/) } |-> B ) u. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) C = sum* k e. ( { k e. A | B = (/) } u. { k e. A | -. B = (/) } ) D )
189 rabxm 
 |-  A = ( { k e. A | B = (/) } u. { k e. A | -. B = (/) } )
190 189 81 mpteq12i 
 |-  ( k e. A |-> B ) = ( k e. ( { k e. A | B = (/) } u. { k e. A | -. B = (/) } ) |-> B )
191 mptun 
 |-  ( k e. ( { k e. A | B = (/) } u. { k e. A | -. B = (/) } ) |-> B ) = ( ( k e. { k e. A | B = (/) } |-> B ) u. ( k e. { k e. A | -. B = (/) } |-> B ) )
192 190 191 eqtri 
 |-  ( k e. A |-> B ) = ( ( k e. { k e. A | B = (/) } |-> B ) u. ( k e. { k e. A | -. B = (/) } |-> B ) )
193 192 rneqi 
 |-  ran ( k e. A |-> B ) = ran ( ( k e. { k e. A | B = (/) } |-> B ) u. ( k e. { k e. A | -. B = (/) } |-> B ) )
194 rnun 
 |-  ran ( ( k e. { k e. A | B = (/) } |-> B ) u. ( k e. { k e. A | -. B = (/) } |-> B ) ) = ( ran ( k e. { k e. A | B = (/) } |-> B ) u. ran ( k e. { k e. A | -. B = (/) } |-> B ) )
195 193 194 eqtri 
 |-  ran ( k e. A |-> B ) = ( ran ( k e. { k e. A | B = (/) } |-> B ) u. ran ( k e. { k e. A | -. B = (/) } |-> B ) )
196 195 a1i 
 |-  ( ph -> ran ( k e. A |-> B ) = ( ran ( k e. { k e. A | B = (/) } |-> B ) u. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) )
197 148 196 esumeq1d 
 |-  ( ph -> sum* y e. ran ( k e. A |-> B ) C = sum* y e. ( ran ( k e. { k e. A | B = (/) } |-> B ) u. ran ( k e. { k e. A | -. B = (/) } |-> B ) ) C )
198 189 a1i 
 |-  ( ph -> A = ( { k e. A | B = (/) } u. { k e. A | -. B = (/) } ) )
199 30 198 esumeq1d 
 |-  ( ph -> sum* k e. A D = sum* k e. ( { k e. A | B = (/) } u. { k e. A | -. B = (/) } ) D )
200 188 197 199 3eqtr4d 
 |-  ( ph -> sum* y e. ran ( k e. A |-> B ) C = sum* k e. A D )