Metamath Proof Explorer

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 ⊢ F ∈ V
Assertion shftf ⊢ F : B ⟶ C ∧ A ∈ ℂ → F shift A : x ∈ ℂ | x − A ∈ B ⟶ C

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ F ∈ V
2 ffn ⊢ F : B ⟶ C → F Fn B
3 1 shftfn ⊢ F Fn B ∧ A ∈ ℂ → F shift A Fn x ∈ ℂ | x − A ∈ B
4 2 3 sylan ⊢ F : B ⟶ C ∧ A ∈ ℂ → F shift A Fn x ∈ ℂ | x − A ∈ B
5 oveq1 ⊢ x = y → x − A = y − A
6 5 eleq1d ⊢ x = y → x − A ∈ B ↔ y − A ∈ B
7 6 elrab ⊢ y ∈ x ∈ ℂ | x − A ∈ B ↔ y ∈ ℂ ∧ y − A ∈ B
8 simpr ⊢ F : B ⟶ C ∧ A ∈ ℂ → A ∈ ℂ
9 simpl ⊢ y ∈ ℂ ∧ y − A ∈ B → y ∈ ℂ
10 1 shftval ⊢ A ∈ ℂ ∧ y ∈ ℂ → F shift A ⁡ y = F ⁡ y − A
11 8 9 10 syl2an ⊢ F : B ⟶ C ∧ A ∈ ℂ ∧ y ∈ ℂ ∧ y − A ∈ B → F shift A ⁡ y = F ⁡ y − A
12 simpl ⊢ F : B ⟶ C ∧ A ∈ ℂ → F : B ⟶ C
13 simpr ⊢ y ∈ ℂ ∧ y − A ∈ B → y − A ∈ B
14 ffvelrn ⊢ F : B ⟶ C ∧ y − A ∈ B → F ⁡ y − A ∈ C
15 12 13 14 syl2an ⊢ F : B ⟶ C ∧ A ∈ ℂ ∧ y ∈ ℂ ∧ y − A ∈ B → F ⁡ y − A ∈ C
16 11 15 eqeltrd ⊢ F : B ⟶ C ∧ A ∈ ℂ ∧ y ∈ ℂ ∧ y − A ∈ B → F shift A ⁡ y ∈ C
17 7 16 sylan2b ⊢ F : B ⟶ C ∧ A ∈ ℂ ∧ y ∈ x ∈ ℂ | x − A ∈ B → F shift A ⁡ y ∈ C
18 17 ralrimiva ⊢ F : B ⟶ C ∧ A ∈ ℂ → ∀ y ∈ x ∈ ℂ | x − A ∈ B F shift A ⁡ y ∈ C
19 ffnfv ⊢ F shift A : x ∈ ℂ | x − A ∈ B ⟶ C ↔ F shift A Fn x ∈ ℂ | x − A ∈ B ∧ ∀ y ∈ x ∈ ℂ | x − A ∈ B F shift A ⁡ y ∈ C
20 4 18 19 sylanbrc ⊢ F : B ⟶ C ∧ A ∈ ℂ → F shift A : x ∈ ℂ | x − A ∈ B ⟶ C