Theorem itg2eqa

Description: Approximate equality of integrals. If F = G for almost all x , then S.2 F = S.2 G . (Contributed by Mario Carneiro, 12-Aug-2014)

	Ref	Expression
Hypotheses	itg2lea.1	|- ( ph -> F : RR --> ( 0 [,] +oo ) )
	itg2lea.2	|- ( ph -> G : RR --> ( 0 [,] +oo ) )
	itg2lea.3	|- ( ph -> A C_ RR )
	itg2lea.4	|- ( ph -> ( vol* ` A ) = 0 )
	itg2eqa.5	|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) = ( G ` x ) )
Assertion	itg2eqa	|- ( ph -> ( S.2 ` F ) = ( S.2 ` G ) )

Proof

Step	Hyp	Ref	Expression
1		itg2lea.1	|- ( ph -> F : RR --> ( 0 [,] +oo ) )
2		itg2lea.2	|- ( ph -> G : RR --> ( 0 [,] +oo ) )
3		itg2lea.3	|- ( ph -> A C_ RR )
4		itg2lea.4	|- ( ph -> ( vol* ` A ) = 0 )
5		itg2eqa.5	|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) = ( G ` x ) )
6		itg2cl	|- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
7	1 6	syl	|- ( ph -> ( S.2 ` F ) e. RR* )
8		itg2cl	|- ( G : RR --> ( 0 [,] +oo ) -> ( S.2 ` G ) e. RR* )
9	2 8	syl	|- ( ph -> ( S.2 ` G ) e. RR* )
10		iccssxr	|- ( 0 [,] +oo ) C_ RR*
11		eldifi	|- ( x e. ( RR \ A ) -> x e. RR )
12		ffvelcdm	|- ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,] +oo ) )
13	1 11 12	syl2an	|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) e. ( 0 [,] +oo ) )
14	10 13	sselid	|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) e. RR* )
15	14	xrleidd	|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( F ` x ) )
16	15 5	breqtrd	|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) )
17	1 2 3 4 16	itg2lea	|- ( ph -> ( S.2 ` F ) <_ ( S.2 ` G ) )
18	5 15	eqbrtrrd	|- ( ( ph /\ x e. ( RR \ A ) ) -> ( G ` x ) <_ ( F ` x ) )
19	2 1 3 4 18	itg2lea	|- ( ph -> ( S.2 ` G ) <_ ( S.2 ` F ) )
20	7 9 17 19	xrletrid	|- ( ph -> ( S.2 ` F ) = ( S.2 ` G ) )