Metamath Proof Explorer

Theorem sitmf

Description: The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018)

Ref Expression
Hypotheses sitmf.0 ⊢ φ → W ∈ Mnd
sitmf.1 ⊢ φ → W ∈ ∞MetSp
sitmf.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
Assertion sitmf ⊢ φ → |. - .| M W : ℑ M W × ℑ M W ⟶ 0 +∞

Proof

Step Hyp Ref Expression
1 sitmf.0 ⊢ φ → W ∈ Mnd
2 sitmf.1 ⊢ φ → W ∈ ∞MetSp
3 sitmf.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
4 eqid ⊢ dist ⁡ W = dist ⁡ W
5 2 adantr ⊢ φ ∧ f ∈ ℑ M W ∧ g ∈ ℑ M W → W ∈ ∞MetSp
6 3 adantr ⊢ φ ∧ f ∈ ℑ M W ∧ g ∈ ℑ M W → M ∈ ⋃ ran ⁡ measures
7 simprl ⊢ φ ∧ f ∈ ℑ M W ∧ g ∈ ℑ M W → f ∈ ℑ M W
8 simprr ⊢ φ ∧ f ∈ ℑ M W ∧ g ∈ ℑ M W → g ∈ ℑ M W
9 4 5 6 7 8 sitmfval ⊢ φ ∧ f ∈ ℑ M W ∧ g ∈ ℑ M W → |g - f| M W = ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dM
10 1 adantr ⊢ φ ∧ f ∈ ℑ M W ∧ g ∈ ℑ M W → W ∈ Mnd
11 10 5 6 7 8 sitmcl ⊢ φ ∧ f ∈ ℑ M W ∧ g ∈ ℑ M W → |g - f| M W ∈ 0 +∞
12 9 11 eqeltrrd ⊢ φ ∧ f ∈ ℑ M W ∧ g ∈ ℑ M W → ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dM ∈ 0 +∞
13 12 ralrimivva ⊢ φ → ∀ f ∈ ℑ M W ∀ g ∈ ℑ M W ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dM ∈ 0 +∞
14 eqid ⊢ 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
15 14 fmpo ⊢ ∀ f ∈ ℑ M W ∀ g ∈ ℑ M W ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dM ∈ 0 +∞ ↔ f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dM : ℑ M W × ℑ M W ⟶ 0 +∞
16 13 15 sylib ⊢ φ → f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dM : ℑ M W × ℑ M W ⟶ 0 +∞
17 4 2 3 sitmval ⊢ φ → W sitm M = f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dM
18 17 feq1d ⊢ φ → |. - .| M W : ℑ M W × ℑ M W ⟶ 0 +∞ ↔ f ∈ ℑ M W , g ∈ ℑ M W ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ W f g dM : ℑ M W × ℑ M W ⟶ 0 +∞
19 16 18 mpbird ⊢ φ → |. - .| M W : ℑ M W × ℑ M W ⟶ 0 +∞