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

Metamath Proof Explorer

Theorem shftidt

Description: Identity law for the shift operation. (Contributed by NM, 19-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

Ref Expression
Hypothesis shftfval.1 ⊢ F ∈ V
Assertion shftidt ⊢ A ∈ ℂ → F shift 0 ⁡ A = F ⁡ A

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ F ∈ V
2 1 shftidt2 ⊢ F shift 0 = F ↾ ℂ
3 2 fveq1i ⊢ F shift 0 ⁡ A = F ↾ ℂ ⁡ A
4 fvres ⊢ A ∈ ℂ → F ↾ ℂ ⁡ A = F ⁡ A
5 3 4 eqtrid ⊢ A ∈ ℂ → F shift 0 ⁡ A = F ⁡ A