Metamath Proof Explorer

Definition df-sumge0

Description: Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020) $.

Ref Expression
Assertion df-sumge0 
|- sum^ = ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csumge0 
 |-  sum^
1 vx 
 |-  x
2 cvv 
 |-  _V
3 cpnf 
 |-  +oo
4 1 cv 
 |-  x
5 4 crn 
 |-  ran x
6 3 5 wcel 
 |-  +oo e. ran x
7 vy 
 |-  y
8 4 cdm 
 |-  dom x
9 8 cpw 
 |-  ~P dom x
10 cfn 
 |-  Fin
11 9 10 cin 
 |-  ( ~P dom x i^i Fin )
12 vw 
 |-  w
13 7 cv 
 |-  y
14 12 cv 
 |-  w
15 14 4 cfv 
 |-  ( x ` w )
16 13 15 12 csu 
 |-  sum_ w e. y ( x ` w )
17 7 11 16 cmpt 
 |-  ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) )
18 17 crn 
 |-  ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) )
19 cxr 
 |-  RR*
20 clt 
 |-  <
21 18 19 20 csup 
 |-  sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < )
22 6 3 21 cif 
 |-  if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) )
23 1 2 22 cmpt 
 |-  ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )
24 0 23 wceq 
 |-  sum^ = ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )