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∈Bx=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∈Bx=y+A
7 6 expcom ⊢x=x-A+A→x−A∈B→∃y∈Bx=y+A
8 4 7 syl ⊢A∈ℂ∧x∈ℂ→x−A∈B→∃y∈Bx=y+A
9 8 expimpd ⊢A∈ℂ→x∈ℂ∧x−A∈B→∃y∈Bx=y+A
10 9 adantr ⊢A∈ℂ∧B⊆ℂ→x∈ℂ∧x−A∈B→∃y∈Bx=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∈Bx=y+A→x∈ℂ∧x−A∈B
27 10 26 impbid ⊢A∈ℂ∧B⊆ℂ→x∈ℂ∧x−A∈B↔∃y∈Bx=y+A
28 27 abbidv ⊢A∈ℂ∧B⊆ℂ→x|x∈ℂ∧x−A∈B=x|∃y∈Bx=y+A
29 1 28 eqtrid ⊢A∈ℂ∧B⊆ℂ→x∈ℂ|x−A∈B=x|∃y∈Bx=y+A