Step | Hyp | Ref
| Expression |
1 | | ovex 7215 |
. . . . . . . . . 10
⊢ (𝑥 − 𝐴) ∈ V |
2 | | vex 3404 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
3 | 1, 2 | breldm 5761 |
. . . . . . . . 9
⊢ ((𝑥 − 𝐴)𝐹𝑦 → (𝑥 − 𝐴) ∈ dom 𝐹) |
4 | | npcan 10985 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) |
5 | 4 | eqcomd 2745 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
6 | 5 | ancoms 462 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
7 | | oveq1 7189 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 − 𝐴) → (𝑤 + 𝐴) = ((𝑥 − 𝐴) + 𝐴)) |
8 | 7 | rspceeqv 3544 |
. . . . . . . . 9
⊢ (((𝑥 − 𝐴) ∈ dom 𝐹 ∧ 𝑥 = ((𝑥 − 𝐴) + 𝐴)) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
9 | 3, 6, 8 | syl2anr 600 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
10 | | vex 3404 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
11 | | eqeq1 2743 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧 = (𝑤 + 𝐴) ↔ 𝑥 = (𝑤 + 𝐴))) |
12 | 11 | rexbidv 3208 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴) ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴))) |
13 | 10, 12 | elab 3578 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
14 | 9, 13 | sylibr 237 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)}) |
15 | 1, 2 | brelrn 5795 |
. . . . . . . 8
⊢ ((𝑥 − 𝐴)𝐹𝑦 → 𝑦 ∈ ran 𝐹) |
16 | 15 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹) |
17 | 14, 16 | jca 515 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)) |
18 | 17 | expl 461 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹))) |
19 | 18 | ssopab2dv 5416 |
. . . 4
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)}) |
20 | | df-xp 5541 |
. . . 4
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)} |
21 | 19, 20 | sseqtrrdi 3938 |
. . 3
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹)) |
22 | | shftfval.1 |
. . . . . 6
⊢ 𝐹 ∈ V |
23 | 22 | dmex 7654 |
. . . . 5
⊢ dom 𝐹 ∈ V |
24 | 23 | abrexex 7700 |
. . . 4
⊢ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∈ V |
25 | 22 | rnex 7655 |
. . . 4
⊢ ran 𝐹 ∈ V |
26 | 24, 25 | xpex 7506 |
. . 3
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V |
27 | | ssexg 5201 |
. . 3
⊢
(({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∧ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
28 | 21, 26, 27 | sylancl 589 |
. 2
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
29 | | breq 5042 |
. . . . . 6
⊢ (𝑧 = 𝐹 → ((𝑥 − 𝑤)𝑧𝑦 ↔ (𝑥 − 𝑤)𝐹𝑦)) |
30 | 29 | anbi2d 632 |
. . . . 5
⊢ (𝑧 = 𝐹 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦))) |
31 | 30 | opabbidv 5106 |
. . . 4
⊢ (𝑧 = 𝐹 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)}) |
32 | | oveq2 7190 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (𝑥 − 𝑤) = (𝑥 − 𝐴)) |
33 | 32 | breq1d 5050 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ((𝑥 − 𝑤)𝐹𝑦 ↔ (𝑥 − 𝐴)𝐹𝑦)) |
34 | 33 | anbi2d 632 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦))) |
35 | 34 | opabbidv 5106 |
. . . 4
⊢ (𝑤 = 𝐴 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
36 | | df-shft 14528 |
. . . 4
⊢ shift =
(𝑧 ∈ V, 𝑤 ∈ ℂ ↦
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)}) |
37 | 31, 35, 36 | ovmpog 7336 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
38 | 22, 37 | mp3an1 1449 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
39 | 28, 38 | mpdan 687 |
1
⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |