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 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )