Metamath Proof Explorer

Theorem iblss2

Description: Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses iblss2.1 ⊢φ→A⊆B
iblss2.2 ⊢φ→B∈dom⁡vol
iblss2.3 ⊢φ∧x∈A→C∈V
iblss2.4 ⊢φ∧x∈B∖A→C=0
iblss2.5 ⊢φ→x∈A⟼C∈𝐿1
Assertion iblss2 ⊢φ→x∈B⟼C∈𝐿1

Proof

Step Hyp Ref Expression
1 iblss2.1 ⊢φ→A⊆B
2 iblss2.2 ⊢φ→B∈dom⁡vol
3 iblss2.3 ⊢φ∧x∈A→C∈V
4 iblss2.4 ⊢φ∧x∈B∖A→C=0
5 iblss2.5 ⊢φ→x∈A⟼C∈𝐿1
6 iblmbf ⊢x∈A⟼C∈𝐿1→x∈A⟼C∈MblFn
7 5 6 syl ⊢φ→x∈A⟼C∈MblFn
8 1 2 3 4 7 mbfss ⊢φ→x∈B⟼C∈MblFn
9 1 adantr ⊢φ∧k∈0…3→A⊆B
10 9 sselda ⊢φ∧k∈0…3∧x∈A→x∈B
11 10 iftrued ⊢φ∧k∈0…3∧x∈A→ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=if0≤ℜ⁡Cikℜ⁡Cik0
12 iftrue ⊢x∈A→ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=if0≤ℜ⁡Cikℜ⁡Cik0
13 12 adantl ⊢φ∧k∈0…3∧x∈A→ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=if0≤ℜ⁡Cikℜ⁡Cik0
14 11 13 eqtr4d ⊢φ∧k∈0…3∧x∈A→ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00
15 ifid ⊢ifx∈B00=0
16 simplll ⊢φ∧k∈0…3∧¬x∈A∧x∈B→φ
17 simpr ⊢φ∧k∈0…3∧¬x∈A∧x∈B→x∈B
18 simplr ⊢φ∧k∈0…3∧¬x∈A∧x∈B→¬x∈A
19 17 18 eldifd ⊢φ∧k∈0…3∧¬x∈A∧x∈B→x∈B∖A
20 16 19 4 syl2anc ⊢φ∧k∈0…3∧¬x∈A∧x∈B→C=0
21 20 oveq1d ⊢φ∧k∈0…3∧¬x∈A∧x∈B→Cik=0ik
22 simpllr ⊢φ∧k∈0…3∧¬x∈A∧x∈B→k∈0…3
23 elfzelz ⊢k∈0…3→k∈ℤ
24 ax-icn ⊢i∈ℂ
25 ine0 ⊢i≠0
26 expclz ⊢i∈ℂ∧i≠0∧k∈ℤ→ik∈ℂ
27 expne0i ⊢i∈ℂ∧i≠0∧k∈ℤ→ik≠0
28 26 27 div0d ⊢i∈ℂ∧i≠0∧k∈ℤ→0ik=0
29 24 25 28 mp3an12 ⊢k∈ℤ→0ik=0
30 22 23 29 3syl ⊢φ∧k∈0…3∧¬x∈A∧x∈B→0ik=0
31 21 30 eqtrd ⊢φ∧k∈0…3∧¬x∈A∧x∈B→Cik=0
32 31 fveq2d ⊢φ∧k∈0…3∧¬x∈A∧x∈B→ℜ⁡Cik=ℜ⁡0
33 re0 ⊢ℜ⁡0=0
34 32 33 eqtrdi ⊢φ∧k∈0…3∧¬x∈A∧x∈B→ℜ⁡Cik=0
35 34 ifeq1d ⊢φ∧k∈0…3∧¬x∈A∧x∈B→if0≤ℜ⁡Cikℜ⁡Cik0=if0≤ℜ⁡Cik00
36 ifid ⊢if0≤ℜ⁡Cik00=0
37 35 36 eqtrdi ⊢φ∧k∈0…3∧¬x∈A∧x∈B→if0≤ℜ⁡Cikℜ⁡Cik0=0
38 37 ifeq1da ⊢φ∧k∈0…3∧¬x∈A→ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=ifx∈B00
39 iffalse ⊢¬x∈A→ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=0
40 39 adantl ⊢φ∧k∈0…3∧¬x∈A→ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=0
41 15 38 40 3eqtr4a ⊢φ∧k∈0…3∧¬x∈A→ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00
42 14 41 pm2.61dan ⊢φ∧k∈0…3→ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00
43 ifan ⊢ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0=ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00
44 ifan ⊢ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0=ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00
45 42 43 44 3eqtr4g ⊢φ∧k∈0…3→ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0=ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
46 45 mpteq2dv ⊢φ∧k∈0…3→x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0=x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
47 46 fveq2d ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
48 eqidd ⊢φ→x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0=x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
49 eqidd ⊢φ∧x∈A→ℜ⁡Cik=ℜ⁡Cik
50 48 49 5 3 iblitg ⊢φ∧k∈ℤ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
51 23 50 sylan2 ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
52 47 51 eqeltrd ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
53 52 ralrimiva ⊢φ→∀k∈0…3∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
54 eqidd ⊢φ→x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0=x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0
55 eqidd ⊢φ∧x∈B→ℜ⁡Cik=ℜ⁡Cik
56 elun ⊢x∈A∪B∖A↔x∈A∨x∈B∖A
57 undif2 ⊢A∪B∖A=A∪B
58 ssequn1 ⊢A⊆B↔A∪B=B
59 1 58 sylib ⊢φ→A∪B=B
60 57 59 eqtrid ⊢φ→A∪B∖A=B
61 60 eleq2d ⊢φ→x∈A∪B∖A↔x∈B
62 56 61 bitr3id ⊢φ→x∈A∨x∈B∖A↔x∈B
63 62 biimpar ⊢φ∧x∈B→x∈A∨x∈B∖A
64 7 3 mbfmptcl ⊢φ∧x∈A→C∈ℂ
65 0cn ⊢0∈ℂ
66 4 65 eqeltrdi ⊢φ∧x∈B∖A→C∈ℂ
67 64 66 jaodan ⊢φ∧x∈A∨x∈B∖A→C∈ℂ
68 63 67 syldan ⊢φ∧x∈B→C∈ℂ
69 54 55 68 isibl2 ⊢φ→x∈B⟼C∈𝐿1↔x∈B⟼C∈MblFn∧∀k∈0…3∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
70 8 53 69 mpbir2and ⊢φ→x∈B⟼C∈𝐿1