Metamath Proof Explorer

Theorem iblsplit

Description: The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iblsplit.1 ⊢φ→vol*⁡A∩B=0
iblsplit.2 ⊢φ→U=A∪B
iblsplit.3 ⊢φ∧x∈U→C∈ℂ
iblsplit.4 ⊢φ→x∈A⟼C∈𝐿1
iblsplit.5 ⊢φ→x∈B⟼C∈𝐿1
Assertion iblsplit ⊢φ→x∈U⟼C∈𝐿1

Proof

Step Hyp Ref Expression
1 iblsplit.1 ⊢φ→vol*⁡A∩B=0
2 iblsplit.2 ⊢φ→U=A∪B
3 iblsplit.3 ⊢φ∧x∈U→C∈ℂ
4 iblsplit.4 ⊢φ→x∈A⟼C∈𝐿1
5 iblsplit.5 ⊢φ→x∈B⟼C∈𝐿1
6 3 fmpttd ⊢φ→x∈U⟼C:U⟶ℂ
7 ssun1 ⊢A⊆A∪B
8 7 2 sseqtrrid ⊢φ→A⊆U
9 8 resmptd ⊢φ→x∈U⟼C↾A=x∈A⟼C
10 eqidd ⊢φ→x∈ℝ⟼ifx∈A∧0≤ℜ⁡Ciyℜ⁡Ciy0=x∈ℝ⟼ifx∈A∧0≤ℜ⁡Ciyℜ⁡Ciy0
11 eqidd ⊢φ∧x∈A→ℜ⁡Ciy=ℜ⁡Ciy
12 8 sseld ⊢φ→x∈A→x∈U
13 12 imdistani ⊢φ∧x∈A→φ∧x∈U
14 13 3 syl ⊢φ∧x∈A→C∈ℂ
15 10 11 14 isibl2 ⊢φ→x∈A⟼C∈𝐿1↔x∈A⟼C∈MblFn∧∀y∈0…3∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Ciyℜ⁡Ciy0∈ℝ
16 4 15 mpbid ⊢φ→x∈A⟼C∈MblFn∧∀y∈0…3∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Ciyℜ⁡Ciy0∈ℝ
17 16 simpld ⊢φ→x∈A⟼C∈MblFn
18 9 17 eqeltrd ⊢φ→x∈U⟼C↾A∈MblFn
19 ssun2 ⊢B⊆A∪B
20 19 2 sseqtrrid ⊢φ→B⊆U
21 20 resmptd ⊢φ→x∈U⟼C↾B=x∈B⟼C
22 eqidd ⊢φ→x∈ℝ⟼ifx∈B∧0≤ℜ⁡Ciyℜ⁡Ciy0=x∈ℝ⟼ifx∈B∧0≤ℜ⁡Ciyℜ⁡Ciy0
23 eqidd ⊢φ∧x∈B→ℜ⁡Ciy=ℜ⁡Ciy
24 20 sseld ⊢φ→x∈B→x∈U
25 24 imdistani ⊢φ∧x∈B→φ∧x∈U
26 25 3 syl ⊢φ∧x∈B→C∈ℂ
27 22 23 26 isibl2 ⊢φ→x∈B⟼C∈𝐿1↔x∈B⟼C∈MblFn∧∀y∈0…3∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Ciyℜ⁡Ciy0∈ℝ
28 5 27 mpbid ⊢φ→x∈B⟼C∈MblFn∧∀y∈0…3∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Ciyℜ⁡Ciy0∈ℝ
29 28 simpld ⊢φ→x∈B⟼C∈MblFn
30 21 29 eqeltrd ⊢φ→x∈U⟼C↾B∈MblFn
31 2 eqcomd ⊢φ→A∪B=U
32 6 18 30 31 mbfres2cn ⊢φ→x∈U⟼C∈MblFn
33 17 14 mbfdm2 ⊢φ→A∈dom⁡vol
34 33 adantr ⊢φ∧k∈0…3→A∈dom⁡vol
35 29 26 mbfdm2 ⊢φ→B∈dom⁡vol
36 35 adantr ⊢φ∧k∈0…3→B∈dom⁡vol
37 1 adantr ⊢φ∧k∈0…3→vol*⁡A∩B=0
38 2 adantr ⊢φ∧k∈0…3→U=A∪B
39 3 adantlr ⊢φ∧k∈0…3∧x∈U→C∈ℂ
40 ax-icn ⊢i∈ℂ
41 40 a1i ⊢k∈0…3→i∈ℂ
42 elfznn0 ⊢k∈0…3→k∈ℕ0
43 41 42 expcld ⊢k∈0…3→ik∈ℂ
44 43 ad2antlr ⊢φ∧k∈0…3∧x∈U→ik∈ℂ
45 40 a1i ⊢φ∧k∈0…3∧x∈U→i∈ℂ
46 ine0 ⊢i≠0
47 46 a1i ⊢φ∧k∈0…3∧x∈U→i≠0
48 elfzelz ⊢k∈0…3→k∈ℤ
49 48 ad2antlr ⊢φ∧k∈0…3∧x∈U→k∈ℤ
50 45 47 49 expne0d ⊢φ∧k∈0…3∧x∈U→ik≠0
51 39 44 50 divcld ⊢φ∧k∈0…3∧x∈U→Cik∈ℂ
52 51 recld ⊢φ∧k∈0…3∧x∈U→ℜ⁡Cik∈ℝ
53 52 rexrd ⊢φ∧k∈0…3∧x∈U→ℜ⁡Cik∈ℝ*
54 53 adantr ⊢φ∧k∈0…3∧x∈U∧0≤ℜ⁡Cik→ℜ⁡Cik∈ℝ*
55 simpr ⊢φ∧k∈0…3∧x∈U∧0≤ℜ⁡Cik→0≤ℜ⁡Cik
56 pnfge ⊢ℜ⁡Cik∈ℝ*→ℜ⁡Cik≤+∞
57 54 56 syl ⊢φ∧k∈0…3∧x∈U∧0≤ℜ⁡Cik→ℜ⁡Cik≤+∞
58 0xr ⊢0∈ℝ*
59 pnfxr ⊢+∞∈ℝ*
60 elicc1 ⊢0∈ℝ*∧+∞∈ℝ*→ℜ⁡Cik∈0+∞↔ℜ⁡Cik∈ℝ*∧0≤ℜ⁡Cik∧ℜ⁡Cik≤+∞
61 58 59 60 mp2an ⊢ℜ⁡Cik∈0+∞↔ℜ⁡Cik∈ℝ*∧0≤ℜ⁡Cik∧ℜ⁡Cik≤+∞
62 54 55 57 61 syl3anbrc ⊢φ∧k∈0…3∧x∈U∧0≤ℜ⁡Cik→ℜ⁡Cik∈0+∞
63 0e0iccpnf ⊢0∈0+∞
64 63 a1i ⊢φ∧k∈0…3∧x∈U∧¬0≤ℜ⁡Cik→0∈0+∞
65 62 64 ifclda ⊢φ∧k∈0…3∧x∈U→if0≤ℜ⁡Cikℜ⁡Cik0∈0+∞
66 eqid ⊢x∈ℝ⟼ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=x∈ℝ⟼ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00
67 eqid ⊢x∈ℝ⟼ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=x∈ℝ⟼ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00
68 ifan ⊢ifx∈U∧0≤ℜ⁡Cikℜ⁡Cik0=ifx∈Uif0≤ℜ⁡Cikℜ⁡Cik00
69 68 mpteq2i ⊢x∈ℝ⟼ifx∈U∧0≤ℜ⁡Cikℜ⁡Cik0=x∈ℝ⟼ifx∈Uif0≤ℜ⁡Cikℜ⁡Cik00
70 ifan ⊢ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0=ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00
71 70 eqcomi ⊢ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
72 71 mpteq2i ⊢x∈ℝ⟼ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
73 72 a1i ⊢φ∧k∈0…3→x∈ℝ⟼ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
74 73 fveq2d ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
75 eqidd ⊢φ→x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0=x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0
76 eqidd ⊢φ∧x∈A→ℜ⁡Cik=ℜ⁡Cik
77 75 76 14 isibl2 ⊢φ→x∈A⟼C∈𝐿1↔x∈A⟼C∈MblFn∧∀k∈0…3∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
78 4 77 mpbid ⊢φ→x∈A⟼C∈MblFn∧∀k∈0…3∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
79 78 simprd ⊢φ→∀k∈0…3∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
80 79 r19.21bi ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
81 74 80 eqeltrd ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00∈ℝ
82 ifan ⊢ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0=ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00
83 82 eqcomi ⊢ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0
84 83 mpteq2i ⊢x∈ℝ⟼ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0
85 84 fveq2i ⊢∫2⁡x∈ℝ⟼ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00=∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0
86 eqidd ⊢φ→x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0=x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0
87 eqidd ⊢φ∧x∈B→ℜ⁡Cik=ℜ⁡Cik
88 86 87 26 isibl2 ⊢φ→x∈B⟼C∈𝐿1↔x∈B⟼C∈MblFn∧∀k∈0…3∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
89 5 88 mpbid ⊢φ→x∈B⟼C∈MblFn∧∀k∈0…3∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
90 89 simprd ⊢φ→∀k∈0…3∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
91 90 r19.21bi ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈B∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
92 85 91 eqeltrid ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00∈ℝ
93 34 36 37 38 65 66 67 69 81 92 itg2split ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈U∧0≤ℜ⁡Cikℜ⁡Cik0=∫2⁡x∈ℝ⟼ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00+∫2⁡x∈ℝ⟼ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00
94 81 92 readdcld ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈Aif0≤ℜ⁡Cikℜ⁡Cik00+∫2⁡x∈ℝ⟼ifx∈Bif0≤ℜ⁡Cikℜ⁡Cik00∈ℝ
95 93 94 eqeltrd ⊢φ∧k∈0…3→∫2⁡x∈ℝ⟼ifx∈U∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
96 95 ralrimiva ⊢φ→∀k∈0…3∫2⁡x∈ℝ⟼ifx∈U∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
97 eqidd ⊢φ→x∈ℝ⟼ifx∈U∧0≤ℜ⁡Cikℜ⁡Cik0=x∈ℝ⟼ifx∈U∧0≤ℜ⁡Cikℜ⁡Cik0
98 eqidd ⊢φ∧x∈U→ℜ⁡Cik=ℜ⁡Cik
99 97 98 3 isibl2 ⊢φ→x∈U⟼C∈𝐿1↔x∈U⟼C∈MblFn∧∀k∈0…3∫2⁡x∈ℝ⟼ifx∈U∧0≤ℜ⁡Cikℜ⁡Cik0∈ℝ
100 32 96 99 mpbir2and ⊢φ→x∈U⟼C∈𝐿1