Theorem shftf

Description: Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

	Ref	Expression
Hypothesis	shftfval.1	⊢ 𝐹 ∈ V
Assertion	shftf	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) : { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	⊢ 𝐹 ∈ V
2		ffn	⊢ ( 𝐹 : 𝐵 ⟶ 𝐶 → 𝐹 Fn 𝐵 )
3	1	shftfn	⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } )
4	2 3	sylan	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } )
5		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 − 𝐴 ) = ( 𝑦 − 𝐴 ) )
6	5	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 − 𝐴 ) ∈ 𝐵 ↔ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) )
7	6	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ↔ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) )
8		simpr	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) → 𝐴 ∈ ℂ )
9		simpl	⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) → 𝑦 ∈ ℂ )
10	1	shftval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 − 𝐴 ) ) )
11	8 9 10	syl2an	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 − 𝐴 ) ) )
12		simpl	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) → 𝐹 : 𝐵 ⟶ 𝐶 )
13		simpr	⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) → ( 𝑦 − 𝐴 ) ∈ 𝐵 )
14		ffvelrn	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑦 − 𝐴 ) ) ∈ 𝐶 )
15	12 13 14	syl2an	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 − 𝐴 ) ) ∈ 𝐶 )
16	11 15	eqeltrd	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝑦 ) ∈ 𝐶 )
17	7 16	sylan2b	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) ∧ 𝑦 ∈ { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝑦 ) ∈ 𝐶 )
18	17	ralrimiva	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) → ∀ 𝑦 ∈ { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ( ( 𝐹 shift 𝐴 ) ‘ 𝑦 ) ∈ 𝐶 )
19		ffnfv	⊢ ( ( 𝐹 shift 𝐴 ) : { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ⟶ 𝐶 ↔ ( ( 𝐹 shift 𝐴 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ( ( 𝐹 shift 𝐴 ) ‘ 𝑦 ) ∈ 𝐶 ) )
20	4 18 19	sylanbrc	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 shift 𝐴 ) : { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ⟶ 𝐶 )