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∈V
Assertion shftfib ⊢A∈ℂ∧B∈ℂ→FshiftAB=FB−A

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢F∈V
2 1 shftfval ⊢A∈ℂ→FshiftA=xy|x∈ℂ∧x−AFy
3 2 breqd ⊢A∈ℂ→BFshiftAz↔Bxy|x∈ℂ∧x−AFyz
4 eleq1 ⊢x=B→x∈ℂ↔B∈ℂ
5 oveq1 ⊢x=B→x−A=B−A
6 5 breq1d ⊢x=B→x−AFy↔B−AFy
7 4 6 anbi12d ⊢x=B→x∈ℂ∧x−AFy↔B∈ℂ∧B−AFy
8 breq2 ⊢y=z→B−AFy↔B−AFz
9 8 anbi2d ⊢y=z→B∈ℂ∧B−AFy↔B∈ℂ∧B−AFz
10 eqid ⊢xy|x∈ℂ∧x−AFy=xy|x∈ℂ∧x−AFy
11 7 9 10 brabg ⊢B∈ℂ∧z∈V→Bxy|x∈ℂ∧x−AFyz↔B∈ℂ∧B−AFz
12 11 elvd ⊢B∈ℂ→Bxy|x∈ℂ∧x−AFyz↔B∈ℂ∧B−AFz
13 3 12 sylan9bb ⊢A∈ℂ∧B∈ℂ→BFshiftAz↔B∈ℂ∧B−AFz
14 ibar ⊢B∈ℂ→B−AFz↔B∈ℂ∧B−AFz
15 14 adantl ⊢A∈ℂ∧B∈ℂ→B−AFz↔B∈ℂ∧B−AFz
16 13 15 bitr4d ⊢A∈ℂ∧B∈ℂ→BFshiftAz↔B−AFz
17 16 abbidv ⊢A∈ℂ∧B∈ℂ→z|BFshiftAz=z|B−AFz
18 imasng ⊢B∈ℂ→FshiftAB=z|BFshiftAz
19 18 adantl ⊢A∈ℂ∧B∈ℂ→FshiftAB=z|BFshiftAz
20 ovex ⊢B−A∈V
21 imasng ⊢B−A∈V→FB−A=z|B−AFz
22 20 21 mp1i ⊢A∈ℂ∧B∈ℂ→FB−A=z|B−AFz
23 17 19 22 3eqtr4d ⊢A∈ℂ∧B∈ℂ→FshiftAB=FB−A