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

Metamath Proof Explorer

Theorem volioofmpt

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

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

Proof

Step Hyp Ref Expression
1 volioofmpt.x ⊢ Ⅎ 𝑥 𝐹
2 volioofmpt.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) )
3 nfcv ⊢ Ⅎ 𝑥 𝐴
4 nfcv ⊢ Ⅎ 𝑥 ( vol ∘ (,) )
5 4 1 nfco ⊢ Ⅎ 𝑥 ( ( vol ∘ (,) ) ∘ 𝐹 )
6 volioof ⊢ ( vol ∘ (,) ) : ( ℝ* × ℝ* ) ⟶ ( 0 [,] +∞ )
7 6 a1i ⊢ ( 𝜑 → ( vol ∘ (,) ) : ( ℝ* × ℝ* ) ⟶ ( 0 [,] +∞ ) )
8 fco ⊢ ( ( ( vol ∘ (,) ) : ( ℝ* × ℝ* ) ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) ) → ( ( vol ∘ (,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
9 7 2 8 syl2anc ⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
10 3 5 9 feqmptdf ⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑥 ) ) )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
13 11 12 fvvolioof ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑥 ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
14 13 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
15 10 14 eqtrd ⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )