Metamath Proof Explorer

Theorem itgaddnclem1

Description: Lemma for itgaddnc ; cf. itgaddlem1 . (Contributed by Brendan Leahy, 7-Nov-2017)

Ref Expression
Hypotheses ibladdnc.1 ⊢φ∧x∈A→B∈V
ibladdnc.2 ⊢φ→x∈A⟼B∈𝐿1
ibladdnc.3 ⊢φ∧x∈A→C∈V
ibladdnc.4 ⊢φ→x∈A⟼C∈𝐿1
ibladdnc.m ⊢φ→x∈A⟼B+C∈MblFn
itgaddnclem.1 ⊢φ∧x∈A→B∈ℝ
itgaddnclem.2 ⊢φ∧x∈A→C∈ℝ
itgaddnclem.3 ⊢φ∧x∈A→0≤B
itgaddnclem.4 ⊢φ∧x∈A→0≤C
Assertion itgaddnclem1 ⊢φ→∫AB+Cdx=∫ABdx+∫ACdx

Proof

Step Hyp Ref Expression
1 ibladdnc.1 ⊢φ∧x∈A→B∈V
2 ibladdnc.2 ⊢φ→x∈A⟼B∈𝐿1
3 ibladdnc.3 ⊢φ∧x∈A→C∈V
4 ibladdnc.4 ⊢φ→x∈A⟼C∈𝐿1
5 ibladdnc.m ⊢φ→x∈A⟼B+C∈MblFn
6 itgaddnclem.1 ⊢φ∧x∈A→B∈ℝ
7 itgaddnclem.2 ⊢φ∧x∈A→C∈ℝ
8 itgaddnclem.3 ⊢φ∧x∈A→0≤B
9 itgaddnclem.4 ⊢φ∧x∈A→0≤C
10 6 7 readdcld ⊢φ∧x∈A→B+C∈ℝ
11 1 2 3 4 5 ibladdnc ⊢φ→x∈A⟼B+C∈𝐿1
12 6 7 8 9 addge0d ⊢φ∧x∈A→0≤B+C
13 10 11 12 itgposval ⊢φ→∫AB+Cdx=∫2⁡x∈ℝ⟼ifx∈AB+C0
14 6 2 8 itgposval ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈AB0
15 7 4 9 itgposval ⊢φ→∫ACdx=∫2⁡x∈ℝ⟼ifx∈AC0
16 14 15 oveq12d ⊢φ→∫ABdx+∫ACdx=∫2⁡x∈ℝ⟼ifx∈AB0+∫2⁡x∈ℝ⟼ifx∈AC0
17 iblmbf ⊢x∈A⟼B∈𝐿1→x∈A⟼B∈MblFn
18 2 17 syl ⊢φ→x∈A⟼B∈MblFn
19 18 1 mbfdm2 ⊢φ→A∈dom⁡vol
20 mblss ⊢A∈dom⁡vol→A⊆ℝ
21 19 20 syl ⊢φ→A⊆ℝ
22 rembl ⊢ℝ∈dom⁡vol
23 22 a1i ⊢φ→ℝ∈dom⁡vol
24 elrege0 ⊢B∈0+∞↔B∈ℝ∧0≤B
25 6 8 24 sylanbrc ⊢φ∧x∈A→B∈0+∞
26 0e0icopnf ⊢0∈0+∞
27 26 a1i ⊢φ∧¬x∈A→0∈0+∞
28 25 27 ifclda ⊢φ→ifx∈AB0∈0+∞
29 28 adantr ⊢φ∧x∈A→ifx∈AB0∈0+∞
30 eldifn ⊢x∈ℝ∖A→¬x∈A
31 30 adantl ⊢φ∧x∈ℝ∖A→¬x∈A
32 iffalse ⊢¬x∈A→ifx∈AB0=0
33 31 32 syl ⊢φ∧x∈ℝ∖A→ifx∈AB0=0
34 iftrue ⊢x∈A→ifx∈AB0=B
35 34 mpteq2ia ⊢x∈A⟼ifx∈AB0=x∈A⟼B
36 35 18 eqeltrid ⊢φ→x∈A⟼ifx∈AB0∈MblFn
37 21 23 29 33 36 mbfss ⊢φ→x∈ℝ⟼ifx∈AB0∈MblFn
38 28 adantr ⊢φ∧x∈ℝ→ifx∈AB0∈0+∞
39 38 fmpttd ⊢φ→x∈ℝ⟼ifx∈AB0:ℝ⟶0+∞
40 6 8 iblpos ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
41 2 40 mpbid ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
42 41 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
43 elrege0 ⊢C∈0+∞↔C∈ℝ∧0≤C
44 7 9 43 sylanbrc ⊢φ∧x∈A→C∈0+∞
45 44 27 ifclda ⊢φ→ifx∈AC0∈0+∞
46 45 adantr ⊢φ∧x∈ℝ→ifx∈AC0∈0+∞
47 46 fmpttd ⊢φ→x∈ℝ⟼ifx∈AC0:ℝ⟶0+∞
48 7 9 iblpos ⊢φ→x∈A⟼C∈𝐿1↔x∈A⟼C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AC0∈ℝ
49 4 48 mpbid ⊢φ→x∈A⟼C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AC0∈ℝ
50 49 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈AC0∈ℝ
51 37 39 42 47 50 itg2addnc ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0+fx∈ℝ⟼ifx∈AC0=∫2⁡x∈ℝ⟼ifx∈AB0+∫2⁡x∈ℝ⟼ifx∈AC0
52 reex ⊢ℝ∈V
53 52 a1i ⊢φ→ℝ∈V
54 eqidd ⊢φ→x∈ℝ⟼ifx∈AB0=x∈ℝ⟼ifx∈AB0
55 eqidd ⊢φ→x∈ℝ⟼ifx∈AC0=x∈ℝ⟼ifx∈AC0
56 53 38 46 54 55 offval2 ⊢φ→x∈ℝ⟼ifx∈AB0+fx∈ℝ⟼ifx∈AC0=x∈ℝ⟼ifx∈AB0+ifx∈AC0
57 iftrue ⊢x∈A→ifx∈AC0=C
58 34 57 oveq12d ⊢x∈A→ifx∈AB0+ifx∈AC0=B+C
59 iftrue ⊢x∈A→ifx∈AB+C0=B+C
60 58 59 eqtr4d ⊢x∈A→ifx∈AB0+ifx∈AC0=ifx∈AB+C0
61 iffalse ⊢¬x∈A→ifx∈AC0=0
62 32 61 oveq12d ⊢¬x∈A→ifx∈AB0+ifx∈AC0=0+0
63 00id ⊢0+0=0
64 62 63 eqtrdi ⊢¬x∈A→ifx∈AB0+ifx∈AC0=0
65 iffalse ⊢¬x∈A→ifx∈AB+C0=0
66 64 65 eqtr4d ⊢¬x∈A→ifx∈AB0+ifx∈AC0=ifx∈AB+C0
67 60 66 pm2.61i ⊢ifx∈AB0+ifx∈AC0=ifx∈AB+C0
68 67 mpteq2i ⊢x∈ℝ⟼ifx∈AB0+ifx∈AC0=x∈ℝ⟼ifx∈AB+C0
69 56 68 eqtrdi ⊢φ→x∈ℝ⟼ifx∈AB0+fx∈ℝ⟼ifx∈AC0=x∈ℝ⟼ifx∈AB+C0
70 69 fveq2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0+fx∈ℝ⟼ifx∈AC0=∫2⁡x∈ℝ⟼ifx∈AB+C0
71 16 51 70 3eqtr2d ⊢φ→∫ABdx+∫ACdx=∫2⁡x∈ℝ⟼ifx∈AB+C0
72 13 71 eqtr4d ⊢φ→∫AB+Cdx=∫ABdx+∫ACdx