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 fvmptelcdm 
 |-  ( ( ( 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 fvmptelcdm 
 |-  ( ( ( 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 ) )