| Step | Hyp | Ref
| Expression |
| 1 | | sitmval.1 |
. . 3
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
| 2 | | elex 3501 |
. . 3
⊢ (𝑊 ∈ 𝑉 → 𝑊 ∈ V) |
| 3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑊 ∈ V) |
| 4 | | sitmval.2 |
. 2
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
| 5 | | oveq1 7438 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑤sitg𝑚) = (𝑊sitg𝑚)) |
| 6 | 5 | dmeqd 5916 |
. . . 4
⊢ (𝑤 = 𝑊 → dom (𝑤sitg𝑚) = dom (𝑊sitg𝑚)) |
| 7 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (dist‘𝑤) = (dist‘𝑊)) |
| 8 | 7 | ofeqd 7699 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ∘f
(dist‘𝑤) =
∘f (dist‘𝑊)) |
| 9 | 8 | oveqd 7448 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑓 ∘f (dist‘𝑤)𝑔) = (𝑓 ∘f (dist‘𝑊)𝑔)) |
| 10 | 9 | fveq2d 6910 |
. . . 4
⊢ (𝑤 = 𝑊 →
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)) =
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑊)𝑔))) |
| 11 | 6, 6, 10 | mpoeq123dv 7508 |
. . 3
⊢ (𝑤 = 𝑊 → (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔))) = (𝑓 ∈ dom (𝑊sitg𝑚), 𝑔 ∈ dom (𝑊sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑊)𝑔)))) |
| 12 | | oveq2 7439 |
. . . . 5
⊢ (𝑚 = 𝑀 → (𝑊sitg𝑚) = (𝑊sitg𝑀)) |
| 13 | 12 | dmeqd 5916 |
. . . 4
⊢ (𝑚 = 𝑀 → dom (𝑊sitg𝑚) = dom (𝑊sitg𝑀)) |
| 14 | | oveq2 7439 |
. . . . 5
⊢ (𝑚 = 𝑀 →
((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚) =
((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)) |
| 15 | | sitmval.d |
. . . . . . . 8
⊢ 𝐷 = (dist‘𝑊) |
| 16 | 15 | eqcomi 2746 |
. . . . . . 7
⊢
(dist‘𝑊) =
𝐷 |
| 17 | | ofeq 7700 |
. . . . . . 7
⊢
((dist‘𝑊) =
𝐷 →
∘f (dist‘𝑊) = ∘f 𝐷) |
| 18 | 16, 17 | mp1i 13 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ∘f
(dist‘𝑊) =
∘f 𝐷) |
| 19 | 18 | oveqd 7448 |
. . . . 5
⊢ (𝑚 = 𝑀 → (𝑓 ∘f (dist‘𝑊)𝑔) = (𝑓 ∘f 𝐷𝑔)) |
| 20 | 14, 19 | fveq12d 6913 |
. . . 4
⊢ (𝑚 = 𝑀 →
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑊)𝑔)) =
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔))) |
| 21 | 13, 13, 20 | mpoeq123dv 7508 |
. . 3
⊢ (𝑚 = 𝑀 → (𝑓 ∈ dom (𝑊sitg𝑚), 𝑔 ∈ dom (𝑊sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑊)𝑔))) = (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔)))) |
| 22 | | df-sitm 34333 |
. . 3
⊢ sitm =
(𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)))) |
| 23 | | ovex 7464 |
. . . . 5
⊢ (𝑊sitg𝑀) ∈ V |
| 24 | 23 | dmex 7931 |
. . . 4
⊢ dom
(𝑊sitg𝑀) ∈ V |
| 25 | 24, 24 | mpoex 8104 |
. . 3
⊢ (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔))) ∈ V |
| 26 | 11, 21, 22, 25 | ovmpo 7593 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝑀 ∈ ∪ ran measures) → (𝑊sitm𝑀) = (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔)))) |
| 27 | 3, 4, 26 | syl2anc 584 |
1
⊢ (𝜑 → (𝑊sitm𝑀) = (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔)))) |