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 ⊢ 𝐷 = ( 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 ofeq ⊢ ( ( dist ‘ 𝑤 ) = ( dist ‘ 𝑊 ) → ∘f ( dist ‘ 𝑤 ) = ∘f ( dist ‘ 𝑊 ) )
10 8 9 syl ⊢ ( 𝑤 = 𝑊 → ∘f ( dist ‘ 𝑤 ) = ∘f ( dist ‘ 𝑊 ) )
11 10 oveqd ⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) = ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) )
12 11 fveq2d ⊢ ( 𝑤 = 𝑊 → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) = ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) )
13 7 7 12 mpoeq123dv ⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∈ dom ( 𝑤 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑤 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) )
14 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 𝑊 sitg 𝑚 ) = ( 𝑊 sitg 𝑀 ) )
15 14 dmeqd ⊢ ( 𝑚 = 𝑀 → dom ( 𝑊 sitg 𝑚 ) = dom ( 𝑊 sitg 𝑀 ) )
16 oveq2 ⊢ ( 𝑚 = 𝑀 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) )
17 1 eqcomi ⊢ ( dist ‘ 𝑊 ) = 𝐷
18 ofeq ⊢ ( ( dist ‘ 𝑊 ) = 𝐷 → ∘f ( dist ‘ 𝑊 ) = ∘f 𝐷 )
19 17 18 mp1i ⊢ ( 𝑚 = 𝑀 → ∘f ( dist ‘ 𝑊 ) = ∘f 𝐷 )
20 19 oveqd ⊢ ( 𝑚 = 𝑀 → ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) = ( 𝑓 ∘f 𝐷 𝑔 ) )
21 16 20 fveq12d ⊢ ( 𝑚 = 𝑀 → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) = ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) )
22 15 15 21 mpoeq123dv ⊢ ( 𝑚 = 𝑀 → ( 𝑓 ∈ dom ( 𝑊 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑊 ) 𝑔 ) ) ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) )
23 df-sitm ⊢ sitm = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ dom ( 𝑤 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑤 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) ) )
24 ovex ⊢ ( 𝑊 sitg 𝑀 ) ∈ V
25 24 dmex ⊢ dom ( 𝑊 sitg 𝑀 ) ∈ V
26 25 25 mpoex ⊢ ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) ∈ V
27 13 22 23 26 ovmpo ⊢ ( ( 𝑊 ∈ V ∧ 𝑀 ∈ ∪ ran measures ) → ( 𝑊 sitm 𝑀 ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) )
28 5 3 27 syl2anc ⊢ ( 𝜑 → ( 𝑊 sitm 𝑀 ) = ( 𝑓 ∈ dom ( 𝑊 sitg 𝑀 ) , 𝑔 ∈ dom ( 𝑊 sitg 𝑀 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝑓 ∘f 𝐷 𝑔 ) ) ) )