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 ∈ ℂ → F shift A = x y | x ∈ ℂ ∧ x − A F y

Proof

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