Theorem ovolfs2

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

	Ref	Expression
Hypothesis	ovolfs2.1	$$⊢G=\left(\mathrm{abs}\circ -\right)\circ F$$
Assertion	ovolfs2	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to G=\left({vol}^{*}\circ \left(.\right)\right)\circ F$$

Proof

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