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 e. _V
Assertion shftidt
|- ( A e. CC -> ( ( F shift 0 ) ` A ) = ( F ` A ) )

Proof

Step Hyp Ref Expression
1 shftfval.1
 |-  F e. _V
2 1 shftidt2
 |-  ( F shift 0 ) = ( F |` CC )
3 2 fveq1i
 |-  ( ( F shift 0 ) ` A ) = ( ( F |` CC ) ` A )
4 fvres
 |-  ( A e. CC -> ( ( F |` CC ) ` A ) = ( F ` A ) )
5 3 4 eqtrid
 |-  ( A e. CC -> ( ( F shift 0 ) ` A ) = ( F ` A ) )