Metamath Proof Explorer

Theorem volicoff

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

Ref Expression
Hypothesis volicoff.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ × ℝ* ) )
Assertion volicoff ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 volicoff.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ × ℝ* ) )
2 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
3 2 a1i ⊢ ( 𝜑 → vol : dom vol ⟶ ( 0 [,] +∞ ) )
4 icof ⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
5 4 a1i ⊢ ( 𝜑 → [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* )
6 ressxr ⊢ ℝ ⊆ ℝ*
7 xpss1 ⊢ ( ℝ ⊆ ℝ* → ( ℝ × ℝ* ) ⊆ ( ℝ* × ℝ* ) )
8 6 7 ax-mp ⊢ ( ℝ × ℝ* ) ⊆ ( ℝ* × ℝ* )
9 8 a1i ⊢ ( 𝜑 → ( ℝ × ℝ* ) ⊆ ( ℝ* × ℝ* ) )
10 5 9 1 fcoss ⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) : 𝐴 ⟶ 𝒫 ℝ* )
11 10 ffnd ⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) Fn 𝐴 )
12 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ ( ℝ × ℝ* ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
14 12 13 fvovco ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
15 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ* ) )
16 xp1st ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ* ) → ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
17 15 16 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
18 xp2nd ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ* ) → ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ* )
19 15 18 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ* )
20 icombl ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ* ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ dom vol )
21 17 19 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ dom vol )
22 14 21 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
23 22 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
24 fnfvrnss ⊢ ( ( ( [,) ∘ 𝐹 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ) → ran ( [,) ∘ 𝐹 ) ⊆ dom vol )
25 11 23 24 syl2anc ⊢ ( 𝜑 → ran ( [,) ∘ 𝐹 ) ⊆ dom vol )
26 ffrn ⊢ ( ( [,) ∘ 𝐹 ) : 𝐴 ⟶ 𝒫 ℝ* → ( [,) ∘ 𝐹 ) : 𝐴 ⟶ ran ( [,) ∘ 𝐹 ) )
27 10 26 syl ⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) : 𝐴 ⟶ ran ( [,) ∘ 𝐹 ) )
28 3 25 27 fcoss ⊢ ( 𝜑 → ( vol ∘ ( [,) ∘ 𝐹 ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
29 coass ⊢ ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( vol ∘ ( [,) ∘ 𝐹 ) )
30 29 feq1i ⊢ ( ( ( vol ∘ [,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) ↔ ( vol ∘ ( [,) ∘ 𝐹 ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
31 30 a1i ⊢ ( 𝜑 → ( ( ( vol ∘ [,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) ↔ ( vol ∘ ( [,) ∘ 𝐹 ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) ) )
32 28 31 mpbird ⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )