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 Z B
uzmptshftfval.b B V
uzmptshftfval.c x = y N B = C
uzmptshftfval.z Z = M
uzmptshftfval.w W = M + N
uzmptshftfval.m φ M
uzmptshftfval.n φ N
Assertion uzmptshftfval φ F shift N = y W C

Proof

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