This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 / 𝐶 ) · 𝑦 ) ∈ 𝐵 } )