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 ) } )