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

Metamath Proof Explorer

Theorem shft2rab

Description: If B is a shift of A by C , then A is a shift of B by -u C . (Contributed by Mario Carneiro, 22-Mar-2014) (Revised by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses ovolshft.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
ovolshft.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
ovolshft.3 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
Assertion shft2rab ( 𝜑 → 𝐴 = { 𝑦 ∈ ℝ ∣ ( 𝑦 − - 𝐶 ) ∈ 𝐵 } )

Proof

Step Hyp Ref Expression
1 ovolshft.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 ovolshft.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3 ovolshft.3 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
4 1 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) )
5 4 pm4.71rd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ) )
6 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
7 2 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
8 subneg ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝑦 − - 𝐶 ) = ( 𝑦 + 𝐶 ) )
9 6 7 8 syl2anr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 − - 𝐶 ) = ( 𝑦 + 𝐶 ) )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
11 9 10 eleq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 − - 𝐶 ) ∈ 𝐵 ↔ ( 𝑦 + 𝐶 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } ) )
12 id ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ )
13 readdcl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑦 + 𝐶 ) ∈ ℝ )
14 12 2 13 syl2anr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 𝐶 ) ∈ ℝ )
15 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 𝐶 ) → ( 𝑥 − 𝐶 ) = ( ( 𝑦 + 𝐶 ) − 𝐶 ) )
16 15 eleq1d ⊢ ( 𝑥 = ( 𝑦 + 𝐶 ) → ( ( 𝑥 − 𝐶 ) ∈ 𝐴 ↔ ( ( 𝑦 + 𝐶 ) − 𝐶 ) ∈ 𝐴 ) )
17 16 elrab3 ⊢ ( ( 𝑦 + 𝐶 ) ∈ ℝ → ( ( 𝑦 + 𝐶 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } ↔ ( ( 𝑦 + 𝐶 ) − 𝐶 ) ∈ 𝐴 ) )
18 14 17 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 + 𝐶 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } ↔ ( ( 𝑦 + 𝐶 ) − 𝐶 ) ∈ 𝐴 ) )
19 pncan ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝑦 + 𝐶 ) − 𝐶 ) = 𝑦 )
20 6 7 19 syl2anr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 + 𝐶 ) − 𝐶 ) = 𝑦 )
21 20 eleq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑦 + 𝐶 ) − 𝐶 ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
22 11 18 21 3bitrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 − - 𝐶 ) ∈ 𝐵 ↔ 𝑦 ∈ 𝐴 ) )
23 22 pm5.32da ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ∧ ( 𝑦 − - 𝐶 ) ∈ 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ) )
24 5 23 bitr4d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − - 𝐶 ) ∈ 𝐵 ) ) )
25 24 eqabdv ⊢ ( 𝜑 → 𝐴 = { 𝑦 ∣ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − - 𝐶 ) ∈ 𝐵 ) } )
26 df-rab ⊢ { 𝑦 ∈ ℝ ∣ ( 𝑦 − - 𝐶 ) ∈ 𝐵 } = { 𝑦 ∣ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − - 𝐶 ) ∈ 𝐵 ) }
27 25 26 eqtr4di ⊢ ( 𝜑 → 𝐴 = { 𝑦 ∈ ℝ ∣ ( 𝑦 − - 𝐶 ) ∈ 𝐵 } )