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

Metamath Proof Explorer

Theorem shftval

Description: Value of a sequence shifted by A . (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 4-Nov-2013)

Ref Expression
Hypothesis shftfval.1 ⊢ 𝐹 ∈ V
Assertion shftval ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐵 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ 𝐹 ∈ V
2 1 shftfib ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) )
3 2 eleq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) ↔ 𝑥 ∈ ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) ) )
4 3 iotabidv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℩ 𝑥 𝑥 ∈ ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) ) )
5 dffv3 ⊢ ( ( 𝐹 shift 𝐴 ) ‘ 𝐵 ) = ( ℩ 𝑥 𝑥 ∈ ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) )
6 dffv3 ⊢ ( 𝐹 ‘ ( 𝐵 − 𝐴 ) ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) )
7 4 5 6 3eqtr4g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐵 − 𝐴 ) ) )