Step | Hyp | Ref
| Expression |
1 | | measssd.1 |
. . . . 5
β’ (π β π β (measuresβπ)) |
2 | | measbase 32557 |
. . . . . . 7
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β π β βͺ ran
sigAlgebra) |
4 | | measssd.3 |
. . . . . 6
β’ (π β π΅ β π) |
5 | | measssd.2 |
. . . . . 6
β’ (π β π΄ β π) |
6 | | difelsiga 32493 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π΅ β π β§ π΄ β π) β (π΅ β π΄) β π) |
7 | 3, 4, 5, 6 | syl3anc 1372 |
. . . . 5
β’ (π β (π΅ β π΄) β π) |
8 | | measvxrge0 32565 |
. . . . 5
β’ ((π β (measuresβπ) β§ (π΅ β π΄) β π) β (πβ(π΅ β π΄)) β (0[,]+β)) |
9 | 1, 7, 8 | syl2anc 585 |
. . . 4
β’ (π β (πβ(π΅ β π΄)) β (0[,]+β)) |
10 | | elxrge0 13303 |
. . . . 5
β’ ((πβ(π΅ β π΄)) β (0[,]+β) β ((πβ(π΅ β π΄)) β β* β§ 0 β€
(πβ(π΅ β π΄)))) |
11 | 10 | simprbi 498 |
. . . 4
β’ ((πβ(π΅ β π΄)) β (0[,]+β) β 0 β€
(πβ(π΅ β π΄))) |
12 | 9, 11 | syl 17 |
. . 3
β’ (π β 0 β€ (πβ(π΅ β π΄))) |
13 | | measvxrge0 32565 |
. . . . . 6
β’ ((π β (measuresβπ) β§ π΄ β π) β (πβπ΄) β (0[,]+β)) |
14 | 1, 5, 13 | syl2anc 585 |
. . . . 5
β’ (π β (πβπ΄) β (0[,]+β)) |
15 | | elxrge0 13303 |
. . . . . 6
β’ ((πβπ΄) β (0[,]+β) β ((πβπ΄) β β* β§ 0 β€
(πβπ΄))) |
16 | 15 | simplbi 499 |
. . . . 5
β’ ((πβπ΄) β (0[,]+β) β (πβπ΄) β
β*) |
17 | 14, 16 | syl 17 |
. . . 4
β’ (π β (πβπ΄) β
β*) |
18 | 10 | simplbi 499 |
. . . . 5
β’ ((πβ(π΅ β π΄)) β (0[,]+β) β (πβ(π΅ β π΄)) β
β*) |
19 | 9, 18 | syl 17 |
. . . 4
β’ (π β (πβ(π΅ β π΄)) β
β*) |
20 | | xraddge02 31443 |
. . . 4
β’ (((πβπ΄) β β* β§ (πβ(π΅ β π΄)) β β*) β (0
β€ (πβ(π΅ β π΄)) β (πβπ΄) β€ ((πβπ΄) +π (πβ(π΅ β π΄))))) |
21 | 17, 19, 20 | syl2anc 585 |
. . 3
β’ (π β (0 β€ (πβ(π΅ β π΄)) β (πβπ΄) β€ ((πβπ΄) +π (πβ(π΅ β π΄))))) |
22 | 12, 21 | mpd 15 |
. 2
β’ (π β (πβπ΄) β€ ((πβπ΄) +π (πβ(π΅ β π΄)))) |
23 | | prssi 4780 |
. . . . . 6
β’ ((π΄ β π β§ (π΅ β π΄) β π) β {π΄, (π΅ β π΄)} β π) |
24 | 5, 7, 23 | syl2anc 585 |
. . . . 5
β’ (π β {π΄, (π΅ β π΄)} β π) |
25 | | prex 5388 |
. . . . . 6
β’ {π΄, (π΅ β π΄)} β V |
26 | 25 | elpw 4563 |
. . . . 5
β’ ({π΄, (π΅ β π΄)} β π« π β {π΄, (π΅ β π΄)} β π) |
27 | 24, 26 | sylibr 233 |
. . . 4
β’ (π β {π΄, (π΅ β π΄)} β π« π) |
28 | | prct 31413 |
. . . . 5
β’ ((π΄ β π β§ (π΅ β π΄) β π) β {π΄, (π΅ β π΄)} βΌ Ο) |
29 | 5, 7, 28 | syl2anc 585 |
. . . 4
β’ (π β {π΄, (π΅ β π΄)} βΌ Ο) |
30 | | disjdifprg 31278 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β Disj π¦ β {(π΅ β π΄), π΄}π¦) |
31 | 5, 4, 30 | syl2anc 585 |
. . . . 5
β’ (π β Disj π¦ β {(π΅ β π΄), π΄}π¦) |
32 | | prcom 4692 |
. . . . . . 7
β’ {(π΅ β π΄), π΄} = {π΄, (π΅ β π΄)} |
33 | 32 | a1i 11 |
. . . . . 6
β’ (π β {(π΅ β π΄), π΄} = {π΄, (π΅ β π΄)}) |
34 | 33 | disjeq1d 5077 |
. . . . 5
β’ (π β (Disj π¦ β {(π΅ β π΄), π΄}π¦ β Disj π¦ β {π΄, (π΅ β π΄)}π¦)) |
35 | 31, 34 | mpbid 231 |
. . . 4
β’ (π β Disj π¦ β {π΄, (π΅ β π΄)}π¦) |
36 | | measvun 32569 |
. . . 4
β’ ((π β (measuresβπ) β§ {π΄, (π΅ β π΄)} β π« π β§ ({π΄, (π΅ β π΄)} βΌ Ο β§ Disj π¦ β {π΄, (π΅ β π΄)}π¦)) β (πββͺ {π΄, (π΅ β π΄)}) = Ξ£*π¦ β {π΄, (π΅ β π΄)} (πβπ¦)) |
37 | 1, 27, 29, 35, 36 | syl112anc 1375 |
. . 3
β’ (π β (πββͺ {π΄, (π΅ β π΄)}) = Ξ£*π¦ β {π΄, (π΅ β π΄)} (πβπ¦)) |
38 | | uniprg 4881 |
. . . . . 6
β’ ((π΄ β π β§ (π΅ β π΄) β π) β βͺ {π΄, (π΅ β π΄)} = (π΄ βͺ (π΅ β π΄))) |
39 | 5, 7, 38 | syl2anc 585 |
. . . . 5
β’ (π β βͺ {π΄,
(π΅ β π΄)} = (π΄ βͺ (π΅ β π΄))) |
40 | | measssd.4 |
. . . . . 6
β’ (π β π΄ β π΅) |
41 | | undif 4440 |
. . . . . 6
β’ (π΄ β π΅ β (π΄ βͺ (π΅ β π΄)) = π΅) |
42 | 40, 41 | sylib 217 |
. . . . 5
β’ (π β (π΄ βͺ (π΅ β π΄)) = π΅) |
43 | 39, 42 | eqtrd 2778 |
. . . 4
β’ (π β βͺ {π΄,
(π΅ β π΄)} = π΅) |
44 | 43 | fveq2d 6842 |
. . 3
β’ (π β (πββͺ {π΄, (π΅ β π΄)}) = (πβπ΅)) |
45 | | fveq2 6838 |
. . . . 5
β’ (π¦ = π΄ β (πβπ¦) = (πβπ΄)) |
46 | 45 | adantl 483 |
. . . 4
β’ ((π β§ π¦ = π΄) β (πβπ¦) = (πβπ΄)) |
47 | | fveq2 6838 |
. . . . 5
β’ (π¦ = (π΅ β π΄) β (πβπ¦) = (πβ(π΅ β π΄))) |
48 | 47 | adantl 483 |
. . . 4
β’ ((π β§ π¦ = (π΅ β π΄)) β (πβπ¦) = (πβ(π΅ β π΄))) |
49 | | eqimss 3999 |
. . . . . . . . . 10
β’ (π΄ = (π΅ β π΄) β π΄ β (π΅ β π΄)) |
50 | | ssdifeq0 4443 |
. . . . . . . . . 10
β’ (π΄ β (π΅ β π΄) β π΄ = β
) |
51 | 49, 50 | sylib 217 |
. . . . . . . . 9
β’ (π΄ = (π΅ β π΄) β π΄ = β
) |
52 | 51 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π΄ = (π΅ β π΄)) β π΄ = β
) |
53 | 52 | fveq2d 6842 |
. . . . . . 7
β’ ((π β§ π΄ = (π΅ β π΄)) β (πβπ΄) = (πββ
)) |
54 | | measvnul 32566 |
. . . . . . . . 9
β’ (π β (measuresβπ) β (πββ
) = 0) |
55 | 1, 54 | syl 17 |
. . . . . . . 8
β’ (π β (πββ
) = 0) |
56 | 55 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ = (π΅ β π΄)) β (πββ
) = 0) |
57 | 53, 56 | eqtrd 2778 |
. . . . . 6
β’ ((π β§ π΄ = (π΅ β π΄)) β (πβπ΄) = 0) |
58 | 57 | orcd 872 |
. . . . 5
β’ ((π β§ π΄ = (π΅ β π΄)) β ((πβπ΄) = 0 β¨ (πβπ΄) = +β)) |
59 | 58 | ex 414 |
. . . 4
β’ (π β (π΄ = (π΅ β π΄) β ((πβπ΄) = 0 β¨ (πβπ΄) = +β))) |
60 | 46, 48, 5, 7, 14, 9,
59 | esumpr2 32427 |
. . 3
β’ (π β Ξ£*π¦ β {π΄, (π΅ β π΄)} (πβπ¦) = ((πβπ΄) +π (πβ(π΅ β π΄)))) |
61 | 37, 44, 60 | 3eqtr3d 2786 |
. 2
β’ (π β (πβπ΅) = ((πβπ΄) +π (πβ(π΅ β π΄)))) |
62 | 22, 61 | breqtrrd 5132 |
1
β’ (π β (πβπ΄) β€ (πβπ΅)) |