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