Theorem sitmf

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

	Ref	Expression
Hypotheses	sitmf.0	⊢ ( 𝜑 → 𝑊 ∈ Mnd )
	sitmf.1	⊢ ( 𝜑 → 𝑊 ∈ ∞MetSp )
	sitmf.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
Assertion	sitmf	⊢ ( 𝜑 → ( 𝑊 sitm 𝑀 ) : ( dom ( 𝑊 sitg 𝑀 ) × dom ( 𝑊 sitg 𝑀 ) ) ⟶ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		sitmf.0	⊢ ( 𝜑 → 𝑊 ∈ Mnd )
2		sitmf.1	⊢ ( 𝜑 → 𝑊 ∈ ∞MetSp )
3		sitmf.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
4		eqid	⊢ ( dist ‘ 𝑊 ) = ( dist ‘ 𝑊 )
5	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∧ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ) ) → 𝑊 ∈ ∞MetSp )
6	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∧ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ) ) → 𝑀 ∈ ∪ ran measures )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∧ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ) ) → 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∧ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ) ) → 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) )
9	4 5 6 7 8	sitmfval	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∧ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ) ) → ( 𝑓 ( 𝑊 sitm 𝑀 ) 𝑔 ) = ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) )
10	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∧ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ) ) → 𝑊 ∈ Mnd )
11	10 5 6 7 8	sitmcl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∧ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ) ) → ( 𝑓 ( 𝑊 sitm 𝑀 ) 𝑔 ) ∈ ( 0 [,] +∞ ) )
12	9 11	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∧ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ) ) → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ∈ ( 0 [,] +∞ ) )
13	12	ralrimivva	⊢ ( 𝜑 → ∀ 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∀ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ∈ ( 0 [,] +∞ ) )
14		eqid	⊢ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) )
15	14	fmpo	⊢ ( ∀ 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) ∀ 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ∈ ( 0 [,] +∞ ) ↔ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) : ( dom ( 𝑊 sitg 𝑀 ) × dom ( 𝑊 sitg 𝑀 ) ) ⟶ ( 0 [,] +∞ ) )
16	13 15	sylib	⊢ ( 𝜑 → ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) : ( dom ( 𝑊 sitg 𝑀 ) × dom ( 𝑊 sitg 𝑀 ) ) ⟶ ( 0 [,] +∞ ) )
17	4 2 3	sitmval	⊢ ( 𝜑 → ( 𝑊 sitm 𝑀 ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) )
18	17	feq1d	⊢ ( 𝜑 → ( ( 𝑊 sitm 𝑀 ) : ( dom ( 𝑊 sitg 𝑀 ) × dom ( 𝑊 sitg 𝑀 ) ) ⟶ ( 0 [,] +∞ ) ↔ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) : ( dom ( 𝑊 sitg 𝑀 ) × dom ( 𝑊 sitg 𝑀 ) ) ⟶ ( 0 [,] +∞ ) ) )
19	16 18	mpbird	⊢ ( 𝜑 → ( 𝑊 sitm 𝑀 ) : ( dom ( 𝑊 sitg 𝑀 ) × dom ( 𝑊 sitg 𝑀 ) ) ⟶ ( 0 [,] +∞ ) )