Step | Hyp | Ref
| Expression |
1 | | elex 3493 |
. . 3
β’ (π β (measuresβπ) β π β V) |
2 | 1 | a1i 11 |
. 2
β’ (π β βͺ ran sigAlgebra β (π β (measuresβπ) β π β V)) |
3 | | simp1 1137 |
. . 3
β’ ((π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))) β π:πβΆ(0[,]+β)) |
4 | | ovex 7442 |
. . . 4
β’
(0[,]+β) β V |
5 | | fex2 7924 |
. . . . . 6
β’ ((π:πβΆ(0[,]+β) β§ π β βͺ ran sigAlgebra β§ (0[,]+β) β V) β
π β
V) |
6 | 5 | 3expb 1121 |
. . . . 5
β’ ((π:πβΆ(0[,]+β) β§ (π β βͺ ran sigAlgebra β§ (0[,]+β) β V)) β
π β
V) |
7 | 6 | expcom 415 |
. . . 4
β’ ((π β βͺ ran sigAlgebra β§ (0[,]+β) β V) β
(π:πβΆ(0[,]+β) β π β V)) |
8 | 4, 7 | mpan2 690 |
. . 3
β’ (π β βͺ ran sigAlgebra β (π:πβΆ(0[,]+β) β π β V)) |
9 | 3, 8 | syl5 34 |
. 2
β’ (π β βͺ ran sigAlgebra β ((π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))) β π β V)) |
10 | | df-meas 33194 |
. . . 4
β’ measures
= (π β βͺ ran sigAlgebra β¦ {π β£ (π:π βΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))}) |
11 | | vex 3479 |
. . . . . 6
β’ π β V |
12 | | mapex 8826 |
. . . . . 6
β’ ((π β V β§ (0[,]+β)
β V) β {π β£
π:π βΆ(0[,]+β)} β
V) |
13 | 11, 4, 12 | mp2an 691 |
. . . . 5
β’ {π β£ π:π βΆ(0[,]+β)} β
V |
14 | | simp1 1137 |
. . . . . 6
β’ ((π:π βΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))) β π:π βΆ(0[,]+β)) |
15 | 14 | ss2abi 4064 |
. . . . 5
β’ {π β£ (π:π βΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))} β {π β£ π:π βΆ(0[,]+β)} |
16 | 13, 15 | ssexi 5323 |
. . . 4
β’ {π β£ (π:π βΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))} β V |
17 | | simpr 486 |
. . . . . 6
β’ ((π = π β§ π = π) β π = π) |
18 | | simpl 484 |
. . . . . 6
β’ ((π = π β§ π = π) β π = π) |
19 | 17, 18 | feq12d 6706 |
. . . . 5
β’ ((π = π β§ π = π) β (π:π βΆ(0[,]+β) β π:πβΆ(0[,]+β))) |
20 | | fveq1 6891 |
. . . . . . 7
β’ (π = π β (πββ
) = (πββ
)) |
21 | 20 | eqeq1d 2735 |
. . . . . 6
β’ (π = π β ((πββ
) = 0 β (πββ
) = 0)) |
22 | 21 | adantl 483 |
. . . . 5
β’ ((π = π β§ π = π) β ((πββ
) = 0 β (πββ
) = 0)) |
23 | 18 | pweqd 4620 |
. . . . . 6
β’ ((π = π β§ π = π) β π« π = π« π) |
24 | | fveq1 6891 |
. . . . . . . . 9
β’ (π = π β (πββͺ π₯) = (πββͺ π₯)) |
25 | | fveq1 6891 |
. . . . . . . . . 10
β’ (π = π β (πβπ¦) = (πβπ¦)) |
26 | 25 | esumeq2sdv 33037 |
. . . . . . . . 9
β’ (π = π β Ξ£*π¦ β π₯(πβπ¦) = Ξ£*π¦ β π₯(πβπ¦)) |
27 | 24, 26 | eqeq12d 2749 |
. . . . . . . 8
β’ (π = π β ((πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))) |
28 | 27 | imbi2d 341 |
. . . . . . 7
β’ (π = π β (((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))) |
29 | 28 | adantl 483 |
. . . . . 6
β’ ((π = π β§ π = π) β (((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))) |
30 | 23, 29 | raleqbidv 3343 |
. . . . 5
β’ ((π = π β§ π = π) β (βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)) β βπ₯ β π« π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))) |
31 | 19, 22, 30 | 3anbi123d 1437 |
. . . 4
β’ ((π = π β§ π = π) β ((π:π βΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))) β (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))))) |
32 | 10, 16, 31 | abfmpel 31880 |
. . 3
β’ ((π β βͺ ran sigAlgebra β§ π β V) β (π β (measuresβπ) β (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))))) |
33 | 32 | ex 414 |
. 2
β’ (π β βͺ ran sigAlgebra β (π β V β (π β (measuresβπ) β (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))))) |
34 | 2, 9, 33 | pm5.21ndd 381 |
1
β’ (π β βͺ ran sigAlgebra β (π β (measuresβπ) β (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))))) |