Proof of Theorem itgaddnclem1
| Step | Hyp | Ref
| Expression |
| 1 | | itgaddnclem.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 2 | | itgaddnclem.2 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
| 3 | 1, 2 | readdcld 11290 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ) |
| 4 | | ibladdnc.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 5 | | ibladdnc.2 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
| 6 | | ibladdnc.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
| 7 | | ibladdnc.4 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) |
| 8 | | ibladdnc.m |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) |
| 9 | 4, 5, 6, 7, 8 | ibladdnc 37684 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈
𝐿1) |
| 10 | | itgaddnclem.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) |
| 11 | | itgaddnclem.4 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐶) |
| 12 | 1, 2, 10, 11 | addge0d 11839 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (𝐵 + 𝐶)) |
| 13 | 3, 9, 12 | itgposval 25831 |
. 2
⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)))) |
| 14 | 1, 5, 10 | itgposval 25831 |
. . . 4
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) |
| 15 | 2, 7, 11 | itgposval 25831 |
. . . 4
⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)))) |
| 16 | 14, 15 | oveq12d 7449 |
. . 3
⊢ (𝜑 → (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))))) |
| 17 | | iblmbf 25802 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
| 18 | 5, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
| 19 | 18, 4 | mbfdm2 25672 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom vol) |
| 20 | | mblss 25566 |
. . . . . 6
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
| 21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 22 | | rembl 25575 |
. . . . . 6
⊢ ℝ
∈ dom vol |
| 23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈ dom
vol) |
| 24 | | elrege0 13494 |
. . . . . . . 8
⊢ (𝐵 ∈ (0[,)+∞) ↔
(𝐵 ∈ ℝ ∧ 0
≤ 𝐵)) |
| 25 | 1, 10, 24 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) |
| 26 | | 0e0icopnf 13498 |
. . . . . . . 8
⊢ 0 ∈
(0[,)+∞) |
| 27 | 26 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
| 28 | 25, 27 | ifclda 4561 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,)+∞)) |
| 29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,)+∞)) |
| 30 | | eldifn 4132 |
. . . . . . 7
⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴) |
| 31 | 30 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴) |
| 32 | | iffalse 4534 |
. . . . . 6
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐵, 0) = 0) |
| 33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if(𝑥 ∈ 𝐴, 𝐵, 0) = 0) |
| 34 | | iftrue 4531 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐵, 0) = 𝐵) |
| 35 | 34 | mpteq2ia 5245 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 36 | 35, 18 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∈ MblFn) |
| 37 | 21, 23, 29, 33, 36 | mbfss 25681 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∈ MblFn) |
| 38 | 28 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ (0[,)+∞)) |
| 39 | 38 | fmpttd 7135 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵,
0)):ℝ⟶(0[,)+∞)) |
| 40 | 1, 10 | iblpos 25828 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) ∈ ℝ))) |
| 41 | 5, 40 | mpbid 232 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) ∈ ℝ)) |
| 42 | 41 | simprd 495 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) ∈ ℝ) |
| 43 | | elrege0 13494 |
. . . . . . . 8
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 ∈ ℝ ∧ 0
≤ 𝐶)) |
| 44 | 2, 11, 43 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞)) |
| 45 | 44, 27 | ifclda 4561 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,)+∞)) |
| 46 | 45 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,)+∞)) |
| 47 | 46 | fmpttd 7135 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶,
0)):ℝ⟶(0[,)+∞)) |
| 48 | 2, 11 | iblpos 25828 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐶, 0))) ∈ ℝ))) |
| 49 | 7, 48 | mpbid 232 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐶, 0))) ∈ ℝ)) |
| 50 | 49 | simprd 495 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐶, 0))) ∈ ℝ) |
| 51 | 37, 39, 42, 47, 50 | itg2addnc 37681 |
. . 3
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))))) |
| 52 | | reex 11246 |
. . . . . . 7
⊢ ℝ
∈ V |
| 53 | 52 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈
V) |
| 54 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
| 55 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
| 56 | 53, 38, 46, 54, 55 | offval2 7717 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)))) |
| 57 | | iftrue 4531 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
| 58 | 34, 57 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = (𝐵 + 𝐶)) |
| 59 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0) = (𝐵 + 𝐶)) |
| 60 | 58, 59 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)) |
| 61 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
| 62 | 32, 61 | oveq12d 7449 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = (0 + 0)) |
| 63 | | 00id 11436 |
. . . . . . . . 9
⊢ (0 + 0) =
0 |
| 64 | 62, 63 | eqtrdi 2793 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = 0) |
| 65 | | iffalse 4534 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0) = 0) |
| 66 | 64, 65 | eqtr4d 2780 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)) |
| 67 | 60, 66 | pm2.61i 182 |
. . . . . 6
⊢ (if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0)) = if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0) |
| 68 | 67 | mpteq2i 5247 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, 𝐵, 0) + if(𝑥 ∈ 𝐴, 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)) |
| 69 | 56, 68 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0))) |
| 70 | 69 | fveq2d 6910 |
. . 3
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)))) |
| 71 | 16, 51, 70 | 3eqtr2d 2783 |
. 2
⊢ (𝜑 → (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐵 + 𝐶), 0)))) |
| 72 | 13, 71 | eqtr4d 2780 |
1
⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) |