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 ⊢φ→A⊆B
itgss3.2 ⊢φ→B⊆ℝ
itgss3.3 ⊢φ→vol*⁡B∖A=0
itgss3.4 ⊢φ∧x∈B→C∈ℂ
Assertion itgss3 ⊢φ→x∈A⟼C∈𝐿1↔x∈B⟼C∈𝐿1∧∫ACdx=∫BCdx

Proof

Step Hyp Ref Expression
1 itgss3.1 ⊢φ→A⊆B
2 itgss3.2 ⊢φ→B⊆ℝ
3 itgss3.3 ⊢φ→vol*⁡B∖A=0
4 itgss3.4 ⊢φ∧x∈B→C∈ℂ
5 nfcv ⊢Ⅎ_yifx∈AC0
6 nfv ⊢Ⅎxy∈A
7 nfcsb1v ⊢Ⅎ_x⦋y/x⦌C
8 nfcv ⊢Ⅎ_x0
9 6 7 8 nfif ⊢Ⅎ_xify∈A⦋y/x⦌C0
10 eleq1w ⊢x=y→x∈A↔y∈A
11 csbeq1a ⊢x=y→C=⦋y/x⦌C
12 10 11 ifbieq1d ⊢x=y→ifx∈AC0=ify∈A⦋y/x⦌C0
13 5 9 12 cbvmpt ⊢x∈B⟼ifx∈AC0=y∈B⟼ify∈A⦋y/x⦌C0
14 1 adantr ⊢φ∧x∈A⟼C∈𝐿1→A⊆B
15 nfcv ⊢Ⅎ_yC
16 15 7 11 cbvmpt ⊢x∈A⟼C=y∈A⟼⦋y/x⦌C
17 iftrue ⊢y∈A→ify∈A⦋y/x⦌C0=⦋y/x⦌C
18 17 mpteq2ia ⊢y∈A⟼ify∈A⦋y/x⦌C0=y∈A⟼⦋y/x⦌C
19 16 18 eqtr4i ⊢x∈A⟼C=y∈A⟼ify∈A⦋y/x⦌C0
20 simpr ⊢φ∧x∈A⟼C∈𝐿1→x∈A⟼C∈𝐿1
21 19 20 eqeltrrid ⊢φ∧x∈A⟼C∈𝐿1→y∈A⟼ify∈A⦋y/x⦌C0∈𝐿1
22 iblmbf ⊢y∈A⟼ify∈A⦋y/x⦌C0∈𝐿1→y∈A⟼ify∈A⦋y/x⦌C0∈MblFn
23 21 22 syl ⊢φ∧x∈A⟼C∈𝐿1→y∈A⟼ify∈A⦋y/x⦌C0∈MblFn
24 1 sselda ⊢φ∧x∈A→x∈B
25 24 4 syldan ⊢φ∧x∈A→C∈ℂ
26 25 fmpttd ⊢φ→x∈A⟼C:A⟶ℂ
27 26 adantr ⊢φ∧x∈A⟼C∈𝐿1→x∈A⟼C:A⟶ℂ
28 19 feq1i ⊢x∈A⟼C:A⟶ℂ↔y∈A⟼ify∈A⦋y/x⦌C0:A⟶ℂ
29 27 28 sylib ⊢φ∧x∈A⟼C∈𝐿1→y∈A⟼ify∈A⦋y/x⦌C0:A⟶ℂ
30 29 fvmptelcdm ⊢φ∧x∈A⟼C∈𝐿1∧y∈A→ify∈A⦋y/x⦌C0∈ℂ
31 23 30 mbfdm2 ⊢φ∧x∈A⟼C∈𝐿1→A∈dom⁡vol
32 undif ⊢A⊆B↔A∪B∖A=B
33 1 32 sylib ⊢φ→A∪B∖A=B
34 33 adantr ⊢φ∧A∈dom⁡vol→A∪B∖A=B
35 id ⊢A∈dom⁡vol→A∈dom⁡vol
36 2 ssdifssd ⊢φ→B∖A⊆ℝ
37 nulmbl ⊢B∖A⊆ℝ∧vol*⁡B∖A=0→B∖A∈dom⁡vol
38 36 3 37 syl2anc ⊢φ→B∖A∈dom⁡vol
39 unmbl ⊢A∈dom⁡vol∧B∖A∈dom⁡vol→A∪B∖A∈dom⁡vol
40 35 38 39 syl2anr ⊢φ∧A∈dom⁡vol→A∪B∖A∈dom⁡vol
41 34 40 eqeltrrd ⊢φ∧A∈dom⁡vol→B∈dom⁡vol
42 31 41 syldan ⊢φ∧x∈A⟼C∈𝐿1→B∈dom⁡vol
43 eldifn ⊢y∈B∖A→¬y∈A
44 43 adantl ⊢φ∧x∈A⟼C∈𝐿1∧y∈B∖A→¬y∈A
45 44 iffalsed ⊢φ∧x∈A⟼C∈𝐿1∧y∈B∖A→ify∈A⦋y/x⦌C0=0
46 14 42 30 45 21 iblss2 ⊢φ∧x∈A⟼C∈𝐿1→y∈B⟼ify∈A⦋y/x⦌C0∈𝐿1
47 13 46 eqeltrid ⊢φ∧x∈A⟼C∈𝐿1→x∈B⟼ifx∈AC0∈𝐿1
48 iftrue ⊢x∈A→ifx∈AC0=C
49 48 mpteq2ia ⊢x∈A⟼ifx∈AC0=x∈A⟼C
50 5 9 12 cbvmpt ⊢x∈A⟼ifx∈AC0=y∈A⟼ify∈A⦋y/x⦌C0
51 49 50 eqtr3i ⊢x∈A⟼C=y∈A⟼ify∈A⦋y/x⦌C0
52 1 adantr ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→A⊆B
53 simpr ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→x∈B⟼ifx∈AC0∈𝐿1
54 13 53 eqeltrrid ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→y∈B⟼ify∈A⦋y/x⦌C0∈𝐿1
55 iblmbf ⊢y∈B⟼ify∈A⦋y/x⦌C0∈𝐿1→y∈B⟼ify∈A⦋y/x⦌C0∈MblFn
56 54 55 syl ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→y∈B⟼ify∈A⦋y/x⦌C0∈MblFn
57 0cn ⊢0∈ℂ
58 ifcl ⊢C∈ℂ∧0∈ℂ→ifx∈AC0∈ℂ
59 4 57 58 sylancl ⊢φ∧x∈B→ifx∈AC0∈ℂ
60 59 fmpttd ⊢φ→x∈B⟼ifx∈AC0:B⟶ℂ
61 13 feq1i ⊢x∈B⟼ifx∈AC0:B⟶ℂ↔y∈B⟼ify∈A⦋y/x⦌C0:B⟶ℂ
62 60 61 sylib ⊢φ→y∈B⟼ify∈A⦋y/x⦌C0:B⟶ℂ
63 62 adantr ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→y∈B⟼ify∈A⦋y/x⦌C0:B⟶ℂ
64 63 fvmptelcdm ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1∧y∈B→ify∈A⦋y/x⦌C0∈ℂ
65 56 64 mbfdm2 ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→B∈dom⁡vol
66 dfss4 ⊢A⊆B↔B∖B∖A=A
67 1 66 sylib ⊢φ→B∖B∖A=A
68 67 adantr ⊢φ∧B∈dom⁡vol→B∖B∖A=A
69 id ⊢B∈dom⁡vol→B∈dom⁡vol
70 difmbl ⊢B∈dom⁡vol∧B∖A∈dom⁡vol→B∖B∖A∈dom⁡vol
71 69 38 70 syl2anr ⊢φ∧B∈dom⁡vol→B∖B∖A∈dom⁡vol
72 68 71 eqeltrrd ⊢φ∧B∈dom⁡vol→A∈dom⁡vol
73 65 72 syldan ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→A∈dom⁡vol
74 52 73 64 54 iblss ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→y∈A⟼ify∈A⦋y/x⦌C0∈𝐿1
75 51 74 eqeltrid ⊢φ∧x∈B⟼ifx∈AC0∈𝐿1→x∈A⟼C∈𝐿1
76 47 75 impbida ⊢φ→x∈A⟼C∈𝐿1↔x∈B⟼ifx∈AC0∈𝐿1
77 67 eleq2d ⊢φ→x∈B∖B∖A↔x∈A
78 77 biimpa ⊢φ∧x∈B∖B∖A→x∈A
79 78 48 syl ⊢φ∧x∈B∖B∖A→ifx∈AC0=C
80 59 4 36 3 79 itgeqa ⊢φ→x∈B⟼ifx∈AC0∈𝐿1↔x∈B⟼C∈𝐿1∧∫Bifx∈AC0dx=∫BCdx
81 80 simpld ⊢φ→x∈B⟼ifx∈AC0∈𝐿1↔x∈B⟼C∈𝐿1
82 76 81 bitrd ⊢φ→x∈A⟼C∈𝐿1↔x∈B⟼C∈𝐿1
83 itgss2 ⊢A⊆B→∫ACdx=∫Bifx∈AC0dx
84 1 83 syl ⊢φ→∫ACdx=∫Bifx∈AC0dx
85 80 simprd ⊢φ→∫Bifx∈AC0dx=∫BCdx
86 84 85 eqtrd ⊢φ→∫ACdx=∫BCdx
87 82 86 jca ⊢φ→x∈A⟼C∈𝐿1↔x∈B⟼C∈𝐿1∧∫ACdx=∫BCdx