Metamath Proof Explorer

Theorem shftfval

Description: The value of the sequence shifter operation is a function on CC . A is ordinarily an integer. (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis shftfval.1 ⊢F∈V
Assertion shftfval ⊢A∈ℂ→FshiftA=xy|x∈ℂ∧x−AFy

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢F∈V
2 ovex ⊢x−A∈V
3 vex ⊢y∈V
4 2 3 breldm ⊢x−AFy→x−A∈dom⁡F
5 npcan ⊢x∈ℂ∧A∈ℂ→x-A+A=x
6 5 eqcomd ⊢x∈ℂ∧A∈ℂ→x=x-A+A
7 6 ancoms ⊢A∈ℂ∧x∈ℂ→x=x-A+A
8 oveq1 ⊢w=x−A→w+A=x-A+A
9 8 rspceeqv ⊢x−A∈dom⁡F∧x=x-A+A→∃w∈dom⁡Fx=w+A
10 4 7 9 syl2anr ⊢A∈ℂ∧x∈ℂ∧x−AFy→∃w∈dom⁡Fx=w+A
11 vex ⊢x∈V
12 eqeq1 ⊢z=x→z=w+A↔x=w+A
13 12 rexbidv ⊢z=x→∃w∈dom⁡Fz=w+A↔∃w∈dom⁡Fx=w+A
14 11 13 elab ⊢x∈z|∃w∈dom⁡Fz=w+A↔∃w∈dom⁡Fx=w+A
15 10 14 sylibr ⊢A∈ℂ∧x∈ℂ∧x−AFy→x∈z|∃w∈dom⁡Fz=w+A
16 2 3 brelrn ⊢x−AFy→y∈ran⁡F
17 16 adantl ⊢A∈ℂ∧x∈ℂ∧x−AFy→y∈ran⁡F
18 15 17 jca ⊢A∈ℂ∧x∈ℂ∧x−AFy→x∈z|∃w∈dom⁡Fz=w+A∧y∈ran⁡F
19 18 expl ⊢A∈ℂ→x∈ℂ∧x−AFy→x∈z|∃w∈dom⁡Fz=w+A∧y∈ran⁡F
20 19 ssopab2dv ⊢A∈ℂ→xy|x∈ℂ∧x−AFy⊆xy|x∈z|∃w∈dom⁡Fz=w+A∧y∈ran⁡F
21 df-xp ⊢z|∃w∈dom⁡Fz=w+A×ran⁡F=xy|x∈z|∃w∈dom⁡Fz=w+A∧y∈ran⁡F
22 20 21 sseqtrrdi ⊢A∈ℂ→xy|x∈ℂ∧x−AFy⊆z|∃w∈dom⁡Fz=w+A×ran⁡F
23 1 dmex ⊢dom⁡F∈V
24 23 abrexex ⊢z|∃w∈dom⁡Fz=w+A∈V
25 1 rnex ⊢ran⁡F∈V
26 24 25 xpex ⊢z|∃w∈dom⁡Fz=w+A×ran⁡F∈V
27 ssexg ⊢xy|x∈ℂ∧x−AFy⊆z|∃w∈dom⁡Fz=w+A×ran⁡F∧z|∃w∈dom⁡Fz=w+A×ran⁡F∈V→xy|x∈ℂ∧x−AFy∈V
28 22 26 27 sylancl ⊢A∈ℂ→xy|x∈ℂ∧x−AFy∈V
29 breq ⊢z=F→x−wzy↔x−wFy
30 29 anbi2d ⊢z=F→x∈ℂ∧x−wzy↔x∈ℂ∧x−wFy
31 30 opabbidv ⊢z=F→xy|x∈ℂ∧x−wzy=xy|x∈ℂ∧x−wFy
32 oveq2 ⊢w=A→x−w=x−A
33 32 breq1d ⊢w=A→x−wFy↔x−AFy
34 33 anbi2d ⊢w=A→x∈ℂ∧x−wFy↔x∈ℂ∧x−AFy
35 34 opabbidv ⊢w=A→xy|x∈ℂ∧x−wFy=xy|x∈ℂ∧x−AFy
36 df-shft ⊢shift=z∈V,w∈ℂ⟼xy|x∈ℂ∧x−wzy
37 31 35 36 ovmpog ⊢F∈V∧A∈ℂ∧xy|x∈ℂ∧x−AFy∈V→FshiftA=xy|x∈ℂ∧x−AFy
38 1 37 mp3an1 ⊢A∈ℂ∧xy|x∈ℂ∧x−AFy∈V→FshiftA=xy|x∈ℂ∧x−AFy
39 28 38 mpdan ⊢A∈ℂ→FshiftA=xy|x∈ℂ∧x−AFy