ovolfs2

Description: Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015)

		Ref	Expression
	Hypothesis	ovolfs2.1	$⊢ G = (abs \circ -) \circ F$
	Assertion	ovolfs2	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to G = ({vol}^{*} \circ (.)) \circ F$

Proof

Step	Hyp	Ref	Expression
1		ovolfs2.1	$⊢ G = (abs \circ -) \circ F$
2		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
3		ovolioo	$⊢ (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n))) \to {vol}^{*} ((1^{st} (F (n)), 2^{nd} (F (n)))) = 2^{nd} (F (n)) - 1^{st} (F (n))$
4	2 3	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to {vol}^{*} ((1^{st} (F (n)), 2^{nd} (F (n)))) = 2^{nd} (F (n)) - 1^{st} (F (n))$
5		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
6		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
7	5 6	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
8		ffvelcdm	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) \in (\leq \cap ℝ^{2})$
9	7 8	sselid	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) \in (ℝ^{} \times ℝ^{})$
10		1st2nd2	$⊢ F (n) \in (ℝ^{} \times ℝ^{}) \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
11	9 10	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
12	11	fveq2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (.) (F (n)) = (.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
13		df-ov	$⊢ (1^{st} (F (n)), 2^{nd} (F (n))) = (.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
14	12 13	eqtr4di	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (.) (F (n)) = (1^{st} (F (n)), 2^{nd} (F (n)))$
15	14	fveq2d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to {vol}^{} ((.) (F (n))) = {vol}^{} ((1^{st} (F (n)), 2^{nd} (F (n))))$
16	1	ovolfsval	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to G (n) = 2^{nd} (F (n)) - 1^{st} (F (n))$
17	4 15 16	3eqtr4rd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to G (n) = {vol}^{*} ((.) (F (n)))$
18	17	mpteq2dva	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to (n \in ℕ ⟼ G (n)) = (n \in ℕ ⟼ {vol}^{*} ((.) (F (n))))$
19	1	ovolfsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to G : ℕ ⟶ [0, +∞)$
20	19	feqmptd	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to G = (n \in ℕ ⟼ G (n))$
21		id	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to F : ℕ ⟶ \leq \cap ℝ^{2}$
22	21	feqmptd	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to F = (n \in ℕ ⟼ F (n))$
23		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
24	23	a1i	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
25	24	ffvelcdmda	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in (ℝ^{} \times ℝ^{})) \to (.) (x) \in 𝒫 ℝ$
26	24	feqmptd	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to (.) = (x \in (ℝ^{} \times ℝ^{}) ⟼ (.) (x))$
27		ovolf	$⊢ {vol}^{*} : 𝒫 ℝ ⟶ [0, +∞]$
28	27	a1i	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to {vol}^{*} : 𝒫 ℝ ⟶ [0, +∞]$
29	28	feqmptd	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to {vol}^{} = (y \in 𝒫 ℝ ⟼ {vol}^{} (y))$
30		fveq2	$⊢ y = (.) (x) \to {vol}^{} (y) = {vol}^{} ((.) (x))$
31	25 26 29 30	fmptco	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to {vol}^{} \circ (.) = (x \in (ℝ^{} \times ℝ^{}) ⟼ {vol}^{} ((.) (x)))$
32		2fveq3	$⊢ x = F (n) \to {vol}^{} ((.) (x)) = {vol}^{} ((.) (F (n)))$
33	9 22 31 32	fmptco	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ({vol}^{} \circ (.)) \circ F = (n \in ℕ ⟼ {vol}^{} ((.) (F (n))))$
34	18 20 33	3eqtr4d	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to G = ({vol}^{*} \circ (.)) \circ F$

Metamath Proof Explorer

Theorem ovolfs2

Proof