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 ⊢ 𝐹 ∈ V
Assertion shftidt2 ( 𝐹 shift 0 ) = ( 𝐹 ↾ ℂ )

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ 𝐹 ∈ V
2 subid1 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 − 0 ) = 𝑥 )
3 2 breq1d ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 − 0 ) 𝐹 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
4 3 pm5.32i ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 0 ) 𝐹 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 𝐹 𝑦 ) )
5 4 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 0 ) 𝐹 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑥 𝐹 𝑦 ) }
6 0cn ⊢ 0 ∈ ℂ
7 1 shftfval ⊢ ( 0 ∈ ℂ → ( 𝐹 shift 0 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 0 ) 𝐹 𝑦 ) } )
8 6 7 ax-mp ⊢ ( 𝐹 shift 0 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 0 ) 𝐹 𝑦 ) }
9 dfres2 ⊢ ( 𝐹 ↾ ℂ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑥 𝐹 𝑦 ) }
10 5 8 9 3eqtr4i ⊢ ( 𝐹 shift 0 ) = ( 𝐹 ↾ ℂ )