Metamath Proof Explorer

Theorem shftlem

Description: Two ways to write a shifted set ( B + A ) . (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion shftlem ⊢ A ∈ ℂ ∧ B ⊆ ℂ → x ∈ ℂ | x − A ∈ B = x | ∃ y ∈ B x = y + A

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ ℂ | x − A ∈ B = x | x ∈ ℂ ∧ x − A ∈ B
2 npcan ⊢ x ∈ ℂ ∧ A ∈ ℂ → x - A + A = x
3 2 ancoms ⊢ A ∈ ℂ ∧ x ∈ ℂ → x - A + A = x
4 3 eqcomd ⊢ A ∈ ℂ ∧ x ∈ ℂ → x = x - A + A
5 oveq1 ⊢ y = x − A → y + A = x - A + A
6 5 rspceeqv ⊢ x − A ∈ B ∧ x = x - A + A → ∃ y ∈ B x = y + A
7 6 expcom ⊢ x = x - A + A → x − A ∈ B → ∃ y ∈ B x = y + A
8 4 7 syl ⊢ A ∈ ℂ ∧ x ∈ ℂ → x − A ∈ B → ∃ y ∈ B x = y + A
9 8 expimpd ⊢ A ∈ ℂ → x ∈ ℂ ∧ x − A ∈ B → ∃ y ∈ B x = y + A
10 9 adantr ⊢ A ∈ ℂ ∧ B ⊆ ℂ → x ∈ ℂ ∧ x − A ∈ B → ∃ y ∈ B x = y + A
11 ssel2 ⊢ B ⊆ ℂ ∧ y ∈ B → y ∈ ℂ
12 addcl ⊢ y ∈ ℂ ∧ A ∈ ℂ → y + A ∈ ℂ
13 11 12 sylan ⊢ B ⊆ ℂ ∧ y ∈ B ∧ A ∈ ℂ → y + A ∈ ℂ
14 pncan ⊢ y ∈ ℂ ∧ A ∈ ℂ → y + A - A = y
15 11 14 sylan ⊢ B ⊆ ℂ ∧ y ∈ B ∧ A ∈ ℂ → y + A - A = y
16 simplr ⊢ B ⊆ ℂ ∧ y ∈ B ∧ A ∈ ℂ → y ∈ B
17 15 16 eqeltrd ⊢ B ⊆ ℂ ∧ y ∈ B ∧ A ∈ ℂ → y + A - A ∈ B
18 13 17 jca ⊢ B ⊆ ℂ ∧ y ∈ B ∧ A ∈ ℂ → y + A ∈ ℂ ∧ y + A - A ∈ B
19 18 ancoms ⊢ A ∈ ℂ ∧ B ⊆ ℂ ∧ y ∈ B → y + A ∈ ℂ ∧ y + A - A ∈ B
20 19 anassrs ⊢ A ∈ ℂ ∧ B ⊆ ℂ ∧ y ∈ B → y + A ∈ ℂ ∧ y + A - A ∈ B
21 eleq1 ⊢ x = y + A → x ∈ ℂ ↔ y + A ∈ ℂ
22 oveq1 ⊢ x = y + A → x − A = y + A - A
23 22 eleq1d ⊢ x = y + A → x − A ∈ B ↔ y + A - A ∈ B
24 21 23 anbi12d ⊢ x = y + A → x ∈ ℂ ∧ x − A ∈ B ↔ y + A ∈ ℂ ∧ y + A - A ∈ B
25 20 24 syl5ibrcom ⊢ A ∈ ℂ ∧ B ⊆ ℂ ∧ y ∈ B → x = y + A → x ∈ ℂ ∧ x − A ∈ B
26 25 rexlimdva ⊢ A ∈ ℂ ∧ B ⊆ ℂ → ∃ y ∈ B x = y + A → x ∈ ℂ ∧ x − A ∈ B
27 10 26 impbid ⊢ A ∈ ℂ ∧ B ⊆ ℂ → x ∈ ℂ ∧ x − A ∈ B ↔ ∃ y ∈ B x = y + A
28 27 abbidv ⊢ A ∈ ℂ ∧ B ⊆ ℂ → x | x ∈ ℂ ∧ x − A ∈ B = x | ∃ y ∈ B x = y + A
29 1 28 syl5eq ⊢ A ∈ ℂ ∧ B ⊆ ℂ → x ∈ ℂ | x − A ∈ B = x | ∃ y ∈ B x = y + A