Proof of Theorem volinun
Step | Hyp | Ref
| Expression |
1 | | inundif 3998 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
2 | 1 | fveq2i 6106 |
. . . 4
⊢
(vol‘((𝐴 ∩
𝐵) ∪ (𝐴 ∖ 𝐵))) = (vol‘𝐴) |
3 | | inmbl 23117 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol) |
4 | 3 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∩ 𝐵) ∈ dom
vol) |
5 | | difmbl 23118 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol) |
6 | 5 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∖ 𝐵) ∈ dom
vol) |
7 | | indifcom 3831 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) |
8 | | difin0 3993 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐵) = ∅ |
9 | 8 | ineq2i 3773 |
. . . . . . . 8
⊢ (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) = (𝐴 ∩ ∅) |
10 | | in0 3920 |
. . . . . . . 8
⊢ (𝐴 ∩ ∅) =
∅ |
11 | 9, 10 | eqtri 2632 |
. . . . . . 7
⊢ (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) = ∅ |
12 | 7, 11 | eqtri 2632 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅ |
13 | 12 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((𝐴
∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅) |
14 | | mblvol 23105 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ dom vol → (vol‘(𝐴 ∩ 𝐵)) = (vol*‘(𝐴 ∩ 𝐵))) |
15 | 4, 14 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) = (vol*‘(𝐴 ∩ 𝐵))) |
16 | | inss1 3795 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∩ 𝐵) ⊆ 𝐴) |
18 | | mblss 23106 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
19 | 18 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → 𝐴
⊆ ℝ) |
20 | | mblvol 23105 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) |
21 | 20 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) = (vol*‘𝐴)) |
22 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) ∈ ℝ) |
23 | 21, 22 | eqeltrrd 2689 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘𝐴) ∈ ℝ) |
24 | | ovolsscl 23061 |
. . . . . . 7
⊢ (((𝐴 ∩ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) →
(vol*‘(𝐴 ∩ 𝐵)) ∈
ℝ) |
25 | 17, 19, 23, 24 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘(𝐴 ∩ 𝐵)) ∈ ℝ) |
26 | 15, 25 | eqeltrd 2688 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) ∈ ℝ) |
27 | | mblvol 23105 |
. . . . . . 7
⊢ ((𝐴 ∖ 𝐵) ∈ dom vol → (vol‘(𝐴 ∖ 𝐵)) = (vol*‘(𝐴 ∖ 𝐵))) |
28 | 6, 27 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) = (vol*‘(𝐴 ∖ 𝐵))) |
29 | | difssd 3700 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∖ 𝐵) ⊆ 𝐴) |
30 | | ovolsscl 23061 |
. . . . . . 7
⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) →
(vol*‘(𝐴 ∖
𝐵)) ∈
ℝ) |
31 | 29, 19, 23, 30 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘(𝐴 ∖ 𝐵)) ∈ ℝ) |
32 | 28, 31 | eqeltrd 2688 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) ∈ ℝ) |
33 | | volun 23120 |
. . . . 5
⊢ ((((𝐴 ∩ 𝐵) ∈ dom vol ∧ (𝐴 ∖ 𝐵) ∈ dom vol ∧ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅) ∧ ((vol‘(𝐴 ∩ 𝐵)) ∈ ℝ ∧ (vol‘(𝐴 ∖ 𝐵)) ∈ ℝ)) →
(vol‘((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
34 | 4, 6, 13, 26, 32, 33 | syl32anc 1326 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
35 | 2, 34 | syl5eqr 2658 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
36 | 35 | oveq1d 6564 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = (((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵))) + (vol‘𝐵))) |
37 | 26 | recnd 9947 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) ∈ ℂ) |
38 | 32 | recnd 9947 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) ∈ ℂ) |
39 | | simprr 792 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐵) ∈ ℝ) |
40 | 39 | recnd 9947 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐵) ∈ ℂ) |
41 | 37, 38, 40 | addassd 9941 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵))) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵)))) |
42 | | undif1 3995 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
43 | 42 | fveq2i 6106 |
. . . 4
⊢
(vol‘((𝐴
∖ 𝐵) ∪ 𝐵)) = (vol‘(𝐴 ∪ 𝐵)) |
44 | | simplr 788 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → 𝐵
∈ dom vol) |
45 | | incom 3767 |
. . . . . . 7
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐵) = (𝐵 ∩ (𝐴 ∖ 𝐵)) |
46 | | disjdif 3992 |
. . . . . . 7
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅ |
47 | 45, 46 | eqtri 2632 |
. . . . . 6
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅ |
48 | 47 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((𝐴
∖ 𝐵) ∩ 𝐵) = ∅) |
49 | | volun 23120 |
. . . . 5
⊢ ((((𝐴 ∖ 𝐵) ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅) ∧ ((vol‘(𝐴 ∖ 𝐵)) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) →
(vol‘((𝐴 ∖
𝐵) ∪ 𝐵)) = ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) |
50 | 6, 44, 48, 32, 39, 49 | syl32anc 1326 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘((𝐴 ∖ 𝐵) ∪ 𝐵)) = ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) |
51 | 43, 50 | syl5reqr 2659 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵)) = (vol‘(𝐴 ∪ 𝐵))) |
52 | 51 | oveq2d 6565 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘(𝐴 ∩ 𝐵)) + ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) |
53 | 36, 41, 52 | 3eqtrd 2648 |
1
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) |