# 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}\in \mathrm{V}$
Assertion shftidt2 ${⊢}{F}\mathrm{shift}0={{F}↾}_{ℂ}$

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 subid1 ${⊢}{x}\in ℂ\to {x}-0={x}$
3 2 breq1d ${⊢}{x}\in ℂ\to \left(\left({x}-0\right){F}{y}↔{x}{F}{y}\right)$
4 3 pm5.32i ${⊢}\left({x}\in ℂ\wedge \left({x}-0\right){F}{y}\right)↔\left({x}\in ℂ\wedge {x}{F}{y}\right)$
5 4 opabbii ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-0\right){F}{y}\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge {x}{F}{y}\right)\right\}$
6 0cn ${⊢}0\in ℂ$
7 1 shftfval ${⊢}0\in ℂ\to {F}\mathrm{shift}0=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-0\right){F}{y}\right)\right\}$
8 6 7 ax-mp ${⊢}{F}\mathrm{shift}0=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-0\right){F}{y}\right)\right\}$
9 dfres2 ${⊢}{{F}↾}_{ℂ}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge {x}{F}{y}\right)\right\}$
10 5 8 9 3eqtr4i ${⊢}{F}\mathrm{shift}0={{F}↾}_{ℂ}$