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 𝐹 } )