Metamath Proof Explorer

Theorem esumnul

Description: Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017)

Ref Expression
Assertion esumnul 
|- sum* x e. (/) A = 0

Proof

Step Hyp Ref Expression
1 nftru 
 |-  F/ x T.
2 nfcv 
 |-  F/_ x (/)
3 0ex 
 |-  (/) e. _V
4 3 a1i 
 |-  ( T. -> (/) e. _V )
5 ral0 
 |-  A. x e. (/) A e. ( 0 [,] +oo )
6 5 a1i 
 |-  ( T. -> A. x e. (/) A e. ( 0 [,] +oo ) )
7 6 r19.21bi 
 |-  ( ( T. /\ x e. (/) ) -> A e. ( 0 [,] +oo ) )
8 pw0 
 |-  ~P (/) = { (/) }
9 8 ineq1i 
 |-  ( ~P (/) i^i Fin ) = ( { (/) } i^i Fin )
10 0fin 
 |-  (/) e. Fin
11 snssi 
 |-  ( (/) e. Fin -> { (/) } C_ Fin )
12 df-ss 
 |-  ( { (/) } C_ Fin <-> ( { (/) } i^i Fin ) = { (/) } )
13 11 12 sylib 
 |-  ( (/) e. Fin -> ( { (/) } i^i Fin ) = { (/) } )
14 10 13 ax-mp 
 |-  ( { (/) } i^i Fin ) = { (/) }
15 9 14 eqtri 
 |-  ( ~P (/) i^i Fin ) = { (/) }
16 15 eleq2i 
 |-  ( y e. ( ~P (/) i^i Fin ) <-> y e. { (/) } )
17 velsn 
 |-  ( y e. { (/) } <-> y = (/) )
18 16 17 sylbb 
 |-  ( y e. ( ~P (/) i^i Fin ) -> y = (/) )
19 18 mpteq1d 
 |-  ( y e. ( ~P (/) i^i Fin ) -> ( x e. y |-> A ) = ( x e. (/) |-> A ) )
20 mpt0 
 |-  ( x e. (/) |-> A ) = (/)
21 19 20 eqtrdi 
 |-  ( y e. ( ~P (/) i^i Fin ) -> ( x e. y |-> A ) = (/) )
22 21 oveq2d 
 |-  ( y e. ( ~P (/) i^i Fin ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( x e. y |-> A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum (/) ) )
23 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
24 23 gsum0 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum (/) ) = 0
25 22 24 eqtrdi 
 |-  ( y e. ( ~P (/) i^i Fin ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( x e. y |-> A ) ) = 0 )
26 25 adantl 
 |-  ( ( T. /\ y e. ( ~P (/) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( x e. y |-> A ) ) = 0 )
27 1 2 4 7 26 esumval 
 |-  ( T. -> sum* x e. (/) A = sup ( ran ( y e. ( ~P (/) i^i Fin ) |-> 0 ) , RR* , < ) )
28 27 mptru 
 |-  sum* x e. (/) A = sup ( ran ( y e. ( ~P (/) i^i Fin ) |-> 0 ) , RR* , < )
29 fconstmpt 
 |-  ( ( ~P (/) i^i Fin ) X. { 0 } ) = ( y e. ( ~P (/) i^i Fin ) |-> 0 )
30 29 eqcomi 
 |-  ( y e. ( ~P (/) i^i Fin ) |-> 0 ) = ( ( ~P (/) i^i Fin ) X. { 0 } )
31 0xr 
 |-  0 e. RR*
32 31 rgenw 
 |-  A. y e. ( ~P (/) i^i Fin ) 0 e. RR*
33 eqid 
 |-  ( y e. ( ~P (/) i^i Fin ) |-> 0 ) = ( y e. ( ~P (/) i^i Fin ) |-> 0 )
34 33 fnmpt 
 |-  ( A. y e. ( ~P (/) i^i Fin ) 0 e. RR* -> ( y e. ( ~P (/) i^i Fin ) |-> 0 ) Fn ( ~P (/) i^i Fin ) )
35 32 34 ax-mp 
 |-  ( y e. ( ~P (/) i^i Fin ) |-> 0 ) Fn ( ~P (/) i^i Fin )
36 3 snnz 
 |-  { (/) } =/= (/)
37 15 36 eqnetri 
 |-  ( ~P (/) i^i Fin ) =/= (/)
38 fconst5 
 |-  ( ( ( y e. ( ~P (/) i^i Fin ) |-> 0 ) Fn ( ~P (/) i^i Fin ) /\ ( ~P (/) i^i Fin ) =/= (/) ) -> ( ( y e. ( ~P (/) i^i Fin ) |-> 0 ) = ( ( ~P (/) i^i Fin ) X. { 0 } ) <-> ran ( y e. ( ~P (/) i^i Fin ) |-> 0 ) = { 0 } ) )
39 35 37 38 mp2an 
 |-  ( ( y e. ( ~P (/) i^i Fin ) |-> 0 ) = ( ( ~P (/) i^i Fin ) X. { 0 } ) <-> ran ( y e. ( ~P (/) i^i Fin ) |-> 0 ) = { 0 } )
40 30 39 mpbi 
 |-  ran ( y e. ( ~P (/) i^i Fin ) |-> 0 ) = { 0 }
41 40 supeq1i 
 |-  sup ( ran ( y e. ( ~P (/) i^i Fin ) |-> 0 ) , RR* , < ) = sup ( { 0 } , RR* , < )
42 xrltso 
 |-  < Or RR*
43 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
44 42 31 43 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
45 28 41 44 3eqtri 
 |-  sum* x e. (/) A = 0