Step | Hyp | Ref
| Expression |
1 | | sitgval.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
2 | | sitgval.j |
. . . . . . . . 9
β’ π½ = (TopOpenβπ) |
3 | | sitgval.s |
. . . . . . . . 9
β’ π = (sigaGenβπ½) |
4 | | sitgval.0 |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
5 | | sitgval.x |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
6 | | sitgval.h |
. . . . . . . . 9
β’ π» =
(βHomβ(Scalarβπ)) |
7 | | sitgval.1 |
. . . . . . . . 9
β’ (π β π β π) |
8 | | sitgval.2 |
. . . . . . . . 9
β’ (π β π β βͺ ran
measures) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | sitgval 33331 |
. . . . . . . 8
β’ (π β (πsitgπ) = (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))))) |
10 | 9 | dmeqd 5906 |
. . . . . . 7
β’ (π β dom (πsitgπ) = dom (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))))) |
11 | | eqid 2733 |
. . . . . . . 8
β’ (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)))) = (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)))) |
12 | 11 | dmmpt 6240 |
. . . . . . 7
β’ dom
(π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)))) = {π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β£ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) β V} |
13 | 10, 12 | eqtrdi 2789 |
. . . . . 6
β’ (π β dom (πsitgπ) = {π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β£ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) β V}) |
14 | 13 | eleq2d 2820 |
. . . . 5
β’ (π β (πΉ β dom (πsitgπ) β πΉ β {π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β£ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) β V})) |
15 | | rneq 5936 |
. . . . . . . . . 10
β’ (π = πΉ β ran π = ran πΉ) |
16 | 15 | difeq1d 4122 |
. . . . . . . . 9
β’ (π = πΉ β (ran π β { 0 }) = (ran πΉ β { 0 })) |
17 | | cnveq 5874 |
. . . . . . . . . . . . 13
β’ (π = πΉ β β‘π = β‘πΉ) |
18 | 17 | imaeq1d 6059 |
. . . . . . . . . . . 12
β’ (π = πΉ β (β‘π β {π₯}) = (β‘πΉ β {π₯})) |
19 | 18 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (π = πΉ β (πβ(β‘π β {π₯})) = (πβ(β‘πΉ β {π₯}))) |
20 | 19 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π = πΉ β (π»β(πβ(β‘π β {π₯}))) = (π»β(πβ(β‘πΉ β {π₯})))) |
21 | 20 | oveq1d 7424 |
. . . . . . . . 9
β’ (π = πΉ β ((π»β(πβ(β‘π β {π₯}))) Β· π₯) = ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯)) |
22 | 16, 21 | mpteq12dv 5240 |
. . . . . . . 8
β’ (π = πΉ β (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)) = (π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯))) |
23 | 22 | oveq2d 7425 |
. . . . . . 7
β’ (π = πΉ β (π Ξ£g (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) = (π Ξ£g (π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯)))) |
24 | 23 | eleq1d 2819 |
. . . . . 6
β’ (π = πΉ β ((π Ξ£g (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) β V β (π Ξ£g (π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯))) β V)) |
25 | 24 | elrab 3684 |
. . . . 5
β’ (πΉ β {π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β£ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) β V} β (πΉ β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β§ (π Ξ£g
(π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯))) β V)) |
26 | 14, 25 | bitrdi 287 |
. . . 4
β’ (π β (πΉ β dom (πsitgπ) β (πΉ β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β§ (π Ξ£g
(π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯))) β V))) |
27 | | ovex 7442 |
. . . . 5
β’ (π Ξ£g
(π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯))) β V |
28 | 27 | biantru 531 |
. . . 4
β’ (πΉ β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β (πΉ β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β§ (π Ξ£g
(π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯))) β V)) |
29 | 26, 28 | bitr4di 289 |
. . 3
β’ (π β (πΉ β dom (πsitgπ) β πΉ β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β
(0[,)+β))})) |
30 | | rneq 5936 |
. . . . . 6
β’ (π = πΉ β ran π = ran πΉ) |
31 | 30 | eleq1d 2819 |
. . . . 5
β’ (π = πΉ β (ran π β Fin β ran πΉ β Fin)) |
32 | 30 | difeq1d 4122 |
. . . . . 6
β’ (π = πΉ β (ran π β { 0 }) = (ran πΉ β { 0 })) |
33 | | cnveq 5874 |
. . . . . . . . 9
β’ (π = πΉ β β‘π = β‘πΉ) |
34 | 33 | imaeq1d 6059 |
. . . . . . . 8
β’ (π = πΉ β (β‘π β {π₯}) = (β‘πΉ β {π₯})) |
35 | 34 | fveq2d 6896 |
. . . . . . 7
β’ (π = πΉ β (πβ(β‘π β {π₯})) = (πβ(β‘πΉ β {π₯}))) |
36 | 35 | eleq1d 2819 |
. . . . . 6
β’ (π = πΉ β ((πβ(β‘π β {π₯})) β (0[,)+β) β (πβ(β‘πΉ β {π₯})) β (0[,)+β))) |
37 | 32, 36 | raleqbidv 3343 |
. . . . 5
β’ (π = πΉ β (βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β) β
βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β))) |
38 | 31, 37 | anbi12d 632 |
. . . 4
β’ (π = πΉ β ((ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β)) β (ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)))) |
39 | 38 | elrab 3684 |
. . 3
β’ (πΉ β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β (πΉ β (dom πMblFnMπ) β§ (ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)))) |
40 | 29, 39 | bitrdi 287 |
. 2
β’ (π β (πΉ β dom (πsitgπ) β (πΉ β (dom πMblFnMπ) β§ (ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β
(0[,)+β))))) |
41 | | 3anass 1096 |
. 2
β’ ((πΉ β (dom πMblFnMπ) β§ ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)) β (πΉ β (dom πMblFnMπ) β§ (ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)))) |
42 | 40, 41 | bitr4di 289 |
1
β’ (π β (πΉ β dom (πsitgπ) β (πΉ β (dom πMblFnMπ) β§ ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)))) |