Step | Hyp | Ref
| Expression |
1 | | sitgval.2 |
. . . 4
β’ (π β π β βͺ ran
measures) |
2 | | dmmeas 32864 |
. . . 4
β’ (π β βͺ ran measures β dom π β βͺ ran
sigAlgebra) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β dom π β βͺ ran
sigAlgebra) |
4 | | sitgval.s |
. . . 4
β’ π = (sigaGenβπ½) |
5 | | sitgval.j |
. . . . . . 7
β’ π½ = (TopOpenβπ) |
6 | 5 | fvexi 6860 |
. . . . . 6
β’ π½ β V |
7 | 6 | a1i 11 |
. . . . 5
β’ (π β π½ β V) |
8 | 7 | sgsiga 32805 |
. . . 4
β’ (π β (sigaGenβπ½) β βͺ ran sigAlgebra) |
9 | 4, 8 | eqeltrid 2838 |
. . 3
β’ (π β π β βͺ ran
sigAlgebra) |
10 | | fconstmpt 5698 |
. . . 4
β’ (βͺ dom π Γ { 0 }) = (π₯ β βͺ dom
π β¦ 0
) |
11 | 10 | a1i 11 |
. . 3
β’ (π β (βͺ dom π Γ { 0 }) = (π₯ β βͺ dom
π β¦ 0
)) |
12 | | sibf0.2 |
. . . . 5
β’ (π β π β Mnd) |
13 | | sitgval.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
14 | | sitgval.0 |
. . . . . 6
β’ 0 =
(0gβπ) |
15 | 13, 14 | mndidcl 18579 |
. . . . 5
β’ (π β Mnd β 0 β π΅) |
16 | 12, 15 | syl 17 |
. . . 4
β’ (π β 0 β π΅) |
17 | | sibf0.1 |
. . . . . 6
β’ (π β π β TopSp) |
18 | 13, 5 | tpsuni 22308 |
. . . . . 6
β’ (π β TopSp β π΅ = βͺ
π½) |
19 | 17, 18 | syl 17 |
. . . . 5
β’ (π β π΅ = βͺ π½) |
20 | 4 | unieqi 4882 |
. . . . . 6
β’ βͺ π =
βͺ (sigaGenβπ½) |
21 | | unisg 32806 |
. . . . . . 7
β’ (π½ β V β βͺ (sigaGenβπ½) = βͺ π½) |
22 | 6, 21 | mp1i 13 |
. . . . . 6
β’ (π β βͺ (sigaGenβπ½) = βͺ π½) |
23 | 20, 22 | eqtrid 2785 |
. . . . 5
β’ (π β βͺ π =
βͺ π½) |
24 | 19, 23 | eqtr4d 2776 |
. . . 4
β’ (π β π΅ = βͺ π) |
25 | 16, 24 | eleqtrd 2836 |
. . 3
β’ (π β 0 β βͺ π) |
26 | 3, 9, 11, 25 | mbfmcst 32923 |
. 2
β’ (π β (βͺ dom π Γ { 0 }) β (dom πMblFnMπ)) |
27 | | xpeq1 5651 |
. . . . . . . 8
β’ (βͺ dom π = β
β (βͺ dom π Γ { 0 }) = (β
Γ {
0
})) |
28 | | 0xp 5734 |
. . . . . . . 8
β’ (β
Γ { 0 }) =
β
|
29 | 27, 28 | eqtrdi 2789 |
. . . . . . 7
β’ (βͺ dom π = β
β (βͺ dom π Γ { 0 }) =
β
) |
30 | 29 | rneqd 5897 |
. . . . . 6
β’ (βͺ dom π = β
β ran (βͺ dom π Γ { 0 }) = ran
β
) |
31 | | rn0 5885 |
. . . . . 6
β’ ran
β
= β
|
32 | 30, 31 | eqtrdi 2789 |
. . . . 5
β’ (βͺ dom π = β
β ran (βͺ dom π Γ { 0 }) =
β
) |
33 | | 0fin 9121 |
. . . . 5
β’ β
β Fin |
34 | 32, 33 | eqeltrdi 2842 |
. . . 4
β’ (βͺ dom π = β
β ran (βͺ dom π Γ { 0 }) β
Fin) |
35 | | rnxp 6126 |
. . . . 5
β’ (βͺ dom π β β
β ran (βͺ dom π Γ { 0 }) = { 0 }) |
36 | | snfi 8994 |
. . . . 5
β’ { 0 } β
Fin |
37 | 35, 36 | eqeltrdi 2842 |
. . . 4
β’ (βͺ dom π β β
β ran (βͺ dom π Γ { 0 }) β
Fin) |
38 | 34, 37 | pm2.61ine 3025 |
. . 3
β’ ran
(βͺ dom π Γ { 0 }) β
Fin |
39 | 38 | a1i 11 |
. 2
β’ (π β ran (βͺ dom π Γ { 0 }) β
Fin) |
40 | | noel 4294 |
. . . . . 6
β’ Β¬
π₯ β
β
|
41 | 32 | difeq1d 4085 |
. . . . . . . . 9
β’ (βͺ dom π = β
β (ran (βͺ dom π Γ { 0 }) β { 0 }) = (β
β { 0 })) |
42 | | 0dif 4365 |
. . . . . . . . 9
β’ (β
β { 0 }) =
β
|
43 | 41, 42 | eqtrdi 2789 |
. . . . . . . 8
β’ (βͺ dom π = β
β (ran (βͺ dom π Γ { 0 }) β { 0 }) =
β
) |
44 | 35 | difeq1d 4085 |
. . . . . . . . 9
β’ (βͺ dom π β β
β (ran (βͺ dom π Γ { 0 }) β { 0 }) = ({ 0 } β {
0
})) |
45 | | difid 4334 |
. . . . . . . . 9
β’ ({ 0 } β {
0 }) =
β
|
46 | 44, 45 | eqtrdi 2789 |
. . . . . . . 8
β’ (βͺ dom π β β
β (ran (βͺ dom π Γ { 0 }) β { 0 }) =
β
) |
47 | 43, 46 | pm2.61ine 3025 |
. . . . . . 7
β’ (ran
(βͺ dom π Γ { 0 }) β { 0 }) =
β
|
48 | 47 | eleq2i 2826 |
. . . . . 6
β’ (π₯ β (ran (βͺ dom π Γ { 0 }) β { 0 }) β
π₯ β
β
) |
49 | 40, 48 | mtbir 323 |
. . . . 5
β’ Β¬
π₯ β (ran (βͺ dom π Γ { 0 }) β { 0
}) |
50 | 49 | pm2.21i 119 |
. . . 4
β’ (π₯ β (ran (βͺ dom π Γ { 0 }) β { 0 }) β
(πβ(β‘(βͺ dom π Γ { 0 }) β {π₯})) β
(0[,)+β)) |
51 | 50 | adantl 483 |
. . 3
β’ ((π β§ π₯ β (ran (βͺ
dom π Γ { 0 }) β {
0 }))
β (πβ(β‘(βͺ dom π Γ { 0 }) β {π₯})) β
(0[,)+β)) |
52 | 51 | ralrimiva 3140 |
. 2
β’ (π β βπ₯ β (ran (βͺ
dom π Γ { 0 }) β {
0
})(πβ(β‘(βͺ dom π Γ { 0 }) β {π₯})) β
(0[,)+β)) |
53 | | sitgval.x |
. . 3
β’ Β· = (
Β·π βπ) |
54 | | sitgval.h |
. . 3
β’ π» =
(βHomβ(Scalarβπ)) |
55 | | sitgval.1 |
. . 3
β’ (π β π β π) |
56 | 13, 5, 4, 14, 53, 54, 55, 1 | issibf 32997 |
. 2
β’ (π β ((βͺ dom π Γ { 0 }) β dom (πsitgπ) β ((βͺ dom
π Γ { 0 }) β
(dom πMblFnMπ) β§ ran (βͺ dom π Γ { 0 }) β Fin β§
βπ₯ β (ran
(βͺ dom π Γ { 0 }) β { 0 })(πβ(β‘(βͺ dom π Γ { 0 }) β {π₯})) β
(0[,)+β)))) |
57 | 26, 39, 52, 56 | mpbir3and 1343 |
1
β’ (π β (βͺ dom π Γ { 0 }) β dom (πsitgπ)) |