Step | Hyp | Ref
| Expression |
1 | | sitgval.1 |
. . 3
β’ (π β π β π) |
2 | 1 | elexd 3479 |
. 2
β’ (π β π β V) |
3 | | sitgval.2 |
. 2
β’ (π β π β βͺ ran
measures) |
4 | | 2fveq3 6867 |
. . . . . . 7
β’ (π€ = π β (sigaGenβ(TopOpenβπ€)) =
(sigaGenβ(TopOpenβπ))) |
5 | | sitgval.s |
. . . . . . . 8
β’ π = (sigaGenβπ½) |
6 | | sitgval.j |
. . . . . . . . 9
β’ π½ = (TopOpenβπ) |
7 | 6 | fveq2i 6865 |
. . . . . . . 8
β’
(sigaGenβπ½) =
(sigaGenβ(TopOpenβπ)) |
8 | 5, 7 | eqtri 2759 |
. . . . . . 7
β’ π =
(sigaGenβ(TopOpenβπ)) |
9 | 4, 8 | eqtr4di 2789 |
. . . . . 6
β’ (π€ = π β (sigaGenβ(TopOpenβπ€)) = π) |
10 | 9 | oveq2d 7393 |
. . . . 5
β’ (π€ = π β (dom πMblFnM(sigaGenβ(TopOpenβπ€))) = (dom πMblFnMπ)) |
11 | | fveq2 6862 |
. . . . . . . . . 10
β’ (π€ = π β (0gβπ€) = (0gβπ)) |
12 | | sitgval.0 |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
13 | 11, 12 | eqtr4di 2789 |
. . . . . . . . 9
β’ (π€ = π β (0gβπ€) = 0 ) |
14 | 13 | sneqd 4618 |
. . . . . . . 8
β’ (π€ = π β {(0gβπ€)} = { 0 }) |
15 | 14 | difeq2d 4102 |
. . . . . . 7
β’ (π€ = π β (ran π β {(0gβπ€)}) = (ran π β { 0 })) |
16 | 15 | raleqdv 3324 |
. . . . . 6
β’ (π€ = π β (βπ₯ β (ran π β {(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β) β
βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))) |
17 | 16 | anbi2d 629 |
. . . . 5
β’ (π€ = π β ((ran π β Fin β§ βπ₯ β (ran π β {(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β)) β (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β)))) |
18 | 10, 17 | rabeqbidv 3435 |
. . . 4
β’ (π€ = π β {π β (dom πMblFnM(sigaGenβ(TopOpenβπ€))) β£ (ran π β Fin β§ βπ₯ β (ran π β {(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β))} = {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))}) |
19 | | id 22 |
. . . . 5
β’ (π€ = π β π€ = π) |
20 | 14 | difeq2d 4102 |
. . . . . 6
β’ (π€ = π β (ran π β {(0gβπ€)}) = (ran π β { 0 })) |
21 | | fveq2 6862 |
. . . . . . . 8
β’ (π€ = π β (
Β·π βπ€) = ( Β·π
βπ)) |
22 | | sitgval.x |
. . . . . . . 8
β’ Β· = (
Β·π βπ) |
23 | 21, 22 | eqtr4di 2789 |
. . . . . . 7
β’ (π€ = π β (
Β·π βπ€) = Β· ) |
24 | | 2fveq3 6867 |
. . . . . . . . 9
β’ (π€ = π β
(βHomβ(Scalarβπ€)) = (βHomβ(Scalarβπ))) |
25 | | sitgval.h |
. . . . . . . . 9
β’ π» =
(βHomβ(Scalarβπ)) |
26 | 24, 25 | eqtr4di 2789 |
. . . . . . . 8
β’ (π€ = π β
(βHomβ(Scalarβπ€)) = π») |
27 | 26 | fveq1d 6864 |
. . . . . . 7
β’ (π€ = π β
((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯}))) = (π»β(πβ(β‘π β {π₯})))) |
28 | | eqidd 2732 |
. . . . . . 7
β’ (π€ = π β π₯ = π₯) |
29 | 23, 27, 28 | oveq123d 7398 |
. . . . . 6
β’ (π€ = π β
(((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯) = ((π»β(πβ(β‘π β {π₯}))) Β· π₯)) |
30 | 20, 29 | mpteq12dv 5216 |
. . . . 5
β’ (π€ = π β (π₯ β (ran π β {(0gβπ€)}) β¦
(((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯)) = (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) |
31 | 19, 30 | oveq12d 7395 |
. . . 4
β’ (π€ = π β (π€ Ξ£g (π₯ β (ran π β {(0gβπ€)}) β¦
(((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯))) = (π Ξ£g (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)))) |
32 | 18, 31 | mpteq12dv 5216 |
. . 3
β’ (π€ = π β (π β {π β (dom πMblFnM(sigaGenβ(TopOpenβπ€))) β£ (ran π β Fin β§ βπ₯ β (ran π β {(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π€ Ξ£g
(π₯ β (ran π β
{(0gβπ€)})
β¦ (((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯)))) = (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))))) |
33 | | dmeq 5879 |
. . . . . 6
β’ (π = π β dom π = dom π) |
34 | 33 | oveq1d 7392 |
. . . . 5
β’ (π = π β (dom πMblFnMπ) = (dom πMblFnMπ)) |
35 | | fveq1 6861 |
. . . . . . . 8
β’ (π = π β (πβ(β‘π β {π₯})) = (πβ(β‘π β {π₯}))) |
36 | 35 | eleq1d 2817 |
. . . . . . 7
β’ (π = π β ((πβ(β‘π β {π₯})) β (0[,)+β) β (πβ(β‘π β {π₯})) β (0[,)+β))) |
37 | 36 | ralbidv 3176 |
. . . . . 6
β’ (π = π β (βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β) β
βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))) |
38 | 37 | anbi2d 629 |
. . . . 5
β’ (π = π β ((ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β)) β (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β)))) |
39 | 34, 38 | rabeqbidv 3435 |
. . . 4
β’ (π = π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} = {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))}) |
40 | | simpl 483 |
. . . . . . . . 9
β’ ((π = π β§ π₯ β (ran π β { 0 })) β π = π) |
41 | 40 | fveq1d 6864 |
. . . . . . . 8
β’ ((π = π β§ π₯ β (ran π β { 0 })) β (πβ(β‘π β {π₯})) = (πβ(β‘π β {π₯}))) |
42 | 41 | fveq2d 6866 |
. . . . . . 7
β’ ((π = π β§ π₯ β (ran π β { 0 })) β (π»β(πβ(β‘π β {π₯}))) = (π»β(πβ(β‘π β {π₯})))) |
43 | 42 | oveq1d 7392 |
. . . . . 6
β’ ((π = π β§ π₯ β (ran π β { 0 })) β ((π»β(πβ(β‘π β {π₯}))) Β· π₯) = ((π»β(πβ(β‘π β {π₯}))) Β· π₯)) |
44 | 43 | mpteq2dva 5225 |
. . . . 5
β’ (π = π β (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)) = (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) |
45 | 44 | oveq2d 7393 |
. . . 4
β’ (π = π β (π Ξ£g (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))) = (π Ξ£g (π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)))) |
46 | 39, 45 | mpteq12dv 5216 |
. . 3
β’ (π = π β (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)))) = (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))))) |
47 | | df-sitg 33053 |
. . 3
β’ sitg =
(π€ β V, π β βͺ ran measures β¦ (π β {π β (dom πMblFnM(sigaGenβ(TopOpenβπ€))) β£ (ran π β Fin β§ βπ₯ β (ran π β {(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π€ Ξ£g
(π₯ β (ran π β
{(0gβπ€)})
β¦ (((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯))))) |
48 | | ovex 7410 |
. . . 4
β’ (dom
πMblFnMπ) β V |
49 | 48 | mptrabex 7195 |
. . 3
β’ (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯)))) β V |
50 | 32, 46, 47, 49 | ovmpo 7535 |
. 2
β’ ((π β V β§ π β βͺ ran measures) β (πsitgπ) = (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))))) |
51 | 2, 3, 50 | syl2anc 584 |
1
β’ (π β (πsitgπ) = (π β {π β (dom πMblFnMπ) β£ (ran π β Fin β§ βπ₯ β (ran π β { 0 })(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π Ξ£g
(π₯ β (ran π β { 0 }) β¦ ((π»β(πβ(β‘π β {π₯}))) Β· π₯))))) |