Metamath Proof Explorer

Theorem sitmval

Description: Value of the simple function integral metric for a given space W and measure M . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses sitmval.d ⊢ D = dist ⁡ W
sitmval.1 ⊢ φ → W ∈ V
sitmval.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
Assertion sitmval ⊢ φ → W sitm M = f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM

Proof

Step Hyp Ref Expression
1 sitmval.d ⊢ D = dist ⁡ W
2 sitmval.1 ⊢ φ → W ∈ V
3 sitmval.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
4 elex ⊢ W ∈ V → W ∈ V
5 2 4 syl ⊢ φ → W ∈ V
6 oveq1 ⊢ w = W → w sitg m = W sitg m
7 6 dmeqd ⊢ w = W → ℑ m w = ℑ m W
8 fveq2 ⊢ w = W → dist ⁡ w = dist ⁡ W
9 8 ofeqd ⊢ w = W → ∘ f ⁡ dist ⁡ w = ∘ f ⁡ dist ⁡ W
10 9 oveqd ⊢ w = W → f dist ⁡ w f g = f dist ⁡ W f g
11 10 fveq2d ⊢ w = W → ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm = ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dm
12 7 7 11 mpoeq123dv ⊢ w = W → f ∈ ℑ m w , g ∈ ℑ m w ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm = f ∈ ℑ m W , g ∈ ℑ m W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dm
13 oveq2 ⊢ m = M → W sitg m = W sitg M
14 13 dmeqd ⊢ m = M → ℑ m W = ℑ M W
15 oveq2 ⊢ m = M → ℝ 𝑠 * ↾ 𝑠 0 +∞ sitg m = ℝ 𝑠 * ↾ 𝑠 0 +∞ sitg M
16 1 eqcomi ⊢ dist ⁡ W = D
17 ofeq ⊢ dist ⁡ W = D → ∘ f ⁡ dist ⁡ W = ∘ f ⁡ D
18 16 17 mp1i ⊢ m = M → ∘ f ⁡ dist ⁡ W = ∘ f ⁡ D
19 18 oveqd ⊢ m = M → f dist ⁡ W f g = f D f g
20 15 19 fveq12d ⊢ m = M → ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dm = ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM
21 14 14 20 mpoeq123dv ⊢ m = M → f ∈ ℑ m W , g ∈ ℑ m W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dm = f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM
22 df-sitm ⊢ sitm = w ∈ V , m ∈ ⋃ ran ⁡ measures ⟼ f ∈ ℑ m w , g ∈ ℑ m w ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm
23 ovex ⊢ W sitg M ∈ V
24 23 dmex ⊢ ℑ M W ∈ V
25 24 24 mpoex ⊢ f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM ∈ V
26 12 21 22 25 ovmpo ⊢ W ∈ V ∧ M ∈ ⋃ ran ⁡ measures → W sitm M = f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM
27 5 3 26 syl2anc ⊢ φ → W sitm M = f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM