| 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 34335 | . 2
⊢ (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg
(𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))) | 
| 10 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) | 
| 11 | 10 | rneqd 5948 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → ran 𝑓 = ran 𝐹) | 
| 12 | 11 | difeq1d 4124 | . . . 4
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → (ran 𝑓 ∖ { 0 }) = (ran 𝐹 ∖ { 0 })) | 
| 13 | 10 | cnveqd 5885 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → ◡𝑓 = ◡𝐹) | 
| 14 | 13 | imaeq1d 6076 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → (◡𝑓 “ {𝑥}) = (◡𝐹 “ {𝑥})) | 
| 15 | 14 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → (𝑀‘(◡𝑓 “ {𝑥})) = (𝑀‘(◡𝐹 “ {𝑥}))) | 
| 16 | 15 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → (𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥})))) | 
| 17 | 16 | oveq1d 7447 | . . . 4
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥) = ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) | 
| 18 | 12, 17 | mpteq12dv 5232 | . . 3
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) | 
| 19 | 18 | oveq2d 7448 | . 2
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)))) | 
| 20 |  | sibfmbl.1 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) | 
| 21 | 1, 2, 3, 4, 5, 6, 7, 8, 20 | sibfmbl 34338 | . . . 4
⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆)) | 
| 22 | 1, 2, 3, 4, 5, 6, 7, 8, 20 | sibfrn 34340 | . . . 4
⊢ (𝜑 → ran 𝐹 ∈ Fin) | 
| 23 | 1, 2, 3, 4, 5, 6, 7, 8, 20 | sibfima 34341 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)) | 
| 24 | 23 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)) | 
| 25 | 21, 22, 24 | jca32 515 | . . 3
⊢ (𝜑 → (𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ (ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)))) | 
| 26 |  | rneq 5946 | . . . . . 6
⊢ (𝑔 = 𝐹 → ran 𝑔 = ran 𝐹) | 
| 27 | 26 | eleq1d 2825 | . . . . 5
⊢ (𝑔 = 𝐹 → (ran 𝑔 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | 
| 28 | 26 | difeq1d 4124 | . . . . . 6
⊢ (𝑔 = 𝐹 → (ran 𝑔 ∖ { 0 }) = (ran 𝐹 ∖ { 0 })) | 
| 29 |  | cnveq 5883 | . . . . . . . . 9
⊢ (𝑔 = 𝐹 → ◡𝑔 = ◡𝐹) | 
| 30 | 29 | imaeq1d 6076 | . . . . . . . 8
⊢ (𝑔 = 𝐹 → (◡𝑔 “ {𝑥}) = (◡𝐹 “ {𝑥})) | 
| 31 | 30 | fveq2d 6909 | . . . . . . 7
⊢ (𝑔 = 𝐹 → (𝑀‘(◡𝑔 “ {𝑥})) = (𝑀‘(◡𝐹 “ {𝑥}))) | 
| 32 | 31 | eleq1d 2825 | . . . . . 6
⊢ (𝑔 = 𝐹 → ((𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ (𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞))) | 
| 33 | 28, 32 | raleqbidv 3345 | . . . . 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 3691 | . . 3
⊢ (𝐹 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↔ (𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ (ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)))) | 
| 36 | 25, 35 | sylibr 234 | . 2
⊢ (𝜑 → 𝐹 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))}) | 
| 37 |  | ovexd 7467 | . 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ V) | 
| 38 | 9, 19, 36, 37 | fvmptd 7022 | 1
⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)))) |