Step |
Hyp |
Ref |
Expression |
1 |
|
oveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 shift 𝐴 ) = ( 𝐹 shift 𝐴 ) ) |
2 |
1
|
fveq1d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 shift 𝐴 ) ‘ 𝐵 ) = ( ( 𝐹 shift 𝐴 ) ‘ 𝐵 ) ) |
3 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝐵 − 𝐴 ) ) = ( 𝐹 ‘ ( 𝐵 − 𝐴 ) ) ) |
4 |
2 3
|
eqeq12d |
⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 shift 𝐴 ) ‘ 𝐵 ) = ( 𝑓 ‘ ( 𝐵 − 𝐴 ) ) ↔ ( ( 𝐹 shift 𝐴 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐵 − 𝐴 ) ) ) ) |
5 |
4
|
imbi2d |
⊢ ( 𝑓 = 𝐹 → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑓 shift 𝐴 ) ‘ 𝐵 ) = ( 𝑓 ‘ ( 𝐵 − 𝐴 ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐵 − 𝐴 ) ) ) ) ) |
6 |
|
vex |
⊢ 𝑓 ∈ V |
7 |
6
|
shftval |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑓 shift 𝐴 ) ‘ 𝐵 ) = ( 𝑓 ‘ ( 𝐵 − 𝐴 ) ) ) |
8 |
5 7
|
vtoclg |
⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐵 − 𝐴 ) ) ) ) |
9 |
8
|
3impib |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐵 − 𝐴 ) ) ) |