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

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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ ) → { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 + 𝐴 ) } )

Proof

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