This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem volicofmpt

Description: ( ( vol o. [,) ) o. F ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses volicofmpt.1 ⊢ Ⅎ 𝑥 𝐹
volicofmpt.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ × ℝ* ) )
Assertion volicofmpt ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 volicofmpt.1 ⊢ Ⅎ 𝑥 𝐹
2 volicofmpt.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ × ℝ* ) )
3 nfcv ⊢ Ⅎ 𝑥 𝐴
4 nfcv ⊢ Ⅎ 𝑥 ( vol ∘ [,) )
5 4 1 nfco ⊢ Ⅎ 𝑥 ( ( vol ∘ [,) ) ∘ 𝐹 )
6 2 volicoff ⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
7 3 5 6 feqmptdf ⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( vol ∘ [,) ) ∘ 𝐹 ) ‘ 𝑥 ) ) )
8 ressxr ⊢ ℝ ⊆ ℝ*
9 xpss1 ⊢ ( ℝ ⊆ ℝ* → ( ℝ × ℝ* ) ⊆ ( ℝ* × ℝ* ) )
10 8 9 ax-mp ⊢ ( ℝ × ℝ* ) ⊆ ( ℝ* × ℝ* )
11 10 a1i ⊢ ( 𝜑 → ( ℝ × ℝ* ) ⊆ ( ℝ* × ℝ* ) )
12 2 11 fssd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
15 13 14 fvvolicof ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( vol ∘ [,) ) ∘ 𝐹 ) ‘ 𝑥 ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
16 15 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( vol ∘ [,) ) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
17 7 16 eqtrd ⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )