Step | Hyp | Ref
| Expression |
1 | | simplr 528 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑥 ∈ ℂ) |
2 | | simpll 527 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝐴 ∈ ℂ) |
3 | 1, 2 | subcld 8258 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 − 𝐴) ∈ ℂ) |
4 | | vex 2740 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
5 | | breldmg 4829 |
. . . . . . . . . . 11
⊢ (((𝑥 − 𝐴) ∈ ℂ ∧ 𝑦 ∈ V ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 − 𝐴) ∈ dom 𝐹) |
6 | 4, 5 | mp3an2 1325 |
. . . . . . . . . 10
⊢ (((𝑥 − 𝐴) ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 − 𝐴) ∈ dom 𝐹) |
7 | 3, 6 | sylancom 420 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 − 𝐴) ∈ dom 𝐹) |
8 | | npcan 8156 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) |
9 | 8 | eqcomd 2183 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
10 | 9 | ancoms 268 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
11 | 10 | adantr 276 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑥 = ((𝑥 − 𝐴) + 𝐴)) |
12 | | oveq1 5876 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑥 − 𝐴) → (𝑤 + 𝐴) = ((𝑥 − 𝐴) + 𝐴)) |
13 | 12 | eqeq2d 2189 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 − 𝐴) → (𝑥 = (𝑤 + 𝐴) ↔ 𝑥 = ((𝑥 − 𝐴) + 𝐴))) |
14 | 13 | rspcev 2841 |
. . . . . . . . 9
⊢ (((𝑥 − 𝐴) ∈ dom 𝐹 ∧ 𝑥 = ((𝑥 − 𝐴) + 𝐴)) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
15 | 7, 11, 14 | syl2anc 411 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
16 | | vex 2740 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
17 | | eqeq1 2184 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧 = (𝑤 + 𝐴) ↔ 𝑥 = (𝑤 + 𝐴))) |
18 | 17 | rexbidv 2478 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴) ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴))) |
19 | 16, 18 | elab 2881 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ↔ ∃𝑤 ∈ dom 𝐹 𝑥 = (𝑤 + 𝐴)) |
20 | 15, 19 | sylibr 134 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)}) |
21 | | brelrng 4854 |
. . . . . . . . 9
⊢ (((𝑥 − 𝐴) ∈ ℂ ∧ 𝑦 ∈ V ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹) |
22 | 4, 21 | mp3an2 1325 |
. . . . . . . 8
⊢ (((𝑥 − 𝐴) ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹) |
23 | 3, 22 | sylancom 420 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → 𝑦 ∈ ran 𝐹) |
24 | 20, 23 | jca 306 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)) |
25 | 24 | expl 378 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦) → (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹))) |
26 | 25 | ssopab2dv 4275 |
. . . 4
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)}) |
27 | | df-xp 4629 |
. . . 4
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∧ 𝑦 ∈ ran 𝐹)} |
28 | 26, 27 | sseqtrrdi 3204 |
. . 3
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹)) |
29 | | shftfval.1 |
. . . . . 6
⊢ 𝐹 ∈ V |
30 | 29 | dmex 4889 |
. . . . 5
⊢ dom 𝐹 ∈ V |
31 | 30 | abrexex 6112 |
. . . 4
⊢ {𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} ∈ V |
32 | 29 | rnex 4890 |
. . . 4
⊢ ran 𝐹 ∈ V |
33 | 31, 32 | xpex 4738 |
. . 3
⊢ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V |
34 | | ssexg 4139 |
. . 3
⊢
(({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ⊆ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∧ ({𝑧 ∣ ∃𝑤 ∈ dom 𝐹 𝑧 = (𝑤 + 𝐴)} × ran 𝐹) ∈ V) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
35 | 28, 33, 34 | sylancl 413 |
. 2
⊢ (𝐴 ∈ ℂ →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) |
36 | | breq 4002 |
. . . . . 6
⊢ (𝑧 = 𝐹 → ((𝑥 − 𝑤)𝑧𝑦 ↔ (𝑥 − 𝑤)𝐹𝑦)) |
37 | 36 | anbi2d 464 |
. . . . 5
⊢ (𝑧 = 𝐹 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦))) |
38 | 37 | opabbidv 4066 |
. . . 4
⊢ (𝑧 = 𝐹 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)}) |
39 | | oveq2 5877 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (𝑥 − 𝑤) = (𝑥 − 𝐴)) |
40 | 39 | breq1d 4010 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ((𝑥 − 𝑤)𝐹𝑦 ↔ (𝑥 − 𝐴)𝐹𝑦)) |
41 | 40 | anbi2d 464 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦) ↔ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦))) |
42 | 41 | opabbidv 4066 |
. . . 4
⊢ (𝑤 = 𝐴 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝐹𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
43 | | df-shft 10808 |
. . . 4
⊢ shift =
(𝑧 ∈ V, 𝑤 ∈ ℂ ↦
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝑤)𝑧𝑦)}) |
44 | 38, 42, 43 | ovmpog 6003 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
45 | 29, 44 | mp3an1 1324 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)} ∈ V) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
46 | 35, 45 | mpdan 421 |
1
⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |