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