volicoff

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

		Ref	Expression
	Hypothesis	volicoff.1	$⊢ φ \to F : A ⟶ ℝ \times ℝ^{*}$
	Assertion	volicoff	$⊢ φ \to ((vol \circ [.)) \circ F) : A ⟶ [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		volicoff.1	$⊢ φ \to F : A ⟶ ℝ \times ℝ^{*}$
2		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
3	2	a1i	$⊢ φ \to vol : dom vol ⟶ [0, +∞]$
4		icof	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
5	4	a1i	$⊢ φ \to [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
6		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
7		xpss1	$⊢ ℝ \subseteq ℝ^{} \to ℝ \times ℝ^{} \subseteq ℝ^{} \times ℝ^{}$
8	6 7	ax-mp	$⊢ ℝ \times ℝ^{} \subseteq ℝ^{} \times ℝ^{*}$
9	8	a1i	$⊢ φ \to ℝ \times ℝ^{} \subseteq ℝ^{} \times ℝ^{*}$
10	5 9 1	fcoss	$⊢ φ \to ([.) \circ F) : A ⟶ 𝒫 ℝ^{*}$
11	10	ffnd	$⊢ φ \to ([.) \circ F) Fn A$
12	1	adantr	$⊢ (φ \land x \in A) \to F : A ⟶ ℝ \times ℝ^{*}$
13		simpr	$⊢ (φ \land x \in A) \to x \in A$
14	12 13	fvovco	$⊢ (φ \land x \in A) \to ([.) \circ F) (x) = [1^{st} (F (x)), 2^{nd} (F (x)))$
15	1	ffvelcdmda	$⊢ (φ \land x \in A) \to F (x) \in (ℝ \times ℝ^{*})$
16		xp1st	$⊢ F (x) \in (ℝ \times ℝ^{*}) \to 1^{st} (F (x)) \in ℝ$
17	15 16	syl	$⊢ (φ \land x \in A) \to 1^{st} (F (x)) \in ℝ$
18		xp2nd	$⊢ F (x) \in (ℝ \times ℝ^{}) \to 2^{nd} (F (x)) \in ℝ^{}$
19	15 18	syl	$⊢ (φ \land x \in A) \to 2^{nd} (F (x)) \in ℝ^{*}$
20		icombl	$⊢ (1^{st} (F (x)) \in ℝ \land 2^{nd} (F (x)) \in ℝ^{*}) \to [1^{st} (F (x)), 2^{nd} (F (x))) \in dom vol$
21	17 19 20	syl2anc	$⊢ (φ \land x \in A) \to [1^{st} (F (x)), 2^{nd} (F (x))) \in dom vol$
22	14 21	eqeltrd	$⊢ (φ \land x \in A) \to ([.) \circ F) (x) \in dom vol$
23	22	ralrimiva	$⊢ φ \to \forall x \in A ([.) \circ F) (x) \in dom vol$
24		fnfvrnss	$⊢ (([.) \circ F) Fn A \land \forall x \in A ([.) \circ F) (x) \in dom vol) \to ran ([.) \circ F) \subseteq dom vol$
25	11 23 24	syl2anc	$⊢ φ \to ran ([.) \circ F) \subseteq dom vol$
26		ffrn	$⊢ ([.) \circ F) : A ⟶ 𝒫 ℝ^{*} \to ([.) \circ F) : A ⟶ ran ([.) \circ F)$
27	10 26	syl	$⊢ φ \to ([.) \circ F) : A ⟶ ran ([.) \circ F)$
28	3 25 27	fcoss	$⊢ φ \to (vol \circ ([.) \circ F)) : A ⟶ [0, +∞]$
29		coass	$⊢ (vol \circ [.)) \circ F = vol \circ ([.) \circ F)$
30	29	feq1i	$⊢ ((vol \circ [.)) \circ F) : A ⟶ [0, +∞] \leftrightarrow (vol \circ ([.) \circ F)) : A ⟶ [0, +∞]$
31	30	a1i	$⊢ φ \to (((vol \circ [.)) \circ F) : A ⟶ [0, +∞] \leftrightarrow (vol \circ ([.) \circ F)) : A ⟶ [0, +∞])$
32	28 31	mpbird	$⊢ φ \to ((vol \circ [.)) \circ F) : A ⟶ [0, +∞]$

Metamath Proof Explorer

Theorem volicoff

Proof