Step | Hyp | Ref
| Expression |
1 | | sitgval.b |
. . 3
β’ π΅ = (Baseβπ) |
2 | | sitgval.j |
. . 3
β’ π½ = (TopOpenβπ) |
3 | | sitgval.s |
. . 3
β’ π = (sigaGenβπ½) |
4 | | sitgval.0 |
. . 3
β’ 0 =
(0gβπ) |
5 | | sitgval.x |
. . 3
β’ Β· = (
Β·π βπ) |
6 | | sitgval.h |
. . 3
β’ π» =
(βHomβ(Scalarβπ)) |
7 | | sitgval.1 |
. . 3
β’ (π β π β π) |
8 | | sitgval.2 |
. . 3
β’ (π β π β βͺ ran
measures) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | sitgval 33331 |
. 2
β’ (π β (πsitgπ) = (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))))) |
10 | | simpr 486 |
. . . . . 6
β’ ((π β§ π = πΉ) β π = πΉ) |
11 | 10 | rneqd 5938 |
. . . . 5
β’ ((π β§ π = πΉ) β ran π = ran πΉ) |
12 | 11 | difeq1d 4122 |
. . . 4
β’ ((π β§ π = πΉ) β (ran π β { 0 }) = (ran πΉ β { 0 })) |
13 | 10 | cnveqd 5876 |
. . . . . . . 8
β’ ((π β§ π = πΉ) β β‘π = β‘πΉ) |
14 | 13 | imaeq1d 6059 |
. . . . . . 7
β’ ((π β§ π = πΉ) β (β‘π β {π₯}) = (β‘πΉ β {π₯})) |
15 | 14 | fveq2d 6896 |
. . . . . 6
β’ ((π β§ π = πΉ) β (πβ(β‘π β {π₯})) = (πβ(β‘πΉ β {π₯}))) |
16 | 15 | fveq2d 6896 |
. . . . 5
β’ ((π β§ π = πΉ) β (π»β(πβ(β‘π β {π₯}))) = (π»β(πβ(β‘πΉ β {π₯})))) |
17 | 16 | oveq1d 7424 |
. . . 4
β’ ((π β§ π = πΉ) β ((π»β(πβ(β‘π β {π₯}))) Β· π₯) = ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯)) |
18 | 12, 17 | mpteq12dv 5240 |
. . 3
β’ ((π β§ π = πΉ) β (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)) = (π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯))) |
19 | 18 | oveq2d 7425 |
. 2
β’ ((π β§ π = πΉ) β (π Ξ£g (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) = (π Ξ£g (π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯)))) |
20 | | sibfmbl.1 |
. . . . 5
β’ (π β πΉ β dom (πsitgπ)) |
21 | 1, 2, 3, 4, 5, 6, 7, 8, 20 | sibfmbl 33334 |
. . . 4
β’ (π β πΉ β (dom πMblFnMπ)) |
22 | 1, 2, 3, 4, 5, 6, 7, 8, 20 | sibfrn 33336 |
. . . 4
β’ (π β ran πΉ β Fin) |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 20 | sibfima 33337 |
. . . . 5
β’ ((π β§ π₯ β (ran πΉ β { 0 })) β (πβ(β‘πΉ β {π₯})) β (0[,)+β)) |
24 | 23 | ralrimiva 3147 |
. . . 4
β’ (π β βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)) |
25 | 21, 22, 24 | jca32 517 |
. . 3
β’ (π β (πΉ β (dom πMblFnMπ) β§ (ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)))) |
26 | | rneq 5936 |
. . . . . 6
β’ (π = πΉ β ran π = ran πΉ) |
27 | 26 | eleq1d 2819 |
. . . . 5
β’ (π = πΉ β (ran π β Fin β ran πΉ β Fin)) |
28 | 26 | difeq1d 4122 |
. . . . . 6
β’ (π = πΉ β (ran π β { 0 }) = (ran πΉ β { 0 })) |
29 | | cnveq 5874 |
. . . . . . . . 9
β’ (π = πΉ β β‘π = β‘πΉ) |
30 | 29 | imaeq1d 6059 |
. . . . . . . 8
β’ (π = πΉ β (β‘π β {π₯}) = (β‘πΉ β {π₯})) |
31 | 30 | fveq2d 6896 |
. . . . . . 7
β’ (π = πΉ β (πβ(β‘π β {π₯})) = (πβ(β‘πΉ β {π₯}))) |
32 | 31 | eleq1d 2819 |
. . . . . 6
β’ (π = πΉ β ((πβ(β‘π β {π₯})) β (0[,)+β) β (πβ(β‘πΉ β {π₯})) β (0[,)+β))) |
33 | 28, 32 | raleqbidv 3343 |
. . . . 5
β’ (π = πΉ β (βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β) β
βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β))) |
34 | 27, 33 | anbi12d 632 |
. . . 4
β’ (π = πΉ β ((ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β)) β (ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)))) |
35 | 34 | elrab 3684 |
. . 3
β’ (πΉ β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β (πΉ β (dom πMblFnMπ) β§ (ran πΉ β Fin β§ βπ₯ β (ran πΉ β { 0 })(πβ(β‘πΉ β {π₯})) β (0[,)+β)))) |
36 | 25, 35 | sylibr 233 |
. 2
β’ (π β πΉ β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))}) |
37 | | ovexd 7444 |
. 2
β’ (π β (π Ξ£g (π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯))) β V) |
38 | 9, 19, 36, 37 | fvmptd 7006 |
1
β’ (π β ((πsitgπ)βπΉ) = (π Ξ£g (π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯)))) |