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 32011 |
. . . . . . . 8
⊢ (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))) |
10 | 9 | dmeqd 5774 |
. . . . . . 7
⊢ (𝜑 → dom (𝑊sitg𝑀) = dom (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))) |
11 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))) |
12 | 11 | dmmpt 6103 |
. . . . . . 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 2794 |
. . . . . 6
⊢ (𝜑 → dom (𝑊sitg𝑀) = {𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ∣ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))) ∈ V}) |
14 | 13 | eleq2d 2823 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ dom (𝑊sitg𝑀) ↔ 𝐹 ∈ {𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ∣ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))) ∈ V})) |
15 | | rneq 5805 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → ran 𝑓 = ran 𝐹) |
16 | 15 | difeq1d 4036 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (ran 𝑓 ∖ { 0 }) = (ran 𝐹 ∖ { 0 })) |
17 | | cnveq 5742 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹) |
18 | 17 | imaeq1d 5928 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → (◡𝑓 “ {𝑥}) = (◡𝐹 “ {𝑥})) |
19 | 18 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑀‘(◡𝑓 “ {𝑥})) = (𝑀‘(◡𝐹 “ {𝑥}))) |
20 | 19 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥})))) |
21 | 20 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥) = ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
22 | 16, 21 | mpteq12dv 5140 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) |
23 | 22 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)))) |
24 | 23 | eleq1d 2822 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))) ∈ V ↔ (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ V)) |
25 | 24 | elrab 3602 |
. . . . 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 290 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ dom (𝑊sitg𝑀) ↔ (𝐹 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ∧ (𝑊 Σg
(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ V))) |
27 | | ovex 7246 |
. . . . 5
⊢ (𝑊 Σg
(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ V |
28 | 27 | biantru 533 |
. . . 4
⊢ (𝐹 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↔ (𝐹 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ∧ (𝑊 Σg
(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ V)) |
29 | 26, 28 | bitr4di 292 |
. . 3
⊢ (𝜑 → (𝐹 ∈ dom (𝑊sitg𝑀) ↔ 𝐹 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈
(0[,)+∞))})) |
30 | | rneq 5805 |
. . . . . 6
⊢ (𝑔 = 𝐹 → ran 𝑔 = ran 𝐹) |
31 | 30 | eleq1d 2822 |
. . . . 5
⊢ (𝑔 = 𝐹 → (ran 𝑔 ∈ Fin ↔ ran 𝐹 ∈ Fin)) |
32 | 30 | difeq1d 4036 |
. . . . . 6
⊢ (𝑔 = 𝐹 → (ran 𝑔 ∖ { 0 }) = (ran 𝐹 ∖ { 0 })) |
33 | | cnveq 5742 |
. . . . . . . . 9
⊢ (𝑔 = 𝐹 → ◡𝑔 = ◡𝐹) |
34 | 33 | imaeq1d 5928 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (◡𝑔 “ {𝑥}) = (◡𝐹 “ {𝑥})) |
35 | 34 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑔 = 𝐹 → (𝑀‘(◡𝑔 “ {𝑥})) = (𝑀‘(◡𝐹 “ {𝑥}))) |
36 | 35 | eleq1d 2822 |
. . . . . 6
⊢ (𝑔 = 𝐹 → ((𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ (𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞))) |
37 | 32, 36 | raleqbidv 3313 |
. . . . 5
⊢ (𝑔 = 𝐹 → (∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔
∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞))) |
38 | 31, 37 | anbi12d 634 |
. . . 4
⊢ (𝑔 = 𝐹 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)))) |
39 | 38 | elrab 3602 |
. . 3
⊢ (𝐹 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↔ (𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ (ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)))) |
40 | 29, 39 | bitrdi 290 |
. 2
⊢ (𝜑 → (𝐹 ∈ dom (𝑊sitg𝑀) ↔ (𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ (ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈
(0[,)+∞))))) |
41 | | 3anass 1097 |
. 2
⊢ ((𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)) ↔ (𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ (ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)))) |
42 | 40, 41 | bitr4di 292 |
1
⊢ (𝜑 → (𝐹 ∈ dom (𝑊sitg𝑀) ↔ (𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)))) |