Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑥 − 𝐴) ∈ V |
2 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
3 | 1, 2 | breldm 5251 |
. . . . . . . . 9
⊢ ((𝑥 − 𝐴)𝐹𝑦 → (𝑥 − 𝐴) ∈ dom 𝐹) |
4 | | npcan 10169 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) |
5 | 4 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
6 | 5 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
7 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑥 − 𝐴) → (𝑤 + 𝐴) = ((𝑥 − 𝐴) + 𝐴)) |
8 | 7 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 − 𝐴) → (𝑥 = (𝑤 + 𝐴) ↔ 𝑥 = ((𝑥 − 𝐴) + 𝐴))) |
9 | 8 | rspcev 3282 |
. . . . . . . . 9
⊢ (((𝑥 − 𝐴) ∈ dom 𝐹 ∧ 𝑥 = ((𝑥 − 𝐴) + 𝐴)) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
10 | 3, 6, 9 | syl2anr 494 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
11 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
12 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧 = (𝑤 + 𝐴) ↔ 𝑥 = (𝑤 + 𝐴))) |
13 | 12 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴) ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴))) |
14 | 11, 13 | elab 3319 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
15 | 10, 14 | sylibr 223 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)}) |
16 | 1, 2 | brelrn 5277 |
. . . . . . . 8
⊢ ((𝑥 − 𝐴)𝐹𝑦 → 𝑦 ∈ ran 𝐹) |
17 | 16 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹) |
18 | 15, 17 | jca 553 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)) |
19 | 18 | expl 646 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹))) |
20 | 19 | ssopab2dv 4929 |
. . . 4
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)}) |
21 | | df-xp 5044 |
. . . 4
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)} |
22 | 20, 21 | syl6sseqr 3615 |
. . 3
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹)) |
23 | | shftfval.1 |
. . . . . 6
⊢ 𝐹 ∈ V |
24 | 23 | dmex 6991 |
. . . . 5
⊢ dom 𝐹 ∈ V |
25 | 24 | abrexex 7033 |
. . . 4
⊢ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∈ V |
26 | 23 | rnex 6992 |
. . . 4
⊢ ran 𝐹 ∈ V |
27 | 25, 26 | xpex 6860 |
. . 3
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V |
28 | | ssexg 4732 |
. . 3
⊢
(({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∧ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
29 | 22, 27, 28 | sylancl 693 |
. 2
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
30 | | breq 4585 |
. . . . . 6
⊢ (𝑧 = 𝐹 → ((𝑥 − 𝑤)𝑧𝑦 ↔ (𝑥 − 𝑤)𝐹𝑦)) |
31 | 30 | anbi2d 736 |
. . . . 5
⊢ (𝑧 = 𝐹 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦))) |
32 | 31 | opabbidv 4648 |
. . . 4
⊢ (𝑧 = 𝐹 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)}) |
33 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (𝑥 − 𝑤) = (𝑥 − 𝐴)) |
34 | 33 | breq1d 4593 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ((𝑥 − 𝑤)𝐹𝑦 ↔ (𝑥 − 𝐴)𝐹𝑦)) |
35 | 34 | anbi2d 736 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦))) |
36 | 35 | opabbidv 4648 |
. . . 4
⊢ (𝑤 = 𝐴 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
37 | | df-shft 13655 |
. . . 4
⊢ shift =
(𝑧 ∈ V, 𝑤 ∈ ℂ ↦
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)}) |
38 | 32, 36, 37 | ovmpt2g 6693 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
39 | 23, 38 | mp3an1 1403 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
40 | 29, 39 | mpdan 699 |
1
⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |