Theorem 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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ovolsca.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
	ovolsca.3	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } )
Assertion	sca2rab	⊢ ( 𝜑 → 𝐴 = { 𝑦 ∈ ℝ ∣ ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		ovolsca.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolsca.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
3		ovolsca.3	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } )
4	1	sseld	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) )
5	4	pm4.71rd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ) )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } )
7	6	eleq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 ↔ ( ( 1 / 𝐶 ) · 𝑦 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } ) )
8	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐶 ∈ ℝ+ )
9	8	rprecred	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 1 / 𝐶 ) ∈ ℝ )
10		remulcl	⊢ ( ( ( 1 / 𝐶 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 1 / 𝐶 ) · 𝑦 ) ∈ ℝ )
11	9 10	sylancom	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 1 / 𝐶 ) · 𝑦 ) ∈ ℝ )
12		oveq2	⊢ ( 𝑥 = ( ( 1 / 𝐶 ) · 𝑦 ) → ( 𝐶 · 𝑥 ) = ( 𝐶 · ( ( 1 / 𝐶 ) · 𝑦 ) ) )
13	12	eleq1d	⊢ ( 𝑥 = ( ( 1 / 𝐶 ) · 𝑦 ) → ( ( 𝐶 · 𝑥 ) ∈ 𝐴 ↔ ( 𝐶 · ( ( 1 / 𝐶 ) · 𝑦 ) ) ∈ 𝐴 ) )
14	13	elrab3	⊢ ( ( ( 1 / 𝐶 ) · 𝑦 ) ∈ ℝ → ( ( ( 1 / 𝐶 ) · 𝑦 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } ↔ ( 𝐶 · ( ( 1 / 𝐶 ) · 𝑦 ) ) ∈ 𝐴 ) )
15	11 14	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( 1 / 𝐶 ) · 𝑦 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } ↔ ( 𝐶 · ( ( 1 / 𝐶 ) · 𝑦 ) ) ∈ 𝐴 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
17	16	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
18	8	rpcnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐶 ∈ ℂ )
19	8	rpne0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐶 ≠ 0 )
20	17 18 19	divrec2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 / 𝐶 ) = ( ( 1 / 𝐶 ) · 𝑦 ) )
21	20	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐶 · ( 𝑦 / 𝐶 ) ) = ( 𝐶 · ( ( 1 / 𝐶 ) · 𝑦 ) ) )
22	17 18 19	divcan2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐶 · ( 𝑦 / 𝐶 ) ) = 𝑦 )
23	21 22	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐶 · ( ( 1 / 𝐶 ) · 𝑦 ) ) = 𝑦 )
24	23	eleq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝐶 · ( ( 1 / 𝐶 ) · 𝑦 ) ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
25	7 15 24	3bitrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 ↔ 𝑦 ∈ 𝐴 ) )
26	25	pm5.32da	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ∧ ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ) )
27	5 26	bitr4d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ ℝ ∧ ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 ) ) )
28	27	eqabdv	⊢ ( 𝜑 → 𝐴 = { 𝑦 ∣ ( 𝑦 ∈ ℝ ∧ ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 ) } )
29		df-rab	⊢ { 𝑦 ∈ ℝ ∣ ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 } = { 𝑦 ∣ ( 𝑦 ∈ ℝ ∧ ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 ) }
30	28 29	eqtr4di	⊢ ( 𝜑 → 𝐴 = { 𝑦 ∈ ℝ ∣ ( ( 1 / 𝐶 ) · 𝑦 ) ∈ 𝐵 } )