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

Metamath Proof Explorer

Theorem shftidt2

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

Ref Expression
Hypothesis shftfval.1 
|- F e. _V
Assertion shftidt2 
|- ( F shift 0 ) = ( F |` CC )

Proof

Step Hyp Ref Expression
1 shftfval.1 
 |-  F e. _V
2 subid1 
 |-  ( x e. CC -> ( x - 0 ) = x )
3 2 breq1d 
 |-  ( x e. CC -> ( ( x - 0 ) F y <-> x F y ) )
4 3 pm5.32i 
 |-  ( ( x e. CC /\ ( x - 0 ) F y ) <-> ( x e. CC /\ x F y ) )
5 4 opabbii 
 |-  { <. x , y >. | ( x e. CC /\ ( x - 0 ) F y ) } = { <. x , y >. | ( x e. CC /\ x F y ) }
6 0cn 
 |-  0 e. CC
7 1 shftfval 
 |-  ( 0 e. CC -> ( F shift 0 ) = { <. x , y >. | ( x e. CC /\ ( x - 0 ) F y ) } )
8 6 7 ax-mp 
 |-  ( F shift 0 ) = { <. x , y >. | ( x e. CC /\ ( x - 0 ) F y ) }
9 dfres2 
 |-  ( F |` CC ) = { <. x , y >. | ( x e. CC /\ x F y ) }
10 5 8 9 3eqtr4i 
 |-  ( F shift 0 ) = ( F |` CC )