Theorem sitmfval

Description: Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	sitmval.d	⊢ 𝐷 = ( dist ‘ 𝑊 )
	sitmval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	sitmval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	sitmfval.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
	sitmfval.2	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
Assertion	sitmfval	⊢ ( 𝜑 → ( 𝐹 ( 𝑊 sitm 𝑀 ) 𝐺 ) = ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝐹 ∘f 𝐷 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sitmval.d	⊢ 𝐷 = ( dist ‘ 𝑊 )
2		sitmval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
3		sitmval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
4		sitmfval.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
5		sitmfval.2	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
6	1 2 3	sitmval	⊢ ( 𝜑 → ( 𝑊 sitm 𝑀 ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → 𝑓 = 𝐹 )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → 𝑔 = 𝐺 )
9	7 8	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( 𝑓 ∘f 𝐷 𝑔 ) = ( 𝐹 ∘f 𝐷 𝐺 ) )
10	9	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) = ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝐹 ∘f 𝐷 𝐺 ) ) )
11		fvexd	⊢ ( 𝜑 → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝐹 ∘f 𝐷 𝐺 ) ) ∈ V )
12	6 10 4 5 11	ovmpod	⊢ ( 𝜑 → ( 𝐹 ( 𝑊 sitm 𝑀 ) 𝐺 ) = ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝐹 ∘f 𝐷 𝐺 ) ) )