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∈ℂ→FshiftA:x∈ℂ|x−A∈B⟶C

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢F∈V
2 ffn ⊢F:B⟶C→FFnB
3 1 shftfn ⊢FFnB∧A∈ℂ→FshiftAFnx∈ℂ|x−A∈B
4 2 3 sylan ⊢F:B⟶C∧A∈ℂ→FshiftAFnx∈ℂ|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∈ℂ→FshiftA⁡y=F⁡y−A
11 8 9 10 syl2an ⊢F:B⟶C∧A∈ℂ∧y∈ℂ∧y−A∈B→FshiftA⁡y=F⁡y−A
12 simpl ⊢F:B⟶C∧A∈ℂ→F:B⟶C
13 simpr ⊢y∈ℂ∧y−A∈B→y−A∈B
14 ffvelcdm ⊢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→FshiftA⁡y∈C
17 7 16 sylan2b ⊢F:B⟶C∧A∈ℂ∧y∈x∈ℂ|x−A∈B→FshiftA⁡y∈C
18 17 ralrimiva ⊢F:B⟶C∧A∈ℂ→∀y∈x∈ℂ|x−A∈BFshiftA⁡y∈C
19 ffnfv ⊢FshiftA:x∈ℂ|x−A∈B⟶C↔FshiftAFnx∈ℂ|x−A∈B∧∀y∈x∈ℂ|x−A∈BFshiftA⁡y∈C
20 4 18 19 sylanbrc ⊢F:B⟶C∧A∈ℂ→FshiftA:x∈ℂ|x−A∈B⟶C