Step |
Hyp |
Ref |
Expression |
1 |
|
sge0sn.1 |
|- ( ph -> A e. V ) |
2 |
|
sge0sn.2 |
|- ( ph -> F : { A } --> ( 0 [,] +oo ) ) |
3 |
|
snex |
|- { A } e. _V |
4 |
3
|
a1i |
|- ( ( ph /\ ( F ` A ) = +oo ) -> { A } e. _V ) |
5 |
2
|
adantr |
|- ( ( ph /\ ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,] +oo ) ) |
6 |
|
id |
|- ( ( F ` A ) = +oo -> ( F ` A ) = +oo ) |
7 |
6
|
eqcomd |
|- ( ( F ` A ) = +oo -> +oo = ( F ` A ) ) |
8 |
7
|
adantl |
|- ( ( ph /\ ( F ` A ) = +oo ) -> +oo = ( F ` A ) ) |
9 |
2
|
ffund |
|- ( ph -> Fun F ) |
10 |
9
|
adantr |
|- ( ( ph /\ ( F ` A ) = +oo ) -> Fun F ) |
11 |
|
snidg |
|- ( A e. V -> A e. { A } ) |
12 |
1 11
|
syl |
|- ( ph -> A e. { A } ) |
13 |
2
|
fdmd |
|- ( ph -> dom F = { A } ) |
14 |
13
|
eqcomd |
|- ( ph -> { A } = dom F ) |
15 |
12 14
|
eleqtrd |
|- ( ph -> A e. dom F ) |
16 |
15
|
adantr |
|- ( ( ph /\ ( F ` A ) = +oo ) -> A e. dom F ) |
17 |
|
fvelrn |
|- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F ) |
18 |
10 16 17
|
syl2anc |
|- ( ( ph /\ ( F ` A ) = +oo ) -> ( F ` A ) e. ran F ) |
19 |
8 18
|
eqeltrd |
|- ( ( ph /\ ( F ` A ) = +oo ) -> +oo e. ran F ) |
20 |
4 5 19
|
sge0pnfval |
|- ( ( ph /\ ( F ` A ) = +oo ) -> ( sum^ ` F ) = +oo ) |
21 |
|
simpr |
|- ( ( ph /\ ( F ` A ) = +oo ) -> ( F ` A ) = +oo ) |
22 |
20 21
|
eqtr4d |
|- ( ( ph /\ ( F ` A ) = +oo ) -> ( sum^ ` F ) = ( F ` A ) ) |
23 |
3
|
a1i |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> { A } e. _V ) |
24 |
2
|
adantr |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,] +oo ) ) |
25 |
|
elsni |
|- ( +oo e. { ( F ` A ) } -> +oo = ( F ` A ) ) |
26 |
25
|
eqcomd |
|- ( +oo e. { ( F ` A ) } -> ( F ` A ) = +oo ) |
27 |
26
|
con3i |
|- ( -. ( F ` A ) = +oo -> -. +oo e. { ( F ` A ) } ) |
28 |
27
|
adantl |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> -. +oo e. { ( F ` A ) } ) |
29 |
1 2
|
rnsnf |
|- ( ph -> ran F = { ( F ` A ) } ) |
30 |
29
|
eqcomd |
|- ( ph -> { ( F ` A ) } = ran F ) |
31 |
30
|
adantr |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> { ( F ` A ) } = ran F ) |
32 |
28 31
|
neleqtrd |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> -. +oo e. ran F ) |
33 |
24 32
|
fge0iccico |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,) +oo ) ) |
34 |
23 33
|
sge0reval |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) |
35 |
|
sum0 |
|- sum_ y e. (/) ( F ` y ) = 0 |
36 |
35
|
eqcomi |
|- 0 = sum_ y e. (/) ( F ` y ) |
37 |
36
|
a1i |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> 0 = sum_ y e. (/) ( F ` y ) ) |
38 |
|
nfcvd |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> F/_ y ( F ` A ) ) |
39 |
|
nfv |
|- F/ y ( ph /\ -. ( F ` A ) = +oo ) |
40 |
|
fveq2 |
|- ( y = A -> ( F ` y ) = ( F ` A ) ) |
41 |
40
|
adantl |
|- ( ( ( ph /\ -. ( F ` A ) = +oo ) /\ y = A ) -> ( F ` y ) = ( F ` A ) ) |
42 |
1
|
adantr |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> A e. V ) |
43 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
44 |
|
ax-resscn |
|- RR C_ CC |
45 |
43 44
|
sstri |
|- ( 0 [,) +oo ) C_ CC |
46 |
42 11
|
syl |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> A e. { A } ) |
47 |
33 46
|
ffvelrnd |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) e. ( 0 [,) +oo ) ) |
48 |
45 47
|
sseldi |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) e. CC ) |
49 |
38 39 41 42 48
|
sumsnd |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> sum_ y e. { A } ( F ` y ) = ( F ` A ) ) |
50 |
49
|
eqcomd |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sum_ y e. { A } ( F ` y ) ) |
51 |
37 50
|
preq12d |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> { 0 , ( F ` A ) } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } ) |
52 |
51
|
supeq1d |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> sup ( { 0 , ( F ` A ) } , RR* , < ) = sup ( { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } , RR* , < ) ) |
53 |
|
xrltso |
|- < Or RR* |
54 |
53
|
a1i |
|- ( ph -> < Or RR* ) |
55 |
|
0xr |
|- 0 e. RR* |
56 |
55
|
a1i |
|- ( ph -> 0 e. RR* ) |
57 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
58 |
2 12
|
ffvelrnd |
|- ( ph -> ( F ` A ) e. ( 0 [,] +oo ) ) |
59 |
57 58
|
sseldi |
|- ( ph -> ( F ` A ) e. RR* ) |
60 |
|
suppr |
|- ( ( < Or RR* /\ 0 e. RR* /\ ( F ` A ) e. RR* ) -> sup ( { 0 , ( F ` A ) } , RR* , < ) = if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) ) |
61 |
54 56 59 60
|
syl3anc |
|- ( ph -> sup ( { 0 , ( F ` A ) } , RR* , < ) = if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) ) |
62 |
|
pnfxr |
|- +oo e. RR* |
63 |
62
|
a1i |
|- ( ph -> +oo e. RR* ) |
64 |
56 63 58
|
3jca |
|- ( ph -> ( 0 e. RR* /\ +oo e. RR* /\ ( F ` A ) e. ( 0 [,] +oo ) ) ) |
65 |
|
iccgelb |
|- ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` A ) e. ( 0 [,] +oo ) ) -> 0 <_ ( F ` A ) ) |
66 |
64 65
|
syl |
|- ( ph -> 0 <_ ( F ` A ) ) |
67 |
56 59
|
xrlenltd |
|- ( ph -> ( 0 <_ ( F ` A ) <-> -. ( F ` A ) < 0 ) ) |
68 |
66 67
|
mpbid |
|- ( ph -> -. ( F ` A ) < 0 ) |
69 |
68
|
iffalsed |
|- ( ph -> if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) = ( F ` A ) ) |
70 |
61 69
|
eqtr2d |
|- ( ph -> ( F ` A ) = sup ( { 0 , ( F ` A ) } , RR* , < ) ) |
71 |
70
|
adantr |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sup ( { 0 , ( F ` A ) } , RR* , < ) ) |
72 |
|
pwsn |
|- ~P { A } = { (/) , { A } } |
73 |
72
|
ineq1i |
|- ( ~P { A } i^i Fin ) = ( { (/) , { A } } i^i Fin ) |
74 |
|
0fin |
|- (/) e. Fin |
75 |
|
snfi |
|- { A } e. Fin |
76 |
|
prssi |
|- ( ( (/) e. Fin /\ { A } e. Fin ) -> { (/) , { A } } C_ Fin ) |
77 |
74 75 76
|
mp2an |
|- { (/) , { A } } C_ Fin |
78 |
|
df-ss |
|- ( { (/) , { A } } C_ Fin <-> ( { (/) , { A } } i^i Fin ) = { (/) , { A } } ) |
79 |
78
|
biimpi |
|- ( { (/) , { A } } C_ Fin -> ( { (/) , { A } } i^i Fin ) = { (/) , { A } } ) |
80 |
77 79
|
ax-mp |
|- ( { (/) , { A } } i^i Fin ) = { (/) , { A } } |
81 |
73 80
|
eqtri |
|- ( ~P { A } i^i Fin ) = { (/) , { A } } |
82 |
|
mpteq1 |
|- ( ( ~P { A } i^i Fin ) = { (/) , { A } } -> ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) ) |
83 |
81 82
|
ax-mp |
|- ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) |
84 |
|
0ex |
|- (/) e. _V |
85 |
84
|
a1i |
|- ( T. -> (/) e. _V ) |
86 |
3
|
a1i |
|- ( T. -> { A } e. _V ) |
87 |
|
sumex |
|- sum_ y e. (/) ( F ` y ) e. _V |
88 |
87
|
a1i |
|- ( T. -> sum_ y e. (/) ( F ` y ) e. _V ) |
89 |
|
sumex |
|- sum_ y e. { A } ( F ` y ) e. _V |
90 |
89
|
a1i |
|- ( T. -> sum_ y e. { A } ( F ` y ) e. _V ) |
91 |
|
sumeq1 |
|- ( x = (/) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) ) |
92 |
91
|
adantl |
|- ( ( T. /\ x = (/) ) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) ) |
93 |
|
sumeq1 |
|- ( x = { A } -> sum_ y e. x ( F ` y ) = sum_ y e. { A } ( F ` y ) ) |
94 |
93
|
adantl |
|- ( ( T. /\ x = { A } ) -> sum_ y e. x ( F ` y ) = sum_ y e. { A } ( F ` y ) ) |
95 |
85 86 88 90 92 94
|
fmptpr |
|- ( T. -> { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) ) |
96 |
95
|
mptru |
|- { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) |
97 |
96
|
eqcomi |
|- ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) = { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } |
98 |
83 97
|
eqtri |
|- ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } |
99 |
98
|
rneqi |
|- ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ran { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } |
100 |
|
rnpropg |
|- ( ( (/) e. _V /\ { A } e. _V ) -> ran { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } ) |
101 |
84 3 100
|
mp2an |
|- ran { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } |
102 |
99 101
|
eqtri |
|- ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } |
103 |
102
|
supeq1i |
|- sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = sup ( { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } , RR* , < ) |
104 |
103
|
a1i |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = sup ( { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } , RR* , < ) ) |
105 |
52 71 104
|
3eqtr4d |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) |
106 |
34 105
|
eqtr4d |
|- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( sum^ ` F ) = ( F ` A ) ) |
107 |
22 106
|
pm2.61dan |
|- ( ph -> ( sum^ ` F ) = ( F ` A ) ) |