Metamath Proof Explorer

Theorem uzmptshftfval

Description: When F is a maps-to function on some set of upper integers Z that returns a set B , ( F shift N ) is another maps-to function on the shifted set of upper integers W . (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses uzmptshftfval.f 
|- F = ( x e. Z |-> B )
uzmptshftfval.b 
|- B e. _V
uzmptshftfval.c 
|- ( x = ( y - N ) -> B = C )
uzmptshftfval.z 
|- Z = ( ZZ>= ` M )
uzmptshftfval.w 
|- W = ( ZZ>= ` ( M + N ) )
uzmptshftfval.m 
|- ( ph -> M e. ZZ )
uzmptshftfval.n 
|- ( ph -> N e. ZZ )
Assertion uzmptshftfval 
|- ( ph -> ( F shift N ) = ( y e. W |-> C ) )

Proof

Step Hyp Ref Expression
1 uzmptshftfval.f 
 |-  F = ( x e. Z |-> B )
2 uzmptshftfval.b 
 |-  B e. _V
3 uzmptshftfval.c 
 |-  ( x = ( y - N ) -> B = C )
4 uzmptshftfval.z 
 |-  Z = ( ZZ>= ` M )
5 uzmptshftfval.w 
 |-  W = ( ZZ>= ` ( M + N ) )
6 uzmptshftfval.m 
 |-  ( ph -> M e. ZZ )
7 uzmptshftfval.n 
 |-  ( ph -> N e. ZZ )
8 2 1 fnmpti 
 |-  F Fn Z
9 7 zcnd 
 |-  ( ph -> N e. CC )
10 4 fvexi 
 |-  Z e. _V
11 10 mptex 
 |-  ( x e. Z |-> B ) e. _V
12 1 11 eqeltri 
 |-  F e. _V
13 12 shftfn 
 |-  ( ( F Fn Z /\ N e. CC ) -> ( F shift N ) Fn { y e. CC | ( y - N ) e. Z } )
14 8 9 13 sylancr 
 |-  ( ph -> ( F shift N ) Fn { y e. CC | ( y - N ) e. Z } )
15 shftuz 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> { y e. CC | ( y - N ) e. ( ZZ>= ` M ) } = ( ZZ>= ` ( M + N ) ) )
16 7 6 15 syl2anc 
 |-  ( ph -> { y e. CC | ( y - N ) e. ( ZZ>= ` M ) } = ( ZZ>= ` ( M + N ) ) )
17 4 eleq2i 
 |-  ( ( y - N ) e. Z <-> ( y - N ) e. ( ZZ>= ` M ) )
18 17 rabbii 
 |-  { y e. CC | ( y - N ) e. Z } = { y e. CC | ( y - N ) e. ( ZZ>= ` M ) }
19 16 18 5 3eqtr4g 
 |-  ( ph -> { y e. CC | ( y - N ) e. Z } = W )
20 19 fneq2d 
 |-  ( ph -> ( ( F shift N ) Fn { y e. CC | ( y - N ) e. Z } <-> ( F shift N ) Fn W ) )
21 14 20 mpbid 
 |-  ( ph -> ( F shift N ) Fn W )
22 dffn5 
 |-  ( ( F shift N ) Fn W <-> ( F shift N ) = ( y e. W |-> ( ( F shift N ) ` y ) ) )
23 21 22 sylib 
 |-  ( ph -> ( F shift N ) = ( y e. W |-> ( ( F shift N ) ` y ) ) )
24 uzssz 
 |-  ( ZZ>= ` ( M + N ) ) C_ ZZ
25 5 24 eqsstri 
 |-  W C_ ZZ
26 zsscn 
 |-  ZZ C_ CC
27 25 26 sstri 
 |-  W C_ CC
28 27 sseli 
 |-  ( y e. W -> y e. CC )
29 12 shftval 
 |-  ( ( N e. CC /\ y e. CC ) -> ( ( F shift N ) ` y ) = ( F ` ( y - N ) ) )
30 9 28 29 syl2an 
 |-  ( ( ph /\ y e. W ) -> ( ( F shift N ) ` y ) = ( F ` ( y - N ) ) )
31 5 eleq2i 
 |-  ( y e. W <-> y e. ( ZZ>= ` ( M + N ) ) )
32 6 7 jca 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ ) )
33 eluzsub 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ y e. ( ZZ>= ` ( M + N ) ) ) -> ( y - N ) e. ( ZZ>= ` M ) )
34 33 3expa 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ y e. ( ZZ>= ` ( M + N ) ) ) -> ( y - N ) e. ( ZZ>= ` M ) )
35 32 34 sylan 
 |-  ( ( ph /\ y e. ( ZZ>= ` ( M + N ) ) ) -> ( y - N ) e. ( ZZ>= ` M ) )
36 31 35 sylan2b 
 |-  ( ( ph /\ y e. W ) -> ( y - N ) e. ( ZZ>= ` M ) )
37 36 4 eleqtrrdi 
 |-  ( ( ph /\ y e. W ) -> ( y - N ) e. Z )
38 3 1 2 fvmpt3i 
 |-  ( ( y - N ) e. Z -> ( F ` ( y - N ) ) = C )
39 37 38 syl 
 |-  ( ( ph /\ y e. W ) -> ( F ` ( y - N ) ) = C )
40 30 39 eqtrd 
 |-  ( ( ph /\ y e. W ) -> ( ( F shift N ) ` y ) = C )
41 40 mpteq2dva 
 |-  ( ph -> ( y e. W |-> ( ( F shift N ) ` y ) ) = ( y e. W |-> C ) )
42 23 41 eqtrd 
 |-  ( ph -> ( F shift N ) = ( y e. W |-> C ) )