Step | Hyp | Ref
| Expression |
1 | | undif1 4434 |
. . . 4
β’ ((π΄ β π΅) βͺ π΅) = (π΄ βͺ π΅) |
2 | 1 | fveq2i 6841 |
. . 3
β’ (πβ((π΄ β π΅) βͺ π΅)) = (πβ(π΄ βͺ π΅)) |
3 | | measunl.1 |
. . . 4
β’ (π β π β (measuresβπ)) |
4 | | measbase 32557 |
. . . . . 6
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β π β βͺ ran
sigAlgebra) |
6 | | measunl.2 |
. . . . 5
β’ (π β π΄ β π) |
7 | | measunl.3 |
. . . . 5
β’ (π β π΅ β π) |
8 | | difelsiga 32493 |
. . . . 5
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) β π) |
9 | 5, 6, 7, 8 | syl3anc 1372 |
. . . 4
β’ (π β (π΄ β π΅) β π) |
10 | | disjdifr 4431 |
. . . . 5
β’ ((π΄ β π΅) β© π΅) = β
|
11 | 10 | a1i 11 |
. . . 4
β’ (π β ((π΄ β π΅) β© π΅) = β
) |
12 | | measun 32571 |
. . . 4
β’ ((π β (measuresβπ) β§ ((π΄ β π΅) β π β§ π΅ β π) β§ ((π΄ β π΅) β© π΅) = β
) β (πβ((π΄ β π΅) βͺ π΅)) = ((πβ(π΄ β π΅)) +π (πβπ΅))) |
13 | 3, 9, 7, 11, 12 | syl121anc 1376 |
. . 3
β’ (π β (πβ((π΄ β π΅) βͺ π΅)) = ((πβ(π΄ β π΅)) +π (πβπ΅))) |
14 | 2, 13 | eqtr3id 2792 |
. 2
β’ (π β (πβ(π΄ βͺ π΅)) = ((πβ(π΄ β π΅)) +π (πβπ΅))) |
15 | | iccssxr 13276 |
. . . 4
β’
(0[,]+β) β β* |
16 | | measvxrge0 32565 |
. . . . 5
β’ ((π β (measuresβπ) β§ (π΄ β π΅) β π) β (πβ(π΄ β π΅)) β (0[,]+β)) |
17 | 3, 9, 16 | syl2anc 585 |
. . . 4
β’ (π β (πβ(π΄ β π΅)) β (0[,]+β)) |
18 | 15, 17 | sselid 3941 |
. . 3
β’ (π β (πβ(π΄ β π΅)) β
β*) |
19 | | measvxrge0 32565 |
. . . . 5
β’ ((π β (measuresβπ) β§ π΄ β π) β (πβπ΄) β (0[,]+β)) |
20 | 3, 6, 19 | syl2anc 585 |
. . . 4
β’ (π β (πβπ΄) β (0[,]+β)) |
21 | 15, 20 | sselid 3941 |
. . 3
β’ (π β (πβπ΄) β
β*) |
22 | | measvxrge0 32565 |
. . . . 5
β’ ((π β (measuresβπ) β§ π΅ β π) β (πβπ΅) β (0[,]+β)) |
23 | 3, 7, 22 | syl2anc 585 |
. . . 4
β’ (π β (πβπ΅) β (0[,]+β)) |
24 | 15, 23 | sselid 3941 |
. . 3
β’ (π β (πβπ΅) β
β*) |
25 | | inelsiga 32495 |
. . . . . . . . 9
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β π) |
26 | 5, 6, 7, 25 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π΄ β© π΅) β π) |
27 | | measvxrge0 32565 |
. . . . . . . 8
β’ ((π β (measuresβπ) β§ (π΄ β© π΅) β π) β (πβ(π΄ β© π΅)) β (0[,]+β)) |
28 | 3, 26, 27 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ(π΄ β© π΅)) β (0[,]+β)) |
29 | | elxrge0 13303 |
. . . . . . 7
β’ ((πβ(π΄ β© π΅)) β (0[,]+β) β ((πβ(π΄ β© π΅)) β β* β§ 0 β€
(πβ(π΄ β© π΅)))) |
30 | 28, 29 | sylib 217 |
. . . . . 6
β’ (π β ((πβ(π΄ β© π΅)) β β* β§ 0 β€
(πβ(π΄ β© π΅)))) |
31 | 30 | simprd 497 |
. . . . 5
β’ (π β 0 β€ (πβ(π΄ β© π΅))) |
32 | 15, 28 | sselid 3941 |
. . . . . 6
β’ (π β (πβ(π΄ β© π΅)) β
β*) |
33 | | xraddge02 31443 |
. . . . . 6
β’ (((πβ(π΄ β π΅)) β β* β§ (πβ(π΄ β© π΅)) β β*) β (0
β€ (πβ(π΄ β© π΅)) β (πβ(π΄ β π΅)) β€ ((πβ(π΄ β π΅)) +π (πβ(π΄ β© π΅))))) |
34 | 18, 32, 33 | syl2anc 585 |
. . . . 5
β’ (π β (0 β€ (πβ(π΄ β© π΅)) β (πβ(π΄ β π΅)) β€ ((πβ(π΄ β π΅)) +π (πβ(π΄ β© π΅))))) |
35 | 31, 34 | mpd 15 |
. . . 4
β’ (π β (πβ(π΄ β π΅)) β€ ((πβ(π΄ β π΅)) +π (πβ(π΄ β© π΅)))) |
36 | | uncom 4112 |
. . . . . . 7
β’ ((π΄ β© π΅) βͺ (π΄ β π΅)) = ((π΄ β π΅) βͺ (π΄ β© π΅)) |
37 | | inundif 4437 |
. . . . . . 7
β’ ((π΄ β© π΅) βͺ (π΄ β π΅)) = π΄ |
38 | 36, 37 | eqtr3i 2768 |
. . . . . 6
β’ ((π΄ β π΅) βͺ (π΄ β© π΅)) = π΄ |
39 | 38 | fveq2i 6841 |
. . . . 5
β’ (πβ((π΄ β π΅) βͺ (π΄ β© π΅))) = (πβπ΄) |
40 | | incom 4160 |
. . . . . . . 8
β’ ((π΄ β© π΅) β© (π΄ β π΅)) = ((π΄ β π΅) β© (π΄ β© π΅)) |
41 | | inindif 31228 |
. . . . . . . 8
β’ ((π΄ β© π΅) β© (π΄ β π΅)) = β
|
42 | 40, 41 | eqtr3i 2768 |
. . . . . . 7
β’ ((π΄ β π΅) β© (π΄ β© π΅)) = β
|
43 | 42 | a1i 11 |
. . . . . 6
β’ (π β ((π΄ β π΅) β© (π΄ β© π΅)) = β
) |
44 | | measun 32571 |
. . . . . 6
β’ ((π β (measuresβπ) β§ ((π΄ β π΅) β π β§ (π΄ β© π΅) β π) β§ ((π΄ β π΅) β© (π΄ β© π΅)) = β
) β (πβ((π΄ β π΅) βͺ (π΄ β© π΅))) = ((πβ(π΄ β π΅)) +π (πβ(π΄ β© π΅)))) |
45 | 3, 9, 26, 43, 44 | syl121anc 1376 |
. . . . 5
β’ (π β (πβ((π΄ β π΅) βͺ (π΄ β© π΅))) = ((πβ(π΄ β π΅)) +π (πβ(π΄ β© π΅)))) |
46 | 39, 45 | eqtr3id 2792 |
. . . 4
β’ (π β (πβπ΄) = ((πβ(π΄ β π΅)) +π (πβ(π΄ β© π΅)))) |
47 | 35, 46 | breqtrrd 5132 |
. . 3
β’ (π β (πβ(π΄ β π΅)) β€ (πβπ΄)) |
48 | | xleadd1a 13101 |
. . 3
β’ ((((πβ(π΄ β π΅)) β β* β§ (πβπ΄) β β* β§ (πβπ΅) β β*) β§ (πβ(π΄ β π΅)) β€ (πβπ΄)) β ((πβ(π΄ β π΅)) +π (πβπ΅)) β€ ((πβπ΄) +π (πβπ΅))) |
49 | 18, 21, 24, 47, 48 | syl31anc 1374 |
. 2
β’ (π β ((πβ(π΄ β π΅)) +π (πβπ΅)) β€ ((πβπ΄) +π (πβπ΅))) |
50 | 14, 49 | eqbrtrd 5126 |
1
β’ (π β (πβ(π΄ βͺ π΅)) β€ ((πβπ΄) +π (πβπ΅))) |