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 ⊢ Ⅎ _ x F
volioofmpt.f ⊢ φ → F : A ⟶ ℝ * × ℝ *
Assertion volioofmpt ⊢ φ → vol ∘ . ∘ F = x ∈ A ⟼ vol ⁡ 1 st ⁡ F ⁡ x 2 nd ⁡ F ⁡ x

Proof

Step Hyp Ref Expression
1 volioofmpt.x ⊢ Ⅎ _ x F
2 volioofmpt.f ⊢ φ → F : A ⟶ ℝ * × ℝ *
3 nfcv ⊢ Ⅎ _ x A
4 nfcv ⊢ Ⅎ _ x vol ∘ .
5 4 1 nfco ⊢ Ⅎ _ x vol ∘ . ∘ F
6 volioof ⊢ vol ∘ . : ℝ * × ℝ * ⟶ 0 +∞
7 6 a1i ⊢ φ → vol ∘ . : ℝ * × ℝ * ⟶ 0 +∞
8 fco ⊢ vol ∘ . : ℝ * × ℝ * ⟶ 0 +∞ ∧ F : A ⟶ ℝ * × ℝ * → vol ∘ . ∘ F : A ⟶ 0 +∞
9 7 2 8 syl2anc ⊢ φ → vol ∘ . ∘ F : A ⟶ 0 +∞
10 3 5 9 feqmptdf ⊢ φ → vol ∘ . ∘ F = x ∈ A ⟼ vol ∘ . ∘ F ⁡ x
11 2 adantr ⊢ φ ∧ x ∈ A → F : A ⟶ ℝ * × ℝ *
12 simpr ⊢ φ ∧ x ∈ A → x ∈ A
13 11 12 fvvolioof ⊢ φ ∧ x ∈ A → vol ∘ . ∘ F ⁡ x = vol ⁡ 1 st ⁡ F ⁡ x 2 nd ⁡ F ⁡ x
14 13 mpteq2dva ⊢ φ → x ∈ A ⟼ vol ∘ . ∘ F ⁡ x = x ∈ A ⟼ vol ⁡ 1 st ⁡ F ⁡ x 2 nd ⁡ F ⁡ x
15 10 14 eqtrd ⊢ φ → vol ∘ . ∘ F = x ∈ A ⟼ vol ⁡ 1 st ⁡ F ⁡ x 2 nd ⁡ F ⁡ x