Step | Hyp | Ref
| Expression |
1 | | sitgval.1 |
. . 3
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
2 | 1 | elexd 3187 |
. 2
⊢ (𝜑 → 𝑊 ∈ V) |
3 | | sitgval.2 |
. 2
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
4 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (TopOpen‘𝑤) = (TopOpen‘𝑊)) |
5 | 4 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) =
(sigaGen‘(TopOpen‘𝑊))) |
6 | | sitgval.s |
. . . . . . . 8
⊢ 𝑆 = (sigaGen‘𝐽) |
7 | | sitgval.j |
. . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝑊) |
8 | 7 | fveq2i 6106 |
. . . . . . . 8
⊢
(sigaGen‘𝐽) =
(sigaGen‘(TopOpen‘𝑊)) |
9 | 6, 8 | eqtri 2632 |
. . . . . . 7
⊢ 𝑆 =
(sigaGen‘(TopOpen‘𝑊)) |
10 | 5, 9 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = 𝑆) |
11 | 10 | oveq2d 6565 |
. . . . 5
⊢ (𝑤 = 𝑊 → (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) = (dom 𝑚MblFnM𝑆)) |
12 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊)) |
13 | | sitgval.0 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑊) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 ) |
15 | 14 | sneqd 4137 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → {(0g‘𝑤)} = { 0 }) |
16 | 15 | difeq2d 3690 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (ran 𝑔 ∖ {(0g‘𝑤)}) = (ran 𝑔 ∖ { 0 })) |
17 | 16 | raleqdv 3121 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔
∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))) |
18 | 17 | anbi2d 736 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))) |
19 | 11, 18 | rabeqbidv 3168 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))}) |
20 | | id 22 |
. . . . 5
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
21 | 15 | difeq2d 3690 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (ran 𝑓 ∖ {(0g‘𝑤)}) = (ran 𝑓 ∖ { 0 })) |
22 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = ( ·𝑠
‘𝑊)) |
23 | | sitgval.x |
. . . . . . . 8
⊢ · = (
·𝑠 ‘𝑊) |
24 | 22, 23 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = · ) |
25 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
26 | 25 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 →
(ℝHom‘(Scalar‘𝑤)) = (ℝHom‘(Scalar‘𝑊))) |
27 | | sitgval.h |
. . . . . . . . 9
⊢ 𝐻 =
(ℝHom‘(Scalar‘𝑊)) |
28 | 26, 27 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 →
(ℝHom‘(Scalar‘𝑤)) = 𝐻) |
29 | 28 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑤 = 𝑊 →
((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑚‘(◡𝑓 “ {𝑥})))) |
30 | | eqidd 2611 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥) |
31 | 24, 29, 30 | oveq123d 6570 |
. . . . . 6
⊢ (𝑤 = 𝑊 →
(((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥) = ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)) |
32 | 21, 31 | mpteq12dv 4663 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦
(((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))) |
33 | 20, 32 | oveq12d 6567 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦
(((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))) |
34 | 19, 33 | mpteq12dv 4663 |
. . 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 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))))) |
35 | | dmeq 5246 |
. . . . . 6
⊢ (𝑚 = 𝑀 → dom 𝑚 = dom 𝑀) |
36 | 35 | oveq1d 6564 |
. . . . 5
⊢ (𝑚 = 𝑀 → (dom 𝑚MblFnM𝑆) = (dom 𝑀MblFnM𝑆)) |
37 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑚‘(◡𝑔 “ {𝑥})) = (𝑀‘(◡𝑔 “ {𝑥}))) |
38 | 37 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ (𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))) |
39 | 38 | ralbidv 2969 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔
∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))) |
40 | 39 | anbi2d 736 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))) |
41 | 36, 40 | rabeqbidv 3168 |
. . . 4
⊢ (𝑚 = 𝑀 → {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))}) |
42 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → 𝑚 = 𝑀) |
43 | 42 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝑚‘(◡𝑓 “ {𝑥})) = (𝑀‘(◡𝑓 “ {𝑥}))) |
44 | 43 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑀‘(◡𝑓 “ {𝑥})))) |
45 | 44 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥) = ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)) |
46 | 45 | mpteq2dva 4672 |
. . . . 5
⊢ (𝑚 = 𝑀 → (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))) |
47 | 46 | oveq2d 6565 |
. . . 4
⊢ (𝑚 = 𝑀 → (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))) |
48 | 41, 47 | mpteq12dv 4663 |
. . 3
⊢ (𝑚 = 𝑀 → (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))) |
49 | | df-sitg 29719 |
. . 3
⊢ sitg =
(𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg
(𝑥 ∈ (ran 𝑓 ∖
{(0g‘𝑤)})
↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥))))) |
50 | | ovex 6577 |
. . . 4
⊢ (dom
𝑀MblFnM𝑆) ∈ V |
51 | 50 | mptrabex 6392 |
. . 3
⊢ (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))) ∈ V |
52 | 34, 48, 49, 51 | ovmpt2 6694 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝑀 ∈ ∪ ran measures) → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))) |
53 | 2, 3, 52 | syl2anc 691 |
1
⊢ (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))) |