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

Metamath Proof Explorer

Theorem shftdm

Description: Domain of a relation shifted by A . The set on the right is more commonly notated as ( dom F + A ) (meaning add A to every element of dom F ). (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis shftfval.1 ⊢ 𝐹 ∈ V
Assertion shftdm ( 𝐴 ∈ ℂ → dom ( 𝐹 shift 𝐴 ) = { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 } )

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ 𝐹 ∈ V
2 1 shftfval ⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
3 2 dmeqd ⊢ ( 𝐴 ∈ ℂ → dom ( 𝐹 shift 𝐴 ) = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
4 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ ∃ 𝑦 ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) )
5 ovex ⊢ ( 𝑥 − 𝐴 ) ∈ V
6 5 eldm ⊢ ( ( 𝑥 − 𝐴 ) ∈ dom 𝐹 ↔ ∃ 𝑦 ( 𝑥 − 𝐴 ) 𝐹 𝑦 )
7 6 anbi2i ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 ) ↔ ( 𝑥 ∈ ℂ ∧ ∃ 𝑦 ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) )
8 4 7 bitr4i ⊢ ( ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 ) )
9 8 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } = { 𝑥 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 ) }
10 dmopab ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) }
11 df-rab ⊢ { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 } = { 𝑥 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 ) }
12 9 10 11 3eqtr4i ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } = { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 }
13 3 12 eqtrdi ⊢ ( 𝐴 ∈ ℂ → dom ( 𝐹 shift 𝐴 ) = { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ dom 𝐹 } )