Metamath Proof Explorer

Theorem itgaddlem1

Description: Lemma for itgadd . (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itgadd.1 ⊢φ∧x∈A→B∈V
itgadd.2 ⊢φ→x∈A⟼B∈𝐿1
itgadd.3 ⊢φ∧x∈A→C∈V
itgadd.4 ⊢φ→x∈A⟼C∈𝐿1
itgadd.5 ⊢φ∧x∈A→B∈ℝ
itgadd.6 ⊢φ∧x∈A→C∈ℝ
itgadd.7 ⊢φ∧x∈A→0≤B
itgadd.8 ⊢φ∧x∈A→0≤C
Assertion itgaddlem1 ⊢φ→∫AB+Cdx=∫ABdx+∫ACdx

Proof

Step Hyp Ref Expression
1 itgadd.1 ⊢φ∧x∈A→B∈V
2 itgadd.2 ⊢φ→x∈A⟼B∈𝐿1
3 itgadd.3 ⊢φ∧x∈A→C∈V
4 itgadd.4 ⊢φ→x∈A⟼C∈𝐿1
5 itgadd.5 ⊢φ∧x∈A→B∈ℝ
6 itgadd.6 ⊢φ∧x∈A→C∈ℝ
7 itgadd.7 ⊢φ∧x∈A→0≤B
8 itgadd.8 ⊢φ∧x∈A→0≤C
9 5 6 readdcld ⊢φ∧x∈A→B+C∈ℝ
10 1 2 3 4 ibladd ⊢φ→x∈A⟼B+C∈𝐿1
11 5 6 7 8 addge0d ⊢φ∧x∈A→0≤B+C
12 9 10 11 itgposval ⊢φ→∫AB+Cdx=∫2⁡x∈ℝ⟼ifx∈AB+C0
13 5 2 7 itgposval ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈AB0
14 6 4 8 itgposval ⊢φ→∫ACdx=∫2⁡x∈ℝ⟼ifx∈AC0
15 13 14 oveq12d ⊢φ→∫ABdx+∫ACdx=∫2⁡x∈ℝ⟼ifx∈AB0+∫2⁡x∈ℝ⟼ifx∈AC0
16 5 7 iblpos ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
17 2 16 mpbid ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
18 17 simpld ⊢φ→x∈A⟼B∈MblFn
19 18 5 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 5 7 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 31 iffalsed ⊢φ∧x∈ℝ∖A→ifx∈AB0=0
33 iftrue ⊢x∈A→ifx∈AB0=B
34 33 mpteq2ia ⊢x∈A⟼ifx∈AB0=x∈A⟼B
35 34 18 eqeltrid ⊢φ→x∈A⟼ifx∈AB0∈MblFn
36 21 23 29 32 35 mbfss ⊢φ→x∈ℝ⟼ifx∈AB0∈MblFn
37 28 adantr ⊢φ∧x∈ℝ→ifx∈AB0∈0+∞
38 37 fmpttd ⊢φ→x∈ℝ⟼ifx∈AB0:ℝ⟶0+∞
39 17 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
40 elrege0 ⊢C∈0+∞↔C∈ℝ∧0≤C
41 6 8 40 sylanbrc ⊢φ∧x∈A→C∈0+∞
42 41 27 ifclda ⊢φ→ifx∈AC0∈0+∞
43 42 adantr ⊢φ∧x∈A→ifx∈AC0∈0+∞
44 31 iffalsed ⊢φ∧x∈ℝ∖A→ifx∈AC0=0
45 iftrue ⊢x∈A→ifx∈AC0=C
46 45 mpteq2ia ⊢x∈A⟼ifx∈AC0=x∈A⟼C
47 6 8 iblpos ⊢φ→x∈A⟼C∈𝐿1↔x∈A⟼C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AC0∈ℝ
48 4 47 mpbid ⊢φ→x∈A⟼C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AC0∈ℝ
49 48 simpld ⊢φ→x∈A⟼C∈MblFn
50 46 49 eqeltrid ⊢φ→x∈A⟼ifx∈AC0∈MblFn
51 21 23 43 44 50 mbfss ⊢φ→x∈ℝ⟼ifx∈AC0∈MblFn
52 42 adantr ⊢φ∧x∈ℝ→ifx∈AC0∈0+∞
53 52 fmpttd ⊢φ→x∈ℝ⟼ifx∈AC0:ℝ⟶0+∞
54 48 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈AC0∈ℝ
55 36 38 39 51 53 54 itg2add ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0+fx∈ℝ⟼ifx∈AC0=∫2⁡x∈ℝ⟼ifx∈AB0+∫2⁡x∈ℝ⟼ifx∈AC0
56 reex ⊢ℝ∈V
57 56 a1i ⊢φ→ℝ∈V
58 eqidd ⊢φ→x∈ℝ⟼ifx∈AB0=x∈ℝ⟼ifx∈AB0
59 eqidd ⊢φ→x∈ℝ⟼ifx∈AC0=x∈ℝ⟼ifx∈AC0
60 57 37 52 58 59 offval2 ⊢φ→x∈ℝ⟼ifx∈AB0+fx∈ℝ⟼ifx∈AC0=x∈ℝ⟼ifx∈AB0+ifx∈AC0
61 33 45 oveq12d ⊢x∈A→ifx∈AB0+ifx∈AC0=B+C
62 iftrue ⊢x∈A→ifx∈AB+C0=B+C
63 61 62 eqtr4d ⊢x∈A→ifx∈AB0+ifx∈AC0=ifx∈AB+C0
64 iffalse ⊢¬x∈A→ifx∈AB0=0
65 iffalse ⊢¬x∈A→ifx∈AC0=0
66 64 65 oveq12d ⊢¬x∈A→ifx∈AB0+ifx∈AC0=0+0
67 00id ⊢0+0=0
68 66 67 eqtrdi ⊢¬x∈A→ifx∈AB0+ifx∈AC0=0
69 iffalse ⊢¬x∈A→ifx∈AB+C0=0
70 68 69 eqtr4d ⊢¬x∈A→ifx∈AB0+ifx∈AC0=ifx∈AB+C0
71 63 70 pm2.61i ⊢ifx∈AB0+ifx∈AC0=ifx∈AB+C0
72 71 mpteq2i ⊢x∈ℝ⟼ifx∈AB0+ifx∈AC0=x∈ℝ⟼ifx∈AB+C0
73 60 72 eqtrdi ⊢φ→x∈ℝ⟼ifx∈AB0+fx∈ℝ⟼ifx∈AC0=x∈ℝ⟼ifx∈AB+C0
74 73 fveq2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0+fx∈ℝ⟼ifx∈AC0=∫2⁡x∈ℝ⟼ifx∈AB+C0
75 15 55 74 3eqtr2d ⊢φ→∫ABdx+∫ACdx=∫2⁡x∈ℝ⟼ifx∈AB+C0
76 12 75 eqtr4d ⊢φ→∫AB+Cdx=∫ABdx+∫ACdx