Proof of Theorem ditgsplitlem
| Step | Hyp | Ref
| Expression |
| 1 | | ditgsplit.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) |
| 2 | | ditgsplit.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 3 | | ditgsplit.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 4 | | elicc2 13452 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌))) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌))) |
| 6 | 1, 5 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌)) |
| 7 | 6 | simp1d 1143 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 8 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝐴 ∈ ℝ) |
| 9 | | ditgsplit.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌)) |
| 10 | | elicc2 13452 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐶 ∈ (𝑋[,]𝑌) ↔ (𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌))) |
| 11 | 2, 3, 10 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ (𝑋[,]𝑌) ↔ (𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌))) |
| 12 | 9, 11 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌)) |
| 13 | 12 | simp1d 1143 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 14 | 13 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝐶 ∈ ℝ) |
| 15 | | ditgsplit.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) |
| 16 | | elicc2 13452 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌))) |
| 17 | 2, 3, 16 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌))) |
| 18 | 15, 17 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌)) |
| 19 | 18 | simp1d 1143 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝐵 ∈ ℝ) |
| 21 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜓 ∧ 𝜃)) |
| 22 | | ditgsplit.1 |
. . . . . . 7
⊢ ((𝜓 ∧ 𝜃) ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) |
| 23 | 21, 22 | sylib 218 |
. . . . . 6
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) |
| 24 | 23 | simpld 494 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝐴 ≤ 𝐵) |
| 25 | 23 | simprd 495 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝐵 ≤ 𝐶) |
| 26 | | elicc2 13452 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ∈ (𝐴[,]𝐶) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶))) |
| 27 | 7, 13, 26 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ (𝐴[,]𝐶) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶))) |
| 28 | 27 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝐵 ∈ (𝐴[,]𝐶) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶))) |
| 29 | 20, 24, 25, 28 | mpbir3and 1343 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝐵 ∈ (𝐴[,]𝐶)) |
| 30 | 2 | rexrd 11311 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
| 31 | 6 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ 𝐴) |
| 32 | | iooss1 13422 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ*
∧ 𝑋 ≤ 𝐴) → (𝐴(,)𝐶) ⊆ (𝑋(,)𝐶)) |
| 33 | 30, 31, 32 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐶) ⊆ (𝑋(,)𝐶)) |
| 34 | 3 | rexrd 11311 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
| 35 | 12 | simp3d 1145 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≤ 𝑌) |
| 36 | | iooss2 13423 |
. . . . . . . . 9
⊢ ((𝑌 ∈ ℝ*
∧ 𝐶 ≤ 𝑌) → (𝑋(,)𝐶) ⊆ (𝑋(,)𝑌)) |
| 37 | 34, 35, 36 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(,)𝐶) ⊆ (𝑋(,)𝑌)) |
| 38 | 33, 37 | sstrd 3994 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐶) ⊆ (𝑋(,)𝑌)) |
| 39 | 38 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝑥 ∈ (𝑋(,)𝑌)) |
| 40 | | ditgsplit.i |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈
𝐿1) |
| 41 | | iblmbf 25802 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿1 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ MblFn) |
| 42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ MblFn) |
| 43 | | ditgsplit.d |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉) |
| 44 | 42, 43 | mbfmptcl 25671 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ ℂ) |
| 45 | 39, 44 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝐷 ∈ ℂ) |
| 46 | 45 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝐷 ∈ ℂ) |
| 47 | | iooss1 13422 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ*
∧ 𝑋 ≤ 𝐴) → (𝐴(,)𝐵) ⊆ (𝑋(,)𝐵)) |
| 48 | 30, 31, 47 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝑋(,)𝐵)) |
| 49 | 18 | simp3d 1145 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ≤ 𝑌) |
| 50 | | iooss2 13423 |
. . . . . . . 8
⊢ ((𝑌 ∈ ℝ*
∧ 𝐵 ≤ 𝑌) → (𝑋(,)𝐵) ⊆ (𝑋(,)𝑌)) |
| 51 | 34, 49, 50 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑋(,)𝐵) ⊆ (𝑋(,)𝑌)) |
| 52 | 48, 51 | sstrd 3994 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝑋(,)𝑌)) |
| 53 | | ioombl 25600 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
| 54 | 53 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
| 55 | 52, 54, 43, 40 | iblss 25840 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈
𝐿1) |
| 56 | 55 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈
𝐿1) |
| 57 | 18 | simp2d 1144 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ≤ 𝐵) |
| 58 | | iooss1 13422 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ*
∧ 𝑋 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝑋(,)𝐶)) |
| 59 | 30, 57, 58 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝑋(,)𝐶)) |
| 60 | 59, 37 | sstrd 3994 |
. . . . . 6
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝑋(,)𝑌)) |
| 61 | | ioombl 25600 |
. . . . . . 7
⊢ (𝐵(,)𝐶) ∈ dom vol |
| 62 | 61 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐵(,)𝐶) ∈ dom vol) |
| 63 | 60, 62, 43, 40 | iblss 25840 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐵(,)𝐶) ↦ 𝐷) ∈
𝐿1) |
| 64 | 63 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝑥 ∈ (𝐵(,)𝐶) ↦ 𝐷) ∈
𝐿1) |
| 65 | 8, 14, 29, 46, 56, 64 | itgsplitioo 25873 |
. . 3
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |
| 66 | 8, 20, 14, 24, 25 | letrd 11418 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝐴 ≤ 𝐶) |
| 67 | 66 | ditgpos 25891 |
. . 3
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = ∫(𝐴(,)𝐶)𝐷 d𝑥) |
| 68 | 24 | ditgpos 25891 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ∫(𝐴(,)𝐵)𝐷 d𝑥) |
| 69 | 25 | ditgpos 25891 |
. . . 4
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → ⨜[𝐵 → 𝐶]𝐷 d𝑥 = ∫(𝐵(,)𝐶)𝐷 d𝑥) |
| 70 | 68, 69 | oveq12d 7449 |
. . 3
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |
| 71 | 65, 67, 70 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥)) |
| 72 | 71 | anassrs 467 |
1
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥)) |