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 ⊢ φ → A ⊆ ℝ
ovolshft.2 ⊢ φ → C ∈ ℝ
ovolshft.3 ⊢ φ → B = x ∈ ℝ | x − C ∈ A
Assertion shft2rab ⊢ φ → A = y ∈ ℝ | y − − C ∈ B

Proof

Step Hyp Ref Expression
1 ovolshft.1 ⊢ φ → A ⊆ ℝ
2 ovolshft.2 ⊢ φ → C ∈ ℝ
3 ovolshft.3 ⊢ φ → B = x ∈ ℝ | x − C ∈ A
4 1 sseld ⊢ φ → y ∈ A → y ∈ ℝ
5 4 pm4.71rd ⊢ φ → y ∈ A ↔ y ∈ ℝ ∧ y ∈ A
6 recn ⊢ y ∈ ℝ → y ∈ ℂ
7 2 recnd ⊢ φ → C ∈ ℂ
8 subneg ⊢ y ∈ ℂ ∧ C ∈ ℂ → y − − C = y + C
9 6 7 8 syl2anr ⊢ φ ∧ y ∈ ℝ → y − − C = y + C
10 3 adantr ⊢ φ ∧ y ∈ ℝ → B = x ∈ ℝ | x − C ∈ A
11 9 10 eleq12d ⊢ φ ∧ y ∈ ℝ → y − − C ∈ B ↔ y + C ∈ x ∈ ℝ | x − C ∈ A
12 id ⊢ y ∈ ℝ → y ∈ ℝ
13 readdcl ⊢ y ∈ ℝ ∧ C ∈ ℝ → y + C ∈ ℝ
14 12 2 13 syl2anr ⊢ φ ∧ y ∈ ℝ → y + C ∈ ℝ
15 oveq1 ⊢ x = y + C → x − C = y + C - C
16 15 eleq1d ⊢ x = y + C → x − C ∈ A ↔ y + C - C ∈ A
17 16 elrab3 ⊢ y + C ∈ ℝ → y + C ∈ x ∈ ℝ | x − C ∈ A ↔ y + C - C ∈ A
18 14 17 syl ⊢ φ ∧ y ∈ ℝ → y + C ∈ x ∈ ℝ | x − C ∈ A ↔ y + C - C ∈ A
19 pncan ⊢ y ∈ ℂ ∧ C ∈ ℂ → y + C - C = y
20 6 7 19 syl2anr ⊢ φ ∧ y ∈ ℝ → y + C - C = y
21 20 eleq1d ⊢ φ ∧ y ∈ ℝ → y + C - C ∈ A ↔ y ∈ A
22 11 18 21 3bitrd ⊢ φ ∧ y ∈ ℝ → y − − C ∈ B ↔ y ∈ A
23 22 pm5.32da ⊢ φ → y ∈ ℝ ∧ y − − C ∈ B ↔ y ∈ ℝ ∧ y ∈ A
24 5 23 bitr4d ⊢ φ → y ∈ A ↔ y ∈ ℝ ∧ y − − C ∈ B
25 24 abbi2dv ⊢ φ → A = y | y ∈ ℝ ∧ y − − C ∈ B
26 df-rab ⊢ y ∈ ℝ | y − − C ∈ B = y | y ∈ ℝ ∧ y − − C ∈ B
27 25 26 eqtr4di ⊢ φ → A = y ∈ ℝ | y − − C ∈ B