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 ofeq ⊢ dist ⁡ w = dist ⁡ W → ∘ f ⁡ dist ⁡ w = ∘ f ⁡ dist ⁡ W
10 8 9 syl ⊢ w = W → ∘ f ⁡ dist ⁡ w = ∘ f ⁡ dist ⁡ W
11 10 oveqd ⊢ w = W → f dist ⁡ w f g = f dist ⁡ W f g
12 11 fveq2d ⊢ w = W → ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm = ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dm
13 7 7 12 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
14 oveq2 ⊢ m = M → W sitg m = W sitg M
15 14 dmeqd ⊢ m = M → ℑ m W = ℑ M W
16 oveq2 ⊢ m = M → ℝ 𝑠 * ↾ 𝑠 0 +∞ sitg m = ℝ 𝑠 * ↾ 𝑠 0 +∞ sitg M
17 1 eqcomi ⊢ dist ⁡ W = D
18 ofeq ⊢ dist ⁡ W = D → ∘ f ⁡ dist ⁡ W = ∘ f ⁡ D
19 17 18 mp1i ⊢ m = M → ∘ f ⁡ dist ⁡ W = ∘ f ⁡ D
20 19 oveqd ⊢ m = M → f dist ⁡ W f g = f D f g
21 16 20 fveq12d ⊢ m = M → ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dm = ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM
22 15 15 21 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
23 df-sitm ⊢ sitm = w ∈ V , m ∈ ⋃ ran ⁡ measures ⟼ f ∈ ℑ m w , g ∈ ℑ m w ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm
24 ovex ⊢ W sitg M ∈ V
25 24 dmex ⊢ ℑ M W ∈ V
26 25 25 mpoex ⊢ f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM ∈ V
27 13 22 23 26 ovmpo ⊢ W ∈ V ∧ M ∈ ⋃ ran ⁡ measures → W sitm M = f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM
28 5 3 27 syl2anc ⊢ φ → W sitm M = f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f D f g dM