| Step | Hyp | Ref
| Expression |
| 1 | | shftfval.1 |
. . . . . . . . 9
⊢ 𝐹 ∈ V |
| 2 | 1 | shftfval 15109 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ℂ ∧ (𝑧 − 𝐴)𝐹𝑤)}) |
| 3 | 2 | breqd 5154 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((𝑥 − 𝐵)(𝐹 shift 𝐴)𝑦 ↔ (𝑥 − 𝐵){〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ℂ ∧ (𝑧 − 𝐴)𝐹𝑤)}𝑦)) |
| 4 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑥 − 𝐵) ∈ V |
| 5 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 6 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥 − 𝐵) → (𝑧 ∈ ℂ ↔ (𝑥 − 𝐵) ∈ ℂ)) |
| 7 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑥 − 𝐵) → (𝑧 − 𝐴) = ((𝑥 − 𝐵) − 𝐴)) |
| 8 | 7 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥 − 𝐵) → ((𝑧 − 𝐴)𝐹𝑤 ↔ ((𝑥 − 𝐵) − 𝐴)𝐹𝑤)) |
| 9 | 6, 8 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑧 = (𝑥 − 𝐵) → ((𝑧 ∈ ℂ ∧ (𝑧 − 𝐴)𝐹𝑤) ↔ ((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑤))) |
| 10 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (((𝑥 − 𝐵) − 𝐴)𝐹𝑤 ↔ ((𝑥 − 𝐵) − 𝐴)𝐹𝑦)) |
| 11 | 10 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑤) ↔ ((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑦))) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢
{〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ℂ ∧ (𝑧 − 𝐴)𝐹𝑤)} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ℂ ∧ (𝑧 − 𝐴)𝐹𝑤)} |
| 13 | 4, 5, 9, 11, 12 | brab 5548 |
. . . . . . 7
⊢ ((𝑥 − 𝐵){〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ℂ ∧ (𝑧 − 𝐴)𝐹𝑤)}𝑦 ↔ ((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑦)) |
| 14 | 3, 13 | bitrdi 287 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((𝑥 − 𝐵)(𝐹 shift 𝐴)𝑦 ↔ ((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑦))) |
| 15 | 14 | ad2antrr 726 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑥 ∈ ℂ) → ((𝑥 − 𝐵)(𝐹 shift 𝐴)𝑦 ↔ ((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑦))) |
| 16 | | subcl 11507 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑥 − 𝐵) ∈ ℂ) |
| 17 | 16 | biantrurd 532 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝑥 − 𝐵) − 𝐴)𝐹𝑦 ↔ ((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑦))) |
| 18 | 17 | ancoms 458 |
. . . . . 6
⊢ ((𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (((𝑥 − 𝐵) − 𝐴)𝐹𝑦 ↔ ((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑦))) |
| 19 | 18 | adantll 714 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑥 ∈ ℂ) → (((𝑥 − 𝐵) − 𝐴)𝐹𝑦 ↔ ((𝑥 − 𝐵) ∈ ℂ ∧ ((𝑥 − 𝐵) − 𝐴)𝐹𝑦))) |
| 20 | | sub32 11543 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑥 − 𝐴) − 𝐵) = ((𝑥 − 𝐵) − 𝐴)) |
| 21 | | subsub4 11542 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑥 − 𝐴) − 𝐵) = (𝑥 − (𝐴 + 𝐵))) |
| 22 | 20, 21 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑥 − 𝐵) − 𝐴) = (𝑥 − (𝐴 + 𝐵))) |
| 23 | 22 | 3expb 1121 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) → ((𝑥 − 𝐵) − 𝐴) = (𝑥 − (𝐴 + 𝐵))) |
| 24 | 23 | ancoms 458 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑥 ∈ ℂ) → ((𝑥 − 𝐵) − 𝐴) = (𝑥 − (𝐴 + 𝐵))) |
| 25 | 24 | breq1d 5153 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑥 ∈ ℂ) → (((𝑥 − 𝐵) − 𝐴)𝐹𝑦 ↔ (𝑥 − (𝐴 + 𝐵))𝐹𝑦)) |
| 26 | 15, 19, 25 | 3bitr2d 307 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑥 ∈ ℂ) → ((𝑥 − 𝐵)(𝐹 shift 𝐴)𝑦 ↔ (𝑥 − (𝐴 + 𝐵))𝐹𝑦)) |
| 27 | 26 | pm5.32da 579 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝐵)(𝐹 shift 𝐴)𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − (𝐴 + 𝐵))𝐹𝑦))) |
| 28 | 27 | opabbidv 5209 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐵)(𝐹 shift 𝐴)𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − (𝐴 + 𝐵))𝐹𝑦)}) |
| 29 | | ovex 7464 |
. . . 4
⊢ (𝐹 shift 𝐴) ∈ V |
| 30 | 29 | shftfval 15109 |
. . 3
⊢ (𝐵 ∈ ℂ → ((𝐹 shift 𝐴) shift 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐵)(𝐹 shift 𝐴)𝑦)}) |
| 31 | 30 | adantl 481 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐵)(𝐹 shift 𝐴)𝑦)}) |
| 32 | | addcl 11237 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| 33 | 1 | shftfval 15109 |
. . 3
⊢ ((𝐴 + 𝐵) ∈ ℂ → (𝐹 shift (𝐴 + 𝐵)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − (𝐴 + 𝐵))𝐹𝑦)}) |
| 34 | 32, 33 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 shift (𝐴 + 𝐵)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − (𝐴 + 𝐵))𝐹𝑦)}) |
| 35 | 28, 31, 34 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵))) |