shftidt2

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

		Ref	Expression
	Hypothesis	shftfval.1	$⊢ F \in V$
	Assertion	shftidt2	$⊢ F shift 0 = {F ↾}_{ℂ}$

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

Metamath Proof Explorer