Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππ |
2 | | vonvolmbllem.a |
. . . . . . . 8
β’ (π β π΄ β π) |
3 | | vonvolmbllem.x |
. . . . . . . 8
β’ (π β π β (β βm {π΄})) |
4 | | vonvolmbllem.y |
. . . . . . . 8
β’ π = βͺ π β π ran π |
5 | 1, 2, 3, 4 | ssmapsn 43524 |
. . . . . . 7
β’ (π β π = (π βm {π΄})) |
6 | 5 | ineq1d 4172 |
. . . . . 6
β’ (π β (π β© (π΅ βm {π΄})) = ((π βm {π΄}) β© (π΅ βm {π΄}))) |
7 | | reex 11147 |
. . . . . . . . 9
β’ β
β V |
8 | 7 | a1i 11 |
. . . . . . . 8
β’ (π β β β
V) |
9 | 3 | sselda 3945 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β (β βm {π΄})) |
10 | | elmapi 8790 |
. . . . . . . . . . . . 13
β’ (π β (β
βm {π΄})
β π:{π΄}βΆβ) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π:{π΄}βΆβ) |
12 | 11 | frnd 6677 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ran π β β) |
13 | 12 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (π β βπ β π ran π β β) |
14 | | iunss 5006 |
. . . . . . . . . 10
β’ (βͺ π β π ran π β β β βπ β π ran π β β) |
15 | 13, 14 | sylibr 233 |
. . . . . . . . 9
β’ (π β βͺ π β π ran π β β) |
16 | 4, 15 | eqsstrid 3993 |
. . . . . . . 8
β’ (π β π β β) |
17 | 8, 16 | ssexd 5282 |
. . . . . . 7
β’ (π β π β V) |
18 | | vonvolmbllem.b |
. . . . . . . 8
β’ (π β π΅ β β) |
19 | 8, 18 | ssexd 5282 |
. . . . . . 7
β’ (π β π΅ β V) |
20 | | snex 5389 |
. . . . . . . 8
β’ {π΄} β V |
21 | 20 | a1i 11 |
. . . . . . 7
β’ (π β {π΄} β V) |
22 | 17, 19, 21 | inmap 43517 |
. . . . . 6
β’ (π β ((π βm {π΄}) β© (π΅ βm {π΄})) = ((π β© π΅) βm {π΄})) |
23 | 6, 22 | eqtrd 2773 |
. . . . 5
β’ (π β (π β© (π΅ βm {π΄})) = ((π β© π΅) βm {π΄})) |
24 | 23 | fveq2d 6847 |
. . . 4
β’ (π β ((voln*β{π΄})β(π β© (π΅ βm {π΄}))) = ((voln*β{π΄})β((π β© π΅) βm {π΄}))) |
25 | 16 | ssinss1d 43344 |
. . . . 5
β’ (π β (π β© π΅) β β) |
26 | 2, 25 | ovnovol 44986 |
. . . 4
β’ (π β ((voln*β{π΄})β((π β© π΅) βm {π΄})) = (vol*β(π β© π΅))) |
27 | 24, 26 | eqtrd 2773 |
. . 3
β’ (π β ((voln*β{π΄})β(π β© (π΅ βm {π΄}))) = (vol*β(π β© π΅))) |
28 | 5 | difeq1d 4082 |
. . . . . 6
β’ (π β (π β (π΅ βm {π΄})) = ((π βm {π΄}) β (π΅ βm {π΄}))) |
29 | 17, 19, 2 | difmapsn 43520 |
. . . . . 6
β’ (π β ((π βm {π΄}) β (π΅ βm {π΄})) = ((π β π΅) βm {π΄})) |
30 | 28, 29 | eqtrd 2773 |
. . . . 5
β’ (π β (π β (π΅ βm {π΄})) = ((π β π΅) βm {π΄})) |
31 | 30 | fveq2d 6847 |
. . . 4
β’ (π β ((voln*β{π΄})β(π β (π΅ βm {π΄}))) = ((voln*β{π΄})β((π β π΅) βm {π΄}))) |
32 | 16 | ssdifssd 4103 |
. . . . 5
β’ (π β (π β π΅) β β) |
33 | 2, 32 | ovnovol 44986 |
. . . 4
β’ (π β ((voln*β{π΄})β((π β π΅) βm {π΄})) = (vol*β(π β π΅))) |
34 | 31, 33 | eqtrd 2773 |
. . 3
β’ (π β ((voln*β{π΄})β(π β (π΅ βm {π΄}))) = (vol*β(π β π΅))) |
35 | 27, 34 | oveq12d 7376 |
. 2
β’ (π β (((voln*β{π΄})β(π β© (π΅ βm {π΄}))) +π
((voln*β{π΄})β(π β (π΅ βm {π΄})))) = ((vol*β(π β© π΅)) +π (vol*β(π β π΅)))) |
36 | 5 | fveq2d 6847 |
. . 3
β’ (π β ((voln*β{π΄})βπ) = ((voln*β{π΄})β(π βm {π΄}))) |
37 | 2, 16 | ovnovol 44986 |
. . 3
β’ (π β ((voln*β{π΄})β(π βm {π΄})) = (vol*βπ)) |
38 | 17, 16 | elpwd 4567 |
. . . 4
β’ (π β π β π« β) |
39 | | vonvolmbllem.e |
. . . 4
β’ (π β βπ¦ β π« β(vol*βπ¦) = ((vol*β(π¦ β© π΅)) +π (vol*β(π¦ β π΅)))) |
40 | | fveq2 6843 |
. . . . . 6
β’ (π¦ = π β (vol*βπ¦) = (vol*βπ)) |
41 | | ineq1 4166 |
. . . . . . . 8
β’ (π¦ = π β (π¦ β© π΅) = (π β© π΅)) |
42 | 41 | fveq2d 6847 |
. . . . . . 7
β’ (π¦ = π β (vol*β(π¦ β© π΅)) = (vol*β(π β© π΅))) |
43 | | difeq1 4076 |
. . . . . . . 8
β’ (π¦ = π β (π¦ β π΅) = (π β π΅)) |
44 | 43 | fveq2d 6847 |
. . . . . . 7
β’ (π¦ = π β (vol*β(π¦ β π΅)) = (vol*β(π β π΅))) |
45 | 42, 44 | oveq12d 7376 |
. . . . . 6
β’ (π¦ = π β ((vol*β(π¦ β© π΅)) +π (vol*β(π¦ β π΅))) = ((vol*β(π β© π΅)) +π (vol*β(π β π΅)))) |
46 | 40, 45 | eqeq12d 2749 |
. . . . 5
β’ (π¦ = π β ((vol*βπ¦) = ((vol*β(π¦ β© π΅)) +π (vol*β(π¦ β π΅))) β (vol*βπ) = ((vol*β(π β© π΅)) +π (vol*β(π β π΅))))) |
47 | 46 | rspcva 3578 |
. . . 4
β’ ((π β π« β β§
βπ¦ β π«
β(vol*βπ¦) =
((vol*β(π¦ β© π΅)) +π
(vol*β(π¦ β
π΅)))) β
(vol*βπ) =
((vol*β(π β© π΅)) +π
(vol*β(π β
π΅)))) |
48 | 38, 39, 47 | syl2anc 585 |
. . 3
β’ (π β (vol*βπ) = ((vol*β(π β© π΅)) +π (vol*β(π β π΅)))) |
49 | 36, 37, 48 | 3eqtrd 2777 |
. 2
β’ (π β ((voln*β{π΄})βπ) = ((vol*β(π β© π΅)) +π (vol*β(π β π΅)))) |
50 | 35, 49 | eqtr4d 2776 |
1
β’ (π β (((voln*β{π΄})β(π β© (π΅ βm {π΄}))) +π
((voln*β{π΄})β(π β (π΅ βm {π΄})))) = ((voln*β{π΄})βπ)) |