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 𝑥 ) )