This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 ∈ V
Assertion shftfval ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ 𝐹 ∈ V
2 ovex ⊢ ( 𝑥 − 𝐴 ) ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 breldm ⊢ ( ( 𝑥 − 𝐴 ) 𝐹 𝑦 → ( 𝑥 − 𝐴 ) ∈ dom 𝐹 )
5 npcan ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) = 𝑥 )
6 5 eqcomd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → 𝑥 = ( ( 𝑥 − 𝐴 ) + 𝐴 ) )
7 6 ancoms ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → 𝑥 = ( ( 𝑥 − 𝐴 ) + 𝐴 ) )
8 oveq1 ⊢ ( 𝑤 = ( 𝑥 − 𝐴 ) → ( 𝑤 + 𝐴 ) = ( ( 𝑥 − 𝐴 ) + 𝐴 ) )
9 8 rspceeqv ⊢ ( ( ( 𝑥 − 𝐴 ) ∈ dom 𝐹 ∧ 𝑥 = ( ( 𝑥 − 𝐴 ) + 𝐴 ) ) → ∃ 𝑤 ∈ dom 𝐹 𝑥 = ( 𝑤 + 𝐴 ) )
10 4 7 9 syl2anr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → ∃ 𝑤 ∈ dom 𝐹 𝑥 = ( 𝑤 + 𝐴 ) )
11 vex ⊢ 𝑥 ∈ V
12 eqeq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 = ( 𝑤 + 𝐴 ) ↔ 𝑥 = ( 𝑤 + 𝐴 ) ) )
13 12 rexbidv ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) ↔ ∃ 𝑤 ∈ dom 𝐹 𝑥 = ( 𝑤 + 𝐴 ) ) )
14 11 13 elab ⊢ ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ↔ ∃ 𝑤 ∈ dom 𝐹 𝑥 = ( 𝑤 + 𝐴 ) )
15 10 14 sylibr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } )
16 2 3 brelrn ⊢ ( ( 𝑥 − 𝐴 ) 𝐹 𝑦 → 𝑦 ∈ ran 𝐹 )
17 16 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → 𝑦 ∈ ran 𝐹 )
18 15 17 jca ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∧ 𝑦 ∈ ran 𝐹 ) )
19 18 expl ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) → ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∧ 𝑦 ∈ ran 𝐹 ) ) )
20 19 ssopab2dv ⊢ ( 𝐴 ∈ ℂ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∧ 𝑦 ∈ ran 𝐹 ) } )
21 df-xp ⊢ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∧ 𝑦 ∈ ran 𝐹 ) }
22 20 21 sseqtrrdi ⊢ ( 𝐴 ∈ ℂ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ⊆ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) )
23 1 dmex ⊢ dom 𝐹 ∈ V
24 23 abrexex ⊢ { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } ∈ V
25 1 rnex ⊢ ran 𝐹 ∈ V
26 24 25 xpex ⊢ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) ∈ V
27 ssexg ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ⊆ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) ∧ ( { 𝑧 ∣ ∃ 𝑤 ∈ dom 𝐹 𝑧 = ( 𝑤 + 𝐴 ) } × ran 𝐹 ) ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∈ V )
28 22 26 27 sylancl ⊢ ( 𝐴 ∈ ℂ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∈ V )
29 breq ⊢ ( 𝑧 = 𝐹 → ( ( 𝑥 − 𝑤 ) 𝑧 𝑦 ↔ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) )
30 29 anbi2d ⊢ ( 𝑧 = 𝐹 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝑧 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) ) )
31 30 opabbidv ⊢ ( 𝑧 = 𝐹 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝑧 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) } )
32 oveq2 ⊢ ( 𝑤 = 𝐴 → ( 𝑥 − 𝑤 ) = ( 𝑥 − 𝐴 ) )
33 32 breq1d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑥 − 𝑤 ) 𝐹 𝑦 ↔ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) )
34 33 anbi2d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) ) )
35 34 opabbidv ⊢ ( 𝑤 = 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝐹 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
36 df-shft ⊢ shift = ( 𝑧 ∈ V , 𝑤 ∈ ℂ ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝑤 ) 𝑧 𝑦 ) } )
37 31 35 36 ovmpog ⊢ ( ( 𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∈ V ) → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
38 1 37 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ∈ V ) → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )
39 28 38 mpdan ⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } )