Step | Hyp | Ref
| Expression |
1 | | ovex 7394 |
. . . . . . . . . 10
⊢ (𝑥 − 𝐴) ∈ V |
2 | | vex 3451 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
3 | 1, 2 | breldm 5868 |
. . . . . . . . 9
⊢ ((𝑥 − 𝐴)𝐹𝑦 → (𝑥 − 𝐴) ∈ dom 𝐹) |
4 | | npcan 11418 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) |
5 | 4 | eqcomd 2739 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
6 | 5 | ancoms 460 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
7 | | oveq1 7368 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 − 𝐴) → (𝑤 + 𝐴) = ((𝑥 − 𝐴) + 𝐴)) |
8 | 7 | rspceeqv 3599 |
. . . . . . . . 9
⊢ (((𝑥 − 𝐴) ∈ dom 𝐹 ∧ 𝑥 = ((𝑥 − 𝐴) + 𝐴)) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
9 | 3, 6, 8 | syl2anr 598 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
10 | | vex 3451 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
11 | | eqeq1 2737 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧 = (𝑤 + 𝐴) ↔ 𝑥 = (𝑤 + 𝐴))) |
12 | 11 | rexbidv 3172 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴) ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴))) |
13 | 10, 12 | elab 3634 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
14 | 9, 13 | sylibr 233 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)}) |
15 | 1, 2 | brelrn 5901 |
. . . . . . . 8
⊢ ((𝑥 − 𝐴)𝐹𝑦 → 𝑦 ∈ ran 𝐹) |
16 | 15 | adantl 483 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹) |
17 | 14, 16 | jca 513 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)) |
18 | 17 | expl 459 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹))) |
19 | 18 | ssopab2dv 5512 |
. . . 4
⊢ (𝐴 ∈ ℂ →
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)}) |
20 | | df-xp 5643 |
. . . 4
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)} |
21 | 19, 20 | sseqtrrdi 3999 |
. . 3
⊢ (𝐴 ∈ ℂ →
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹)) |
22 | | shftfval.1 |
. . . . . 6
⊢ 𝐹 ∈ V |
23 | 22 | dmex 7852 |
. . . . 5
⊢ dom 𝐹 ∈ V |
24 | 23 | abrexex 7899 |
. . . 4
⊢ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∈ V |
25 | 22 | rnex 7853 |
. . . 4
⊢ ran 𝐹 ∈ V |
26 | 24, 25 | xpex 7691 |
. . 3
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V |
27 | | ssexg 5284 |
. . 3
⊢
(({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∧ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
28 | 21, 26, 27 | sylancl 587 |
. 2
⊢ (𝐴 ∈ ℂ →
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
29 | | breq 5111 |
. . . . . 6
⊢ (𝑧 = 𝐹 → ((𝑥 − 𝑤)𝑧𝑦 ↔ (𝑥 − 𝑤)𝐹𝑦)) |
30 | 29 | anbi2d 630 |
. . . . 5
⊢ (𝑧 = 𝐹 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦))) |
31 | 30 | opabbidv 5175 |
. . . 4
⊢ (𝑧 = 𝐹 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)}) |
32 | | oveq2 7369 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (𝑥 − 𝑤) = (𝑥 − 𝐴)) |
33 | 32 | breq1d 5119 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ((𝑥 − 𝑤)𝐹𝑦 ↔ (𝑥 − 𝐴)𝐹𝑦)) |
34 | 33 | anbi2d 630 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦))) |
35 | 34 | opabbidv 5175 |
. . . 4
⊢ (𝑤 = 𝐴 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
36 | | df-shft 14961 |
. . . 4
⊢ shift =
(𝑧 ∈ V, 𝑤 ∈ ℂ ↦
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)}) |
37 | 31, 35, 36 | ovmpog 7518 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
38 | 22, 37 | mp3an1 1449 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
39 | 28, 38 | mpdan 686 |
1
⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |