Proof of Theorem itgaddlem1
Step | Hyp | Ref
| Expression |
1 | | itgadd.5 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
2 | | itgadd.6 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
3 | 1, 2 | readdcld 9948 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ) |
4 | | itgadd.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
5 | | itgadd.2 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
6 | | itgadd.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
7 | | itgadd.4 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) |
8 | 4, 5, 6, 7 | ibladd 23393 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈
𝐿1) |
9 | | itgadd.7 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) |
10 | | itgadd.8 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐶) |
11 | 1, 2, 9, 10 | addge0d 10482 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (𝐵 + 𝐶)) |
12 | 3, 8, 11 | itgposval 23368 |
. 2
⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)))) |
13 | 1, 5, 9 | itgposval 23368 |
. . . 4
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) |
14 | 2, 7, 10 | itgposval 23368 |
. . . 4
⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)))) |
15 | 13, 14 | oveq12d 6567 |
. . 3
⊢ (𝜑 → (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))))) |
16 | 1, 9 | iblpos 23365 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) ∈ ℝ))) |
17 | 5, 16 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) ∈ ℝ)) |
18 | 17 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
19 | 18, 1 | mbfdm2 23211 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom vol) |
20 | | mblss 23106 |
. . . . . 6
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
22 | | rembl 23115 |
. . . . . 6
⊢ ℝ
∈ dom vol |
23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈ dom
vol) |
24 | | elrege0 12149 |
. . . . . . . 8
⊢ (𝐵 ∈ (0[,)+∞) ↔
(𝐵 ∈ ℝ ∧ 0
≤ 𝐵)) |
25 | 1, 9, 24 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) |
26 | | 0e0icopnf 12153 |
. . . . . . . 8
⊢ 0 ∈
(0[,)+∞) |
27 | 26 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
28 | 25, 27 | ifclda 4070 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,)+∞)) |
29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,)+∞)) |
30 | | eldifn 3695 |
. . . . . . 7
⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴) |
31 | 30 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴) |
32 | 31 | iffalsed 4047 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if(𝑥 ∈ 𝐴, 𝐵, 0) = 0) |
33 | | iftrue 4042 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐵, 0) = 𝐵) |
34 | 33 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
35 | 34, 18 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∈ MblFn) |
36 | 21, 23, 29, 32, 35 | mbfss 23219 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∈ MblFn) |
37 | 28 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,)+∞)) |
38 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
39 | 37, 38 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵,
0)):ℝ⟶(0[,)+∞)) |
40 | 17 | simprd 478 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) ∈ ℝ) |
41 | | elrege0 12149 |
. . . . . . . 8
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 ∈ ℝ ∧ 0
≤ 𝐶)) |
42 | 2, 10, 41 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞)) |
43 | 42, 27 | ifclda 4070 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,)+∞)) |
44 | 43 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,)+∞)) |
45 | 31 | iffalsed 4047 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
46 | | iftrue 4042 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
47 | 46 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
48 | 2, 10 | iblpos 23365 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐶, 0))) ∈ ℝ))) |
49 | 7, 48 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐶, 0))) ∈ ℝ)) |
50 | 49 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
51 | 47, 50 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ MblFn) |
52 | 21, 23, 44, 45, 51 | mbfss 23219 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) ∈ MblFn) |
53 | 43 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,)+∞)) |
54 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
55 | 53, 54 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶,
0)):ℝ⟶(0[,)+∞)) |
56 | 49 | simprd 478 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐶, 0))) ∈ ℝ) |
57 | 36, 39, 40, 52, 55, 56 | itg2add 23332 |
. . 3
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))))) |
58 | | reex 9906 |
. . . . . . 7
⊢ ℝ
∈ V |
59 | 58 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈
V) |
60 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
61 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
62 | 59, 37, 53, 60, 61 | offval2 6812 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)))) |
63 | 33, 46 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝐵 + 𝐶)) |
64 | | iftrue 4042 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0) = (𝐵 + 𝐶)) |
65 | 63, 64 | eqtr4d 2647 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)) |
66 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐵, 0) = 0) |
67 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
68 | 66, 67 | oveq12d 6567 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = (0 + 0)) |
69 | | 00id 10090 |
. . . . . . . . 9
⊢ (0 + 0) =
0 |
70 | 68, 69 | syl6eq 2660 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = 0) |
71 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0) = 0) |
72 | 70, 71 | eqtr4d 2647 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)) |
73 | 65, 72 | pm2.61i 175 |
. . . . . 6
⊢ (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0) |
74 | 73 | mpteq2i 4669 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)) |
75 | 62, 74 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0))) |
76 | 75 | fveq2d 6107 |
. . 3
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)))) |
77 | 15, 57, 76 | 3eqtr2d 2650 |
. 2
⊢ (𝜑 → (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)))) |
78 | 12, 77 | eqtr4d 2647 |
1
⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) |