Proof of Theorem volinun
Step | Hyp | Ref
| Expression |
1 | | inundif 4413 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
2 | 1 | fveq2i 6770 |
. . . 4
⊢
(vol‘((𝐴 ∩
𝐵) ∪ (𝐴 ∖ 𝐵))) = (vol‘𝐴) |
3 | | inmbl 24694 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol) |
4 | 3 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∩ 𝐵) ∈ dom
vol) |
5 | | difmbl 24695 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol) |
6 | 5 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∖ 𝐵) ∈ dom
vol) |
7 | | indifcom 4207 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) |
8 | | difin0 4408 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐵) = ∅ |
9 | 8 | ineq2i 4144 |
. . . . . . . 8
⊢ (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) = (𝐴 ∩ ∅) |
10 | | in0 4326 |
. . . . . . . 8
⊢ (𝐴 ∩ ∅) =
∅ |
11 | 9, 10 | eqtri 2766 |
. . . . . . 7
⊢ (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) = ∅ |
12 | 7, 11 | eqtri 2766 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅ |
13 | 12 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((𝐴
∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅) |
14 | | mblvol 24682 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ dom vol → (vol‘(𝐴 ∩ 𝐵)) = (vol*‘(𝐴 ∩ 𝐵))) |
15 | 4, 14 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) = (vol*‘(𝐴 ∩ 𝐵))) |
16 | | inss1 4163 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∩ 𝐵) ⊆ 𝐴) |
18 | | mblss 24683 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
19 | 18 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → 𝐴
⊆ ℝ) |
20 | | mblvol 24682 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) |
21 | 20 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) = (vol*‘𝐴)) |
22 | | simprl 768 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) ∈ ℝ) |
23 | 21, 22 | eqeltrrd 2840 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘𝐴) ∈ ℝ) |
24 | | ovolsscl 24638 |
. . . . . . 7
⊢ (((𝐴 ∩ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) →
(vol*‘(𝐴 ∩ 𝐵)) ∈
ℝ) |
25 | 17, 19, 23, 24 | syl3anc 1370 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘(𝐴 ∩ 𝐵)) ∈ ℝ) |
26 | 15, 25 | eqeltrd 2839 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) ∈ ℝ) |
27 | | mblvol 24682 |
. . . . . . 7
⊢ ((𝐴 ∖ 𝐵) ∈ dom vol → (vol‘(𝐴 ∖ 𝐵)) = (vol*‘(𝐴 ∖ 𝐵))) |
28 | 6, 27 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) = (vol*‘(𝐴 ∖ 𝐵))) |
29 | | difssd 4067 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∖ 𝐵) ⊆ 𝐴) |
30 | | ovolsscl 24638 |
. . . . . . 7
⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) →
(vol*‘(𝐴 ∖
𝐵)) ∈
ℝ) |
31 | 29, 19, 23, 30 | syl3anc 1370 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘(𝐴 ∖ 𝐵)) ∈ ℝ) |
32 | 28, 31 | eqeltrd 2839 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) ∈ ℝ) |
33 | | volun 24697 |
. . . . 5
⊢ ((((𝐴 ∩ 𝐵) ∈ dom vol ∧ (𝐴 ∖ 𝐵) ∈ dom vol ∧ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅) ∧ ((vol‘(𝐴 ∩ 𝐵)) ∈ ℝ ∧ (vol‘(𝐴 ∖ 𝐵)) ∈ ℝ)) →
(vol‘((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
34 | 4, 6, 13, 26, 32, 33 | syl32anc 1377 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
35 | 2, 34 | eqtr3id 2792 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
36 | 35 | oveq1d 7283 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = (((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵))) + (vol‘𝐵))) |
37 | 26 | recnd 10991 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) ∈ ℂ) |
38 | 32 | recnd 10991 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) ∈ ℂ) |
39 | | simprr 770 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐵) ∈ ℝ) |
40 | 39 | recnd 10991 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐵) ∈ ℂ) |
41 | 37, 38, 40 | addassd 10985 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵))) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵)))) |
42 | | simplr 766 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → 𝐵
∈ dom vol) |
43 | | disjdifr 4407 |
. . . . . 6
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅ |
44 | 43 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((𝐴
∖ 𝐵) ∩ 𝐵) = ∅) |
45 | | volun 24697 |
. . . . 5
⊢ ((((𝐴 ∖ 𝐵) ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅) ∧ ((vol‘(𝐴 ∖ 𝐵)) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) →
(vol‘((𝐴 ∖
𝐵) ∪ 𝐵)) = ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) |
46 | 6, 42, 44, 32, 39, 45 | syl32anc 1377 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘((𝐴 ∖ 𝐵) ∪ 𝐵)) = ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) |
47 | | undif1 4410 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
48 | 47 | fveq2i 6770 |
. . . 4
⊢
(vol‘((𝐴
∖ 𝐵) ∪ 𝐵)) = (vol‘(𝐴 ∪ 𝐵)) |
49 | 46, 48 | eqtr3di 2793 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵)) = (vol‘(𝐴 ∪ 𝐵))) |
50 | 49 | oveq2d 7284 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘(𝐴 ∩ 𝐵)) + ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) |
51 | 36, 41, 50 | 3eqtrd 2782 |
1
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) |