# 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 ${⊢}{F}\in \mathrm{V}$
Assertion shftfib ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\left[\left\{{B}\right\}\right]={F}\left[\left\{{B}-{A}\right\}\right]$

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 1 shftfval ${⊢}{A}\in ℂ\to {F}\mathrm{shift}{A}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
3 2 breqd ${⊢}{A}\in ℂ\to \left({B}\left({F}\mathrm{shift}{A}\right){z}↔{B}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{z}\right)$
4 eleq1 ${⊢}{x}={B}\to \left({x}\in ℂ↔{B}\in ℂ\right)$
5 oveq1 ${⊢}{x}={B}\to {x}-{A}={B}-{A}$
6 5 breq1d ${⊢}{x}={B}\to \left(\left({x}-{A}\right){F}{y}↔\left({B}-{A}\right){F}{y}\right)$
7 4 6 anbi12d ${⊢}{x}={B}\to \left(\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)↔\left({B}\in ℂ\wedge \left({B}-{A}\right){F}{y}\right)\right)$
8 breq2 ${⊢}{y}={z}\to \left(\left({B}-{A}\right){F}{y}↔\left({B}-{A}\right){F}{z}\right)$
9 8 anbi2d ${⊢}{y}={z}\to \left(\left({B}\in ℂ\wedge \left({B}-{A}\right){F}{y}\right)↔\left({B}\in ℂ\wedge \left({B}-{A}\right){F}{z}\right)\right)$
10 eqid ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
11 7 9 10 brabg ${⊢}\left({B}\in ℂ\wedge {z}\in \mathrm{V}\right)\to \left({B}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{z}↔\left({B}\in ℂ\wedge \left({B}-{A}\right){F}{z}\right)\right)$
12 11 elvd ${⊢}{B}\in ℂ\to \left({B}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{z}↔\left({B}\in ℂ\wedge \left({B}-{A}\right){F}{z}\right)\right)$
13 3 12 sylan9bb ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({B}\left({F}\mathrm{shift}{A}\right){z}↔\left({B}\in ℂ\wedge \left({B}-{A}\right){F}{z}\right)\right)$
14 ibar ${⊢}{B}\in ℂ\to \left(\left({B}-{A}\right){F}{z}↔\left({B}\in ℂ\wedge \left({B}-{A}\right){F}{z}\right)\right)$
15 14 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({B}-{A}\right){F}{z}↔\left({B}\in ℂ\wedge \left({B}-{A}\right){F}{z}\right)\right)$
16 13 15 bitr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({B}\left({F}\mathrm{shift}{A}\right){z}↔\left({B}-{A}\right){F}{z}\right)$
17 16 abbidv ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left\{{z}|{B}\left({F}\mathrm{shift}{A}\right){z}\right\}=\left\{{z}|\left({B}-{A}\right){F}{z}\right\}$
18 imasng ${⊢}{B}\in ℂ\to \left({F}\mathrm{shift}{A}\right)\left[\left\{{B}\right\}\right]=\left\{{z}|{B}\left({F}\mathrm{shift}{A}\right){z}\right\}$
19 18 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\left[\left\{{B}\right\}\right]=\left\{{z}|{B}\left({F}\mathrm{shift}{A}\right){z}\right\}$
20 ovex ${⊢}{B}-{A}\in \mathrm{V}$
21 imasng ${⊢}{B}-{A}\in \mathrm{V}\to {F}\left[\left\{{B}-{A}\right\}\right]=\left\{{z}|\left({B}-{A}\right){F}{z}\right\}$
22 20 21 mp1i ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {F}\left[\left\{{B}-{A}\right\}\right]=\left\{{z}|\left({B}-{A}\right){F}{z}\right\}$
23 17 19 22 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\left[\left\{{B}\right\}\right]={F}\left[\left\{{B}-{A}\right\}\right]$