sca2rab

Description: If B is a scale of A by C , then A is a scale of B by 1 / C . (Contributed by Mario Carneiro, 22-Mar-2014)

	Ref	Expression
Hypotheses	ovolsca.1	$⊢ φ \to A \subseteq ℝ$
	ovolsca.2	$⊢ φ \to C \in ℝ^{+}$
	ovolsca.3	$⊢ φ \to B = \{x \in ℝ \| C x \in A\}$
Assertion	sca2rab	$⊢ φ \to A = \{y \in ℝ \| (\frac{1}{C}) y \in B\}$

Proof

Step	Hyp	Ref	Expression
1		ovolsca.1	$⊢ φ \to A \subseteq ℝ$
2		ovolsca.2	$⊢ φ \to C \in ℝ^{+}$
3		ovolsca.3	$⊢ φ \to B = \{x \in ℝ \| C x \in A\}$
4	1	sseld	$⊢ φ \to (y \in A \to y \in ℝ)$
5	4	pm4.71rd	$⊢ φ \to (y \in A \leftrightarrow (y \in ℝ \land y \in A))$
6	3	adantr	$⊢ (φ \land y \in ℝ) \to B = \{x \in ℝ \| C x \in A\}$
7	6	eleq2d	$⊢ (φ \land y \in ℝ) \to ((\frac{1}{C}) y \in B \leftrightarrow (\frac{1}{C}) y \in \{x \in ℝ \| C x \in A\})$
8	2	adantr	$⊢ (φ \land y \in ℝ) \to C \in ℝ^{+}$
9	8	rprecred	$⊢ (φ \land y \in ℝ) \to \frac{1}{C} \in ℝ$
10		remulcl	$⊢ (\frac{1}{C} \in ℝ \land y \in ℝ) \to (\frac{1}{C}) y \in ℝ$
11	9 10	sylancom	$⊢ (φ \land y \in ℝ) \to (\frac{1}{C}) y \in ℝ$
12		oveq2	$⊢ x = (\frac{1}{C}) y \to C x = C (\frac{1}{C}) y$
13	12	eleq1d	$⊢ x = (\frac{1}{C}) y \to (C x \in A \leftrightarrow C (\frac{1}{C}) y \in A)$
14	13	elrab3	$⊢ (\frac{1}{C}) y \in ℝ \to ((\frac{1}{C}) y \in \{x \in ℝ \| C x \in A\} \leftrightarrow C (\frac{1}{C}) y \in A)$
15	11 14	syl	$⊢ (φ \land y \in ℝ) \to ((\frac{1}{C}) y \in \{x \in ℝ \| C x \in A\} \leftrightarrow C (\frac{1}{C}) y \in A)$
16		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
17	16	recnd	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
18	8	rpcnd	$⊢ (φ \land y \in ℝ) \to C \in ℂ$
19	8	rpne0d	$⊢ (φ \land y \in ℝ) \to C \neq 0$
20	17 18 19	divrec2d	$⊢ (φ \land y \in ℝ) \to \frac{y}{C} = (\frac{1}{C}) y$
21	20	oveq2d	$⊢ (φ \land y \in ℝ) \to C (\frac{y}{C}) = C (\frac{1}{C}) y$
22	17 18 19	divcan2d	$⊢ (φ \land y \in ℝ) \to C (\frac{y}{C}) = y$
23	21 22	eqtr3d	$⊢ (φ \land y \in ℝ) \to C (\frac{1}{C}) y = y$
24	23	eleq1d	$⊢ (φ \land y \in ℝ) \to (C (\frac{1}{C}) y \in A \leftrightarrow y \in A)$
25	7 15 24	3bitrd	$⊢ (φ \land y \in ℝ) \to ((\frac{1}{C}) y \in B \leftrightarrow y \in A)$
26	25	pm5.32da	$⊢ φ \to ((y \in ℝ \land (\frac{1}{C}) y \in B) \leftrightarrow (y \in ℝ \land y \in A))$
27	5 26	bitr4d	$⊢ φ \to (y \in A \leftrightarrow (y \in ℝ \land (\frac{1}{C}) y \in B))$
28	27	eqabdv	$⊢ φ \to A = \{y \| (y \in ℝ \land (\frac{1}{C}) y \in B)\}$
29		df-rab	$⊢ \{y \in ℝ \| (\frac{1}{C}) y \in B\} = \{y \| (y \in ℝ \land (\frac{1}{C}) y \in B)\}$
30	28 29	eqtr4di	$⊢ φ \to A = \{y \in ℝ \| (\frac{1}{C}) y \in B\}$

Metamath Proof Explorer

Theorem sca2rab

Proof