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

Metamath Proof Explorer

Theorem shftfib

Description: Value of a fiber of the relation F . (Contributed by Mario Carneiro, 4-Nov-2013)

Ref Expression
Hypothesis shftfval.1 ⊢ 𝐹 ∈ V
Assertion shftfib ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) )

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ 𝐹 ∈ V
2 1 shftfval ⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
3 2 breqd ⊢ ( 𝐴 ∈ ℂ → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ 𝐵 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ) )
4 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
5 oveq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 − 𝐴 ) = ( 𝐵 − 𝐴 ) )
6 5 breq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 − 𝐴 ) 𝐹 𝑦 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) )
7 4 6 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) ) )
8 breq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝐵 − 𝐴 ) 𝐹 𝑦 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) )
9 8 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
10 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) }
11 7 9 10 brabg ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑧 ∈ V ) → ( 𝐵 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
12 11 elvd ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
13 3 12 sylan9bb ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
14 ibar ⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 − 𝐴 ) 𝐹 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
15 14 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐹 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) )
16 13 15 bitr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) )
17 16 abbidv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } )
18 imasng ⊢ ( 𝐵 ∈ ℂ → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } )
19 18 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } )
20 ovex ⊢ ( 𝐵 − 𝐴 ) ∈ V
21 imasng ⊢ ( ( 𝐵 − 𝐴 ) ∈ V → ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } )
22 20 21 mp1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } )
23 17 19 22 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) )