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 ∈ ℂ → F shift A B = F B − A

Proof

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