Metamath Proof Explorer

Theorem itgaddlem1

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

Ref Expression
Hypotheses itgadd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgadd.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
itgadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
itgadd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
itgadd.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
itgadd.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
itgadd.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
itgadd.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐶 )
Assertion itgaddlem1 ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgadd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 itgadd.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 itgadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4 itgadd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5 itgadd.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
6 itgadd.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
7 itgadd.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
8 itgadd.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐶 )
9 5 6 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
10 1 2 3 4 ibladd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )
11 5 6 7 8 addge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( 𝐵 + 𝐶 ) )
12 9 10 11 itgposval ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) ) ) )
13 5 2 7 itgposval ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
14 6 4 8 itgposval ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) )
15 13 14 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) ) )
16 5 7 iblpos ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ∈ ℝ ) ) )
17 2 16 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ∈ ℝ ) )
18 17 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
19 18 5 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
20 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
21 19 20 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
22 rembl ⊢ ℝ ∈ dom vol
23 22 a1i ⊢ ( 𝜑 → ℝ ∈ dom vol )
24 elrege0 ⊢ ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
25 5 7 24 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
26 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
27 26 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
28 25 27 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
30 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
32 31 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
33 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
34 33 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
35 34 18 eqeltrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∈ MblFn )
36 21 23 29 32 35 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∈ MblFn )
37 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
38 37 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
39 17 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ∈ ℝ )
40 elrege0 ⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
41 6 8 40 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
42 41 27 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
44 31 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
45 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
46 45 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
47 6 8 iblpos ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) ∈ ℝ ) ) )
48 4 47 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) ∈ ℝ ) )
49 48 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
50 46 49 eqeltrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ∈ MblFn )
51 21 23 43 44 50 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ∈ MblFn )
52 42 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
53 52 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
54 48 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) ∈ ℝ )
55 36 38 39 51 53 54 itg2add ⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) ) )
56 reex ⊢ ℝ ∈ V
57 56 a1i ⊢ ( 𝜑 → ℝ ∈ V )
58 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
59 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) )
60 57 37 52 58 59 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) + if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) )
61 33 45 oveq12d ⊢ ( 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) + if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = ( 𝐵 + 𝐶 ) )
62 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) = ( 𝐵 + 𝐶 ) )
63 61 62 eqtr4d ⊢ ( 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) + if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) )
64 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
65 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
66 64 65 oveq12d ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) + if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = ( 0 + 0 ) )
67 00id ⊢ ( 0 + 0 ) = 0
68 66 67 eqtrdi ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) + if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = 0 )
69 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) = 0 )
70 68 69 eqtr4d ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) + if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) )
71 63 70 pm2.61i ⊢ ( if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) + if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 )
72 71 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) + if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) )
73 60 72 eqtrdi ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) ) )
74 73 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) ) ) )
75 15 55 74 3eqtr2d ⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐵 + 𝐶 ) , 0 ) ) ) )
76 12 75 eqtr4d ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )