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 e. _V
Assertion shftfval
|- ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )

Proof

Step Hyp Ref Expression
1 shftfval.1
 |-  F e. _V
2 ovex
 |-  ( x - A ) e. _V
3 vex
 |-  y e. _V
4 2 3 breldm
 |-  ( ( x - A ) F y -> ( x - A ) e. dom F )
5 npcan
 |-  ( ( x e. CC /\ A e. CC ) -> ( ( x - A ) + A ) = x )
6 5 eqcomd
 |-  ( ( x e. CC /\ A e. CC ) -> x = ( ( x - A ) + A ) )
7 6 ancoms
 |-  ( ( A e. CC /\ x e. CC ) -> x = ( ( x - A ) + A ) )
8 oveq1
 |-  ( w = ( x - A ) -> ( w + A ) = ( ( x - A ) + A ) )
9 8 rspceeqv
 |-  ( ( ( x - A ) e. dom F /\ x = ( ( x - A ) + A ) ) -> E. w e. dom F x = ( w + A ) )
10 4 7 9 syl2anr
 |-  ( ( ( A e. CC /\ x e. CC ) /\ ( x - A ) F y ) -> E. w e. dom F x = ( w + A ) )
11 vex
 |-  x e. _V
12 eqeq1
 |-  ( z = x -> ( z = ( w + A ) <-> x = ( w + A ) ) )
13 12 rexbidv
 |-  ( z = x -> ( E. w e. dom F z = ( w + A ) <-> E. w e. dom F x = ( w + A ) ) )
14 11 13 elab
 |-  ( x e. { z | E. w e. dom F z = ( w + A ) } <-> E. w e. dom F x = ( w + A ) )
15 10 14 sylibr
 |-  ( ( ( A e. CC /\ x e. CC ) /\ ( x - A ) F y ) -> x e. { z | E. w e. dom F z = ( w + A ) } )
16 2 3 brelrn
 |-  ( ( x - A ) F y -> y e. ran F )
17 16 adantl
 |-  ( ( ( A e. CC /\ x e. CC ) /\ ( x - A ) F y ) -> y e. ran F )
18 15 17 jca
 |-  ( ( ( A e. CC /\ x e. CC ) /\ ( x - A ) F y ) -> ( x e. { z | E. w e. dom F z = ( w + A ) } /\ y e. ran F ) )
19 18 expl
 |-  ( A e. CC -> ( ( x e. CC /\ ( x - A ) F y ) -> ( x e. { z | E. w e. dom F z = ( w + A ) } /\ y e. ran F ) ) )
20 19 ssopab2dv
 |-  ( A e. CC -> { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } C_ { <. x , y >. | ( x e. { z | E. w e. dom F z = ( w + A ) } /\ y e. ran F ) } )
21 df-xp
 |-  ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) = { <. x , y >. | ( x e. { z | E. w e. dom F z = ( w + A ) } /\ y e. ran F ) }
22 20 21 sseqtrrdi
 |-  ( A e. CC -> { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } C_ ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) )
23 1 dmex
 |-  dom F e. _V
24 23 abrexex
 |-  { z | E. w e. dom F z = ( w + A ) } e. _V
25 1 rnex
 |-  ran F e. _V
26 24 25 xpex
 |-  ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) e. _V
27 ssexg
 |-  ( ( { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } C_ ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) /\ ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) e. _V ) -> { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } e. _V )
28 22 26 27 sylancl
 |-  ( A e. CC -> { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } e. _V )
29 breq
 |-  ( z = F -> ( ( x - w ) z y <-> ( x - w ) F y ) )
30 29 anbi2d
 |-  ( z = F -> ( ( x e. CC /\ ( x - w ) z y ) <-> ( x e. CC /\ ( x - w ) F y ) ) )
31 30 opabbidv
 |-  ( z = F -> { <. x , y >. | ( x e. CC /\ ( x - w ) z y ) } = { <. x , y >. | ( x e. CC /\ ( 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 e. CC /\ ( x - w ) F y ) <-> ( x e. CC /\ ( x - A ) F y ) ) )
35 34 opabbidv
 |-  ( w = A -> { <. x , y >. | ( x e. CC /\ ( x - w ) F y ) } = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
36 df-shft
 |-  shift = ( z e. _V , w e. CC |-> { <. x , y >. | ( x e. CC /\ ( x - w ) z y ) } )
37 31 35 36 ovmpog
 |-  ( ( F e. _V /\ A e. CC /\ { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } e. _V ) -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
38 1 37 mp3an1
 |-  ( ( A e. CC /\ { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } e. _V ) -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
39 28 38 mpdan
 |-  ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )