Step |
Hyp |
Ref |
Expression |
1 |
|
i1fd.1 |
|- ( ph -> F : RR --> RR ) |
2 |
|
i1fd.2 |
|- ( ph -> ran F e. Fin ) |
3 |
|
i1fd.3 |
|- ( ( ph /\ x e. ( ran F \ { 0 } ) ) -> ( `' F " { x } ) e. dom vol ) |
4 |
|
i1fd.4 |
|- ( ( ph /\ x e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR ) |
5 |
1
|
ad2antrr |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> F : RR --> RR ) |
6 |
|
ffun |
|- ( F : RR --> RR -> Fun F ) |
7 |
|
funcnvcnv |
|- ( Fun F -> Fun `' `' F ) |
8 |
|
imadif |
|- ( Fun `' `' F -> ( `' F " ( RR \ ( RR \ x ) ) ) = ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) ) |
9 |
5 6 7 8
|
4syl |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " ( RR \ ( RR \ x ) ) ) = ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) ) |
10 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
11 |
|
frn |
|- ( (,) : ( RR* X. RR* ) --> ~P RR -> ran (,) C_ ~P RR ) |
12 |
10 11
|
ax-mp |
|- ran (,) C_ ~P RR |
13 |
12
|
sseli |
|- ( x e. ran (,) -> x e. ~P RR ) |
14 |
13
|
elpwid |
|- ( x e. ran (,) -> x C_ RR ) |
15 |
14
|
ad2antlr |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> x C_ RR ) |
16 |
|
dfss4 |
|- ( x C_ RR <-> ( RR \ ( RR \ x ) ) = x ) |
17 |
15 16
|
sylib |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( RR \ ( RR \ x ) ) = x ) |
18 |
17
|
imaeq2d |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " ( RR \ ( RR \ x ) ) ) = ( `' F " x ) ) |
19 |
9 18
|
eqtr3d |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) = ( `' F " x ) ) |
20 |
|
fimacnv |
|- ( F : RR --> RR -> ( `' F " RR ) = RR ) |
21 |
5 20
|
syl |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " RR ) = RR ) |
22 |
|
rembl |
|- RR e. dom vol |
23 |
21 22
|
eqeltrdi |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " RR ) e. dom vol ) |
24 |
1
|
adantr |
|- ( ( ph /\ -. 0 e. y ) -> F : RR --> RR ) |
25 |
|
inpreima |
|- ( Fun F -> ( `' F " ( y i^i ran F ) ) = ( ( `' F " y ) i^i ( `' F " ran F ) ) ) |
26 |
|
iunid |
|- U_ x e. ( y i^i ran F ) { x } = ( y i^i ran F ) |
27 |
26
|
imaeq2i |
|- ( `' F " U_ x e. ( y i^i ran F ) { x } ) = ( `' F " ( y i^i ran F ) ) |
28 |
|
imaiun |
|- ( `' F " U_ x e. ( y i^i ran F ) { x } ) = U_ x e. ( y i^i ran F ) ( `' F " { x } ) |
29 |
27 28
|
eqtr3i |
|- ( `' F " ( y i^i ran F ) ) = U_ x e. ( y i^i ran F ) ( `' F " { x } ) |
30 |
|
cnvimass |
|- ( `' F " y ) C_ dom F |
31 |
|
cnvimarndm |
|- ( `' F " ran F ) = dom F |
32 |
30 31
|
sseqtrri |
|- ( `' F " y ) C_ ( `' F " ran F ) |
33 |
|
df-ss |
|- ( ( `' F " y ) C_ ( `' F " ran F ) <-> ( ( `' F " y ) i^i ( `' F " ran F ) ) = ( `' F " y ) ) |
34 |
32 33
|
mpbi |
|- ( ( `' F " y ) i^i ( `' F " ran F ) ) = ( `' F " y ) |
35 |
25 29 34
|
3eqtr3g |
|- ( Fun F -> U_ x e. ( y i^i ran F ) ( `' F " { x } ) = ( `' F " y ) ) |
36 |
24 6 35
|
3syl |
|- ( ( ph /\ -. 0 e. y ) -> U_ x e. ( y i^i ran F ) ( `' F " { x } ) = ( `' F " y ) ) |
37 |
2
|
adantr |
|- ( ( ph /\ -. 0 e. y ) -> ran F e. Fin ) |
38 |
|
inss2 |
|- ( y i^i ran F ) C_ ran F |
39 |
|
ssfi |
|- ( ( ran F e. Fin /\ ( y i^i ran F ) C_ ran F ) -> ( y i^i ran F ) e. Fin ) |
40 |
37 38 39
|
sylancl |
|- ( ( ph /\ -. 0 e. y ) -> ( y i^i ran F ) e. Fin ) |
41 |
|
simpll |
|- ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ph ) |
42 |
|
elinel1 |
|- ( 0 e. ( y i^i ran F ) -> 0 e. y ) |
43 |
42
|
con3i |
|- ( -. 0 e. y -> -. 0 e. ( y i^i ran F ) ) |
44 |
43
|
adantl |
|- ( ( ph /\ -. 0 e. y ) -> -. 0 e. ( y i^i ran F ) ) |
45 |
|
disjsn |
|- ( ( ( y i^i ran F ) i^i { 0 } ) = (/) <-> -. 0 e. ( y i^i ran F ) ) |
46 |
44 45
|
sylibr |
|- ( ( ph /\ -. 0 e. y ) -> ( ( y i^i ran F ) i^i { 0 } ) = (/) ) |
47 |
|
reldisj |
|- ( ( y i^i ran F ) C_ ran F -> ( ( ( y i^i ran F ) i^i { 0 } ) = (/) <-> ( y i^i ran F ) C_ ( ran F \ { 0 } ) ) ) |
48 |
38 47
|
ax-mp |
|- ( ( ( y i^i ran F ) i^i { 0 } ) = (/) <-> ( y i^i ran F ) C_ ( ran F \ { 0 } ) ) |
49 |
46 48
|
sylib |
|- ( ( ph /\ -. 0 e. y ) -> ( y i^i ran F ) C_ ( ran F \ { 0 } ) ) |
50 |
49
|
sselda |
|- ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> x e. ( ran F \ { 0 } ) ) |
51 |
41 50 3
|
syl2anc |
|- ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( `' F " { x } ) e. dom vol ) |
52 |
51
|
ralrimiva |
|- ( ( ph /\ -. 0 e. y ) -> A. x e. ( y i^i ran F ) ( `' F " { x } ) e. dom vol ) |
53 |
|
finiunmbl |
|- ( ( ( y i^i ran F ) e. Fin /\ A. x e. ( y i^i ran F ) ( `' F " { x } ) e. dom vol ) -> U_ x e. ( y i^i ran F ) ( `' F " { x } ) e. dom vol ) |
54 |
40 52 53
|
syl2anc |
|- ( ( ph /\ -. 0 e. y ) -> U_ x e. ( y i^i ran F ) ( `' F " { x } ) e. dom vol ) |
55 |
36 54
|
eqeltrrd |
|- ( ( ph /\ -. 0 e. y ) -> ( `' F " y ) e. dom vol ) |
56 |
55
|
ex |
|- ( ph -> ( -. 0 e. y -> ( `' F " y ) e. dom vol ) ) |
57 |
56
|
alrimiv |
|- ( ph -> A. y ( -. 0 e. y -> ( `' F " y ) e. dom vol ) ) |
58 |
57
|
ad2antrr |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> A. y ( -. 0 e. y -> ( `' F " y ) e. dom vol ) ) |
59 |
|
elndif |
|- ( 0 e. x -> -. 0 e. ( RR \ x ) ) |
60 |
59
|
adantl |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> -. 0 e. ( RR \ x ) ) |
61 |
|
reex |
|- RR e. _V |
62 |
61
|
difexi |
|- ( RR \ x ) e. _V |
63 |
|
eleq2 |
|- ( y = ( RR \ x ) -> ( 0 e. y <-> 0 e. ( RR \ x ) ) ) |
64 |
63
|
notbid |
|- ( y = ( RR \ x ) -> ( -. 0 e. y <-> -. 0 e. ( RR \ x ) ) ) |
65 |
|
imaeq2 |
|- ( y = ( RR \ x ) -> ( `' F " y ) = ( `' F " ( RR \ x ) ) ) |
66 |
65
|
eleq1d |
|- ( y = ( RR \ x ) -> ( ( `' F " y ) e. dom vol <-> ( `' F " ( RR \ x ) ) e. dom vol ) ) |
67 |
64 66
|
imbi12d |
|- ( y = ( RR \ x ) -> ( ( -. 0 e. y -> ( `' F " y ) e. dom vol ) <-> ( -. 0 e. ( RR \ x ) -> ( `' F " ( RR \ x ) ) e. dom vol ) ) ) |
68 |
62 67
|
spcv |
|- ( A. y ( -. 0 e. y -> ( `' F " y ) e. dom vol ) -> ( -. 0 e. ( RR \ x ) -> ( `' F " ( RR \ x ) ) e. dom vol ) ) |
69 |
58 60 68
|
sylc |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " ( RR \ x ) ) e. dom vol ) |
70 |
|
difmbl |
|- ( ( ( `' F " RR ) e. dom vol /\ ( `' F " ( RR \ x ) ) e. dom vol ) -> ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) e. dom vol ) |
71 |
23 69 70
|
syl2anc |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) e. dom vol ) |
72 |
19 71
|
eqeltrrd |
|- ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " x ) e. dom vol ) |
73 |
|
eleq2 |
|- ( y = x -> ( 0 e. y <-> 0 e. x ) ) |
74 |
73
|
notbid |
|- ( y = x -> ( -. 0 e. y <-> -. 0 e. x ) ) |
75 |
|
imaeq2 |
|- ( y = x -> ( `' F " y ) = ( `' F " x ) ) |
76 |
75
|
eleq1d |
|- ( y = x -> ( ( `' F " y ) e. dom vol <-> ( `' F " x ) e. dom vol ) ) |
77 |
74 76
|
imbi12d |
|- ( y = x -> ( ( -. 0 e. y -> ( `' F " y ) e. dom vol ) <-> ( -. 0 e. x -> ( `' F " x ) e. dom vol ) ) ) |
78 |
77
|
spvv |
|- ( A. y ( -. 0 e. y -> ( `' F " y ) e. dom vol ) -> ( -. 0 e. x -> ( `' F " x ) e. dom vol ) ) |
79 |
57 78
|
syl |
|- ( ph -> ( -. 0 e. x -> ( `' F " x ) e. dom vol ) ) |
80 |
79
|
imp |
|- ( ( ph /\ -. 0 e. x ) -> ( `' F " x ) e. dom vol ) |
81 |
80
|
adantlr |
|- ( ( ( ph /\ x e. ran (,) ) /\ -. 0 e. x ) -> ( `' F " x ) e. dom vol ) |
82 |
72 81
|
pm2.61dan |
|- ( ( ph /\ x e. ran (,) ) -> ( `' F " x ) e. dom vol ) |
83 |
82
|
ralrimiva |
|- ( ph -> A. x e. ran (,) ( `' F " x ) e. dom vol ) |
84 |
|
ismbf |
|- ( F : RR --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) ) |
85 |
1 84
|
syl |
|- ( ph -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) ) |
86 |
83 85
|
mpbird |
|- ( ph -> F e. MblFn ) |
87 |
|
mblvol |
|- ( ( `' F " y ) e. dom vol -> ( vol ` ( `' F " y ) ) = ( vol* ` ( `' F " y ) ) ) |
88 |
55 87
|
syl |
|- ( ( ph /\ -. 0 e. y ) -> ( vol ` ( `' F " y ) ) = ( vol* ` ( `' F " y ) ) ) |
89 |
|
mblss |
|- ( ( `' F " y ) e. dom vol -> ( `' F " y ) C_ RR ) |
90 |
55 89
|
syl |
|- ( ( ph /\ -. 0 e. y ) -> ( `' F " y ) C_ RR ) |
91 |
|
mblvol |
|- ( ( `' F " { x } ) e. dom vol -> ( vol ` ( `' F " { x } ) ) = ( vol* ` ( `' F " { x } ) ) ) |
92 |
51 91
|
syl |
|- ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( vol ` ( `' F " { x } ) ) = ( vol* ` ( `' F " { x } ) ) ) |
93 |
41 50 4
|
syl2anc |
|- ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( vol ` ( `' F " { x } ) ) e. RR ) |
94 |
92 93
|
eqeltrrd |
|- ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( vol* ` ( `' F " { x } ) ) e. RR ) |
95 |
40 94
|
fsumrecl |
|- ( ( ph /\ -. 0 e. y ) -> sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) e. RR ) |
96 |
36
|
fveq2d |
|- ( ( ph /\ -. 0 e. y ) -> ( vol* ` U_ x e. ( y i^i ran F ) ( `' F " { x } ) ) = ( vol* ` ( `' F " y ) ) ) |
97 |
|
mblss |
|- ( ( `' F " { x } ) e. dom vol -> ( `' F " { x } ) C_ RR ) |
98 |
51 97
|
syl |
|- ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( `' F " { x } ) C_ RR ) |
99 |
98 94
|
jca |
|- ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( ( `' F " { x } ) C_ RR /\ ( vol* ` ( `' F " { x } ) ) e. RR ) ) |
100 |
99
|
ralrimiva |
|- ( ( ph /\ -. 0 e. y ) -> A. x e. ( y i^i ran F ) ( ( `' F " { x } ) C_ RR /\ ( vol* ` ( `' F " { x } ) ) e. RR ) ) |
101 |
|
ovolfiniun |
|- ( ( ( y i^i ran F ) e. Fin /\ A. x e. ( y i^i ran F ) ( ( `' F " { x } ) C_ RR /\ ( vol* ` ( `' F " { x } ) ) e. RR ) ) -> ( vol* ` U_ x e. ( y i^i ran F ) ( `' F " { x } ) ) <_ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) ) |
102 |
40 100 101
|
syl2anc |
|- ( ( ph /\ -. 0 e. y ) -> ( vol* ` U_ x e. ( y i^i ran F ) ( `' F " { x } ) ) <_ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) ) |
103 |
96 102
|
eqbrtrrd |
|- ( ( ph /\ -. 0 e. y ) -> ( vol* ` ( `' F " y ) ) <_ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) ) |
104 |
|
ovollecl |
|- ( ( ( `' F " y ) C_ RR /\ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) e. RR /\ ( vol* ` ( `' F " y ) ) <_ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) ) -> ( vol* ` ( `' F " y ) ) e. RR ) |
105 |
90 95 103 104
|
syl3anc |
|- ( ( ph /\ -. 0 e. y ) -> ( vol* ` ( `' F " y ) ) e. RR ) |
106 |
88 105
|
eqeltrd |
|- ( ( ph /\ -. 0 e. y ) -> ( vol ` ( `' F " y ) ) e. RR ) |
107 |
106
|
ex |
|- ( ph -> ( -. 0 e. y -> ( vol ` ( `' F " y ) ) e. RR ) ) |
108 |
107
|
alrimiv |
|- ( ph -> A. y ( -. 0 e. y -> ( vol ` ( `' F " y ) ) e. RR ) ) |
109 |
|
neldifsn |
|- -. 0 e. ( RR \ { 0 } ) |
110 |
61
|
difexi |
|- ( RR \ { 0 } ) e. _V |
111 |
|
eleq2 |
|- ( y = ( RR \ { 0 } ) -> ( 0 e. y <-> 0 e. ( RR \ { 0 } ) ) ) |
112 |
111
|
notbid |
|- ( y = ( RR \ { 0 } ) -> ( -. 0 e. y <-> -. 0 e. ( RR \ { 0 } ) ) ) |
113 |
|
imaeq2 |
|- ( y = ( RR \ { 0 } ) -> ( `' F " y ) = ( `' F " ( RR \ { 0 } ) ) ) |
114 |
113
|
fveq2d |
|- ( y = ( RR \ { 0 } ) -> ( vol ` ( `' F " y ) ) = ( vol ` ( `' F " ( RR \ { 0 } ) ) ) ) |
115 |
114
|
eleq1d |
|- ( y = ( RR \ { 0 } ) -> ( ( vol ` ( `' F " y ) ) e. RR <-> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) |
116 |
112 115
|
imbi12d |
|- ( y = ( RR \ { 0 } ) -> ( ( -. 0 e. y -> ( vol ` ( `' F " y ) ) e. RR ) <-> ( -. 0 e. ( RR \ { 0 } ) -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) ) |
117 |
110 116
|
spcv |
|- ( A. y ( -. 0 e. y -> ( vol ` ( `' F " y ) ) e. RR ) -> ( -. 0 e. ( RR \ { 0 } ) -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) |
118 |
108 109 117
|
mpisyl |
|- ( ph -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) |
119 |
1 2 118
|
3jca |
|- ( ph -> ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) |
120 |
|
isi1f |
|- ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) ) |
121 |
86 119 120
|
sylanbrc |
|- ( ph -> F e. dom S.1 ) |