Theorem ovolsca

Description: The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015)

	Ref	Expression
Hypotheses	ovolsca.1	$$⊢\phi \to A\subseteq ℝ$$
	ovolsca.2	$$⊢\phi \to C\in {ℝ}^{+}$$
	ovolsca.3	$$⊢\phi \to B=\left\{x\in ℝ|Cx\in A\right\}$$
	ovolsca.4	$$⊢\phi \to {vol}^{*}\left(A\right)\in ℝ$$
Assertion	ovolsca	$$⊢\phi \to {vol}^{*}\left(B\right)=\frac{{vol}^{*}\left(A\right)}{C}$$

Proof

Step	Hyp	Ref	Expression
1		ovolsca.1	$$⊢\phi \to A\subseteq ℝ$$
2		ovolsca.2	$$⊢\phi \to C\in {ℝ}^{+}$$
3		ovolsca.3	$$⊢\phi \to B=\left\{x\in ℝ|Cx\in A\right\}$$
4		ovolsca.4	$$⊢\phi \to {vol}^{*}\left(A\right)\in ℝ$$
5	1 2 3 4	ovolscalem2	$$⊢\phi \to {vol}^{*}\left(B\right)\le \frac{{vol}^{*}\left(A\right)}{C}$$
6	4	recnd	$$⊢\phi \to {vol}^{*}\left(A\right)\in ℂ$$
7	2	rpcnd	$$⊢\phi \to C\in ℂ$$
8	2	rpne0d	$$⊢\phi \to C\ne 0$$
9	6 7 8	divrecd	$$⊢\phi \to \frac{{vol}^{*}\left(A\right)}{C}={vol}^{*}\left(A\right)\left(\frac{1}{C}\right)$$
10		ssrab2	$$⊢\left\{x\in ℝ|Cx\in A\right\}\subseteq ℝ$$
11	3 10	eqsstrdi	$$⊢\phi \to B\subseteq ℝ$$
12	2	rpreccld	$$⊢\phi \to \frac{1}{C}\in {ℝ}^{+}$$
13	1 2 3	sca2rab	$$⊢\phi \to A=\left\{y\in ℝ|\left(\frac{1}{C}\right)y\in B\right\}$$
14	4 2	rerpdivcld	$$⊢\phi \to \frac{{vol}^{*}\left(A\right)}{C}\in ℝ$$
15		ovollecl	$$⊢\left(B\subseteq ℝ\wedge \frac{{vol}^{*}\left(A\right)}{C}\in ℝ\wedge {vol}^{*}\left(B\right)\le \frac{{vol}^{*}\left(A\right)}{C}\right)\to {vol}^{*}\left(B\right)\in ℝ$$
16	11 14 5 15	syl3anc	$$⊢\phi \to {vol}^{*}\left(B\right)\in ℝ$$
17	11 12 13 16	ovolscalem2	$$⊢\phi \to {vol}^{*}\left(A\right)\le \frac{{vol}^{*}\left(B\right)}{\frac{1}{C}}$$
18	4 16 12	lemuldivd	$$⊢\phi \to \left({vol}^{*}\left(A\right)\left(\frac{1}{C}\right)\le {vol}^{*}\left(B\right)\leftrightarrow {vol}^{*}\left(A\right)\le \frac{{vol}^{*}\left(B\right)}{\frac{1}{C}}\right)$$
19	17 18	mpbird	$$⊢\phi \to {vol}^{*}\left(A\right)\left(\frac{1}{C}\right)\le {vol}^{*}\left(B\right)$$
20	9 19	eqbrtrd	$$⊢\phi \to \frac{{vol}^{*}\left(A\right)}{C}\le {vol}^{*}\left(B\right)$$
21	16 14	letri3d	$$⊢\phi \to \left({vol}^{*}\left(B\right)=\frac{{vol}^{*}\left(A\right)}{C}\leftrightarrow \left({vol}^{*}\left(B\right)\le \frac{{vol}^{*}\left(A\right)}{C}\wedge \frac{{vol}^{*}\left(A\right)}{C}\le {vol}^{*}\left(B\right)\right)\right)$$
22	5 20 21	mpbir2and	$$⊢\phi \to {vol}^{*}\left(B\right)=\frac{{vol}^{*}\left(A\right)}{C}$$