Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝑥 − 𝐴) ∈ V |
2 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
3 | 1, 2 | breldm 5329 |
. . . . . . . . 9
⊢ ((𝑥 − 𝐴)𝐹𝑦 → (𝑥 − 𝐴) ∈ dom 𝐹) |
4 | | npcan 10290 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) |
5 | 4 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
6 | 5 | ancoms 469 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
7 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑥 − 𝐴) → (𝑤 + 𝐴) = ((𝑥 − 𝐴) + 𝐴)) |
8 | 7 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 − 𝐴) → (𝑥 = (𝑤 + 𝐴) ↔ 𝑥 = ((𝑥 − 𝐴) + 𝐴))) |
9 | 8 | rspcev 3309 |
. . . . . . . . 9
⊢ (((𝑥 − 𝐴) ∈ dom 𝐹 ∧ 𝑥 = ((𝑥 − 𝐴) + 𝐴)) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
10 | 3, 6, 9 | syl2anr 495 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
11 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
12 | | eqeq1 2626 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧 = (𝑤 + 𝐴) ↔ 𝑥 = (𝑤 + 𝐴))) |
13 | 12 | rexbidv 3052 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴) ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴))) |
14 | 11, 13 | elab 3350 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
15 | 10, 14 | sylibr 224 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)}) |
16 | 1, 2 | brelrn 5356 |
. . . . . . . 8
⊢ ((𝑥 − 𝐴)𝐹𝑦 → 𝑦 ∈ ran 𝐹) |
17 | 16 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹) |
18 | 15, 17 | jca 554 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)) |
19 | 18 | expl 648 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹))) |
20 | 19 | ssopab2dv 5004 |
. . . 4
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)}) |
21 | | df-xp 5120 |
. . . 4
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)} |
22 | 20, 21 | syl6sseqr 3652 |
. . 3
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹)) |
23 | | shftfval.1 |
. . . . . 6
⊢ 𝐹 ∈ V |
24 | 23 | dmex 7099 |
. . . . 5
⊢ dom 𝐹 ∈ V |
25 | 24 | abrexex 7141 |
. . . 4
⊢ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∈ V |
26 | 23 | rnex 7100 |
. . . 4
⊢ ran 𝐹 ∈ V |
27 | 25, 26 | xpex 6962 |
. . 3
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V |
28 | | ssexg 4804 |
. . 3
⊢
(({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∧ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
29 | 22, 27, 28 | sylancl 694 |
. 2
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
30 | | breq 4655 |
. . . . . 6
⊢ (𝑧 = 𝐹 → ((𝑥 − 𝑤)𝑧𝑦 ↔ (𝑥 − 𝑤)𝐹𝑦)) |
31 | 30 | anbi2d 740 |
. . . . 5
⊢ (𝑧 = 𝐹 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦))) |
32 | 31 | opabbidv 4716 |
. . . 4
⊢ (𝑧 = 𝐹 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)}) |
33 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (𝑥 − 𝑤) = (𝑥 − 𝐴)) |
34 | 33 | breq1d 4663 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ((𝑥 − 𝑤)𝐹𝑦 ↔ (𝑥 − 𝐴)𝐹𝑦)) |
35 | 34 | anbi2d 740 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦))) |
36 | 35 | opabbidv 4716 |
. . . 4
⊢ (𝑤 = 𝐴 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
37 | | df-shft 13807 |
. . . 4
⊢ shift =
(𝑧 ∈ V, 𝑤 ∈ ℂ ↦
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)}) |
38 | 32, 36, 37 | ovmpt2g 6795 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
39 | 23, 38 | mp3an1 1411 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
40 | 29, 39 | mpdan 702 |
1
⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |