Metamath Proof Explorer


Theorem itgss3

Description: Expand the set of an integral by a nullset. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses itgss3.1
|- ( ph -> A C_ B )
itgss3.2
|- ( ph -> B C_ RR )
itgss3.3
|- ( ph -> ( vol* ` ( B \ A ) ) = 0 )
itgss3.4
|- ( ( ph /\ x e. B ) -> C e. CC )
Assertion itgss3
|- ( ph -> ( ( ( x e. A |-> C ) e. L^1 <-> ( x e. B |-> C ) e. L^1 ) /\ S. A C _d x = S. B C _d x ) )

Proof

Step Hyp Ref Expression
1 itgss3.1
 |-  ( ph -> A C_ B )
2 itgss3.2
 |-  ( ph -> B C_ RR )
3 itgss3.3
 |-  ( ph -> ( vol* ` ( B \ A ) ) = 0 )
4 itgss3.4
 |-  ( ( ph /\ x e. B ) -> C e. CC )
5 nfcv
 |-  F/_ y if ( x e. A , C , 0 )
6 nfv
 |-  F/ x y e. A
7 nfcsb1v
 |-  F/_ x [_ y / x ]_ C
8 nfcv
 |-  F/_ x 0
9 6 7 8 nfif
 |-  F/_ x if ( y e. A , [_ y / x ]_ C , 0 )
10 eleq1w
 |-  ( x = y -> ( x e. A <-> y e. A ) )
11 csbeq1a
 |-  ( x = y -> C = [_ y / x ]_ C )
12 10 11 ifbieq1d
 |-  ( x = y -> if ( x e. A , C , 0 ) = if ( y e. A , [_ y / x ]_ C , 0 ) )
13 5 9 12 cbvmpt
 |-  ( x e. B |-> if ( x e. A , C , 0 ) ) = ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) )
14 1 adantr
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> A C_ B )
15 nfcv
 |-  F/_ y C
16 15 7 11 cbvmpt
 |-  ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
17 iftrue
 |-  ( y e. A -> if ( y e. A , [_ y / x ]_ C , 0 ) = [_ y / x ]_ C )
18 17 mpteq2ia
 |-  ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) = ( y e. A |-> [_ y / x ]_ C )
19 16 18 eqtr4i
 |-  ( x e. A |-> C ) = ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) )
20 simpr
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> ( x e. A |-> C ) e. L^1 )
21 19 20 eqeltrrid
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. L^1 )
22 iblmbf
 |-  ( ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. L^1 -> ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. MblFn )
23 21 22 syl
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. MblFn )
24 1 sselda
 |-  ( ( ph /\ x e. A ) -> x e. B )
25 24 4 syldan
 |-  ( ( ph /\ x e. A ) -> C e. CC )
26 25 fmpttd
 |-  ( ph -> ( x e. A |-> C ) : A --> CC )
27 26 adantr
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> ( x e. A |-> C ) : A --> CC )
28 19 feq1i
 |-  ( ( x e. A |-> C ) : A --> CC <-> ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) : A --> CC )
29 27 28 sylib
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) : A --> CC )
30 29 fvmptelrn
 |-  ( ( ( ph /\ ( x e. A |-> C ) e. L^1 ) /\ y e. A ) -> if ( y e. A , [_ y / x ]_ C , 0 ) e. CC )
31 23 30 mbfdm2
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> A e. dom vol )
32 undif
 |-  ( A C_ B <-> ( A u. ( B \ A ) ) = B )
33 1 32 sylib
 |-  ( ph -> ( A u. ( B \ A ) ) = B )
34 33 adantr
 |-  ( ( ph /\ A e. dom vol ) -> ( A u. ( B \ A ) ) = B )
35 id
 |-  ( A e. dom vol -> A e. dom vol )
36 2 ssdifssd
 |-  ( ph -> ( B \ A ) C_ RR )
37 nulmbl
 |-  ( ( ( B \ A ) C_ RR /\ ( vol* ` ( B \ A ) ) = 0 ) -> ( B \ A ) e. dom vol )
38 36 3 37 syl2anc
 |-  ( ph -> ( B \ A ) e. dom vol )
39 unmbl
 |-  ( ( A e. dom vol /\ ( B \ A ) e. dom vol ) -> ( A u. ( B \ A ) ) e. dom vol )
40 35 38 39 syl2anr
 |-  ( ( ph /\ A e. dom vol ) -> ( A u. ( B \ A ) ) e. dom vol )
41 34 40 eqeltrrd
 |-  ( ( ph /\ A e. dom vol ) -> B e. dom vol )
42 31 41 syldan
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> B e. dom vol )
43 eldifn
 |-  ( y e. ( B \ A ) -> -. y e. A )
44 43 adantl
 |-  ( ( ( ph /\ ( x e. A |-> C ) e. L^1 ) /\ y e. ( B \ A ) ) -> -. y e. A )
45 44 iffalsed
 |-  ( ( ( ph /\ ( x e. A |-> C ) e. L^1 ) /\ y e. ( B \ A ) ) -> if ( y e. A , [_ y / x ]_ C , 0 ) = 0 )
46 14 42 30 45 21 iblss2
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. L^1 )
47 13 46 eqeltrid
 |-  ( ( ph /\ ( x e. A |-> C ) e. L^1 ) -> ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 )
48 iftrue
 |-  ( x e. A -> if ( x e. A , C , 0 ) = C )
49 48 mpteq2ia
 |-  ( x e. A |-> if ( x e. A , C , 0 ) ) = ( x e. A |-> C )
50 5 9 12 cbvmpt
 |-  ( x e. A |-> if ( x e. A , C , 0 ) ) = ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) )
51 49 50 eqtr3i
 |-  ( x e. A |-> C ) = ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) )
52 1 adantr
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> A C_ B )
53 simpr
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 )
54 13 53 eqeltrrid
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. L^1 )
55 iblmbf
 |-  ( ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. L^1 -> ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. MblFn )
56 54 55 syl
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. MblFn )
57 0cn
 |-  0 e. CC
58 ifcl
 |-  ( ( C e. CC /\ 0 e. CC ) -> if ( x e. A , C , 0 ) e. CC )
59 4 57 58 sylancl
 |-  ( ( ph /\ x e. B ) -> if ( x e. A , C , 0 ) e. CC )
60 59 fmpttd
 |-  ( ph -> ( x e. B |-> if ( x e. A , C , 0 ) ) : B --> CC )
61 13 feq1i
 |-  ( ( x e. B |-> if ( x e. A , C , 0 ) ) : B --> CC <-> ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) : B --> CC )
62 60 61 sylib
 |-  ( ph -> ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) : B --> CC )
63 62 adantr
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> ( y e. B |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) : B --> CC )
64 63 fvmptelrn
 |-  ( ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) /\ y e. B ) -> if ( y e. A , [_ y / x ]_ C , 0 ) e. CC )
65 56 64 mbfdm2
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> B e. dom vol )
66 dfss4
 |-  ( A C_ B <-> ( B \ ( B \ A ) ) = A )
67 1 66 sylib
 |-  ( ph -> ( B \ ( B \ A ) ) = A )
68 67 adantr
 |-  ( ( ph /\ B e. dom vol ) -> ( B \ ( B \ A ) ) = A )
69 id
 |-  ( B e. dom vol -> B e. dom vol )
70 difmbl
 |-  ( ( B e. dom vol /\ ( B \ A ) e. dom vol ) -> ( B \ ( B \ A ) ) e. dom vol )
71 69 38 70 syl2anr
 |-  ( ( ph /\ B e. dom vol ) -> ( B \ ( B \ A ) ) e. dom vol )
72 68 71 eqeltrrd
 |-  ( ( ph /\ B e. dom vol ) -> A e. dom vol )
73 65 72 syldan
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> A e. dom vol )
74 52 73 64 54 iblss
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> ( y e. A |-> if ( y e. A , [_ y / x ]_ C , 0 ) ) e. L^1 )
75 51 74 eqeltrid
 |-  ( ( ph /\ ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) -> ( x e. A |-> C ) e. L^1 )
76 47 75 impbida
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 ) )
77 67 eleq2d
 |-  ( ph -> ( x e. ( B \ ( B \ A ) ) <-> x e. A ) )
78 77 biimpa
 |-  ( ( ph /\ x e. ( B \ ( B \ A ) ) ) -> x e. A )
79 78 48 syl
 |-  ( ( ph /\ x e. ( B \ ( B \ A ) ) ) -> if ( x e. A , C , 0 ) = C )
80 59 4 36 3 79 itgeqa
 |-  ( ph -> ( ( ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 <-> ( x e. B |-> C ) e. L^1 ) /\ S. B if ( x e. A , C , 0 ) _d x = S. B C _d x ) )
81 80 simpld
 |-  ( ph -> ( ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 <-> ( x e. B |-> C ) e. L^1 ) )
82 76 81 bitrd
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( x e. B |-> C ) e. L^1 ) )
83 itgss2
 |-  ( A C_ B -> S. A C _d x = S. B if ( x e. A , C , 0 ) _d x )
84 1 83 syl
 |-  ( ph -> S. A C _d x = S. B if ( x e. A , C , 0 ) _d x )
85 80 simprd
 |-  ( ph -> S. B if ( x e. A , C , 0 ) _d x = S. B C _d x )
86 84 85 eqtrd
 |-  ( ph -> S. A C _d x = S. B C _d x )
87 82 86 jca
 |-  ( ph -> ( ( ( x e. A |-> C ) e. L^1 <-> ( x e. B |-> C ) e. L^1 ) /\ S. A C _d x = S. B C _d x ) )