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

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 ⊢ 𝐹 ∈ 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 ffvelcdm ⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝑦 − 𝐴 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑦 − 𝐴 ) ) ∈ 𝐶 )
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 𝐴 ) : { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ 𝐵 } ⟶ 𝐶 )