Step |
Hyp |
Ref |
Expression |
1 |
|
itg10a.1 |
|- ( ph -> F e. dom S.1 ) |
2 |
|
itg10a.2 |
|- ( ph -> A C_ RR ) |
3 |
|
itg10a.3 |
|- ( ph -> ( vol* ` A ) = 0 ) |
4 |
|
itg1lea.4 |
|- ( ph -> G e. dom S.1 ) |
5 |
|
itg1lea.5 |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) ) |
6 |
|
i1fsub |
|- ( ( G e. dom S.1 /\ F e. dom S.1 ) -> ( G oF - F ) e. dom S.1 ) |
7 |
4 1 6
|
syl2anc |
|- ( ph -> ( G oF - F ) e. dom S.1 ) |
8 |
|
eldifi |
|- ( x e. ( RR \ A ) -> x e. RR ) |
9 |
|
i1ff |
|- ( G e. dom S.1 -> G : RR --> RR ) |
10 |
4 9
|
syl |
|- ( ph -> G : RR --> RR ) |
11 |
10
|
ffvelrnda |
|- ( ( ph /\ x e. RR ) -> ( G ` x ) e. RR ) |
12 |
|
i1ff |
|- ( F e. dom S.1 -> F : RR --> RR ) |
13 |
1 12
|
syl |
|- ( ph -> F : RR --> RR ) |
14 |
13
|
ffvelrnda |
|- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR ) |
15 |
11 14
|
subge0d |
|- ( ( ph /\ x e. RR ) -> ( 0 <_ ( ( G ` x ) - ( F ` x ) ) <-> ( F ` x ) <_ ( G ` x ) ) ) |
16 |
8 15
|
sylan2 |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( 0 <_ ( ( G ` x ) - ( F ` x ) ) <-> ( F ` x ) <_ ( G ` x ) ) ) |
17 |
5 16
|
mpbird |
|- ( ( ph /\ x e. ( RR \ A ) ) -> 0 <_ ( ( G ` x ) - ( F ` x ) ) ) |
18 |
10
|
ffnd |
|- ( ph -> G Fn RR ) |
19 |
13
|
ffnd |
|- ( ph -> F Fn RR ) |
20 |
|
reex |
|- RR e. _V |
21 |
20
|
a1i |
|- ( ph -> RR e. _V ) |
22 |
|
inidm |
|- ( RR i^i RR ) = RR |
23 |
|
eqidd |
|- ( ( ph /\ x e. RR ) -> ( G ` x ) = ( G ` x ) ) |
24 |
|
eqidd |
|- ( ( ph /\ x e. RR ) -> ( F ` x ) = ( F ` x ) ) |
25 |
18 19 21 21 22 23 24
|
ofval |
|- ( ( ph /\ x e. RR ) -> ( ( G oF - F ) ` x ) = ( ( G ` x ) - ( F ` x ) ) ) |
26 |
8 25
|
sylan2 |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( ( G oF - F ) ` x ) = ( ( G ` x ) - ( F ` x ) ) ) |
27 |
17 26
|
breqtrrd |
|- ( ( ph /\ x e. ( RR \ A ) ) -> 0 <_ ( ( G oF - F ) ` x ) ) |
28 |
7 2 3 27
|
itg1ge0a |
|- ( ph -> 0 <_ ( S.1 ` ( G oF - F ) ) ) |
29 |
|
itg1sub |
|- ( ( G e. dom S.1 /\ F e. dom S.1 ) -> ( S.1 ` ( G oF - F ) ) = ( ( S.1 ` G ) - ( S.1 ` F ) ) ) |
30 |
4 1 29
|
syl2anc |
|- ( ph -> ( S.1 ` ( G oF - F ) ) = ( ( S.1 ` G ) - ( S.1 ` F ) ) ) |
31 |
28 30
|
breqtrd |
|- ( ph -> 0 <_ ( ( S.1 ` G ) - ( S.1 ` F ) ) ) |
32 |
|
itg1cl |
|- ( G e. dom S.1 -> ( S.1 ` G ) e. RR ) |
33 |
4 32
|
syl |
|- ( ph -> ( S.1 ` G ) e. RR ) |
34 |
|
itg1cl |
|- ( F e. dom S.1 -> ( S.1 ` F ) e. RR ) |
35 |
1 34
|
syl |
|- ( ph -> ( S.1 ` F ) e. RR ) |
36 |
33 35
|
subge0d |
|- ( ph -> ( 0 <_ ( ( S.1 ` G ) - ( S.1 ` F ) ) <-> ( S.1 ` F ) <_ ( S.1 ` G ) ) ) |
37 |
31 36
|
mpbid |
|- ( ph -> ( S.1 ` F ) <_ ( S.1 ` G ) ) |