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	⊢ 𝐷 = ( dist ‘ 𝑊 )
	sitmval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	sitmval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
Assertion	sitmval	⊢ ( 𝜑 → ( 𝑊 sitm 𝑀 ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sitmval.d	⊢ 𝐷 = ( dist ‘ 𝑊 )
2		sitmval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
3		sitmval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
4		elex	⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V )
5	2 4	syl	⊢ ( 𝜑 → 𝑊 ∈ V )
6		oveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 sitg 𝑚 ) = ( 𝑊 sitg 𝑚 ) )
7	6	dmeqd	⊢ ( 𝑤 = 𝑊 → dom ( 𝑤 sitg 𝑚 ) = dom ( 𝑊 sitg 𝑚 ) )
8		fveq2	⊢ ( 𝑤 = 𝑊 → ( dist ‘ 𝑤 ) = ( dist ‘ 𝑊 ) )
9	8	ofeqd	⊢ ( 𝑤 = 𝑊 → ∘f ( dist ‘ 𝑤 ) = ∘f ( dist ‘ 𝑊 ) )
10	9	oveqd	⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) = ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) )
11	10	fveq2d	⊢ ( 𝑤 = 𝑊 → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) = ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) )
12	7 7 11	mpoeq123dv	⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∈ dom ( 𝑤 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑤 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) )
13		oveq2	⊢ ( 𝑚 = 𝑀 → ( 𝑊 sitg 𝑚 ) = ( 𝑊 sitg 𝑀 ) )
14	13	dmeqd	⊢ ( 𝑚 = 𝑀 → dom ( 𝑊 sitg 𝑚 ) = dom ( 𝑊 sitg 𝑀 ) )
15		oveq2	⊢ ( 𝑚 = 𝑀 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) )
16	1	eqcomi	⊢ ( dist ‘ 𝑊 ) = 𝐷
17		ofeq	⊢ ( ( dist ‘ 𝑊 ) = 𝐷 → ∘f ( dist ‘ 𝑊 ) = ∘f 𝐷 )
18	16 17	mp1i	⊢ ( 𝑚 = 𝑀 → ∘f ( dist ‘ 𝑊 ) = ∘f 𝐷 )
19	18	oveqd	⊢ ( 𝑚 = 𝑀 → ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) = ( 𝑓 ∘f 𝐷 𝑔 ) )
20	15 19	fveq12d	⊢ ( 𝑚 = 𝑀 → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) = ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) )
21	14 14 20	mpoeq123dv	⊢ ( 𝑚 = 𝑀 → ( 𝑓 ∈ dom ( 𝑊 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) )
22		df-sitm	⊢ sitm = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ dom ( 𝑤 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑤 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) ) )
23		ovex	⊢ ( 𝑊 sitg 𝑀 ) ∈ V
24	23	dmex	⊢ dom ( 𝑊 sitg 𝑀 ) ∈ V
25	24 24	mpoex	⊢ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) ∈ V
26	12 21 22 25	ovmpo	⊢ ( ( 𝑊 ∈ V ∧ 𝑀 ∈ ∪ ran measures ) → ( 𝑊 sitm 𝑀 ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) )
27	5 3 26	syl2anc	⊢ ( 𝜑 → ( 𝑊 sitm 𝑀 ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) )